The type variable ‘a0’ is ambiguous

Question

I don't understand why the following code won't compile:

{-# LANGUAGE GADTs, ScopedTypeVariables #-}

data A = A

class C a where
  c :: a -> Bool

instance C A where
  c _ = True

data D a where
  D :: C a => D a

toBool :: D a -> Bool
toBool D = c (undefined::a)

Here is the error message:

Could not deduce (C a0) arising from a use of ‘c’
from the context (C a)
  bound by a pattern with constructor
             D :: forall a. C a => D a,
           in an equation for ‘toBool’
  at test.hs:15:8
The type variable ‘a0’ is ambiguous
Note: there is a potential instance available:
  instance C A -- Defined at test.hs:8:10
In the expression: c (undefined :: a)
In an equation for ‘toBool’: toBool D = c (undefined :: a)

Can someone explain what's going on ?                                        

Answer 1

The type variables introduced in a top-level type declaration are not the same as those introduced inside the body of the function. Another way of saying this is the nested type declarations introduce "fresh" variables. Another another way to say this is to put explicit foralls in your code where Haskell automatically introduces them, silently:

toBool :: forall a . D a -> Bool
toBool D = c (undefined :: forall a . a)   -- another forall here?

What you really intended was

toBool :: forall a . D a -> Bool
toBool D = c (undefined :: a)   -- capture `a` from prior scope

and, you're in luck. It turns out that almost everyone needs this kind of functionality from time to time so a very common Haskell extension exists called ScopedTypeVariables. The following code ought to compile

{-# LANGUAGE ScopedTypeVariables #-}

toBool :: forall a . D a -> Bool
toBool D = c (undefined :: a)

Note that in order to invoke ScopedTypeVariables you must now manually introduce the foralls that you want to be treated specially. Without that manual forall Haskell will automatically introduce them at all the same locations it normally does.