GADT pattern match with non-rigid return type
|Reported by:||simonpj||Owned by:||simonpj|
|Type of failure:||Difficulty:||Unknown|
|Test Case:||gadt-escape1||Blocked By:|
Chris Casinghino (ccasin@…) 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