GADT pattern match with non-rigid return type

Chris Casinghino (ccasin@seas.upenn.edu) writes: I've been playing with some GADT stuff with Stephanie Weirich and I think we've found a bug in GHC at the intersection of GADTs and existentials. The HEAD version gives a type error when :loading this program into ghci:

> data ExpGADT t where
>   ExpInt :: Int -> ExpGADT Int
>
> data Hidden = forall t . Hidden (ExpGADT t) (ExpGADT t)
>
> hval = Hidden (ExpInt 0) (ExpInt 1)
>
> weird = case (hval :: Hidden) of Hidden (ExpInt _) a -> a

ghc thinks the existential type variable has escaped:

test.hs:11:33:
     Inferred type is less polymorphic than expected
       Quantified type variable `t' escapes
     When checking an existential match that binds
         a :: ExpGADT t
     The pattern(s) have type(s): Hidden
     The body has type: ExpGADT t
     In a case alternative: Hidden (ExpInt _) a -> a
     In the expression:
         case (hval :: Hidden) of Hidden (ExpInt _) a -> a

According to the rules in the wobbly types paper, this should typecheck and weird should be given the wobbly type (ExpGADT Int).

Perhaps this type error is an intentional deviation from the spec? If so, I'd love to know what implementation issues brought about the change. If not, I suppose it's a bug.

Everything works fine if we add a type annotation for weird. Strangely, in ghc 6.8.2, the program is accepted when :loaded, but if after doing so I copy:

   let weird2 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a

into ghci, I get an error.

Anyway, I thought I should point out this discrepancy. I hope it's helpful!

Trac metadata

Trac field	Value
Version	6.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ccasin@seas.upenn.edu
Operating system	Unknown
Architecture	Unknown