Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`? In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of Fω


  30.4.1 Deﬁnition: In System F1 , the only kind is * and no quantiﬁcation (∀) or abstraction (λ) over types is permitted. 
  
  F1 is just our simply typed lambda-calculus, λ → . Its deﬁnition is super-
  ﬁcially more complicated than Figure 9-1 because it includes kinding and
  type equivalence relations, but these are both trivial: every syntactically well formed type is also well kinded, with kind *, and the only type equivalent to a type T is T itself


Is it correct that  quantification ∀ means universal types?

* is the kind of proper types, which are introduced on p442:


  The level of types contains two sorts of expressions. First, there are proper
  types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are inhabited
  by terms. (Of course, not all terms have a type; for example (λx:Nat.x) true
  does not.)


So universal types such as ∀X.X→X are proper types, and thus belong to kind *. 
Why can System F1 have kind *, but no universal types, i.e. quantification ∀?

But if System F1 could have kind * and quantification ∀, then wouldn't it become the same as System F2 a.k.a. System F? Quoted from on p461:


  In System F2 , we still have only kind * and no lambda-abstraction at the level of types, but we allow quantiﬁcation over proper types (of kind *).
  
  F2 is our System F; 


Thanks.
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".