Well I'll go to 'foot of our stairs!

[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