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 |=  *)

5 files changed, 128 insertions, 99 deletions

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