<div dir="ltr"><div dir="ltr">On Mon, 17 Aug 2020 at 07:10, Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz">anthony_clayden@clear.net.nz</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><pre style="white-space:pre-wrap;color:rgb(0,0,0)">Hi Tom, I see nothing bizarre nor counterintuitive. Perhaps you need to retrain your intuitions ;-)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> 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
<br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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.</pre></div></blockquote><div><br></div><div>I can't speak for Tom, but to me the above feels very similar to writing something like:</div><div><br></div><div><span style="font-family:monospace">    add :: _ => a -> b -> _</span></div><div><span style="font-family:monospace">    add x y = x + y</span></div><div><span style="font-family:monospace"><br></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif">But that doesn't type check, since the types `a` and `b` are not the same, but `+` needs them to be.</font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif"><br></font></span></div><div><span style="font-family:monospace"><font face="arial,sans-serif">Erik</font></span><br></div></div></div>