On Wed, Aug 19, 2020 at 04:58:00PM -0500, Alexis King wrote:
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:
1. Scoped type variables stand for type variables, not arbitrary types. 2. Distinct scoped type variables correspond to distinct type variables. 3. The type variables are always rigid.
Though perhaps much too careful/complete a read of the documentation is needed to see support in the documentation for the conclusions I ultimately reached, I do believe that the text is on some level there (that is, the behaviour essentially matches the documentation when all of it is read with some care, to some extent "between the lines"), but it could/should be much more explicit. Specifically, though reading the high-level overview indeed leads to your summary above: 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.) [ This is the part that's later relaxed in 15050 ] * 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. [ Item 2 + 3 ] * Lexical type variables may be alpha-renamed freely, without changing the program. [ More of 3. ] These are later refined in a way that reduces the universality of 2 and 3. First we have: A declaration type signature that has explicit quantification (using forall) brings into scope the explicitly-quantified type variables, in the definition of the named function. that shows that scoped type variables are typically introduced via an explicit "forall", and of course in this case, given "forall a b. ..." the "a" and "b" in question are distinct. But when we get to "9.17.4. Pattern type signatures": http://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/glasgow_exts.h... In the case where all the type variables in the pattern type signature are already in scope (i.e. bound by the enclosing context), matters are simple: the signature simply constrains the type of the pattern in the obvious way. Unlike expression and declaration type signatures, pattern type signatures are not implicitly generalised. The pattern in a pattern binding may only mention type variables that are already in scope. ... However, in all patterns other than pattern bindings, a pattern type signature may mention a type variable that is not in scope; in this case, the signature brings that type variable into scope. we see that are they are rather different beasts, that deviate from the description in the overview. In particular, "2" no longer holds, because these are neither generalised, nor universally quantified. Instead, most of the time they are just references to allready bound lexical variables constraining the type of the term to be the type of some variable already in scope. These are different provided the earlier definitions are different (e.g. forall a b. ...). However, when a Pattern Type Signature brings a new variable into scope, it is simply a type alias for the type of the term, and by virtue of not being univsally quantified or generalised, ... is a mere alias of whatever type variable (after 15050, relaxed to also allow actual types) is associated with the term in question. Now admittedly, this involves some "reading between the lines" to infer that the crucial thing that (unavoidably) gives us "2" and "3" is introduction via universal quantification. And that the overview does not adequately carve out an exemption from that far more common case to the case where instead a Pattern Type Signature just pattern matches the existing type of a term and gives a name so we can reuse that name in other terms. And it is these pattern matched type aliases, that while not directly unified, might under various conditions refer to the same actual type even if bound to different lexical names, because their bindings at the point of introduction are not to new universally quantified types, but are to known (possibly inferred) types of the terms in the pattern. So my conclusion is that enough information is present in the documentation to understand the observed behaviour as consistent with the detailed case-by-case breakdown, even while not matching the general overview.
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.
Well, in fact the major deviations from the overview are there even even as far back as GHC 7.10. All that changed more recently (GHC 8.8) is a more minor shift to allow the "aliased" term type to be a concrete type, rather than just a type variable. I do agree that the documentation should be more clear, in particular the overview is NOT a good (correct) description of lexicals brought into scope via Pattern Type Signatures. -- Viktor.