From d1fe597eee63caccd50d4a6da529856f295872be Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2020 15:21:29 +0100
Subject: [kernel] Fix #13495: incompleteness in cases typing for cumulative
 inductive types

---
 test-suite/bugs/closed/bug_13495.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13495.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13495.v b/test-suite/bugs/closed/bug_13495.v
new file mode 100644
index 0000000000..489574b854
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13495.v
@@ -0,0 +1,18 @@
+Universe u.
+(* Constraint Set < u. *)
+Polymorphic Cumulative Record pack@{u} := Pack { pack_type : Type@{u} }.
+(* u is covariant *)
+
+Polymorphic Definition pack_id@{u} (p : pack@{u}) : pack@{u} :=
+  match p with
+  | Pack T => Pack T
+  end.
+Definition packid_nat (p : pack@{Set}) := pack_id@{u} p.
+(* No constraints: Set <= u *)
+
+Definition sr_dont_break := Eval compute in packid_nat.
+(* Incorrect elimination of "p" in the inductive type "pack":
+  ill-formed elimination predicate.
+
+  This is because it tries to enforce Set = u
+  *)
-- 
cgit v1.2.3