Errata for System F

[Blaisorblade]

(In case this material is reused for next edition of the course, as I guess).

The presentation of System F (in TAPL itself, and in 25-subtyping_and_systemf.pdf) in is not quite right, because it doesn't check that types are well-formed — therefore, it does not check that type variables are bound in the context. In particular, I can IMHO type 𝜆 x: X. 𝜆 y: Y. x (where X and Y are type variables) in the empty context. That's different from what happens in either Harper's PFPL presentation, or if you treat System F as a PTS instance.

This is addressed (differently) in Pierce's errata:

p 342, near bottom

In addition to

 We continue the convention (5.3.4) that the names of (term or type)
 variables should be chosen so as to be different from all the names
 already bound by $\Gamma$, ...

we should add the restriction that a context of the form $\Gamma, x : T$
is well-formed only if every type variable free in $T$ is bound by
$\Gamma$.

I prefer the PTS approach of checking types for well-formedness/well-kindedness before adding them to the context, maybe because I'm more used to it, and I'm not convinced Pierce's fix actually works. I think it still lets me type:

f: ∀ X . X → X �⊦ f [Y] : Y → Y

If that's right, I'll also try to mail Pierce.