GADTs and pattern matching

[Francesco Mazzoli]

At Wed, 19 Jun 2013 11:25:49 +0100,
Francesco Mazzoli wrote:
> 
> Hi list,
> 
> I had asked this on haskell-cafe but this looks particularly fishy, so
> posting here in case it is an issue:
> 
>     {-# LANGUAGE GADTs #-}
>     
>     data Foo v where
>         Foo :: forall v. Foo (Maybe v)
>     
>     -- Works
>     foo1 :: Foo a -> a -> Int
>     foo1 Foo Nothing  = undefined
>     foo1 Foo (Just x) = undefined
>     
>     -- This works
>     foo2 :: a -> Foo a -> Int
>     foo2 x Foo = foo2' x
>     
>     foo2' :: Maybe a -> Int
>     foo2' Nothing = undefined
>     foo2' (Just x) = undefined
>     
>     -- This doesn't!
>     foo3 :: a -> Foo a -> Int
>     foo3 Nothing  Foo  = undefined
>     foo3 (Just x) Foo = undefined
> 
> So it looks like constraints in pattern matching only propagate
> forwards.  Is this intended?

shachaf on #haskell pointed out that matches get desugared into a series
of ‘case’s matching the argument successively, and given that the
behaviour above makes sense.

Francesco