[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Viktor Dukhovni]

On Sun, Aug 16, 2020 at 01:17:11PM +0100, Tom Ellis wrote:

>     -- Inferred signature:
>     -- add :: Num a => a -> a -> a
>     add (x :: a) (y :: b) = x + y
> [...]
> 
> 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?

Back to Tom's original question, the answer is "no" because in fact no
unification of `a` and `b` is taking place.  The type variables `a` and
`b` in the above lexical Pattern Type Signatures are not "generalised":

    http://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/glasgow_exts.html#pattern-type-signatures

    Unlike expression and declaration type signatures, pattern type
    signatures are not implicitly generalised.

So what the example definition of `add` says (beyond giving a formula
for add x y) is that also the lexical type variables `a` and `b`
satisfy:

    a ~ TypeOf(x)
    b ~ TypeOf(y)

but since we've already inferred: TypeOf(x) ~ TypeOf(y), bringing `a`
and `b` into scope does not change that in any way.

-- 
    Viktor.