From 6d64bcb55e53563f6ec4ea84aa0ba5a8a1c55aa0 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Mon, 16 May 2022 14:14:30 +0200
Subject: [PATCH 1/3] Enable cumulativity for telescopes.

---
 tests/telescopes.v    | 9 +++++++++
 theories/telescopes.v | 1 +
 2 files changed, 10 insertions(+)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index d231e291..416d29c8 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -79,3 +79,12 @@ Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False
 assert_succeeds exact [tele_arg true; 0].
 assert_succeeds refine [tele_arg true; 0].
 Abort.
+
+(* Assert that telescopes are cumulatively universe polymorphic.
+   See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
+ *)
+Section Cumulativity.
+  Monomorphic Universes Quant local.
+  Monomorphic Constraint local < Quant.
+  Example cumul (t : tele@{local}) : tele@{Quant} := t.
+End Cumulativity.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 2378216e..33f44ad9 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -2,6 +2,7 @@ From stdpp Require Import base tactics.
 From stdpp Require Import options.
 
 Local Set Universe Polymorphism.
+Local Set Polymorphic Inductive Cumulativity.
 
 (** Without this flag, Coq minimizes some universes to [Set] when they
     should not be, e.g. in [texist_exist].
-- 
GitLab


From 8eb17fc82e690cd44e1a1f5b29f086b4cbd8504a Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Mon, 16 May 2022 14:18:41 +0200
Subject: [PATCH 2/3] Move `Universe Minimization ToSet` test case higher.

The accessor test case also fails when the flag is enabled so that
the dedicated test case for it never has a chance to run.
---
 tests/telescopes.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index 416d29c8..30027fb5 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,11 @@ From stdpp Require Import tactics telescopes.
 
 Local Unset Mangle Names. (* for stable goal printing *)
 
+(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
+Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
+  texist P ↔ ex P.
+Proof. by rewrite texist_exist. Qed.
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
@@ -48,11 +53,6 @@ is essentially just a (dependent) product.
  *)
 Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
 
-(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
-Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
-  texist P ↔ ex P.
-Proof. by rewrite texist_exist. Qed.
-
 (** [tele_arg ..] notation tests.
     These tests mainly test type annotations and casts in the [tele_arg]
     notations.
-- 
GitLab


From b0065fea071bf41ebac861c1c69061cd31540724 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Mon, 16 May 2022 16:46:55 +0200
Subject: [PATCH 3/3] Move universe-related telescope tests closer together.

---
 tests/telescopes.v | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index 30027fb5..7388dfb3 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,11 +2,28 @@ From stdpp Require Import tactics telescopes.
 
 Local Unset Mangle Names. (* for stable goal printing *)
 
+Section universes.
 (** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
 Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
   texist P ↔ ex P.
 Proof. by rewrite texist_exist. Qed.
 
+(** [tele_arg t] should live at the same universe
+as the types inside of [t] because [tele_arg t]
+is essentially just a (dependent) product.
+ *)
+Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
+
+(* Assert that telescopes are cumulatively universe polymorphic.
+   See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
+ *)
+Section cumulativity.
+Monomorphic Universes Quant local.
+Monomorphic Constraint local < Quant.
+Example cumul (t : tele@{local}) : tele@{Quant} := t.
+End cumulativity.
+End universes.
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
@@ -47,12 +64,6 @@ Notation "'[TEST'  x .. z ,  P ']'" :=
   (x binder, z binder).
 Check [TEST (x y : nat), x = y].
 
-(** [tele_arg t] should live at the same universe
-as the types inside of [t] because [tele_arg t]
-is essentially just a (dependent) product.
- *)
-Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
-
 (** [tele_arg ..] notation tests.
     These tests mainly test type annotations and casts in the [tele_arg]
     notations.
@@ -79,12 +90,3 @@ Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False
 assert_succeeds exact [tele_arg true; 0].
 assert_succeeds refine [tele_arg true; 0].
 Abort.
-
-(* Assert that telescopes are cumulatively universe polymorphic.
-   See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
- *)
-Section Cumulativity.
-  Monomorphic Universes Quant local.
-  Monomorphic Constraint local < Quant.
-  Example cumul (t : tele@{local}) : tele@{Quant} := t.
-End Cumulativity.
-- 
GitLab