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

1 files changed, 49 insertions, 13 deletions

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;}