| 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