id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential
2899 GADT type inference with existentials jochemb "
The following code works in GHC 6.8.2:
{{{
{-# OPTIONS -fglasgow-exts #-}
module Test where
data Existential = forall a. Ex (GADT a)
data GADT :: * -> * where
GCon :: Int -> GADT ()
-- g :: Existential -> Int
g (Ex (GCon x)) = x
}}}
The compiler correctly infers the type of x in the definition of g, and correctly infers the type of g.
In GHC 6.10.1, however, this fails with:
{{{
Test.hs:10:12:
GADT pattern match with non-rigid result type `t'
Solution: add a type signature
In the definition of `g': g (Ex (GCon x)) = x
Failed, modules loaded: none.
}}}
The solution, to include the type signature of g (that I have commented out), works, but why can't GHC figure out the type of g? GHC 6.8.2 could!
An equivalent version with a non-GADT instead, works correctly:
{{{
data GADT a = GCon Int
}}}
Ticket #2206 might be related." bug closed normal Compiler (Type checker) 6.10.1 invalid GADT, existential types jochem@… Unknown/Multiple Unknown/Multiple