1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v
new file mode 100644
index 00000000..66dfa0e6
--- /dev/null
+++ b/test-suite/bugs/closed/4443.v
@@ -0,0 +1,31 @@
+Set Universe Polymorphism.
+
+Record TYPE@{i} := cType {
+  type : Type@{i};
+}.
+
+Definition PROD@{i j k}
+  (A : Type@{i})
+  (B : A -> Type@{j})
+  : TYPE@{k}.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+Local Unset Strict Universe Declaration.
+Definition PRODinj
+  (A : Type@{i})
+  (B : A -> Type)
+  : TYPE.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+  Monomorphic Universe i j.
+  Monomorphic Constraint j < i.
+Set Printing Universes.
+Check PROD@{i i i}.
+Check PRODinj@{i j}.
+Fail Check PRODinj@{j i}.
+\ No newline at end of file