Broken type variable scoping

[jstolarek]

Consider this program:

let (f : forall a b. a -> b -> b) =
  let (g : forall b. a -> b -> b) = \(y:a).\z.z in id ~g
in f

There are two problems:

1. It hits an assertion in SolverLo (assert (G.all_generic_vars_bound s)) because it doesn't recognise that variable a in the signature of g is bound. Possibly related to #28. My email to @frank-emrich from 22/01/2021, 12:50 has some additional explanation of how scoping in type signatures currently works.
2. After commenting out that assertion it generates an incorrect System F term:

Pretty-printing the System F term...
  Λ33. Λ32. let id = Λ26. λ(x : 26). x in
  let f = Λ1. Λ2. let g = Λ2. λ(y : 1). λ(z : 2). z in
  id [∀ [2]. 1 → 2 → 2] g in
  f [32] [33]
Converting the System F term to de Bruijn style...
Type-checking the System F term...
Expected type does not match actual type!
Expected:
  ∀(). ∀(). (1 → 0) → 0
Actual:
  ∀(). ∀(). ∀(). 1 → 0 → 0

I believe the Λ2 abstraction on f is unnecessary.

[frank-emrich]

Note that according to our discussion, this example shouldn't type-check. The only system in which this example may type-check is "pure FreezeML", a system briefly mentioned in the PLDI paper. This would be a variant of FreezeML that does not obey the value restriction, but has some complicated (we never stated how exactly) behavior regarding type variable scoping. In particular, this "pure FreezeML" is different from the much simpler variant of FreezeML without the VR that we presented in the Explicit FreezeML paper.