Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear universes

Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot

2 files changed, 40 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v
new file mode 100644
index 0000000000..6e66a6a90a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10504.v
@@ -0,0 +1,14 @@
+Inductive any_list {A} :=
+| nil : @any_list A
+| cons : forall X, A -> @any_list X -> @any_list A.
+
+Arguments nil {A}.
+Arguments cons {A X}.
+
+Notation "[]" := (@nil Type).
+Notation "hd :: tl" := (cons hd tl).
+
+Definition xs := true :: 2137 :: false :: 0 :: [].
+Fail Definition ys := xs :: xs.
+
+(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *)
diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v
new file mode 100644
index 0000000000..f02a3ef177
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11039.v
@@ -0,0 +1,26 @@
+(* this bug was a proof of False *)
+
+(* when we require template poly Coq recognizes that it's not allowed *)
+Fail #[universes(template)]
+  Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A.
+
+(* variants with letin *)
+Fail #[universes(template)]
+ Inductive foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A.
+
+Fail #[universes(template)]
+ Record foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }.
+
+
+(* no implicit template poly, no explicit universe annotations *)
+Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty.
+Arguments nonempty {_}.
+
+Fail Check foo nat : Type@{foo.u0}.
+(* template poly didn't activate *)
+
+Definition U := Type.
+Definition A : U := foo nat.
+
+Fail Definition down : U -> A := fun u => bar nat u nonempty.
+(* this is the one where it's important that it fails *)