[Haskell-cafe] GADTs and pattern matching

[AntC]

Francesco Mazzoli <f <at> mazzo.li> writes:

> 
> I have stumbled upon a strange annoyance:
> 
>     {-# LANGUAGE GADTs #-}

Hi Francesco, I think you'll find that the 'annoyance' is nothing to do 
with GADTs. I suggest you take the type signature off of foo1, and see 
what type ghc infers for it. It isn't :: a -> Foo a -> Int.

>     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
  ...
 
> The first definition fails with the error
> 
>     Couldn't match expected type `a' with actual type `Maybe t0'
 ...
>     In the pattern: Nothing

Yep, that message explains what's going on well enough for me.