diff --git a/test-suite/bugs/bug_16880.v b/test-suite/bugs/bug_16880.v
new file mode 100644
index 000000000000..b1fc1f211ede
--- /dev/null
+++ b/test-suite/bugs/bug_16880.v
@@ -0,0 +1,13 @@
+Polymorphic Axiom T@{u} : Prop.
+
+Universe u1 u2.
+
+Definition t1 := T@{u1}.
+Definition t2 := T@{u2}.
+
+Constraint u1 = u2.
+
+Check fun P : t1 => P <: t2.
+(* Error: In environment
+P : t1
+The term "P" has type "t1" while it is expected to have type "t2". *)