Why an infinite type hierarchy? Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, which has only two sorts, $*$ and $◽$, and these rules?

$$\frac {} {∅ ⊢ * : ◽}$$

$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ t : T _ 2} {Γ ⊢ (λ \: x : T _ 1, \: t) : (Π \: x : T _ 1, \: T _ 2)}$$

$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ T _ 2 : s _ 2} {Γ ⊢ (Π \: x : T _ 1, \: T _ 2) : s _ 2}$$

This seems simpler. Does this system have important limitations?
Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.

The reason it is not widely used is because impredicative quantification is incompatible with classical logic. If you have it, you cannot give a model of type theory where types are interpreted as sets in the naive way --- see John Reynolds's famous paper Polymorphism is Not Set-theoretic. 

Since many people want to use type theory as a way to machine-check ordinary mathematical proofs, they are generally unenthusiastic about type-theoretic features which are incompatible with the usual foundations. In fact, Coq  originally supported impredicativity, but they have steadily abandoned it.