Why Set < Top.i by default?

The coq manual says " To ensure compatibility, every global universe is set to be strictly greater than Set when it is introduced". Why is that? What compatibility is being considered? I know Set needs to be different when using -impredicative-set, but what about the common case where that option is not passed?

(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" ) -*- *)
Universe u.
Inductive unit : Type@{u} := tt.
Print Universes.
(* Set < Top.24 *)
(*     < u *)
(* Prop < Set *)

I am asking because this makes non-polymorphic container types and non-container types have different universes (e.g. nat is in Set but list nat is <Set if `list is not universe polymorohic or template polymorphic).

I think the idea is that if you have a Type you probably don’t want it
lowered to Set. ie if you have universe-monomorphic list, when using
list nat : Set the options are either that every list and types it’s
been applied to becoming Set and prevent anyone else from applying list
to non-Set, or an error. (I guess in practice probably someone has
already applied list to something that can’t be Set so you can’t avoid
the error)

Gaëtan Gilbert

That’s an historic choice, I think everything would be fine if only Set <= i was required (I don’t think potential impredicativity is important here). However that would still leave your list type in i unless you make it Set -> Set explicitly. Note that the universe of list has to be greater or equal to its parameter universe, so any later instantiation of list A with A’s type larger than Set will make its conclusion type “grow” accordingly.