<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Adding to my previous email, I’ve noticed that the behavior I’ve described appears to be inconsistent with the documentation. From the <a href="http://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/glasgow_exts.html#id59" class="">GHC 8.10.1 User’s Guide § 9.17.1, Lexically scoped type variables » Overview</a>:<div class=""><br class=""></div><div class=""><blockquote type="cite" class="">The design follows the following principles<br class=""><div class=""><ul class=""><li class="">A scoped type variable <b class="">stands for a type variable, and not for a type</b>. (This is a change from GHC’s earlier design.)</li><li class="">Furthermore, <b class="">distinct lexical type variables stand for distinct type variables</b>. This means that every programmer-written type signature (including one that contains free scoped type variables) <b class="">denotes a rigid type</b>; that is, <b class="">the type is fully known to the type checker, and no inference is involved</b>.</li><li class="">Lexical type variables may be alpha-renamed freely, without changing the program.</li></ul></div></blockquote>Emphasis mine. This suggests that your program <i class="">should not</i><span style="font-style: normal;" class=""> be accepted (and that GHC </span><i class="">shouldn’t</i><span style="font-style: normal;" class=""> work the way I describe, even if that’s how it works in practice today), so</span> either the current implementation is buggy, or the documentation is buggy. I am not sure which.</div><div class=""><br class=""></div><div class="">I have opened <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/18591" class="">GHC issue #18591</a> to track this inconsistency.</div><div class=""><br class=""></div><div class="">Alexis</div></body></html>