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-ty... https://github.com/ghc-proposals/ghc-proposals/blob/scoped-type-variables-ty....
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.