Scoped type variables

[byorgey]

Type variables in polymorphic types now scope over any nested local type signatures by default. Closes #2168.

• Any polymorphic type, whether written with an explicit forall or not, brings all its variables into scope in the body of its definition.
• Any type variables declared with an explicit forall are introduced as new variables, and in particular they will shadow any type variables already in scope with the same names.
• Any type variables not bound by an explicit forall which are not already in scope will be implicitly quantified. Any such type variable names which are in scope will simply refer to the name in the enclosing scope.

So, for example, this will work:

def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : RBTree k v = inr t in
  let balanceRR : RBNode k v -> RBTree k v = ...
  in undefined
end

The type signature on balance will bring k and v into scope in its body (even though there is not an explicit forall written); then the k and v in the type signatures on baseCase and balanceRR will both refer to the k and v bound in the type of balance. In particular, this means that inr t is a valid definition for baseCase since their types match. On the other hand, if one were to write

def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : forall k v. RBTree k v = inr t in
  undefined
end

then the k and v in the type of baseCase would be new type variables which are different than the k and v in the type of balance (which would now be shadowed within the definition of baseCase). This would now be a type error (which is what happens currently), since baseCase is required to be an RBTree k v for any types k and v, but inr t only has the specific type that was given as an input to balance.

Finally, if one wrote

def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : forall k. RBTree k v = inr t in
  undefined
end

then only k would be a new type variable, whereas v would refer to the v from the type of balance. (This would still be a type error, of course.)

In addition, what used to be Polytype is now two separate types: RawPolytype is what we get out of the parser, before implicit quantification has been carried out. A Polytype is guaranteed to be properly quantified, i.e. variables bound by the forall are explicitly listed. We carefully do not export the constructor so we can be sure that the typechecker is making sure that we never accidentally use a RawPolytype before we implicitly quantify over it.

[byorgey]

@xsebek I think it works now. I would appreciate any additional torture-testing you are able to do.

[byorgey]

Actually, I think this is not ready to merge --- I'm afraid I've made it too easy to make mistakes and this will just lead to problems down the road. Currently working on adding more type indexing so the Haskell type system will prevent us from using parsed polytypes that haven't been properly implicitly quanitified. I'd still appreciate any feedback / testing anyone would like to do in the meantime.

[byorgey]

@xsebek OK, I think this is ready to go now!

[xsebek]

Works well and the documentation is neat. 👍