Hi Simon, I appreciate that everything must be rigid, but am still confused. Given the following operation: op (Foo GadtValue) = () I can add a top-level type signature, and it works: op :: Foo -> () But just putting those same type annotations in the actual function doesn't work: op (Foo GadtValue :: Foo) = () :: () From a simple point of view those two functions seem to have the same amount of type information, but GHC gives different behaviour. I think this is the underlying problem I'm getting. For things like list-comps and cases I don't seem to be able to find any combination of annotations that works, but that is because I'm not using top-level annotations. Thanks Neil
-----Original Message----- From: Simon Peyton-Jones [mailto:simonpj@microsoft.com] Sent: 14 September 2008 3:11 pm To: Mitchell, Neil; glasgow-haskell-users@haskell.org Subject: RE: GADT problems
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
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================