> [Erik] the above feels very similar to writing something like:

>        add :: _ => a -> b -> _
>        add x y = x + y
>
> But that doesn't type check, since the types `a` and `b` are not the same,
> but `+` needs them to be.

Replying to both Erik's and Tom's replies. I'm afraid Alexis' went completely over my head.

As I mentioned, the `PatternSignatures` part of `ScopedTypeVariables` has been around a long time. So long that it's in Hugs 2006. The same? Not quite. If I try Tom's O.P.

    add (x :: aa) (y :: b) = x + y

Hugs complains 'Type annotation uses distinct variables aa and b where a single variable was inferred'.

So the short answer is: if that's how your intuitions go, use Hugs.

My explanation was going to be (this now only applies for GHC): just as using `x, y` as the dummy arguments to `add` doesn't come with any guarantees they're distinct values; so using `aa, b` as the dummy variables doesn't come with any guarantees they're distinct types.

Specifying distinct tyvars in a stand-alone signature is different: you're giving the most general type to which `add` must conform. And using distinct tyvars means `add` must cope with those being distinct types. (Which it's equation doesn't.) BTW GHC accepts:

    add (x :: aa) (y :: b) = (x + y :: aa) :: b

which shows how happy it is to use distinct tyvars for the same type.

AntC