Algebraic universe on the right (polyproj)

[JasonGross]

Am I supposed to see Algebraic universe on the right? The following code fails at Defined (it should probably fail to pose?), but prints out Algebraic universe on the right at pose.

Monomorphic Definition U1 := Type.
Monomorphic Definition U2 := Type.

Set Printing Universes.
Definition foo : True.
let t1 := type of U1 in
let t2 := type of U2 in
pose (t1 : t2). (* Algebraic universe on the right *)
exact I.
Fail Defined.
(* The command has indeed failed with message:
=> Error:
The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)"
while it is expected to have type "Type (* Top.2+1 *)". *)