[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Viktor Dukhovni]

On Wed, Aug 19, 2020 at 12:41:13PM -0500, Alexis King wrote:

> …and now Krzysztof Gogolewski has already chimed in with an explanation:
> 
> > The documentation is outdated (it was written in 2006). Scoped type
> > variables can use arbitrary types since #15050 (closed),
> > https://github.com/ghc-proposals/ghc-proposals/blob/scoped-type-variables-types/proposals/scoped-type-variables-types.rst
> > <https://github.com/ghc-proposals/ghc-proposals/blob/scoped-type-variables-types/proposals/scoped-type-variables-types.rst>.
> 
> So the issue is a documentation bug, and my explanation is how GHC is
> intended to operate. The linked proposal includes a little additional
> context, including a short paper, Type variables in patterns
> <https://arxiv.org/pdf/1806.03476.pdf> (published at Haskell ’18).
> Mystery resolved—though the docs still need fixing.

I added some follow up comments to the ticket you opened.  I don't agree
with the analysis.  Best I can tell (with some confidence after also
testing with GHC 8.0 which predates the above proposal), is that instead
what's happening is:

    1.  The function has no explicit type signature, the below is
        just a term-level formula for its value:

            add (x :: a) (y :: a) = x + y

    2.  The type signature is inferred as usual:

            add :: Num c => c -> c -> c

        unifying the type `c` with the types of both of the terms `x`
        and `y`.

    3.  But the formula contains two Pattern Type Signatures, binding
        the lexical type variable `a` to the type of `x` and the lexical
        type variable `b` to the type of `y`.

    4.  However the types of `x` and `y` are both `c` (really some
        arbitrary fixed type variable, modulo alpha-renaming).

    5.  Therefore, `a` and `b` are both the same type, not by virtue
        of type inference between `a` and `b`, but by virtue of simple
        pattern matching to an ultimately common type.

The only thing that changed after the proposal was broadening of the
acceptable pattern matching to allow the pattern to match something
other than a type *variable*:

Before:

    f :: a -> Int
    f (x :: b) = 1      -- OK b ~ a

    f :: Int -> Int
    f (x :: b) = 1      -- Bad b ~ Int, not a type variable!

After: 

    f :: a -> Int
    f (x :: b) = 1      -- OK b ~ a
    f :: Int -> Int
    f (x :: b) = 1      -- OK b ~ Int

However, Tom's example works both with GHC 8.0.x -- 8.6.x which fall
into the *before* case, and with GHC 8.8 and up, which are in the
*after* case.

-- 
    Viktor.