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 http://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/glasgow_exts.h...:
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 https://gitlab.haskell.org/ghc/ghc/-/issues/18591 to track this inconsistency. Alexis