[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Anthony Clayden]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200818/21451e90/attachment.html>