id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential,wikipage
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,,,,,,,