[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Tom Ellis]

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

The reason for this behaviour is that

> in all patterns other than pattern bindings, a pattern type
> signature may mention a type variable that is not in scope; in this
> case, the signature brings that type variable into scope.

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#pattern-type-signatures

and the justification is that

> Bringing type variables into scope is particularly important for
> existential data constructors

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`.  `k3` would also be forbidden (the type variables
called `a` are actually distinct) as would `k4` (the type variable for
the inferred signature would be fresh and distinct from `a`).

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?

Tom


    data T = forall a. MkT [a]
    
    k :: T -> T
    k (MkT [t::a]) =
        MkT t3
      where
       (t3::[a]) = [t,t,t]

    data T2 a = MkT2 [a]
    
    k2 :: T2 b -> T2 b
    k2 (MkT2 [t::a]) =
        MkT2 t3
      where
       (t3::[a]) = [t,t,t]

    k3 :: T2 a -> T2 a
    k3 (MkT2 [t::a]) =
        MkT2 t3
      where
       (t3::[a]) = [t,t,t]

    k4 (MkT2 [t::a]) =
        MkT2 t3
      where
       (t3::[a]) = [t,t,t]