From a5d124dd7c3d43a5ead81cfac30c7d1448002d56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Nov 2019 15:53:48 +0100
Subject: Fix #11039: proof of False with template poly and nonlinear universes

Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.
---
 test-suite/bugs/closed/bug_10504.v | 14 ++++++++++++++
 test-suite/bugs/closed/bug_11039.v | 26 ++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10504.v
 create mode 100644 test-suite/bugs/closed/bug_11039.v

(limited to 'test-suite')

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 *)
-- 
cgit v1.2.3