[Haskell-cafe] GADTs and pattern matching

[Francesco Mazzoli]

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