Good point. I stand corrected. -Brent
On Wed, Jun 19, 2013 at 11:42:23AM -0300, Felipe Almeida Lessa wrote: > Brent, maybe I'm misunderstanding what you're saying, but I don't > think that the order of the arguments is playing any role here besides > defining the order in which the pattern matches are desugared. > > To illustrate, > > -- This does work > foo1' :: a -> Foo a -> Int > foo1' m Foo = case m of > Nothing -> undefined > Just _ -> undefined > > Despite having the same type as foo1, foo1' does work because now I've > pattern matched on the GADT first. As soon as I do that, its equality > constraint of (a ~ Maybe v) enters into scope of the case branches. > > Cheers, > > On Wed, Jun 19, 2013 at 7:59 AM, Brent Yorgey <byor...@seas.upenn.edu> wrote: > > 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 > > > > -- > Felipe. > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe