As it often happens with Coq, the answer is historical reasons.
In the original version dating back from 1984, Coq was based on the Calculus of Constructions, a barebone dependent type theory. In particular, it did not feature inductive types. Instead, following the PTS tradition, it had impredicative universes.
The introduction of inductive types did not change this state of affair, and for a long time Coq had two impredicative universes,
Set. The difference between both lied in the fact that the former was erased by extraction, but not the latter. This phase separation had been around for a long time already.
When dealing with several impredicative universes, one has to be extremely careful because proofs of
False lurk around the corner. In particular,
Prop : Set when both are impredicative is enough be a variant of Girard's system U⁻ and thus inconsistent. The Coq developers of yore were well aware of this issue and relied on an alternative hierarchy, so that
Prop : Type and
Set : Type.
Now, at some point it was decided to make
Set predicative by default, for other somewhat related reasons. Indeed, impredicative proof-relevant universes are very much inconsistent with many slightly classical principles like excluded middle in
Type or some forms of choice. In particular and ironically, with an impredicative
Set, Coq has no set-theoretical model (as in Polymorphism is not set-theoretic). Nowadays,
Set is thus predicative except if the user opts in impredicativity with a specific flag.
Impredicative set is essentially not used as of today, and really not tested so it has fallen to bitrot. It is extremely likely that it is not usable anymore, and there is an evergreen discussion about its removal. Yet, since the flag still exists Coq needs to at least pretend to avoid inconsistencies when the user sets it, and therefore one cannot have
Prop : Set.
If the flag ever gets removed, maybe we can consider adding this rule, but then there might be weird backwards incompatibilities. Therefore, it is not even clear we will ever perform this change even in a situation where it is perfectly sound.
Setis not actually predicative $\endgroup$