GADT problems

[Simon Peyton-Jones]

| 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) = () :: ()

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".


| 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.

Perhaps you can give an example that shows your difficulty?

Simon