[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In TAPL's constraint typing rules (Figure 22-1), is it possible for the context to contain free type variables that aren’t part of the fresh variables? Because the typing rules are based on the STLC with an infinite number of base types (and T-Var allows anything in Γ to be introduced into t or T), a naïve reading would allow for Γ, t, or T to contain type variables not mentioned in χ. However, this implies to me that pathological typing derivations exist where e.g. I can apply CT-Abs to two subderivations for which 𝐶₂ contains type variables in χ₁. Intuitively, this seems to defeat the purpose of the fresh variable sets. Does TAPL implicitly assume that Γ is “closed” with respect to χ, maybe? Thanks, Joshua Grosso
