Error on empty constraints @{|} with universe checking off

[drcicero]

Description of the problem

I was hoping to use unset universe checking to disable universes, and temporarily work in Type:Type bliss. However, occasionally my code still fails on a universe constraint even though I have disabled universe checking. I tried to minimize the problem and came up with the idea to define an identity universe cast function. And indeed it does not work; the error message “Universe constraints are not implied by the ones declared” comes up independent of whether universe checking is set or not:

Set Universe Checking.
Fail Definition castU@{u v |}(t: Type@{u}): Type@{v} := t.
(* The command has indeed failed with message:
Universe constraints are not implied by the ones declared: u <= v *)

Unset Universe Checking.
Fail Definition castU@{u v |}(t: Type@{u}): Type@{v} := t.
(* The command has indeed failed with message:
Universe constraints are not implied by the ones declared: u <= v *)

Furthermore, if I leave all universes to be inferred, and unset universe checking Coq will nevertheless generate universe constraints, e.g., u <= u0:

Set Universe Checking.
Set Universe Polymorphism.
Definition castU(t: Type): Type := t.
Set Printing Universes.
Print castU.
(* castU@{u u0} = fun t : Type@{u} => t
        : Type@{u} -> Type@{u0}
   (* u u0 |= u <= u0 *)
*)

I asked this on discourse first https://coq.discourse.group/t/is-it-possible-to-define-a-cbn-able-universe-cast-with-universe-checking-disabled/1899/1 and SkySkimmer encouraged me that this could be considered a bug.

Coq Version

The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.13.1