<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><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> The reason for this behaviour is that
>
>><i> in all patterns other than pattern bindings, a pattern type
</i>>><i> signature may mention a type variable that is not in scope; in this
</i>>><i> case, the signature brings that type variable into scope.
</i><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">OK so your `PatternSignatures` (a part of `ScopedTypeVariables` that existed long before the more dubious parts of that extension) are bringing `a`, `b`, into scope. It might have been clearer if you'd used `b`, `c`, to avoid confusing yours with some `a` that might have been lurking in the environment.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">Anyhoo your definition is equivalent to this, by eta-reduction:</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    add = (+)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">and `(+) :: Num a => a -> a -> a` from the Prelude. So the inferred signature for `add` must be the same, possibly alpha-renamed.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">Perhaps you think you could add an Int to a Float, as you can in languages (COBOL, Algol 68) with implicit type coercion? That's not what the signatures from the Prelude Num methods support. And with Haskell's proclivity for partial application, type inference would rapidly become incoherent; so we don't do that.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> But this leads to a rather puzzling user experience.  Was it really
> not possible to design this extension in a way that would allow
> bringing new type variables into scope locally but not allow them to
> unify with other type variables from outer scopes?
>
> To be more concrete, what I would like to see is a design where `k` is
> allowed because the type `a` (bound within a pattern) does not need to
> unify with anything but `k2` is not allowed because `a` is forbidden
> to unify with `b`. ...</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">No: any tyvar might unify with any other. You can't ban tyvars from unifying. Unification would be useless if you can't unify globally. That's why all tyvars are (implicitly) universally quantified. (With the exception of existentially-quantified tyvars as you quote, which is another can of worms and we don't want to go there.)  You can use as many distinct tyvars as you like, but if type inference resolves them to  the same type, it must use the same tyvar in the inferred signature.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> I believe this design might lead to much less puzzling behaviour.
> Would it be possible (within a new extension, of course) or have I
> overlooked something?
<br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">There's the `GADTs` or `TypeFamilies` extensions that introduce `~` as a constraint-level equality on types. I suppose we might use that, but (thinking creatively) any of these would be a legitimate resulting signature; how should GHC choose amongst them?</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    add :: (Num a, a ~ b) => a -> b -> a</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    add :: (Num b, a ~ b) => a -> b -> b</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    add :: (Num a, Num b, a ~ b) => a -> b -> a
</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><pre style="white-space:pre-wrap"></pre>The point is: the return type for `add` aka `(+)` must be the same as the first argument type must be the same as the second argument type must be the same as the `Num` constraint applies to.
<br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">Any of those three signatures I've given (and there could be several more in the same vein) obfuscates what's going on.
<br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">Actually, thinking a bit more: we want to infer a 'Principal type' (see wikipedia). Precisely because there's no good reason to choose amongst those I gave, none of them can be Principal.

</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">AntC

</pre><br class="gmail-Apple-interchange-newline"></div>