generate variance data for section universes (not yet used)

preparation for direct discharge

13 files changed, 68 insertions, 15 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 06ee4fcc7a..cd00bf35ee 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -139,7 +139,7 @@ let check_inductive env mind mb =
   let entry = to_entry mb in
   let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
-        mind_universes; mind_variance;
+        mind_universes; mind_variance; mind_sec_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
@@ -148,7 +148,7 @@ let check_inductive env mind mb =
                                                                   check_positive = mb_flags.check_positive;
                                                                   check_universes = mb_flags.check_universes;
                                                                   conv_oracle = mb_flags.conv_oracle} env in
-    Indtypes.check_inductive env mind entry
+    Indtypes.check_inductive env ~sec_univs:None mind entry
   in
   let check = check mind in
 
@@ -165,7 +165,9 @@ let check_inductive env mind mb =
 
   check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
   ignore mind_universes; (* Indtypes did the necessary checking *)
-  ignore mind_variance; (* Indtypes did the necessary checking *)
+  check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal)
+                           mb.mind_variance mind_variance);
+  check "mind_sec_variance" (Option.is_empty mind_sec_variance);
   ignore mind_private; (* passed through Indtypes *)
 
   ignore mind_typing_flags;
diff --git a/checker/values.ml b/checker/values.ml
index 56321a27ff..df6a9136c8 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -299,6 +299,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_rctxt;
     v_univs; (* universes *)
     Opt (Array v_variance);
+    Opt (Array v_variance);
     Opt v_bool;
     v_typing_flags|]
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9fd10b32e6..948f52884e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -223,6 +223,9 @@ type mutual_inductive_body = {
 
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
+    mind_sec_variance : Univ.Variance.t array option;
+    (** Variance info for section polymorphic universes. [None] outside sections. *)
+
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
     mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 35185b6a5e..27e3f84464 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -248,6 +248,7 @@ let subst_mind_body sub mib =
     mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
     mind_variance = mib.mind_variance;
+    mind_sec_variance = mib.mind_sec_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 3f2f9f4fc0..591cd050a5 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -276,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
   let kelim = allowed_sorts univ_info in
   (arity,lc), (indices,splayed_lc), kelim
 
-let typecheck_inductive env (mie:mutual_inductive_entry) =
+let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   let () = match mie.mind_entry_inds with
   | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
   | _ -> ()
@@ -341,7 +341,12 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
         CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
       | Polymorphic_entry (_,uctx) ->
         let univs = Instance.to_array @@ UContext.instance uctx in
-        Some (InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds)
+        let univs = match sec_univs with
+          | None -> univs
+          | Some sec_univs -> Array.append sec_univs univs
+        in
+        let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
+        Some variances
   in
 
   (* Abstract universes *)
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 5c04e860a2..8dea8f046d 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
     - environment with inductives + parameters in rel context
     - abstracted universes
     - checked variance info
+      (variance for section universes is at the beginning of the array)
     - record entry (checked to be OK)
     - parameters
     - for each inductive,
@@ -24,9 +25,11 @@ open Declarations
       * (indices * splayed constructor types) (both without params)
       * top allowed elimination
  *)
-val typecheck_inductive : env -> mutual_inductive_entry ->
-  env
-  * universes * Univ.Variance.t array option
+val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
+  -> mutual_inductive_entry
+  -> env
+  * universes
+  * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0d900c2ec9..3771454db5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -466,7 +466,8 @@ let compute_projections (kn, i as ind) mib =
   Array.of_list (List.rev rs),
   Array.of_list (List.rev pbs)
 
-let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env ~sec_univs names prv univs variance
+    paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env paramsctxt inds in
@@ -517,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
         mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map3 build_one_packet names inds recargs in
+  let variance, sec_variance = match variance with
+    | None -> None, None
+    | Some variance -> match sec_univs with
+      | None -> Some variance, None
+      | Some sec_univs ->
+        let nsec = Array.length sec_univs in
+        Some (Array.sub variance nsec (Array.length variance - nsec)),
+        Some (Array.sub variance 0 nsec)
+  in
   let mib =
       (* Build the mutual inductive *)
     { mind_record = NotRecord;
@@ -529,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
       mind_packets = packets;
       mind_universes = univs;
       mind_variance = variance;
+      mind_sec_variance = sec_variance;
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
@@ -549,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 (************************************************************************)
 (************************************************************************)
 
-let check_inductive env kn mie =
+let check_inductive env ~sec_univs kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+  let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+    IndTyping.typecheck_inductive env ~sec_univs mie
+  in
   (* Then check positivity conditions *)
   let chkpos = (Environ.typing_flags env).check_positive in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -562,6 +575,6 @@ let check_inductive env kn mie =
       (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
   in
   (* Build the inductive packets *)
-    build_inductive env names mie.mind_entry_private univs variance
+    build_inductive env ~sec_univs names mie.mind_entry_private univs variance
       paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 240ba4e2bb..9b54e8b878 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,4 +14,5 @@ open Environ
 open Entries
 
 (** Check an inductive. *)
-val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
+val check_inductive : env -> sec_univs:Univ.Level.t array option
+  -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ee101400d6..b732ef5900 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -911,7 +911,9 @@ let check_mind mie lab =
 let add_mind l mie senv =
   let () = check_mind mie l in
   let kn = MutInd.make2 senv.modpath l in
-  let mib = Indtypes.check_inductive senv.env kn mie in
+  let sec_univs = Option.map Section.all_poly_univs  senv.sections
+  in
+  let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
   in
diff --git a/kernel/section.ml b/kernel/section.ml
index 603ef5d006..6fa0543b23 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -28,6 +28,8 @@ type 'a t = {
   sec_mono_universes : ContextSet.t;
   sec_poly_universes : Name.t array * UContext.t;
   (** Universes local to the section *)
+  all_poly_univs : Univ.Level.t array;
+  (** All polymorphic universes, including from previous sections. *)
   has_poly_univs : bool;
   (** Are there polymorphic universes or constraints, including in previous sections. *)
   sec_entries : section_entry list;
@@ -41,6 +43,8 @@ let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth p
 
 let has_poly_univs sec = sec.has_poly_univs
 
+let all_poly_univs sec = sec.all_poly_univs
+
 let find_emap e (cmap, imap) = match e with
 | SecDefinition con -> Cmap.find con cmap
 | SecInductive ind -> Mindmap.find ind imap
@@ -57,7 +61,10 @@ let push_context (nas, ctx) sec =
   else
     let (snas, sctx) = sec.sec_poly_universes in
     let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
-    { sec with sec_poly_universes; has_poly_univs = true }
+    let all_poly_univs =
+      Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx)
+    in
+    { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true }
 
 let rec is_polymorphic_univ u sec =
   let (_, uctx) = sec.sec_poly_universes in
@@ -81,6 +88,7 @@ let open_section ~custom sec_prev =
     sec_context = 0;
     sec_mono_universes = ContextSet.empty;
     sec_poly_universes = ([||], UContext.empty);
+    all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev;
     has_poly_univs = Option.cata has_poly_univs false sec_prev;
     sec_entries = [];
     sec_data = (Cmap.empty, Mindmap.empty);
diff --git a/kernel/section.mli b/kernel/section.mli
index fbd3d8254e..37d0dab317 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 
 (** {6 Retrieving section data} *)
 
+val all_poly_univs : 'a t -> Univ.Level.t array
+(** Returns all polymorphic universes, including those from previous
+   sections. Earlier sections are earlier in the array.
+
+    NB: even if the array is empty there may be polymorphic
+   constraints about monomorphic universes, which prevent declaring
+   monomorphic globals. *)
+
 type abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0029ff96d5..51440147ad 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -755,6 +755,10 @@ struct
     | Invariant, _ | _, Invariant -> Invariant
     | Covariant, Covariant -> Covariant
 
+  let equal a b = match a,b with
+    | Irrelevant, Irrelevant | Covariant, Covariant | Invariant, Invariant -> true
+    | (Irrelevant | Covariant | Invariant), _ -> false
+
   let check_subtype x y = match x, y with
   | (Irrelevant | Covariant | Invariant), Irrelevant -> true
   | Irrelevant, Covariant -> false
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ccb5c80cbf..1914ce5e34 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -263,6 +263,8 @@ sig
 
   val pr : t -> Pp.t
 
+  val equal : t -> t -> bool
+
 end
 
 (** {6 Universe instances} *)