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