GADT problems
Simon PeytonJones
simonpj at microsoft.com
Sun Sep 14 10:11:20 EDT 2008
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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskell
 usersbounces at haskell.org] On Behalf Of Mitchell, Neil
 Sent: 12 September 2008 13:51
 To: glasgowhaskellusers at 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 nonrigid 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.creditsuisse.com/legal/en/disclaimer_email_ib.html
 =============================================================================
 =

 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list