Add test for coq#16880

SkySkimmer · Sep 7, 2023 · 64b667b · 64b667b
1 parent c4b4e02
commit 64b667b
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/test-suite/bugs/bug_16880.v 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". *)