On Sun, Sep 14, 2008 at 7:11 AM, Simon Peyton-Jones
Neil
It's by design, and for (I think) good reason. GHC now enforces the rule that in a GADT pattern match - the type of the scrutinee must be rigid - the result type must be rigid - the type of any variable free in the case branch must be rigid
Here "rigid" means "fully known to the compiler, usually by way of a type signature". This rule is to make type inference simple and predictable -- it dramatically simplifies inference.
To see the issue, ask yourself what is the type of this function
data E a where EI :: E Int
f EI = 3::Int
Should the inferred type be f :: E a -> a or f :: E a -> Int We can't tell, and neither is more general than the other. So GHC insists on knowing the result type. That's why you had to give the signature g::[()] in your example.
So that's the story. If you find situations in which it's very hard to give a signature for the result type, I'd like to see them.
I find that usually when it becomes difficult is when I'm using existential types and lexically scoped type variables. I don't have an example ready but I could vaguely describe it. For example, using a case expression to pattern match on a constructor that has an existential type and also expecting part of the type of that expression to match a lexically scope type variable (I'm often also using phantom types, if that matters). In this case, I usually end up adding a where clause to specify the type signature while dancing around the other issues. It's typically not pretty but at the end of the day I've always been able to find a way to specify the type I need. Although, it does make me quite aware that GHC could report the type errors better when dealing with phantom types that are bound to an existential type. If you have multiple such phantoms as part of the type it can be quite confusing to figure out which ones the type checker isn't happy with. data Sealed a where Sealed :: a x y -> Sealed a data Foo a x y where .... case sealedFoo where Sealed (Foo 4) -> ... If you get a type error in the above sometimes it's hard to figure out if it's happening with x or with y. Sometimes the type parameter name chosen doesn't give you a hint about which type parameter of Foo is not unifying. I wish I had a concrete example to show you. I guess the next time it shows up I should send it in. Thanks, Jason