[Haskell-cafe] GADTs and pattern matching

[Francesco Mazzoli]

At Wed, 19 Jun 2013 10:03:27 +0000 (UTC),
AntC wrote:
> 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.
> 
> [...]
>
> Yep, that message explains what's going on well enough for me.

Did you read the rest of the code?  That ought to work, because GHC
infers and uses the type equality (something like ‘v ~ Var v1’) and uses
it to coerce the ‘x’.

And, surprise surprise, if the argument order is switched, it works!

    data Foo v where
        Foo :: forall v. Foo (Maybe v)
    
    foo1 :: Foo a -> a -> Int
    foo1 Foo Nothing  = undefined
    foo1 Foo (Just x) = undefined

Francesco