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.