Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`?
Why can System F1 have kind *, but no universal types, i.e. quantification ∀?


Because "System F1 has types of kind *" does not mean "any types which have kind * in some other system (e.g. universal types) are allowed in F1".