Adding to my previous email, I’ve noticed that the behavior I’ve described appears to be inconsistent with the documentation. 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. This suggests that your program should not be accepted (and that GHC shouldn’t work the way I describe, even if that’s how it works in practice today), so either the current implementation is buggy, or the documentation is buggy. I am not sure which.

I have opened GHC issue #18591 to track this inconsistency.

Alexis