
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. Dimitrios has just written an Appendix to our ICFP paper about GADT inference, explaining the inference scheme -- it is not otherwise written up anywhere. I'll put it up shortly. Thanks Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Mitchell, Neil | Sent: 12 September 2008 13:51 | To: glasgow-haskell-users@haskell.org | Subject: GADT problems | | Hi | | The following code works in GHC 6.8.3, works in GHC 6.9.20071111, but | doesn't work in GHC HEAD. | | {-# LANGUAGE GADTs, ScopedTypeVariables #-} | | module Test where | | data E x = E x | | data Foo where | Foo :: Gadt a -> Foo | | data Gadt a where | GadtValue :: Gadt (E a) | | f (Foo GadtValue) = True | f _ = False | | Under GHC HEAD I get the error: | | GADT pattern match with non-rigid result type `t' | Solution: add a type signature | In the definition of `f': f (Foo GadtValue) = True | | Adding a type signature to f fixes this problem: | | f :: Foo -> Bool | | But I haven't found anywhere other than the top level f to add a type | signature. When the match is in a list comprehension, it becomes much | harder. While playing further I discovered this example: | | foos = undefined | g = [() | Foo GadtValue <- foos] | | This code doesn't compile under GHC HEAD, but does under 6.8.3. However, | adding the type signature: | | g :: [()] | | Makes the code compile. This is surprising, as [()] isn't a GADT type, | so shouldn't need stating explicitly. | | Any help on what these errors mean, or how they can be fixed with local | type annotations? | | Thanks | | Neil | | ============================================================================= | = | Please access the attached hyperlink for an important electronic | communications disclaimer: | | http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html | ============================================================================= | = | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users