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