[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Tom Ellis]

On Mon, Aug 17, 2020 at 05:08:10PM +1200, Anthony Clayden wrote:
> Hi Tom, I see nothing bizarre nor counterintuitive. Perhaps you need
> to retrain your intuitions ;-)

Perhaps, but I think my intuitions are fairly sound.

> > 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?

Erik in his sibling post gave the reason: x and y are given types that
appear not to match, but for the function to type check the types do
indeed need to match.  (My objection is really nothing to do with the
choice of "a" for the inferred signature; I only put the inferred
signature there to confirm that's indeed what it is.)

> > 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`. ...
> 
> 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.)
[...]

I think that's exactly where we (or I at least) want to go!  It feels
that what I'm asking for is very similar to the typechecking rules for
existentials, although I'm not familiar enough with that part of the
typechecker to say for sure.

Tom