Ambigous instance resolution in Haskell

Question

Introduction and example use case

Hello! I've got a problem in Haskell. Let's consider following code

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b

which just declares a poly monad binding. A good example use case scenario would be:

newtype Pure a = Pure { fromPure :: a } deriving (Show)

instance PolyMonad Pure Pure Pure where
    polyBind a f = f (fromPure a)

instance PolyMonad Pure IO IO where
    polyBind a f = f (fromPure a)

instance PolyMonad IO Pure IO where
    polyBind a f = (fromPure . f) <$> a

instance PolyMonad IO IO IO where
    polyBind a f = a >>= f

and using it with -XRebindableSyntax like so:

test = do
    Pure 5
    print "hello"
    Pure ()

but we can do much more with it - this was only a test to show you an example case.

The problem

Lets consider a little more complex usage. I want to write a polymonad-like class, which will not always output m3 b, but in some specific cases it will output m3 (X b) for a specific X. For simplicity, lets assume we want to output m3 (X b) ONLY when either m1 or m2 was IO.

It seems we cannot do it right now in Haskell without losing flexibility. I need the following functions to compile without adding any type informations (the Haskell code is a generated one):

tst1 x = x `polyBind` (\_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0)
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0))

Anyway these functions compile well using the PolyMonad class.

Fundep attempt to solve the problem

One of the attempts could be:

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out

and of course we can easily write all the necessary instances, like:

instance PolyMonad2 Pure Pure b (Pure b) where
    polyBind2 a f = f (fromPure a)

instance PolyMonad2 Pure IO b (IO (X b)) where
    polyBind2 a f = fmap X $ f (fromPure a)

-- ...

but our test functions will not compile when using polyBind2 instead of polyBind. The first function (tst1 x = xpolyBind2(\_ -> Pure 0)) outputs a compilation error:

Could not deduce (PolyMonad2 m1 Pure b0 out)
  arising from the ambiguity check for ‘tst1’
from the context (PolyMonad2 m1 Pure b out, Num b)
  bound by the inferred type for ‘tst1’:
             (PolyMonad2 m1 Pure b out, Num b) => m1 a -> out
  at /tmp/Problem.hs:51:1-37
The type variable ‘b0’ is ambiguous
When checking that ‘tst1’
  has the inferred type ‘forall (m1 :: * -> *) b out a.
                         (PolyMonad2 m1 Pure b out, Num b) =>
                         m1 a -> out’
Probable cause: the inferred type is ambiguous

Closed type families attempt to solve the problem

A slightly better way would be to use closed type families here, like:

class PolyMonad3 m1 m2 where
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b

type family OutputOf m1 m2 a where
    OutputOf Pure Pure a = Pure a
    OutputOf x    y    a = Pure (X a)

but then when trying to compile the tst1 function (tst1 x = xpolyBind3(\_ -> Pure 0)) we get another compile time error:

Could not deduce (OutputOf m1 Pure b0 ~ OutputOf m1 Pure b)
from the context (PolyMonad3 m1 Pure, Num b)
  bound by the inferred type for ‘tst1’:
             (PolyMonad3 m1 Pure, Num b) => m1 a -> OutputOf m1 Pure b
  at /tmp/Problem.hs:59:1-37
NB: ‘OutputOf’ is a type function, and may not be injective
The type variable ‘b0’ is ambiguous
Expected type: m1 a -> OutputOf m1 Pure b
  Actual type: m1 a -> OutputOf m1 Pure b0
When checking that ‘tst1’
  has the inferred type ‘forall (m1 :: * -> *) a b.
                         (PolyMonad3 m1 Pure, Num b) =>
                         m1 a -> OutputOf m1 Pure b’
Probable cause: the inferred type is ambiguous

A hacky attempt to do it around

I've found another solution, but hacky and in the end not working. But it is very interesting one. Lets consider following type class:

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
    polyBind4 :: m1 a -> (a -> m2 b) -> out

Of course the functional dependency out -> b is just wrong, because we cannot define such instances like:

instance PolyMonad4 Pure IO b (IO (X b)) where
    polyBind4 a f = fmap X $ f (fromPure a)

instance PolyMonad4 IO IO b (IO b) where
    polyBind4 = undefined

but lets play with it and declare them so (using -XUndecidableInstances):

instance out~(Pure b) => PolyMonad4 Pure Pure b out where
    polyBind4 a f = f (fromPure a)

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
    polyBind4 a f = fmap X $ f (fromPure a)

instance out~(IO b) => PolyMonad4 IO IO b out where
    polyBind4 = undefined

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
    polyBind4 = undefined

What's funny, some of our test functions DOES compile and work, namely:

tst1' x = x `polyBind4` (\_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0)

but this one not:

tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0))

resulting in compile time error:

Could not deduce (PolyMonad4 m3 Pure b0 (m20 b))
  arising from the ambiguity check for ‘tst3'’
from the context (PolyMonad4 m3 Pure b1 (m2 b),
                  PolyMonad4 m1 m2 b out,
                  Num b1)
  bound by the inferred type for ‘tst3'’:
             (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
             m1 a -> m3 a1 -> out
  at /tmp/Problem.hs:104:1-62
The type variables ‘m20’, ‘b0’ are ambiguous
When checking that ‘tst3'’
  has the inferred type ‘forall (m1 :: * -> *)
                                (m2 :: * -> *)
                                b
                                out
                                a
                                (m3 :: * -> *)
                                b1
                                a1.
                         (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
                         m1 a -> m3 a1 -> out’
Probable cause: the inferred type is ambiguous

Even more hacky attempt using newtype wrapping

I told it is even more hacky, because it leads us to use -XIncoherentInstances, which are Just (Pure evil). One of the ideas could be of course to write newtype wrapper:

newtype XWrapper m a = XWrapper (m (X (a)))

and some utils to unpack it:

class UnpackWrapper a b | a -> b where
    unpackWrapper :: a -> b

instance UnpackWrapper (XWrapper m a) (m (X a)) where
    unpackWrapper (XWrapper a) = a

instance UnpackWrapper (Pure a) (Pure a) where
    unpackWrapper = id

instance UnpackWrapper (IO a) (IO a) where
    unpackWrapper = id

now we can easly declare following instances:

instance PolyMonad Pure Pure Pure 
instance PolyMonad Pure IO (XWrapper IO) 
instance PolyMonad IO Pure (XWrapper IO) 
instance PolyMonad IO IO IO 

but again, we cannot run our tests when combining the bind and unwrap functions:

polyBindUnwrap a f = unpackWrapper $ polyBind a f

the test functions fail to compile again. We can mess here with some -XIncoherentInstances (see the code listing on the end), but I did not get any ok results so far.

The final question

Is this a problem which cannot be done using current GHC Haskell implementation?

Full code listing

Here is a full code listing, which can be run in GHC >= 7.8:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Control.Applicative

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b


----------------------------------------------------------------------
-- Some utils
----------------------------------------------------------------------

newtype Pure a = Pure { fromPure :: a } deriving (Show)
newtype X a = X { fromX :: a } deriving (Show)

main = return ()

----------------------------------------------------------------------
-- Example use cases
----------------------------------------------------------------------

instance PolyMonad Pure Pure Pure where
    polyBind a f = f (fromPure a)

instance PolyMonad Pure IO IO where
    polyBind a f = f (fromPure a)

instance PolyMonad IO Pure IO where
    polyBind a f = (fromPure . f) <$> a

instance PolyMonad IO IO IO where
    polyBind a f = a >>= f

-- works when using rebindable syntax
--test = do
--    Pure 5
--    print "hello"
--    Pure ()

tst1 x = x `polyBind` (\_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0)
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0))

----------------------------------------------------------------------
-- First attempt to solve the problem
----------------------------------------------------------------------


class PolyMonad2 m1 m2 b out | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out


instance PolyMonad2 Pure Pure b (Pure b) where
    polyBind2 a f = f (fromPure a)

instance PolyMonad2 Pure IO b (IO (X b)) where
    polyBind2 a f = fmap X $ f (fromPure a)

-- ...

-- tst1 x = x `polyBind2` (\_ -> Pure 0) -- does NOT compile


----------------------------------------------------------------------
-- Second attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad3 m1 m2 where
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b

type family OutputOf m1 m2 a where
    OutputOf Pure Pure a = Pure a
    OutputOf x    y    a = Pure (X a)

-- tst1 x = x `polyBind3` (\_ -> Pure 0) -- does NOT compile


----------------------------------------------------------------------
-- Third attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
    polyBind4 :: m1 a -> (a -> m2 b) -> out


instance out~(Pure b) => PolyMonad4 Pure Pure b out where
    polyBind4 a f = f (fromPure a)

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
    polyBind4 a f = fmap X $ f (fromPure a)

instance out~(IO b) => PolyMonad4 IO IO b out where
    polyBind4 = undefined

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
    polyBind4 = undefined


tst1' x = x `polyBind4` (\_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0)
--tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile


----------------------------------------------------------------------
-- Fourth attempt to solve the problem
----------------------------------------------------------------------

class PolyMonad6 m1 m2 m3 | m1 m2 -> m3 where
    polyBind6 :: m1 a -> (a -> m2 b) -> m3 b

newtype XWrapper m a = XWrapper (m (X (a)))


class UnpackWrapper a b | a -> b where
    unpackWrapper :: a -> b

instance UnpackWrapper (XWrapper m a) (m (X a)) where
    unpackWrapper (XWrapper a) = a

instance UnpackWrapper (Pure a) (Pure a) where
    unpackWrapper = id

instance UnpackWrapper (IO a) (IO a) where
    unpackWrapper = id

--instance (a1~a2, out~(m a2)) => UnpackWrapper (m a1) out where
--    unpackWrapper = id


--{-# LANGUAGE OverlappingInstances #-}
--{-# LANGUAGE IncoherentInstances #-}

instance PolyMonad6 Pure Pure Pure where
    polyBind6 = undefined

instance PolyMonad6 Pure IO (XWrapper IO) where
    polyBind6 = undefined

instance PolyMonad6 IO Pure (XWrapper IO) where
    polyBind6 = undefined

instance PolyMonad6 IO IO IO where
    polyBind6 = undefined

--polyBind6' a f = unpackWrapper $ polyBind6 a f

--tst1'' x = x `polyBind6'` (\_ -> Pure 0)
--tst2'' = (Pure 1) `polyBind4` (\_ -> Pure 0)
--tst3'' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile

Answer 1

I don't think this question hinges on injective type families.

The injective type families bit is mentioned in the error message around the closed type family OutputOf. But, that function really is not injective -- the second equation for it allows for any x and y. GHC likes to remind users about the fact that it does not do injectivity analysis for type families, but sometimes (like here), this warning is not helpful.

Instead, the problems you're encountering all seem to stem from overloaded numbers. When you say Pure 0, GHC correctly infers the type Num a => Pure a. The problem is that the type-level features you're accessing (type class resolution, functional dependencies, type families) care very much what specific choice is made for a here. For example, it's quite possible that any one of your approaches behaves differently for Int than it does for Integer. (For example, you could have differing instances of PolyMonad2 or extra equations in OutputOf.)

The solution to all of this might be to use RebindableSyntax and define fromInteger to be monomorphic, thus fixing the numeric type and avoiding the hassle.

Answer 2

I believe the fundamental difference is that here:

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
    polyBind :: m1 a -> (a -> m2 b) -> m3 b

The b is fully polymorphic; it's not a parameter to the type class, so the instance can be selected and the functional dependency applied to determine m3 from m1 and m2 independently of b. It also appears in two places; if the type inferencer knows the result type or the type of the function passed to polyBind, then it can sufficiently determine b. And a type like Num b => b will happily "flow through" many applications of polyBind until it's used in a place that fixes a concrete type. Although I think it may be just the monomorphism restriction defaulting the type that saves you from an ambiguous type variable error in this case (exactly what it was designed to do).

Whereas here:

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
    polyBind2 :: m1 a -> (a -> m2 b) -> out

b appears as a type class parameter. If we're trying to infer what out is, we need to fully determine b before we can select an instance. And there's no reason for b to bear any particular relation to the structure of the type out (or rather, that relationship can be different for each individual instance, which is after all what you're trying to achieve), so it's not possible to "follow the b through" a chain of polyBind2 calls unless you've fully resolved all of the instances.

And if b is a polymorphic number Num b => b and out is constrained by its use to be of the form Num c => m c (for some type constructor m), there's no reason that the c and the b have to be the same Num instance. So in a chained series of polyBind2 calls operating on numbers, every intermediate result could be using a different Num instance, and without knowing any of them there's no way to select the correct PolyMonad2 instances that do unify the b with something in out. Type defaulting only applies if all the constraints on the variable are numeric prelude classes, but here the b is involved in the constraint PolyMonad2 m1 m2 m3 b, so it can't be defaulted (which is probably a good thing, since exactly what type you choose could affect which instance is used and dramatically change the program behaviour; it's only the numeric classes that are known to be "approximations" of each other, so that if the program is ambiguous about which instance to use then it's semi-reasonable to just arbitrarily pick one rather than complain about the ambiguity).

The same really goes for any method for determining out from m1, m2, and b as far as I know, whether it's functional dependencies, type families, or something else. I'm not sure how to actually resolve that issue here though, without providing more type annotations.