Hi list, I have stumbled upon a strange annoyance: {-# LANGUAGE GADTs #-} data Foo v where Foo :: Foo (Maybe v) -- This doesn't work foo1 :: a -> Foo a -> Int foo1 Nothing Foo = undefined foo1 (Just x) Foo = undefined -- This does foo2 :: a -> Foo a -> Int foo2 x Foo = foo2' x foo2' :: Maybe a -> Int foo2' Nothing = undefined foo2' (Just x) = undefined The first definition fails with the error Couldn't match expected type `a' with actual type `Maybe t0' `a' is a rigid type variable bound by the type signature for foo1 :: a -> Foo a -> Int at /tmp/foo_flymake.hs:8:9 In the pattern: Nothing In an equation for `foo1': foo1 Nothing Foo = undefined Now, GHC can clearly derive and use the type equalities correctly, given that the second definition works, but why can’t I pattern match directly? Thanks, Francesco