Merge PR #9439: Separate variance and universe fields in inductives.

Ack-by: ppedrot

12 files changed, 46 insertions, 71 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 8374a5c84f..823177d4d1 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -215,7 +215,7 @@ let build_id_coercion idf_opt source poly =
 	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
-  let univs = Evd.const_univ_entry ~poly sigma in
+  let univs = Evd.univ_entry ~poly sigma in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
       (definition_entry ~types:typ_f ~univs
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea434dbc4f..27d8b7390d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,7 +374,7 @@ let context poly l =
   let univs =
     match ctx with
     | [] -> assert false
-    | [_] -> Evd.const_univ_entry ~poly sigma
+    | [_] -> Evd.univ_entry ~poly sigma
     | _::_::_ ->
       if Lib.sections_are_opened ()
       then
@@ -384,19 +384,19 @@ let context poly l =
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
-          else Monomorphic_const_entry Univ.ContextSet.empty
+          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
+          else Monomorphic_entry Univ.ContextSet.empty
         end
       else if poly then
         (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
-        Evd.const_univ_entry ~poly sigma
+        Evd.univ_entry ~poly sigma
       else
         (* Multiple monomorphic axioms: declare universes separately
            to avoid redeclaring them. *)
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          Monomorphic_const_entry Univ.ContextSet.empty
+          Monomorphic_entry Univ.ContextSet.empty
         end
   in
   let fn status (id, b, t) =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 73d0be04df..466757c6bd 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -46,8 +46,8 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ide
 match local with
 | Discharge when Lib.sections_are_opened () ->
   let ctx = match ctx with
-    | Monomorphic_const_entry ctx -> ctx
-    | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx
+    | Monomorphic_entry ctx -> ctx
+    | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
   in
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
@@ -79,8 +79,8 @@ match local with
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
-    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
-    | Monomorphic_const_entry _ -> Univ.Instance.empty
+    | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+    | Monomorphic_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
 
@@ -90,10 +90,10 @@ let interp_assumption ~program_mode sigma env impls c =
 
 (* When monomorphic the universe constraints are declared with the first declaration only. *)
 let next_uctx =
-  let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in
+  let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in
   function
-  | Polymorphic_const_entry _ as uctx -> uctx
-  | Monomorphic_const_entry _ -> empty_uctx
+  | Polymorphic_entry _ as uctx -> uctx
+  | Monomorphic_entry _ -> empty_uctx
 
 let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
   let refs, status, _ =
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 385ec33bea..2b794b001a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -29,7 +29,7 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind ->
-  types in_constant_universes_entry ->
+  types in_universes_entry ->
   UnivNames.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
   GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 68ad276113..9bbfb8eec6 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -457,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
         indimpls, List.map (fun impls ->
           userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
-  let univs =
-    match uctx with
-    | Polymorphic_const_entry (nas, uctx) ->
-      if cum then
-        Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
-      else Polymorphic_ind_entry (nas, uctx)
-    | Monomorphic_const_entry uctx ->
-      Monomorphic_ind_entry uctx
-  in
+  let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -473,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       mind_entry_finite = finite;
       mind_entry_inds = entries;
       mind_entry_private = if prv then Some false else None;
-      mind_entry_universes = univs;
+      mind_entry_universes = uctx;
+      mind_entry_variance = variance;
     }
   in
   (if poly && cum then
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1e3644c371..e455b59ab2 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -19,7 +19,7 @@ val declare_definition : Id.t -> definition_kind ->
   GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
-  UnivNames.universe_binders -> Entries.constant_universes_entry ->
+  UnivNames.universe_binders -> Entries.universes_entry ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
   GlobRef.t
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 367fa4ce98..9dd321be51 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -923,6 +923,8 @@ let explain_not_match_error = function
     str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++
     (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else
        fnl() ++ str "(incompatible constraints)")
+  | IncompatibleVariance ->
+    str "incompatible variance information"
 
 let explain_signature_mismatch l spec why =
   str "Signature components for label " ++ Label.print l ++
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index d29f66f81f..caafd6ac2f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -103,7 +103,7 @@ let () =
 
 let define ~poly id internal sigma c t =
   let f = declare_constant ~internal in
-  let univs = Evd.const_univ_entry ~poly sigma in
+  let univs = Evd.univ_entry ~poly sigma in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 79182a3f9d..83dd1aa8e4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -230,10 +230,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let univs = match univs with
-            | Polymorphic_const_entry (_, univs) ->
+            | Polymorphic_entry (_, univs) ->
               (* What is going on here? *)
               Univ.ContextSet.of_context univs
-            | Monomorphic_const_entry univs -> univs
+            | Monomorphic_entry univs -> univs
           in
           let c = SectionLocalAssum ((t_i, univs),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
@@ -476,7 +476,7 @@ let save_proof ?proof = function
             if const_entry_type = None then
               user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
-            let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
+            let ctx = UState.univ_entry ~poly:(pi2 k) universes in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b20758dac5..ba78c73131 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -557,7 +557,7 @@ let declare_mutual_definition l =
             mk_proof (mkCoFix (i,fixdecls))) 0 l
   in
   (* Declare the recursive definitions *)
-  let univs = UState.const_univ_entry ~poly first.prg_ctx in
+  let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
   let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
     fixnames fixdecls fixtypes fiximps in
@@ -656,9 +656,9 @@ let declare_obligation prg obl body ty uctx =
       if not opaque then add_hint (Locality.make_section_locality None) prg constant;
       definition_message obl.obl_name;
       let body = match uctx with
-        | Polymorphic_const_entry (_, uctx) ->
+        | Polymorphic_entry (_, uctx) ->
           Some (DefinedObl (constant, Univ.UContext.instance uctx))
-        | Monomorphic_const_entry _ ->
+        | Monomorphic_entry _ ->
           Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
       in
       true, { obl with obl_body = body }
@@ -879,7 +879,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
       if pi2 prg.prg_kind then ctx
       else UState.union prg.prg_ctx ctx
     in
-    let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+    let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
     let (defined, obl) = declare_obligation prg obl body ty uctx in
     let obls = Array.copy obls in
     let () = obls.(num) <- obl in
@@ -1010,7 +1010,7 @@ and solve_obligation_by_tac prg obls i tac =
                 (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with
         | None -> None
         | Some (t, ty, ctx) ->
-          let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+          let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
           let prg = {prg with prg_ctx = ctx} in
           let def, obl' = declare_obligation prg obl t ty uctx in
           obls.(i) <- obl';
@@ -1159,7 +1159,7 @@ let admit_prog prg =
         match x.obl_body with
         | None ->
             let x = subst_deps_obl obls x in
-            let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
+            let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
             let kn = Declare.declare_constant x.obl_name ~local:true
               (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b9a564b9e..0bd15e203b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,8 +277,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
   let u = match ctx with
-    | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
-    | Monomorphic_const_entry ctx -> Univ.Instance.empty
+    | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+    | Monomorphic_entry ctx -> Univ.Instance.empty
   in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let r = mkIndU (indsp,u) in
@@ -369,17 +369,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 open Typeclasses
 
 
-let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
+let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
   let nparams = List.length params in
   let poly, ctx =
     match univs with
-    | Monomorphic_ind_entry ctx ->
-      false, Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry (nas, ctx) ->
-      true, Polymorphic_const_entry (nas, ctx)
-    | Cumulative_ind_entry (nas, cumi) ->
-      true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
+    | Monomorphic_entry ctx ->
+      false, Monomorphic_entry Univ.ContextSet.empty
+    | Polymorphic_entry (nas, ctx) ->
+      true, Polymorphic_entry (nas, ctx)
   in
+  let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in
   let binder_name =
     match name with
     | None ->
@@ -427,6 +426,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
       mind_entry_inds = blocks;
       mind_entry_private = None;
       mind_entry_universes = univs;
+      mind_entry_variance = variance;
     }
   in
   let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
@@ -472,8 +472,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
       let inst, univs = match univs with
-        | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
-        | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
+        | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
+        | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty
       in
       let cstu = (cst, inst) in
       let inst_type = appvectc (mkConstU cstu)
@@ -496,18 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-       let univs =
-         match univs with
-         | Polymorphic_const_entry (nas, univs) ->
-           if cum then
-             Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
-           else
-             Polymorphic_ind_entry (nas, univs)
-         | Monomorphic_const_entry univs ->
-           Monomorphic_ind_entry univs
-       in
       let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
-      let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls
+      let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Method ~name:[|binder_name|] record_data
       in
        let coers = List.map2 (fun coe pri -> 
@@ -531,14 +521,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
   in
   let univs, ctx_context, fields =
     match univs with
-    | Polymorphic_const_entry (nas, univs) ->
+    | Polymorphic_entry (nas, univs) ->
       let usubst, auctx = Univ.abstract_universes nas univs in
       let usubst = Univ.make_instance_subst usubst in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
       let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
       auctx, ctx_context, fields
-    | Monomorphic_const_entry _ ->
+    | Monomorphic_entry _ ->
       Univ.AUContext.empty, ctx_context, fields
   in
   let map (impl, projs) =
@@ -670,21 +660,11 @@ let definition_structure udecl kind ~template cum poly finite records =
   | _ ->
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
-      let univs =
-        match univs with
-        | Polymorphic_const_entry (nas, univs) ->
-          if cum then
-            Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
-          else
-            Polymorphic_ind_entry (nas, univs)
-        | Monomorphic_const_entry univs ->
-          Monomorphic_ind_entry univs
-      in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
       let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
-    let inds = declare_structure finite ubinders univs implpars params template data in
+    let inds = declare_structure ~cum finite ubinders univs implpars params template data in
     List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 04984030f7..9852840d12 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -16,7 +16,7 @@ val primitive_flag : bool ref
 
 val declare_projections :
   inductive ->
-  Entries.constant_universes_entry ->
+  Entries.universes_entry ->
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
   bool list ->