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?
Why an infinite type hierarchy?
coq;dependent type;calculus of constructions
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. 