Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

25 files changed, 345 insertions, 76 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 7bb714aa17..7513564cf0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -69,6 +69,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   in
   let mind_entry_template = Array.exists check_template mb.mind_packets in
   let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
+  let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
@@ -76,7 +77,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_template;
-    mind_entry_cumulative= Option.has_some mb.mind_variance;
+    mind_entry_variance;
     mind_entry_private = mb.mind_private;
   }
 
diff --git a/checker/checker.ml b/checker/checker.ml
index e2c90e2b93..08d92bb7b3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -298,7 +298,9 @@ let explain_exn = function
       | DisallowedSProp -> str"DisallowedSProp"
       | BadRelevance -> str"BadRelevance"
       | BadInvert -> str"BadInvert"
-      | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
+      | UndeclaredUniverse _ -> str"UndeclaredUniverse"
+      | BadVariance _ -> str "BadVariance"
+      ))
 
   | InductiveError e ->
       hov 0 (str "Error related to inductive types")
diff --git a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
new file mode 100644
index 0000000000..1473f6df8b
--- /dev/null
+++ b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12653" ] || [ "$CI_BRANCH" = "cumul-syntax" ]; then
+
+    overlay elpi https://github.com/SkySkimmer/coq-elpi cumul-syntax
+
+    overlay equations https://github.com/SkySkimmer/Coq-Equations cumul-syntax
+
+    overlay mtac2 https://github.com/SkySkimmer/Mtac2 cumul-syntax
+
+    overlay paramcoq https://github.com/SkySkimmer/paramcoq cumul-syntax
+
+    overlay rewriter https://github.com/SkySkimmer/rewriter cumul-syntax
+
+    overlay metacoq https://github.com/SkySkimmer/metacoq cumul-syntax
+
+fi
diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
new file mode 100644
index 0000000000..ba97f7c796
--- /dev/null
+++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
@@ -0,0 +1,5 @@
+- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now
+  support syntax `Inductive foo@{=i +j *k l}` to specify variance
+  information for their universes (in :ref:`Cumulative <cumulative>`
+  mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan
+  Gilbert).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1fb337b30a..064107d088 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation:
 .. coqtop:: all
 
    Polymorphic Cumulative Record packType := {pk : Type}.
+   About packType.
 
 :g:`packType` binds a covariant universe, i.e.
 
@@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
+Specifying cumulativity
+~~~~~~~~~~~~~~~~~~~~~~~
+
+The variance of the universe parameters for a cumulative inductive may be specified by the user.
+
+For the following type, universe ``a`` has its variance automatically
+inferred (it is irrelevant), ``b`` is required to be irrelevant,
+``c`` is covariant and ``d`` is invariant. With these annotations
+``c`` and ``d`` have less general variances than would be inferred.
+
+.. coqtop:: all
+
+   Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy.
+   About Dummy.
+
+Insufficiently restrictive variance annotations lead to errors:
+
+.. coqtop:: all
+
+   Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}.
+
 An example of a proof using cumulativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -280,7 +302,7 @@ An example of a proof using cumulativity
    End down.
 
 Cumulativity Weak Constraints
------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. flag:: Cumulativity Weak Constraints
 
@@ -383,6 +405,7 @@ Explicit Universes
    | _
    | @qualid
    univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
    univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 The syntax has been extended to allow users to explicitly bind names
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index d3bd787587..ad7d6f3963 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -8,13 +8,14 @@ Inductive types
 
 .. cmd:: Inductive @inductive_definition {* with @inductive_definition }
 
-   .. insertprodn inductive_definition constructor
+   .. insertprodn inductive_definition cumul_ident_decl
 
    .. prodn::
-      inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
       | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
+      cumul_ident_decl ::= @ident {? @cumul_univ_decl }
 
    This command defines one or more
    inductive types and its constructors.  Coq generates destructors
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index e6fc6188b7..dfd3a18908 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -434,6 +434,10 @@ univ_decl: [
 | "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
+cumul_univ_decl: [
+| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
 univ_constraint: [
 | universe_name [ "<" | "=" | "<=" ] universe_name
 ]
@@ -695,7 +699,7 @@ field_def: [
 ]
 
 inductive_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
 constructors_or_record: [
@@ -707,6 +711,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+cumul_ident_decl: [
+| ident OPT cumul_univ_decl
+]
+
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 235310660b..977cbbccf2 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -15,8 +15,11 @@ open Libnames
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
 type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+type cumul_univ_decl_expr =
+  ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
+type cumul_ident_decl = lident * cumul_univ_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
 type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 02c3c047d5..0eb915561e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2648,13 +2648,34 @@ let interp_univ_decl env decl =
   let binders : lident list = decl.univdecl_instance in
   let evd = Evd.from_env ~binders env in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = binders;
+  let decl = {
+    univdecl_instance = binders;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
   in evd, decl
 
+let interp_cumul_univ_decl env decl =
+  let open UState in
+  let binders = List.map fst decl.univdecl_instance in
+  let variances = Array.map_of_list snd decl.univdecl_instance in
+  let evd = Evd.from_ctx (UState.from_env ~binders env) in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = {
+    univdecl_instance = binders;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+  }
+  in
+  evd, decl, variances
+
 let interp_univ_decl_opt env l =
   match l with
   | None -> Evd.from_env env, UState.default_univ_decl
   | Some decl -> interp_univ_decl env decl
+
+let interp_cumul_univ_decl_opt env = function
+  | None -> Evd.from_env env, UState.default_univ_decl, [| |]
+  | Some decl -> interp_cumul_univ_decl env decl
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9037ed5414..0de6c3e89d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -204,3 +204,8 @@ val interp_univ_decl : Environ.env -> universe_decl_expr ->
 
 val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
                        Evd.evar_map * UState.universe_decl
+
+val interp_cumul_univ_decl_opt : Environ.env -> cumul_univ_decl_expr option ->
+  Evd.evar_map * UState.universe_decl * Entries.variance_entry
+(** BEWARE the variance entry needs to be adjusted by
+   [ComInductive.variance_of_entry] if the instance is extensible. *)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index ae64112e33..1bfc740017 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -20,6 +20,8 @@ type universes_entry =
   | Monomorphic_entry of Univ.ContextSet.t
   | Polymorphic_entry of Name.t array * Univ.UContext.t
 
+type variance_entry = Univ.Variance.t option array
+
 type 'a in_universes_entry = 'a * universes_entry
 
 (** {6 Declaration of inductive types. } *)
@@ -50,9 +52,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
   mind_entry_template : bool; (* Use template polymorphism *)
-  mind_entry_cumulative : bool;
-  (* universe constraints and the constraints for subtyping of
-     inductive types in the block. *)
+  mind_entry_variance : variance_entry option;
+  (* [None] if non-cumulative, otherwise associates each universe of
+     the entry to [None] if to be inferred or [Some v] if to be
+     checked. *)
   mind_entry_private : bool option;
 }
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b2520b780f..33ee8c325a 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -369,15 +369,20 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  let variance = if not mie.mind_entry_cumulative then None
-    else match mie.mind_entry_universes with
+  let variance = match mie.mind_entry_variance with
+    | None -> None
+    | Some variances ->
+      match mie.mind_entry_universes with
       | Monomorphic_entry _ ->
         CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
       | Polymorphic_entry (_,uctx) ->
         let univs = Instance.to_array @@ UContext.instance uctx in
+        let univs = Array.map2 (fun a b -> a,b) univs variances in
         let univs = match sec_univs with
           | None -> univs
-          | Some sec_univs -> Array.append sec_univs univs
+          | Some sec_univs ->
+            let sec_univs = Array.map (fun u -> u, None) sec_univs in
+            Array.append sec_univs univs
         in
         let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
         Some variances
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 8191a5b0f3..d02f92ef26 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -15,30 +15,82 @@ open Univ
 open Variance
 open Util
 
-type inferred = IrrelevantI | CovariantI
-
-(** Throughout this module we modify a map [variances] from local
-    universes to [inferred]. It starts as a trivial mapping to
-    [Irrelevant] and every time we encounter a local universe we
-    restrict it accordingly.
-    [Invariant] universes are removed from the map.
-*)
 exception TrivialVariance
 
-let maybe_trivial variances =
-  if LMap.is_empty variances then raise TrivialVariance
-  else variances
+(** Not the same as Type_errors.BadVariance because we don't have the env where we raise. *)
+exception BadVariance of Level.t * Variance.t * Variance.t
+(* some ocaml bug is triggered if we make this an inline record *)
 
-let infer_level_eq u variances =
-  maybe_trivial (LMap.remove u variances)
+module Inf : sig
+  type variances
+  val infer_level_eq : Level.t -> variances -> variances
+  val infer_level_leq : Level.t -> variances -> variances
+  val start : (Level.t * Variance.t option) array -> variances
+  val finish : variances -> Variance.t array
+end = struct
+  type inferred = IrrelevantI | CovariantI
+  type mode = Check | Infer
 
-let infer_level_leq u variances =
-  (* can only set Irrelevant -> Covariant so nontrivial *)
-  LMap.update u (function
-      | None -> None
-      | Some CovariantI as x -> x
-      | Some IrrelevantI -> Some CovariantI)
-    variances
+  (**
+     Each local universe is either in the [univs] map or is Invariant.
+
+     If [univs] is empty all universes are Invariant and there is nothing more to do,
+     so we stop by raising [TrivialVariance]. The [soft] check comes before that.
+  *)
+  type variances = {
+    orig_array : (Level.t * Variance.t option) array;
+    univs : (mode * inferred) LMap.t;
+  }
+
+  let to_variance = function
+    | IrrelevantI -> Irrelevant
+    | CovariantI -> Covariant
+
+  let to_variance_opt o = Option.cata to_variance Invariant o
+
+  let infer_level_eq u variances =
+    match LMap.find_opt u variances.univs with
+    | None -> variances
+    | Some (Check, expected) ->
+      let expected = to_variance expected in
+      raise (BadVariance (u, expected, Invariant))
+    | Some (Infer, _) ->
+      let univs = LMap.remove u variances.univs in
+      if LMap.is_empty univs then raise TrivialVariance;
+      {variances with univs}
+
+  let infer_level_leq u variances =
+    (* can only set Irrelevant -> Covariant so no TrivialVariance *)
+    let univs =
+      LMap.update u (function
+          | None -> None
+          | Some (_,CovariantI) as x -> x
+          | Some (Infer,IrrelevantI) -> Some (Infer,CovariantI)
+          | Some (Check,IrrelevantI) ->
+            raise (BadVariance (u, Irrelevant, Covariant)))
+        variances.univs
+    in
+    if univs == variances.univs then variances else {variances with univs}
+
+  let start us =
+    let univs = Array.fold_left (fun univs (u,variance) ->
+        match variance with
+        | None -> LMap.add u (Infer,IrrelevantI) univs
+        | Some Invariant -> univs
+        | Some Covariant -> LMap.add u (Check,CovariantI) univs
+        | Some Irrelevant -> LMap.add u (Check,IrrelevantI) univs)
+        LMap.empty us
+    in
+    if LMap.is_empty univs then raise TrivialVariance;
+    {univs; orig_array=us}
+
+  let finish variances =
+    Array.map
+      (fun (u,_check) -> to_variance_opt (Option.map snd (LMap.find_opt u variances.univs)))
+      variances.orig_array
+
+end
+open Inf
 
 let infer_generic_instance_eq variances u =
   Array.fold_left (fun variances u -> infer_level_eq u variances)
@@ -204,11 +256,7 @@ let infer_arity_constructor is_arity env variances arcn =
 open Entries
 
 let infer_inductive_core env univs entries =
-  if Array.is_empty univs then raise TrivialVariance;
-  let variances =
-    Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
-      LMap.empty univs
-  in
+  let variances = Inf.start univs in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -218,12 +266,11 @@ let infer_inductive_core env univs entries =
       variances
       entries
   in
-  Array.map (fun u -> match LMap.find u variances with
-      | exception Not_found -> Invariant
-      | IrrelevantI -> Irrelevant
-      | CovariantI -> Covariant)
-    univs
+  Inf.finish variances
 
 let infer_inductive ~env_params univs entries =
   try infer_inductive_core env_params univs entries
-  with TrivialVariance -> Array.make (Array.length univs) Invariant
+  with
+  | TrivialVariance -> Array.make (Array.length univs) Invariant
+  | BadVariance (lev, expected, actual) ->
+    Type_errors.error_bad_variance env_params ~lev ~expected ~actual
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index db5539a0ff..99d8f0c98d 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -12,8 +12,8 @@ val infer_inductive
   : env_params:Environ.env
   (** Environment containing the polymorphic universes and the
      parameters. *)
-  -> Univ.Level.t array
-  (** Universes whose cumulativity we want to infer. *)
+  -> (Univ.Level.t * Univ.Variance.t option) array
+  (** Universes whose cumulativity we want to infer or check. *)
   -> Entries.one_inductive_entry list
   (** The inductive block data we want to infer cumulativity for.
       NB: we ignore the template bool and the names, only the terms
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index ae5c4b6880..bcb7aa88ca 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
+  | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
 
 type type_error = (constr, types) ptype_error
 
@@ -163,6 +164,9 @@ let error_bad_relevance env =
 let error_bad_invert env =
   raise (TypeError (env, BadInvert))
 
+let error_bad_variance env ~lev ~expected ~actual =
+  raise (TypeError (env, BadVariance {lev;expected;actual}))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -207,3 +211,4 @@ let map_ptype_error f = function
 | DisallowedSProp -> DisallowedSProp
 | BadRelevance -> BadRelevance
 | BadInvert -> BadInvert
+| BadVariance u -> BadVariance u
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b1f7eb8a34..bcdcab9db7 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -70,6 +70,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
+  | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
 
 type type_error = (constr, types) ptype_error
 
@@ -146,5 +147,7 @@ val error_bad_relevance : env -> 'a
 
 val error_bad_invert : env -> 'a
 
+val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
+
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v
new file mode 100644
index 0000000000..f24d13b8af
--- /dev/null
+++ b/test-suite/success/CumulInd.v
@@ -0,0 +1,20 @@
+
+(* variances other than Invariant are forbidden for non-cumul inductives *)
+Fail Inductive foo@{+u} : Prop := .
+Fail Polymorphic Inductive foo@{*u} : Prop := .
+Inductive foo@{=u} : Prop := .
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+Inductive force_invariant@{=u} : Prop := .
+Fail Definition lift@{u v | u < v} (x:force_invariant@{u}) : force_invariant@{v} := x.
+
+Inductive force_covariant@{+u} : Prop := .
+Fail Definition lift@{u v | v < u} (x:force_covariant@{u}) : force_covariant@{v} := x.
+Definition lift@{u v | u < v} (x:force_covariant@{u}) : force_covariant@{v} := x.
+
+Fail Inductive not_irrelevant@{*u} : Prop := nirr (_ : Type@{u}).
+Inductive check_covariant@{+u} : Prop := cov (_ : Type@{u}).
+
+Fail Inductive not_covariant@{+u} : Prop := ncov (_ : Type@{u} -> nat).
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..597e55a39e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +367,26 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let check_trivial_variances variances =
+  Array.iter (function
+      | None | Some Univ.Variance.Invariant -> ()
+      | Some _ ->
+        CErrors.user_err
+          Pp.(strbrk "Universe variance was specified but this inductive will not be cumulative."))
+    variances
+
+let variance_of_entry ~cumulative ~variances uctx =
+  match uctx with
+  | Monomorphic_entry _ -> check_trivial_variances variances; None
+  | Polymorphic_entry (nas,_) ->
+    if not cumulative then begin check_trivial_variances variances; None end
+    else
+      let lvs = Array.length variances in
+      let lus = Array.length nas in
+      assert (lvs <= lus);
+      Some (Array.append variances (Array.make (lus - lvs) None))
+
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
@@ -429,13 +448,13 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
       mind_entry_template = is_template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = variance_of_entry ~cumulative ~variances uctx;
     }
   in
   mind_ent, Evd.universe_binders sigma
 
 let interp_params env udecl uparamsl paramsl =
-  let sigma, udecl = interp_univ_decl_opt env udecl in
+  let sigma, udecl, variances = interp_cumul_univ_decl_opt env udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
     interp_context_evars ~program_mode:false env sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -443,7 +462,7 @@ let interp_params env udecl uparamsl paramsl =
   in
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
-  userimpls, useruimpls, impls, udecl)
+  userimpls, useruimpls, impls, udecl, variances)
 
 (* When a hole remains for a param, pretend the param is uniform and
    do the unification.
@@ -485,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   (* In case of template polymorphism, we need to compute more constraints *)
   let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
-  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl) =
+  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
     interp_params env0 udecl uparamsl paramsl
   in
 
@@ -563,7 +582,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
             userimpls @ impls) cimpls)
       indimpls cimpls
   in
-  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+  let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~variances ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
   (mie, pl, impls)
 
 
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 91e8f609d5..8bce884ba4 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -22,7 +22,7 @@ type uniform_inductive_flag =
 
 val do_mutual_inductive
   :  template:bool option
-  -> universe_decl_expr option
+  -> cumul_univ_decl_expr option
   -> (one_inductive_expr * decl_notation list) list
   -> cumulative:bool
   -> poly:bool
@@ -45,6 +45,7 @@ val interp_mutual_inductive_constr
   : sigma:Evd.evar_map
   -> template:bool option
   -> udecl:UState.universe_decl
+  -> variances:Entries.variance_entry
   -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
   -> indnames:Names.Id.t list
   -> arities:EConstr.t list
@@ -86,3 +87,13 @@ val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:
 (** [nparams] is the number of parameters which aren't treated as
     uniform, ie the length of params (including letins) where the env
     is [uniform params, inductives, params, binders]. *)
+
+val variance_of_entry
+  : cumulative:bool
+  -> variances:Entries.variance_entry
+  -> Entries.universes_entry
+  -> Entries.variance_entry option
+(** Will return None if non-cumulative, and resize if there are more
+    universes than originally specified.
+    If monomorphic, [cumulative] is treated as [false].
+*)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1c80d71ea5..1aff76114b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -194,6 +194,12 @@ let lname_of_lident : lident -> lname =
 let name_of_ident_decl : ident_decl -> name_decl =
   on_fst lname_of_lident
 
+let test_variance_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_variance_ident" begin
+    lk_kws ["=";"+";"*"] >> lk_ident
+  end
+
 }
 
 (* Gallina declarations *)
@@ -283,7 +289,7 @@ GRAMMAR EXTEND Gram
     [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
         r = universe_name -> { (l, ord, r) } ] ]
   ;
-  univ_decl :
+  univ_decl:
     [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
          cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
                 ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
@@ -296,10 +302,40 @@ GRAMMAR EXTEND Gram
            univdecl_extensible_constraints = snd cs } }
     ] ]
   ;
+  variance:
+    [ [ "+" -> { Univ.Variance.Covariant }
+      | "=" -> { Univ.Variance.Invariant }
+      | "*" -> { Univ.Variance.Irrelevant }
+    ] ]
+  ;
+  variance_identref:
+    [ [ id = identref -> { (id, None) }
+      | test_variance_ident; v = variance; id = identref -> { (id, Some v) }
+        (* We need this test to help the parser avoid the conflict
+           between "+" before ident (covariance) and trailing "+" (extra univs allowed) *)
+    ] ]
+  ;
+  cumul_univ_decl:
+    [ [  "@{" ; l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
+         cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
+                ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
+              | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ]
+         ->
+         { let open UState in
+         { univdecl_instance = l;
+           univdecl_extensible_instance = ext;
+           univdecl_constraints = fst cs;
+           univdecl_extensible_constraints = snd cs } }
+    ] ]
+  ;
   ident_decl:
     [ [ i = identref; l = OPT univ_decl -> { (i, l) }
   ] ]
   ;
+  cumul_ident_decl:
+    [ [ i = identref; l = OPT cumul_univ_decl -> { (i, l) }
+  ] ]
+  ;
   finite_token:
     [ [ IDENT "Inductive" -> { Inductive_kw }
       | IDENT "CoInductive" -> { CoInductive }
@@ -345,7 +381,7 @@ GRAMMAR EXTEND Gram
       | -> { RecordDecl (None, []) } ] ]
   ;
   inductive_definition:
-    [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+    [ [ oc = opt_coercion; id = cumul_ident_decl; indpar = binders;
         extrapar = OPT [ "|"; p = binders -> { p } ];
         c = OPT [ ":"; c = lconstr -> { c } ];
         lc=opt_constructors_or_fields; ntn = decl_notations ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..9d86ea90e6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,11 @@ let explain_bad_relevance env =
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."
 
+let explain_bad_variance env sigma ~lev ~expected ~actual =
+  str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma lev ++
+  str": expected " ++ Univ.Variance.pr expected ++
+  str " but cannot be less restrictive than " ++ Univ.Variance.pr actual ++ str "."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -788,6 +793,7 @@ let explain_type_error env sigma err =
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
   | BadInvert -> explain_bad_invert env
+  | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0e660bf20c..442269ebda 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -68,10 +68,18 @@ let pr_univ_name_list = function
   | Some l ->
     str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
 
+let pr_variance_lident (lid,v) =
+  let v = Option.cata Univ.Variance.pr (mt()) v in
+  v ++ pr_lident lid
+
 let pr_univdecl_instance l extensible =
   prlist_with_sep spc pr_lident l ++
   (if extensible then str"+" else mt ())
 
+let pr_cumul_univdecl_instance l extensible =
+  prlist_with_sep spc pr_variance_lident l ++
+  (if extensible then str"+" else mt ())
+
 let pr_univdecl_constraints l extensible =
   if List.is_empty l && extensible then mt ()
   else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
@@ -85,9 +93,20 @@ let pr_universe_decl l =
     str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
     pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
 
+let pr_cumul_univ_decl l =
+  let open UState in
+  match l with
+  | None -> mt ()
+  | Some l ->
+    str"@{" ++ pr_cumul_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
+    pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
+
 let pr_ident_decl (lid, l) =
   pr_lident lid ++ pr_universe_decl l
 
+let pr_cumul_ident_decl (lid, l) =
+  pr_lident lid ++ pr_cumul_univ_decl l
+
 let string_of_fqid fqid =
   String.concat "." (List.map Id.to_string fqid)
 
@@ -848,7 +867,7 @@ let pr_vernac_expr v =
     let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
       hov 0 (
         str key ++ spc() ++
-        (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
+        (if coe then str"> " else str"") ++ pr_cumul_ident_decl iddecl ++
         pr_and_type_binders_arg indupar ++
         pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
         pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 891d7fcebe..583164a524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -190,11 +190,12 @@ type tc_result =
   (* Part relative to closing the definitions *)
   * UnivNames.universe_binders
   * Entries.universes_entry
+  * Entries.variance_entry
   * Constr.rel_context
   * DataR.t list
 
 (* ps = parameter list *)
-let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result =
+let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_result =
   let env0 = Global.env () in
   (* Special case elaboration for template-polymorphic inductives,
      lower bound on introduced universes is Prop so that we do not miss
@@ -202,7 +203,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
   let is_template =
     List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
   let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
-  let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in
+  let sigma, decl, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl in
   let () = List.iter check_parameters_must_be_named ps in
   let sigma, (impls_env, ((env1,newps), imps)) =
     Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
@@ -256,7 +257,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_res
   let ubinders = Evd.universe_binders sigma in
   let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
   let () = List.iter (iter_constr ce) (List.rev newps) in
-  template, imps, ubinders, univs, newps, ans
+  template, imps, ubinders, univs, variances, newps, ans
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -525,7 +526,7 @@ let declare_structure_entry o =
   - prepares and declares the corresponding record projections, mainly taken care of by
     [declare_projections]
 *)
-let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
+let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
   let nparams = List.length params in
   let poly, ctx =
     match univs with
@@ -568,7 +569,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat
       mind_entry_private = None;
       mind_entry_universes = univs;
       mind_entry_template = template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = ComInductive.variance_of_entry ~cumulative ~variances univs;
     }
   in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
@@ -633,7 +634,8 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind
   } in
   [cref, [m]]
 
-let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name =
+let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+    fields params paramimpls coers id idbuild binder_name =
   let record_data =
     { Data.id
     ; idbuild
@@ -641,7 +643,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
     ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
     ; rdata
     } in
-  let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls
+  let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs ~variances paramimpls
       params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
   in
   let map ind =
@@ -677,7 +679,7 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para
   2. declare the class, using the information from 1. in the form of [Classes.typeclass]
 
   *)
-let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
+let declare_class def ~cumulative ~ubind ~univs ~variances id idbuild paramimpls params
     rdata template ?(kind=Decls.StructureComponent) coers =
   let implfs =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -694,7 +696,8 @@ let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
       let binder = {binder with binder_name=Name binder_name} in
       build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
     | _ ->
-      build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name
+      build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
+        fields params paramimpls coers id idbuild binder_name
   in
   let univs, params, fields =
     match univs with
@@ -852,7 +855,8 @@ let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def reco
   declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild
     impargs params rdata template coers
 
-let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data =
+let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+    records data =
   let adjust_impls impls = impargs @ [CAst.make None] @ impls in
   let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
   (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
@@ -866,30 +870,36 @@ let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~fini
     { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers }
   in
   let data = List.map2 map data records in
-  let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in
+  let inds = declare_structure ~cumulative finite ~ubind ~univs ~variances
+      impargs params template data
+  in
   List.map (fun ind -> GlobRef.IndRef ind) inds
 
 (** [fs] corresponds to fields and [ps] to parameters; [coers] is a
     list telling if the corresponding fields must me declared as coercions
     or subinstances. *)
-let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) =
+let definition_structure udecl kind ~template ~cumulative ~poly
+    finite (records : Ast.t list) : GlobRef.t list =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
-  let auto_template, impargs, ubind, univs, params, data =
+  let auto_template, impargs, ubind, univs, variances, params, data =
     (* In theory we should be able to use
        [Notation.with_notation_protection], due to the call to
        Metasyntax.set_notation_for_interpretation, however something
        is messing state beyond that.
     *)
     Vernacstate.System.protect (fun () ->
-      typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
+        typecheck_params_and_fields (kind = Class true) poly udecl ps data) ()
+  in
   let template = template, auto_template in
   match kind with
   | Class def ->
-    class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data
+    class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs ~variances
+      def records data
   | Inductive_kw | CoInductive | Variant | Record | Structure ->
-    regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data
+    regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
+      records data
 
 module Internal = struct
   type nonrec projection_flags = projection_flags = {
diff --git a/vernac/record.mli b/vernac/record.mli
index ffcae2975e..7a40af048c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,7 +24,7 @@ module Ast : sig
 end
 
 val definition_structure
-  :  universe_decl_expr option
+  :  cumul_univ_decl_expr option
   -> inductive_kind
   -> template:bool option
   -> cumulative:bool
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a9a74144f..defb0691c0 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -189,8 +189,9 @@ type inductive_params_expr = local_binder_expr list * local_binder_expr list opt
 (** If the option is nonempty the "|" marker was used *)
 
 type inductive_expr =
-  ident_decl with_coercion * inductive_params_expr * constr_expr option *
-    constructor_list_or_record_decl_expr
+  cumul_ident_decl with_coercion
+  * inductive_params_expr * constr_expr option
+  * constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
   lident * inductive_params_expr * constr_expr option * constructor_expr list