[Haskell-cafe] GADTs and pattern matching

[Brent Yorgey]

On Wed, Jun 19, 2013 at 11:11:16AM +0100, Francesco Mazzoli wrote:
> 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

Yes, I was going to suggest switching the argument order before
reading your message.  This is an interesting way in which you can
observe that Haskell does not really have "multi-argument functions".
All multi-argument functions are really one-argument functions which
return functions.  So a function of type

  foo1 :: a -> (Foo a -> Int)

must take something of type a (for *any* choice of a, which the caller
gets to choose) and return a function of type (Foo a -> Int).  *Which*
function is returned (e.g. one that tries to pattern match on the Foo)
makes no difference to whether foo1 typechecks.

On the other hand, a function of type

  foo2 :: Foo a -> (a -> Int)

receives something of type Foo a as an argument.  It may pattern-match
on the Foo a, thus bringing into scope the fact that (a ~ Maybe v).
Now when constructing the output function of type (a -> Int) it may
make use of this fact.

-Brent