This is an example of Coq collapsing any universe level i to Set when we have a constraint of the form Set <= i.

CollapseToSet.v

Set Universe Polymorphism.
Set Printing Universes.

Record X : Type :=
  {
    A : Type;
    x : A
  }.

Definition untt := {|A := unit; x := tt|}.

Print untt.
(*
untt = {| A := unit; x := tt |}
     : X@{Set}

untt is universe polymorphic
 *)

Definition UNTT := {|A := unit : Type; x := tt|}.

Print UNTT.
(*
UNTT = 
{| A := unit:Type@{Top.8}; x := tt |}
     : X@{Top.8}
(* Top.8 |= Set <= Top.8
             *)

UNTT is universe polymorphic
*)

Definition W := UNTT.

Print W.
(*
W = UNTT@{Set}
     : X@{Set}

W is universe polymorphic
 *)


Definition W' := UNTT@{i}.

Print W'.
(*
W' = UNTT@{Top.7}
     : X@{Top.7}
(* Top.7 |= Set <= Top.7
             *)

W' is universe polymorphic
*)