#2206: GADT pattern match with non-rigid return type
-------------------------+--------------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.8.2
Severity: normal | Keywords:
Difficulty: Unknown | Testcase: gadt-escape1
Architecture: Unknown | Os: Unknown
-------------------------+--------------------------------------------------
Chris Casinghino ([EMAIL PROTECTED]) 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!
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2206>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
