Re: [Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

What you say may be true, but the behavior you describe is still inconsistent with the documentation. After all, the documentation states these things must all be simultaneously true: Scoped type variables stand for type variables, not arbitrary types. Distinct scoped type variables correspond to distinct type variables. The type variables are always rigid. Tom’s program can’t possibly obey all three of these things because that would imply that `x :: a` and `y :: b` where `a` and `b` are distinct skolems, so `add` could not possibly typecheck. But it does—so it sounds like older versions of GHC just diverged from the documentation in other, less significant ways. Alexis

On Aug 19, 2020, at 14:53, Viktor Dukhovni wrote:

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.