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... 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]