Merge PR #6128: Simplification: cumulativity information is variance information.

5 files changed, 220 insertions, 241 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b117f8714..cfca335d3 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_susbst 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 =
+      CumulativityInfo.leq_constraints 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 6e42764a4..159d2ea66 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -200,13 +200,9 @@ let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
-      Univ.Instance.t -> int -> 'a -> 'a;
-    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
-      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
-  } 
+    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -215,18 +211,68 @@ 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
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
-  (check.compare env pb s0 s1 u, check)
+  (check.compare_sorts env pb s0 s1 u, check)
 
 (* [flex] should be true for constants, false for inductive types and
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
-  
-let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
-  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
 
-let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
-  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
+let get_cumulativity_constraints cv_pb cumi u u' =
+  match cv_pb with
+  | CONV ->
+    Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
+  | CUMUL ->
+    Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
+
+let inductive_cumulativity_arguments (mind,ind) =
+  mind.Declarations.mind_nparams +
+  mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+
+let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    s
+  | Declarations.Polymorphic_ind _ ->
+    cmp_instances u1 u2 s
+  | Declarations.Cumulative_ind cumi ->
+    let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
+    if not (Int.equal num_param_arity nargs) then
+      cmp_instances u1 u2 s
+    else
+      let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
+      cmp_cumul csts s
+
+let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
+  convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    cv_pb ind nargs u1 u2 s, check
+
+let constructor_cumulativity_arguments (mind, ind, ctor) =
+  let nparamsctxt =
+    mind.Declarations.mind_nparams +
+    mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+  nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
+
+let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    s
+  | Declarations.Polymorphic_ind _ ->
+    cmp_instances u1 u2 s
+  | Declarations.Cumulative_ind cumi ->
+    let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
+    if not (Int.equal num_cnstr_args nargs) then
+      cmp_instances u1 u2 s
+    else
+      let csts = get_cumulativity_constraints CONV cumi u1 u2 in
+      cmp_cumul csts s
+
+let convert_constructors ctor nargs u1 u2 (s, check) =
+  convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    ctor nargs u1 u2 s, check
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -518,15 +564,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              convert_instances ~flex:false u1 u2 cuniv
-            | Declarations.Cumulative_ind cumi ->
-              convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
-                u2 (CClosure.stack_args_size v2) cuniv
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
@@ -536,16 +579,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              convert_instances ~flex:false u1 u2 cuniv
-            | Declarations.Cumulative_ind _ ->
-              convert_constructors
-                (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
-                u2 (CClosure.stack_args_size v2) cuniv
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -666,84 +705,14 @@ let check_convert_instances ~flex u u' univs =
   else raise NotConvertible
 
 (* general conversion and inference functions *)
-let infer_check_conv_inductives
-    infer_check_convert_instances
-    infer_check_inductive_instances
-    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-    infer_check_convert_instances ~flex:false u1 u2 univs
-  | Declarations.Cumulative_ind cumi ->
-    let num_param_arity =
-      mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-    in
-    if not (num_param_arity = sv1 && num_param_arity = sv2) then
-      infer_check_convert_instances ~flex:false u1 u2 univs
-    else
-      infer_check_inductive_instances cv_pb cumi u1 u2 univs
-
-let infer_check_conv_constructors
-    infer_check_convert_instances
-    infer_check_inductive_instances
-    (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-    infer_check_convert_instances ~flex:false u1 u2 univs
-  | Declarations.Cumulative_ind cumi ->
-    let num_cnstr_args =
-      let nparamsctxt =
-        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
-    in
-    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-      infer_check_convert_instances ~flex:false u1 u2 univs
-    else
-      infer_check_inductive_instances CONV cumi u1 u2 univs
-
-let check_inductive_instances cv_pb cumi u u' univs =
-  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
-    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
-    in
-    if (UGraph.check_constraints comp_cst univs) then univs
-    else raise NotConvertible
-
-let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    check_convert_instances
-    check_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let check_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    check_convert_instances
-    check_inductive_instances
-    cns u1 sv1 u2 sv2 univs
+let check_inductive_instances csts univs =
+  if (UGraph.check_constraints csts univs) then univs
+  else raise NotConvertible
 
 let checked_universes =
-  { compare = checked_sort_cmp_universes;
+  { compare_sorts = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
-    conv_inductives = check_conv_inductives;
-    conv_constructors = check_conv_constructors}
+    compare_cumul_instances = check_inductive_instances; }
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -786,49 +755,13 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
-  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
-    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
-    in
-    (univs, Univ.Constraint.union cstrs comp_cst)
-
-
-let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    infer_convert_instances
-    infer_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    infer_convert_instances
-    infer_inductive_instances
-    cns u1 sv1 u2 sv2 univs
-    
-let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
-  { compare = infer_cmp_universes;
+let infer_inductive_instances csts (univs,csts') =
+  (univs, Univ.Constraint.union csts csts')
+
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
+  { compare_sorts = infer_cmp_universes;
     compare_instances = infer_convert_instances;
-    conv_inductives = infer_conv_inductives;
-    conv_constructors = infer_conv_constructors}
+    compare_cumul_instances = infer_inductive_instances; }
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 573e4c8bd..0e6a2b819 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -35,15 +35,11 @@ type 'a extended_conversion_function =
 
 type conv_pb = CONV | CUMUL
 
-type 'a universe_compare = 
+type 'a universe_compare =
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
-      Univ.Instance.t -> int -> 'a -> 'a;
-    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
-      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
-  } 
+    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -51,6 +47,12 @@ 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 inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
+val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
+
 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 f72f6f26a..080bb7ad4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,7 +712,48 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-module Instance : sig 
+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
+
+module Instance : sig
     type t = Level.t array
 
     val empty : t
@@ -732,7 +773,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.t) -> t -> Pp.t
+    val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
@@ -808,8 +849,12 @@ struct
 
   let levels x = LSet.of_array x
 
-  let pr =
-    prvect_with_sep spc
+  let pr prl ?variance =
+    let ppu i u =
+      let v = Option.map (fun v -> v.(i)) variance in
+      pr_opt_no_spc Variance.pr v ++ prl u
+    in
+    prvecti_with_sep spc ppu
 
   let equal t u = 
     t == u ||
@@ -873,9 +918,9 @@ struct
   let empty = (Instance.empty, Constraint.empty)
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
 
-  let pr prl (univs, cst as ctx) =
+  let pr prl ?variance (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -911,66 +956,42 @@ 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.
+(** 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 context for
-    subtyping constraints is exactly twice as big as the context for
-    universe constraints. *)
+    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 (univs, variance) =
+    UContext.pr prl ~variance univs
 
-  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 (univs, variance) = (* should variance be hconsed? *)
+    (UContext.hcons univs, variance)
 
-  let hcons (univcst, subtypcst) =
-    (UContext.hcons univcst, UContext.hcons subtypcst)
-
-  let univ_context (univcst, subtypcst) = univcst
-  let subtyp_context (univcst, subtypcst) = subtypcst
-
-  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_susbst (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))
+
+  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
 
 end
 
@@ -1138,10 +1159,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 63bef1b81..77ebf5a11 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,6 +238,20 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
+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
+
+end
+
 (** {6 Universe instances} *)
 
 module Instance :
@@ -273,7 +287,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -347,36 +361,32 @@ 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.
+(** 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 context for
-    subtyping Constraint.t is exactly twice as big as the context for
-    universe Constraint.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_susbst : 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
 
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type cumulativity_info = CumulativityInfo.t
@@ -387,7 +397,9 @@ sig
   type t
 
   val univ_context : t -> AUContext.t
-  val subtyp_context : t -> AUContext.t
+  val variance : t -> Variance.t array
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type abstract_cumulativity_info = ACumulativityInfo.t
@@ -481,9 +493,11 @@ val make_abstract_instance : AUContext.t -> Instance.t
 
 val pr_constraint_type : constraint_type -> Pp.t
 val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
-val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  UContext.t -> Pp.t
 val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
-val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  AUContext.t -> Pp.t
 val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
 val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
 val explain_universe_inconsistency : (Level.t -> Pp.t) ->