Simplification: cumulativity information is variance information.

Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.

As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).

Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie

         Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
         Print Foo.

gives

        Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
          { foo : Type@{i} -> Type@{j} }
          (* =i +j *k |=  *)

19 files changed, 260 insertions, 168 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 4de597766..1807ae0ec 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -564,14 +564,23 @@ let check_subtyping cumi paramsctxt env inds =
       We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
       and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
       with the cumulativity constraints [ cumul_cst ]. *)
-  let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
-  let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+  let uctx = ACumulativityInfo.univ_context cumi in
+  let len = AUContext.size uctx in
+  let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
+
   let other_context = ACumulativityInfo.univ_context cumi in
   let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
-  let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
-  let cumul_cst = UContext.constraints cumul_context in
+  let cumul_cst =
+    Array.fold_left_i (fun i csts var ->
+        match var with
+        | Variance.Irrelevant -> csts
+        | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts
+        | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts)
+      Constraint.empty (ACumulativityInfo.variance cumi)
+  in
   let env = Environ.push_context uctx_other env in
   let env = Environ.add_constraints cumul_cst env in
+
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 29bb8901e..2297c90b3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,24 +158,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
 let convert_inductive_instances cv_pb cumi u u' univs =
   let len_instance =
       Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
-  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((len_instance = Univ.Instance.length u) &&
           (len_instance = Univ.Instance.length u')) then
     anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_subtypctx
-    in
+    let variance = Univ.ACumulativityInfo.variance cumi in
     let comp_cst =
       match cv_pb with
-        CONV ->
-        let comp_cst' =
-          let comp_subst = (Univ.Instance.append u' u) in
-          Univ.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
+      | CONV ->
+        Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
+      | CUMUL ->
+        Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
     in
     if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d01657df..46b3ce680 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1003,12 +1003,42 @@ end
 
 type abstract_universe_context = AUContext.t
 
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> Constraint.add (u, Le, u') csts
+    | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
 module CumulativityInfo =
 struct
-  type t = universe_context * universe_context
+  type t = universe_context * Variance.t array
 
   let univ_context (univcst, subtypcst) = univcst
-  let subtyp_context (univcst, subtypcst) = subtypcst
+  let variance (univs, variance) = variance
 
 end
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 21c94d952..8c0685e0b 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -218,12 +218,25 @@ end
 
 type abstract_universe_context = AUContext.t
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val leq_constraints : t array -> Instance.t constraint_function
+  val eq_constraints : t array -> Instance.t constraint_function
+end
+
+
 module ACumulativityInfo :
 sig
   type t
 
   val univ_context : t -> abstract_universe_context
-  val subtyp_context : t -> abstract_universe_context
+  val variance : t -> Variance.t array
 
 end
 
diff --git a/checker/values.ml b/checker/values.ml
index 313067cb6..55e1cdb6f 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -110,10 +110,12 @@ let v_cstrs =
        (v_tuple "univ_constraint"
           [|v_level;v_enum "order_request" 3;v_level|]))
 
+let v_variance = v_enum "variance" 3
+
 let v_instance = Annot ("instance", Array v_level)
 let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
 let v_abs_context = v_context (* only for clarity *)
-let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|]
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
diff --git a/engine/universes.ml b/engine/universes.ml
index eaddf98a8..3a00f0fd1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1103,14 +1103,3 @@ let solve_constraints_system levels level_bounds level_min =
     done;
   done;
   v
-
-
-(** Operations for universe_info_ind *)
-
-(** Given a universe context representing constraints of an inductive
-    this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-let univ_inf_ind_from_universe_context univcst =
-  let freshunivs = Instance.of_array
-      (Array.map (fun _ -> new_univ_level ())
-         (Instance.to_array (UContext.instance univcst)))
-  in CumulativityInfo.from_universe_context univcst freshunivs
diff --git a/engine/universes.mli b/engine/universes.mli
index 130dcf8bb..cb6e2ba1b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -221,9 +221,3 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
 
 val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
   Universe.t array
-
-(** Operations for universe_info_ind *)
-
-(** Given a universe context representing constraints of an inductive
-    this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-val univ_inf_ind_from_universe_context : UContext.t -> CumulativityInfo.t
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 75bfca307..710f88c3f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -92,7 +92,7 @@ let process_inductive info modlist mib =
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
+      subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c2e4d5908..f2677acd6 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
-    let sbsubst = CumulativityInfo.subtyping_subst cumi in
-    let dosubst = subst_univs_level_constr sbsubst in
     let uctx = CumulativityInfo.univ_context cumi in
-    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+    let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
+        LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
+    in
+    let dosubst = subst_univs_level_constr lmap in
+    let instance_other = Instance.of_array new_levels in
+    let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
     let env = Environ.push_context uctx env_ar in
     let env = Environ.push_context uctx_other env in
-    let env = push_context (CumulativityInfo.subtyp_context cumi) env in
+    let subtyp_constraints =
+      Variance.leq_constraints (CumulativityInfo.variance cumi)
+        (UContext.instance uctx) instance_other
+        Constraint.empty
+    in
+    let env = Environ.add_constraints subtyp_constraints env in
     (* process individual inductive types: *)
     Array.iter (fun (id,cn,lc,(sign,arity)) ->
       match arity with
         | RegularArity (_, full_arity, _) ->
            check_subtyping_arity_constructor env dosubst full_arity numparams true;
            Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
-        | TemplateArity _ -> ()
+        | TemplateArity _ ->
+          anomaly ~label:"check_subtyping"
+            Pp.(str "template polymorphism and cumulative polymorphism are not compatible")
     ) inds
 
 (* Type-check an inductive definition. Does not check positivity
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index dc46ac01b..083692e91 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -219,26 +219,13 @@ let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
 
 let get_cumulativity_constraints cv_pb cumi u u' =
-  let length_ind_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (length_ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_subtypctx
-    in
-    match cv_pb with
-    | CONV ->
-      let comp_cst' =
-        let comp_subst = (Univ.Instance.append u' u) in
-        Univ.AUContext.instantiate comp_subst ind_subtypctx
-      in
-      Univ.Constraint.union comp_cst comp_cst'
-    | CUMUL -> comp_cst
+  match cv_pb with
+  | CONV ->
+    Univ.Variance.eq_constraints (Univ.ACumulativityInfo.variance cumi)
+      u u' Univ.Constraint.empty
+  | CUMUL ->
+    Univ.Variance.leq_constraints (Univ.ACumulativityInfo.variance cumi)
+      u u' Univ.Constraint.empty
 
 let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 059f259ae..d064b3687 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -47,6 +47,9 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
+val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+  Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
+
 val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 50692ca59..7ae099246 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -911,66 +911,86 @@ end
 type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
 
-(** Universe info for cumulative inductive types:
-    A context of universe levels
-    with universe constraints, representing local universe variables
-    and constraints, together with a context of universe levels with
-    universe constraints, representing conditions for subtyping used
-    for inductive types.
-
-    This data structure maintains the invariant that the context for
-    subtyping constraints is exactly twice as big as the context for
-    universe constraints. *)
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let sup x y =
+    match x, y with
+    | Irrelevant, s | s, Irrelevant -> s
+    | Invariant, _ | _, Invariant -> Invariant
+    | Covariant, Covariant -> Covariant
+
+  let pr = function
+    | Irrelevant -> str "*"
+    | Covariant -> str "+"
+    | Invariant -> str "="
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> enforce_leq_level u u' csts
+    | Invariant -> enforce_eq_level u u' csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> enforce_eq_level u u' csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+(** Universe info for cumulative inductive types: A context of
+   universe levels with universe constraints, representing local
+   universe variables and constraints, together with an array of
+   Variance.t.
+
+    This data structure maintains the invariant that the variance
+   array has the same length as the universe instance. *)
 module CumulativityInfo =
 struct
-  type t = universe_context * universe_context
+  type t = universe_context * Variance.t array
 
   let make x =
-    if (Instance.length (UContext.instance (snd x))) =
-       (Instance.length (UContext.instance (fst x))) * 2 then x
+    if (Instance.length (UContext.instance (fst x))) =
+       (Array.length (snd x)) then x
     else anomaly (Pp.str "Invalid subtyping information encountered!")
 
-  let empty = (UContext.empty, UContext.empty)
-  let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst
+  let empty = (UContext.empty, [||])
+  let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
 
-  let halve_context ctx =
-    let len = Array.length (Instance.to_array ctx) in
-    let halflen = len / 2 in
-    (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
-     Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
-
-  let pr prl (univcst, subtypcst) =
-    if UContext.is_empty univcst then mt() else
-      let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
-      (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
-        h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
-         ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
-
-  let hcons (univcst, subtypcst) =
-    (UContext.hcons univcst, UContext.hcons subtypcst)
+  let pr prl (univs, variance) =
+    if UContext.is_empty univs then mt() else
+      let ppu i u =
+        let v = variance.(i) in
+        Variance.pr v ++ prl u
+      in
+      h 0 (prvecti_with_sep spc ppu (UContext.instance univs) ++ str " |= ") ++
+      h 0 (v 0 (Constraint.pr prl (UContext.constraints univs)))
 
-  let univ_context (univcst, subtypcst) = univcst
-  let subtyp_context (univcst, subtypcst) = subtypcst
+  let hcons (univs, variance) = (* should variance be hconsed? *)
+    (UContext.hcons univs, variance)
 
-  let create_trivial_subtyping ctx ctx' =
-    CArray.fold_left_i
-      (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
-      Constraint.empty (Instance.to_array ctx)
+  let univ_context (univs, subtypcst) = univs
+  let variance (univs, variance) = variance
 
   (** This function takes a universe context representing constraints
-      of an inductive and a Instance.t of fresh universe names for the
-      subtyping (with the same length as the context in the given
-      universe context) and produces a UInfoInd.t that with the
-      trivial subtyping relation. *)
-  let from_universe_context univcst freshunivs =
-    let inst = (UContext.instance univcst) in
-    assert (Instance.length freshunivs = Instance.length inst);
-    (univcst, UContext.make (Instance.append inst freshunivs,
-                             create_trivial_subtyping inst freshunivs))
-
-  let subtyping_subst (univcst, subtypcst) =
-      let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in
-      Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
+     of an inductive and produces a CumulativityInfo.t with the
+     trivial subtyping relation. *)
+  let from_universe_context univs =
+    (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
 
 end
 
@@ -1138,10 +1158,9 @@ let abstract_universes ctx =
   let ctx = UContext.make (instance, cstrs) in
   instance, ctx
 
-let abstract_cumulativity_info (univcst, substcst) = 
-  let instance, univcst = abstract_universes univcst in
-  let _, substcst = abstract_universes substcst in
-  (instance, (univcst, substcst))
+let abstract_cumulativity_info (univs, variance) =
+  let subst, univs = abstract_universes univs in
+  subst, (univs, variance)
 
 (** Pretty-printing *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 975d9045e..e8f5ba568 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -347,35 +347,45 @@ end
 type abstract_universe_context = AUContext.t
 [@@ocaml.deprecated "Use AUContext.t"]
 
-(** Universe info for inductive types: A context of universe levels
-    with universe Constraint.t, representing local universe variables
-    and Constraint.t, together with a context of universe levels with
-    universe Constraint.t, representing conditions for subtyping used
-    for inductive types.
-
-    This data structure maintains the invariant that the context for
-    subtyping Constraint.t is exactly twice as big as the context for
-    universe Constraint.t. *)
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val sup : t -> t -> t
+
+  val pr : t -> Pp.t
+
+  val leq_constraints : t array -> Instance.t constraint_function
+  val eq_constraints : t array -> Instance.t constraint_function
+end
+
+(** Universe info for cumulative inductive types: A context of
+   universe levels with universe constraints, representing local
+   universe variables and constraints, together with an array of
+   Variance.t.
+
+    This data structure maintains the invariant that the variance
+   array has the same length as the universe instance. *)
 module CumulativityInfo :
 sig
   type t
 
-  val make : UContext.t * UContext.t -> t
+  val make : UContext.t * Variance.t array -> t
 
   val empty : t
   val is_empty : t -> bool
 
   val univ_context : t -> UContext.t
-  val subtyp_context : t -> UContext.t
-
-  (** This function takes a universe context representing Constraint.t
-      of an inductive and a Instance.t of fresh universe names for the
-      subtyping (with the same length as the context in the given
-      universe context) and produces a UInfoInd.t that with the
-      trivial subtyping relation. *)
-  val from_universe_context : UContext.t -> Instance.t -> t
+  val variance : t -> Variance.t array
 
-  val subtyping_subst : t -> universe_level_subst
+  (** This function takes a universe context representing constraints
+     of an inductive and produces a CumulativityInfo.t with the
+     trivial subtyping relation. *)
+  val from_universe_context : UContext.t -> t
 
 end
 
@@ -387,7 +397,7 @@ sig
   type t
 
   val univ_context : t -> AUContext.t
-  val subtyp_context : t -> AUContext.t
+  val variance : t -> Variance.t array
 end
 
 type abstract_cumulativity_info = ACumulativityInfo.t
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 41c4616f7..dc3acbc3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  let length_ind_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (length_ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    begin
-     let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst =  Univ.AUContext.instantiate comp_subst ind_sbcst in
-     Evd.add_constraints evd comp_cst
-    end
+  Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f73f84118..df0b53e9c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -694,6 +694,43 @@ let infer_inductive_subtyping_arity_constructor
   let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
   if not is_arity then basic_check last_contexts codom else last_contexts
 
+type ukind =
+  Global | Orig of int | New of int
+
+let make_variance uctx lmap csts =
+  let variance = Array.init (UContext.size uctx) (fun _ -> Variance.Irrelevant) in
+  let geti = Array.fold_left_i (fun i geti u -> LMap.add u i geti)
+      LMap.empty (Instance.to_array @@ UContext.instance uctx)
+  in
+  let lmap_rev = LMap.fold (fun u v lmap_rev -> LMap.add v u lmap_rev) lmap LMap.empty in
+  let analyse_univ u =
+    match LMap.find u lmap_rev with
+    | exception Not_found ->
+      begin match LMap.find u lmap with
+        | exception Not_found -> Global
+        | _ -> Orig (LMap.find u geti)
+      end
+    | uorig -> New (LMap.find uorig geti)
+  in
+  Constraint.iter (fun (l,d,r) ->
+      match analyse_univ l, analyse_univ r with
+      | Orig i, New j when Int.equal i j ->
+        begin match d with
+          | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig < new constraint")
+          | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant
+          | Le -> variance.(i) <- Variance.sup variance.(i) Variance.Covariant
+        end
+      | New i, Orig j when Int.equal i j ->
+        begin match d with
+          | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig > new constraint")
+          | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant
+          | Le -> anomaly ~label:"make_variance" Pp.(str "unexpected orig >= new constraint")
+        end
+      | (Global | Orig _ | New _), _ ->
+        anomaly ~label:"make_variance" Pp.(str "unexpected constraint between non copy universes")
+    ) csts;
+  variance
+
 let infer_inductive_subtyping env evd mind_ent =
   let { Entries.mind_entry_params = params;
         Entries.mind_entry_inds = entries;
@@ -706,22 +743,23 @@ let infer_inductive_subtyping env evd mind_ent =
     | Entries.Polymorphic_ind_entry _ -> ground_univs
     | Entries.Cumulative_ind_entry cumi -> 
       begin
-        let uctx = Univ.CumulativityInfo.univ_context cumi in
-        let sbsubst = Univ.CumulativityInfo.subtyping_subst cumi in
-        let dosubst = subst_univs_level_constr sbsubst in
-        let instance_other = 
-          Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) 
+        let uctx = CumulativityInfo.univ_context cumi in
+        let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+        let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
+            LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
         in
+        let dosubst = subst_univs_level_constr lmap in
+        let instance_other = Instance.of_array new_levels in
         let constraints_other = 
           Univ.subst_univs_level_constraints
-            sbsubst (Univ.UContext.constraints uctx) 
+            lmap (Univ.UContext.constraints uctx)
         in
         let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
         let env = Environ.push_context uctx env in
         let env = Environ.push_context uctx_other env in
         let evd = 
-          Evd.merge_universe_context
-            evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) 
+          Evd.merge_context_set UState.UnivRigid
+            evd (Univ.ContextSet.of_context uctx_other)
         in
         let (_, _, subtyp_constraints) =
           List.fold_left
@@ -737,12 +775,10 @@ let infer_inductive_subtyping env evd mind_ent =
                  )
                  ctxs' indentry.Entries.mind_entry_lc
             ) (env, evd, Univ.Constraint.empty) entries
-        in 
+        in
+        let variance = make_variance uctx lmap subtyp_constraints in
         Entries.Cumulative_ind_entry
           (Univ.CumulativityInfo.make 
-             (Univ.CumulativityInfo.univ_context cumi,
-              Univ.UContext.make
-                (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
-                 subtyp_constraints)))
+             (uctx, variance))
       end
   in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a79..35487e09c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -113,13 +113,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
 let instantiate_cumulativity_info cumi =
   let open Univ in
   let univs = ACumulativityInfo.univ_context cumi in
-  let subtyp = ACumulativityInfo.subtyp_context cumi in
   let expose ctx =
     let inst = AUContext.instance ctx in
     let cst = AUContext.instantiate inst ctx in
     UContext.make (inst, cst)
   in
-  CumulativityInfo.make (expose univs, expose subtyp)
+  CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
 
 let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 0ee85712e..303cd7146 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -98,3 +98,13 @@ Section down.
     intros H f g Hfg. exact (H f g Hfg).
   Defined.
 End down.
+
+Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }.
+
+Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
+  : Arrow@{i j} -> Arrow@{i' j'}
+  := fun x => x.
+
+Definition arrow_lift@{i i' j j' | i' = i, j < j'}
+  : Arrow@{i j} -> Arrow@{i' j'}
+  := fun x => x.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 1c8677e9c..3f8d413b7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -340,7 +340,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
     match uctx with
     | Polymorphic_const_entry uctx ->
       if cum then
-        Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+        Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
       else Polymorphic_ind_entry uctx
     | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
diff --git a/vernac/record.ml b/vernac/record.ml
index 1e464eb8b..31c0483b4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -501,7 +501,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
          match univs with
          | Polymorphic_const_entry univs ->
            if cum then
-             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+             Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
            else
              Polymorphic_ind_entry univs
          | Monomorphic_const_entry univs ->
@@ -632,7 +632,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
         match univs with
         | Polymorphic_const_entry univs ->
           if cum then
-            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+            Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
           else
             Polymorphic_ind_entry univs
         | Monomorphic_const_entry univs ->