GADTs and pattern matching

Francesco Mazzoli f at
Wed Jun 19 12:25:49 CEST 2013

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?


More information about the Glasgow-haskell-users mailing list