GADT pattern match with non-rigid return type
Chris Casinghino (firstname.lastname@example.org) 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
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!