[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Viktor Dukhovni]

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.html#pattern-type-signatures

    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.