The documentation for scoped type variables is outdated and does not reflect the implementation
In a recent message on the haskell-cafe mailing list, Tom Ellis provided the following program, which uses
-- Inferred signature: -- add :: Num a => a -> a -> a add (x :: a) (y :: b) = x + y
GHC accepts this program. Tom describes the program as “bizarre,” since it allows two different type variables to refer to the same type, which is inconsistent with the way type variables work in other situations.
This behavior seems inconsistent with the documentation to me. From the GHC 8.10.1 User’s Guide § 9.17.1, Lexically scoped type variables » Overview:
The design follows the following principles
A scoped type variable stands for a type variable, and not for a type. (This is a change from GHC’s earlier design.)
Furthermore, distinct lexical type variables stand for distinct type variables. This means that every programmer-written type signature (including one that contains free scoped type variables) denotes a rigid type; that is, the type is fully known to the type checker, and no inference is involved.
Lexical type variables may be alpha-renamed freely, without changing the program.
Emphasis mine. These principles suggest that a program like Tom’s should not be accepted, since
b should be distinct rigid type variables. This seems like either an implementation bug or a documentation bug to me.