test-suite file for spurious universe generation

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_11722.v b/test-suite/bugs/closed/bug_11722.v
new file mode 100644
index 0000000000..d4bd5f48b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11722.v
@@ -0,0 +1,20 @@
+Require Import Program.
+Set Universe Polymorphism.
+
+Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} :=
+  idpath : paths A a a.
+
+Inductive nat :=
+  | O : nat
+  | S : nat -> nat.
+
+Axiom cheat : forall {A}, A.
+
+Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _.
+Next Obligation.
+  destruct x.
+  constructor.
+  apply cheat.
+Defined. (* FIXED: Universe unbound error *)
+
+Check foo@{_}.