Opened 2 years ago

Closed 2 years ago

Last modified 2 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 Difficulty:
Test Case: Blocked By:
Blocking: Related Tickets:

Description

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.

Change History (3)

comment:1 Changed 2 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

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 2 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 2 years ago by mikhail.vorozhtsov

Ah, now I get it.

Note: See TracTickets for help on using tickets.