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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
