Unexpected cryptic GADT type error

[mikhail.vorozhtsov]

Consider the following module:

{-# LANGUAGE GADTs #-}

module Bug where

import Control.Monad (void)

data D = D

data G a where
  G :: G Int

ok :: (Functor m, Monad m) => m ()
ok = void $ case D of D -> return "xyz"

bad :: (Functor m, Monad m) => m ()
bad = void $ case G of G -> return "xyz"

Function "ok" is accepted by GHC, but function "bad" triggers a cryptic type error:

Bug.hs:16:24:
    Couldn't match type `a0' with `[Char]'
      `a0' is untouchable
           inside the constraints (Int ~ Int)
           bound at a pattern with constructor
                      G :: G Int,
                    in a case alternative
    In the pattern: G
    In a case alternative: G -> return "xyz"
    In the second argument of `($)', namely
      `case G of { G -> return "xyz" }'

I hope this is a bug in typechecker. Tested on 7.2.2 and 7.3.20111130.

[simonpj]

It's not a bug, I'm afraid. Type inference for GADT programs requires enough type signatures to work, and this program doesn't. Consider

  void :: Functor f => f a -> f ()

So the call of void gives no clue about what the a of f a is. It would have to be purely inferred. So what is the type of the argument?

   case G of G -> return "xyz"

In this case it can only be String, but suppose we had (x :: G a); what is the type of

   case x of G -> return 3

is it n a or m Int? There is no most-general type, and that's the trouble.

Now, the error message is not a thing of beauty. But it means that we are unifying the type inside (String here) with the type from outside a0, which instantiated the call to void. If people can think of a better way to report such errors it'd be great.

[mikhail.vorozhtsov]

Wow, that's really confusing. Is the "a" in "n a" is the same as in "x :: G a"? That makes no sense to me. Would it be right to say that GHC "dumbs" itself down a bit when it sees a GADT (perhaps in order to guarantee termination of the type inferencing)? Because it sure has no problem with

ok :: (Functor m, Monad m) => m ()
ok = void $ case x of D -> return 3
  where x :: D
        x = undefined

and I can't see how "return 3" becomes any more ambiguous when the "x" changes its type.

[mikhail.vorozhtsov]

Ah, now I get it.