Anomaly "File "kernel/constr.ml", line 1483, characters 28-34: Assertion failed." with sort poly

[SkySkimmer]

  Inductive Box@{s|u|} (A:Type@{s|u}) := box (_:A).

  Definition t1@{s|u|} (A:Type@{s|u}) (x y : A) := box _ x.
  Definition t2@{s|u|} (A:Type@{s|u}) (x y : A) := box _ y.

  Definition ignore@{s|u|} {A:Type@{s|u}} (x:A) := tt.
  Definition unfold_ignore@{s|u|} (A:Type@{s|u}) : ignore (t1 A) = ignore (t2 A) := eq_refl.

The kernel first tries first conversion t1 A == t2 A so looks at the relevance of t1, it's a (bound) qvar so assert false in the kernel default_evar_handler.

[SkySkimmer]

also

Set Universe Polymorphism.

Inductive Box (A:SProp) : Prop := box (_:A).
Arguments box {_} _.

Definition t1'@{s|u|} (A:Type@{s|u}) (x y : A) := x.
Definition t2'@{s|u|} (A:Type@{s|u}) (x y : A) := y.

Check fun A:SProp => eq_refl : box (t1' A) = box (t2' A).
(* fails with anomaly instead of succeeding *)

because we don't store the right relevance in constr_relevance