In a system where Type:Type, the typing rule for the product would be trivial:
$$\frac{\Gamma \vdash A:Type\hspace{1cm} \Gamma, x:A \vdash B:Type}
{\Gamma \vdash \forall x\!:\!A.B : Type}$$
Unfortunately, Type:Type is known to be inconsistent, and Type must
inhabit some different sort, say Type:BigType. Then, the following case of the
product becomes problematic:
$$\Gamma \vdash A:BigType\hspace{1cm} \Gamma, x:A \vdash B:Type$$
You may either conclude that
$$ (*)\;\;\Gamma \vdash \forall x:A.B : BigType$$
or
$$ (**)\;\; \Gamma \vdash \forall x:A.B : Type $$
The first approach, where you take the maximum among the type of A and
B is the so called predicative approach, giving rise to a strictly
stratified type theory. This is indeed consistent with our intuition of
types as data structures.
The second approach is "impredicative": since Type:BigType, if B:Type, we get
$$ \forall X\!:\!Type.B: Type$$
but this expression is quantifying over a collection of items (Type)
comprising the product type we are defining as one of its elements.
Note however that is not so unreasonable in case you are interpreting Types as
propositions: if $B:Prop$, then $\forall X\!:\!Prop.B$ looks like a legitimate, higher order
proposition, hence it looks quite "natural" (for everybody who is not a
constructivist) to conclude that
$\forall X\!:\!Prop.B : Prop$
In fact, (**) is not inconsistent (system F adopts this rule).
The only price you have to pay is that you must renounce to have strong
elimination rules. In Coq terms, you
cannot extract from a proposition anything but a proof of some other
proposition. As a corollary, you have no way in Coq to prove that two proofs of a same proposition are different from each other.