On Mon, 17 Aug 2020 at 07:10, Anthony Clayden <anthony_clayden@clear.net.nz> wrote:

Hi Tom, I see nothing bizarre nor counterintuitive. Perhaps you need to retrain your intuitions ;-)

> I have just noticed that with ScopedTypeVariables one can write the
> following bizarre definition
>
>    -- Inferred signature:
>    -- add :: Num a => a -> a -> a
>    add (x :: a) (y :: b) = x + y

What do you think is bizarre? GHC makes a reasonable attempt to use the tyvar names you put in a signature -- remembering that alpha-renaming means the name is not really significant. I can get `add :: Num c => c -> c -> c`, etc.

I can't speak for Tom, but to me 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.

Erik