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
