Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumulative inductive types

Reviewed-by: SkySkimmer

1 files changed, 18 insertions, 0 deletions

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
+  *)