Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#5678 closed bug (invalid)

Unexpected cryptic GADT type error

Reported by: mikhail.vorozhtsov Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


Consider the following module:


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:

    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.

Change History (3)

comment:1 Changed 5 years ago by simonpj

Resolution: invalid
Status: newclosed

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.

comment:2 Changed 5 years ago by 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.

comment:3 Changed 5 years ago by mikhail.vorozhtsov

Ah, now I get it.

Note: See TracTickets for help on using tickets.