>>123
> 逆に型推論も型クラスもないSystem Fなんかは型レべルのラムダを許す

GirardのSystem Fには型レベルのラムダ（型についてパラメタ化された型、つまり型構成子のユーザ定義能力）は存在しないよ。
項で型についてパラメタ化するのは多相型の項を構築する手段だからもちろん許してるけどね。
System Fが型レベルで許しているのは、多相型、つまり型変数を含む型式をその自由型変数について全称束縛する事。
∀ｔ. τ(t) と λt. τ(t) とを混同しては駄目だよ。（ここで t は型変数で τ(t)は型変数 t が自由に出現し得る型式、例えば int × t とかね）