<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">What you say may be true, but the behavior you describe is still inconsistent with the documentation. After all, the documentation states these things must all be simultaneously true:<div class=""><br class=""></div><div class=""><ul class="MailOutline"><li class="">Scoped type variables stand for type variables, not arbitrary types.<br class=""></li><li class="">Distinct scoped type variables correspond to distinct type variables.<br class=""></li><li class="">The type variables are always rigid.<br class=""></li></ul><div class=""><br class=""></div><div class="">Tom’s program can’t possibly obey all three of these things because that would imply that `x :: a` and `y :: b` where `a` and `b` are distinct skolems, so `add` could not possibly typecheck. But it does—so it sounds like older versions of GHC just diverged from the documentation in other, less significant ways.</div><div class=""><br class=""></div><div class="">Alexis</div><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 19, 2020, at 14:53, Viktor Dukhovni <<a href="mailto:ietf-dane@dukhovni.org" class="">ietf-dane@dukhovni.org</a>> wrote:</div><div class=""><div class=""><br class="">I added some follow up comments to the ticket you opened. I don't agree<br class="">with the analysis. Best I can tell (with some confidence after also<br class="">testing with GHC 8.0 which predates the above proposal), is that instead<br class="">what's happening is:<br class=""><br class=""> 1. The function has no explicit type signature, the below is<br class=""> just a term-level formula for its value:<br class=""><br class=""> add (x :: a) (y :: a) = x + y<br class=""><br class=""> 2. The type signature is inferred as usual:<br class=""><br class=""> add :: Num c => c -> c -> c<br class=""><br class=""> unifying the type `c` with the types of both of the terms `x`<br class=""> and `y`.<br class=""><br class=""> 3. But the formula contains two Pattern Type Signatures, binding<br class=""> the lexical type variable `a` to the type of `x` and the lexical<br class=""> type variable `b` to the type of `y`.<br class=""><br class=""> 4. However the types of `x` and `y` are both `c` (really some<br class=""> arbitrary fixed type variable, modulo alpha-renaming).<br class=""><br class=""> 5. Therefore, `a` and `b` are both the same type, not by virtue<br class=""> of type inference between `a` and `b`, but by virtue of simple<br class=""> pattern matching to an ultimately common type.<br class=""><br class="">The only thing that changed after the proposal was broadening of the<br class="">acceptable pattern matching to allow the pattern to match something<br class="">other than a type *variable*:<br class=""><br class="">Before:<br class=""><br class=""> f :: a -> Int<br class=""> f (x :: b) = 1 -- OK b ~ a<br class=""><br class=""> f :: Int -> Int<br class=""> f (x :: b) = 1 -- Bad b ~ Int, not a type variable!<br class=""><br class="">After: <br class=""><br class=""> f :: a -> Int<br class=""> f (x :: b) = 1 -- OK b ~ a<br class=""> f :: Int -> Int<br class=""> f (x :: b) = 1 -- OK b ~ Int<br class=""><br class="">However, Tom's example works both with GHC 8.0.x -- 8.6.x which fall<br class="">into the *before* case, and with GHC 8.8 and up, which are in the<br class="">*after* case.<br class=""><br class="">-- <br class=""> Viktor.</div></div></blockquote></div></div></body></html>