GADT problems

Simon Peyton-Jones 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: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Mitchell, Neil
| Sent: 12 September 2008 13:51
| To: glasgow-haskell-users 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 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



More information about the Glasgow-haskell-users mailing list