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 |