Foralls, Kinds with Arrows, and Impredicativity (?)

I can't figure out why the kinding rule for universal quantification in F_ω is:

           C, x : k1 |- y : *
(1)    -----------------------------
       C |- (\forall x : k1 . y) : *

That is, why the type inside the universal quantification must be of kind *.

I would expect the rule to be

            C, x : k1 |- y : k2
(1')    ------------------------------
        C |- (\forall x : k1 . y) : k2

Using (1), I can still get

              C, x : k1 |- y : * -> *
(2)    ------------------------------------------------------
       C |- (\Lambda z : * . \forall x : k1 . y @ z) : * -> *

by eta-expansion, so using (1) instead of (1') doesn't seem to reduce the available power, it just makes the notation more annoying.

I suspect that the reason for (1) instead of (1') has something to do with impredicativity, since (1) is only valid in impredicative systems anyway.