In Haskell, why are types ambiguous even with AllowAmbiguousTypes enabled?

Question

So lets assume you have two type classes defined like this:

{-# LANGUAGE MultiParamTypeClasses #-}

class F a c where f :: a -> c
class G c b where g :: c -> b

And then you want to define a new function h in a general way by using f and g.

h a = g (f a)

We know that this function has type a -> b so c is implicit in there. I want to leave it to the implementer of f and g what c might be. Haskell complains about this saying c is ambiguous.

Then as suggested by the error I turned on this extension:

{-# LANGUAGE AllowAmbiguousTypes #-}

Now it works! Nice.

I believe usually as a good software engineering practice, I want to write explicit specifications of my functions, to tell the compiler what I expect my functions should behave like. So that later compiler can complain about me not respecting what I set.

So I want to add the type of my function before it:

h :: (F a c, G c b) => a -> b
h a = g (f a)

And now the type ambiguousity error comes again... Why?

To summarize why does Haskell complain about this below piece of code? even if AllowAmbiguousTypes is explictly enabled. How to fix it while keeping an explicit function type definition? I know that removing the type definition of the function solves it but I don't want to underspecify things.

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

class F a c where f :: a -> c
class G c b where g :: c -> b

h :: (F a c, G c b) => a -> b
h a = g (f a)

And why doesn't Haskell complain about this?

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

class F a c where f :: a -> c
class G c b where g :: c -> b

h a = g (f a)

Error messages:

error:
    * Could not deduce (G c0 b) arising from a use of `g'
      from the context: (F a c, G c b)
        bound by the type signature for:
                   h :: forall a c b. (F a c, G c b) => a -> b

      The type variable `c0' is ambiguous
      Relevant bindings include
        h :: a -> b 
    * In the expression: g (f a)
      In an equation for `h': h a = g (f a)
    |
    | h a = g (f a)
    |       ^^^^^^^
error:
    * Could not deduce (F a c0) arising from a use of `f'
      from the context: (F a c, G c b)
        bound by the type signature for:
                   h :: forall a c b. (F a c, G c b) => a -> b
      The type variable `c0' is ambiguous
      Relevant bindings include
        a :: a 
        h :: a -> b 
    * In the first argument of `g', namely `(f a)'
      In the expression: g (f a)
      In an equation for `h': h a = g (f a)
    |
    | h a = g (f a)
    |          ^^^

user_3234959 · Answer

Your code is ambiguous, in a way that it can't be solved automatically by the compiler. Assume this:

class F a c where f :: a -> c
class G c b where g :: c -> b

instance F Int String where f = show
instance G String Bool where g = null

h :: (F Int c, G c Bool) => Int -> Bool
h a = g (f a)

Now, which instances are used in the last line? We have two options: using the instances provided by the context (F Int c, G c Bool), or ignoring that context and using the instances above, with String as the middle type. Both interpretations are correct, and indeed we can explicitly write

h1 :: forall c. (F Int c, G c Bool) => Int -> Bool
h1 a = (g :: c -> Bool) (f a)

h2 :: forall c. (F Int c, G c Bool) => Int -> Bool
h2 a = (g :: String -> Bool) (f a)

to choose one way or the other. GHC can not do this choice for us in a reasonable way. It could choose one according to some heuristics, but that can cause much surprise to the programmer. Hence, we can argue that GHC must not choose at all, report the ambiguity, and let the programmer clarify their intent.

Finally, note that the fact that your code does not include the two instances above is irrelevant, since those could be added later on, or even in another module, so GHC has to be conservative and avoid assuming they will never exist.

And why doesn't Haskell complain about this?

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

class F a c where f :: a -> c
class G c b where g :: c -> b

h x = g (f x)  -- [renamed to x for clarity]

Good point. Here GHC can find a most general type, which is

h :: forall a b c. (F a c, G c b) => a -> b
h x = (g :: c -> b) ((f :: a -> b) x)

Since here it is GHC that added the type variable c, GHC can be sure that such type is the intermediate type. That type variable was created during type inference to denote the intermediate type, after all.

Instead, when the user explicitly writes the context, GHC can not guess the intention of the user. It is possible, even if it's unlikely in practice, that the user does not want to use that instance, but another one (available in the program, and not present in the context).

It might be helpful to think about this case as well:

data T = ....

h :: forall a b c. (F a c, G c b, F a T, G T b) => a -> b
h x = g (f x)

I think you can agree that this code should be rejected: the intermediate type could be T or c, and there is no sane way to solve it. Now consider this case:

h :: forall a b c. (F a c, G c b) => a -> b
h x = g (f x)

instance F a T where ...
instance G T b where ...

Now, this is not too different than the previous case. Instead of having two options in the context, we have moved one outside. GHC still has two options to choose from, though. So, again, the sane thing is to reject the code, and ask the programmer for more detail.

A simpler scenario, in GHCi:

> :set -XScopedTypeVariables
> :set -XAllowAmbiguousTypes
> class C a where c :: String
> instance C Int where c = "Int"
> instance C Bool where c = "Bool"
> let g :: forall a. C a => String ; g = c

:7:40: error:
    * Could not deduce (C a0) arising from a use of `c'

Here, how could GHC know that when I wrote g = c I meant "the c coming from the context C a? I could have written that meaning "the c from the instance for Int". Or Bool.

GHC internally generates a fresh type variable a0 and then tries to solve the constraint C a0. It has three choices: choosing a0 = a, a0 = Int, or a0 = Bool. (And more instances could be added later on!)

So, it is ambiguous, and there is no sane way to fix it without guessing what the programmer intended. The only safe option is to reject.

In Haskell, why are types ambiguous even with AllowAmbiguousTypes enabled?

1 Answers