Merge branch 'janno/cumulative-telescopes' into 'master'

Enable cumulativity for telescopes

Closes iris#461

See merge request iris/stdpp!380

tests/telescopes.v

@@ -2,6 +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 :=
@@ -42,17 +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.
-
-(** 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.

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].