GADT problems

[Simon Peyton-Jones]

| > | op (Foo GadtValue :: Foo) = () :: ()
| >
| > The thing is that GHC doesn't know the result type of the
| > match *at the match point*.  Suppose you had written
| >
| >         op (Foo GadtValue :: Foo) = id (() :: ()) or
| >         op (Foo GadtValue :: Foo) = if blah then () :: () else () or
| >         op (Foo GadtValue :: Foo) = let x = blah in () :: ()
| >
| > The signature is too far "inside".   We need to know it from
| > "outside".
|
| Ah, this is the crucial bit I've been misunderstanding! Instinctively it
| feels that when a GADT can't type check I should be annotating the GADT
| part - but that's not the case, I should be annotating the expression
| containing both the GADT match and its right-hand side. I think the way
| the error message is formatted (add a type signature, followed by giving
| the local pattern) seems to hint at this. With this insight I've managed
| to fix up all the real problems I was experiencing.

Great.  Now you can help me!  Look at the documentation here
http://www.haskell.org/ghc/dist/current/docs/users_guide/data-type-extensions.html#gadt
The last bullet.

What could I add that would eliminate your misunderstanding?    You are in the ideal position to suggest concrete wording, because you know the problem and the solution.  Examples are fine.

Thanks

| > Perhaps you can give an example that shows your difficulty?
|
| The following is a fake example I was playing with:
|
| {-# LANGUAGE GADTs, ScopedTypeVariables #-}
| module Test where
|
| data E x = E x
|
| data Foo a where
|   Foo :: Gadt a -> Foo a
|
| data Gadt a where
|   GadtValue :: a -> Gadt (E a)
|
| g :: [()]
| g = [() | Foo (GadtValue _) <- undefined] :: [()]
|
| I couldn't figure out how to supply enough annotations to allow the code
| to work.

The error message here is:

    GADT pattern match in non-rigid context for `GadtValue'
      Solution: add a type signature
    In the pattern: GadtValue _
    In the pattern: Foo (GadtValue _)
    In a stmt of a list comprehension: Foo (GadtValue _) <- undefined

And indeed, the type of 'undefined' (which is the scrutinee of this particular pattern match) is forall a. a.   Very non-rigid!

You need a type signature for the scrutinee.  For example, this works:

  g :: [()]
  g = [() | Foo (GadtValue _) <- undefined :: [Foo (E ())]]

Does that help?  Again, what words would help in the user manual.

Simon