Ensure that template parameters are shared in the same inductive block.

This could have been at the root of strange behaviours (read unsoundness).

14 files changed, 142 insertions, 86 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index b93b03ec16..c4c6d9bb4f 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string
 
 let check mind field b = if not b then raise (InductiveMismatch (mind,field))
 
-let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
+let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   let open Entries in
   let nparams = List.length mb.mind_params_ctxt in (* include letins *)
   let mind_entry_record = match mb.mind_record with
@@ -33,20 +33,9 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
         inductive types. The set of monomorphic constraints is already part of
         the graph at that point, but we need to emulate a broken bound variable
         mechanism for template inductive types. *)
-      let fold accu ind = match ind.mind_arity with
-      | RegularArity _ -> accu
-      | TemplateArity ar ->
-        match accu with
-        | None -> Some ar.template_context
-        | Some ctx ->
-          (* Ensure that all template contexts agree. This is enforced by the
-             kernel. *)
-          let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in
-          Some ctx
-      in
-      let univs = match Array.fold_left fold None mb.mind_packets with
+      let univs = match mb.mind_template with
       | None -> ContextSet.empty
-      | Some ctx -> ctx
+      | Some ctx -> ctx.template_context
       in
       Monomorphic_entry univs
     | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
@@ -95,13 +84,18 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
   | RegularArity ar, RegularArity {mind_user_arity;mind_sort} ->
     Constr.equal ar.mind_user_arity mind_user_arity &&
     Sorts.equal ar.mind_sort mind_sort
-  | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} ->
-    List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
-    ContextSet.equal template_context ar.template_context &&
+  | TemplateArity ar, TemplateArity {template_level} ->
     UGraph.check_leq (universes env) template_level ar.template_level
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> assert false
 
+let check_template ar1 ar2 = match ar1, ar2 with
+| None, None -> true
+| Some ar, Some {template_context; template_param_levels} ->
+  List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
+  ContextSet.equal template_context ar.template_context
+| None, Some _ | Some _, None -> false
+
 let check_kelim k1 k2 = Sorts.family_leq k1 k2
 
 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost
@@ -163,10 +157,10 @@ let check_same_record r1 r2 = match r1, r2 with
   | (NotRecord | FakeRecord | PrimRecord _), _ -> false
 
 let check_inductive env mind mb =
-  let entry = to_entry mind mb in
+  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_sec_variance;
+        mind_universes; mind_template; mind_variance; mind_sec_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
@@ -197,6 +191,7 @@ 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 *)
+  check "mind_template" (check_template mb.mind_template mind_template);
   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);
diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
index ac9ea2fb31..9ef6ff017c 100644
--- a/checker/checkTypes.mli
+++ b/checker/checkTypes.mli
@@ -17,4 +17,4 @@ open Environ
 (*s Typing functions (not yet tagged as safe) *)
 
 val check_polymorphic_arity :
-  env -> rel_context -> template_arity -> unit
+  env -> rel_context -> template_universes -> unit
diff --git a/checker/values.ml b/checker/values.ml
index ed730cff8e..cba96e6636 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -227,8 +227,11 @@ let v_oracle =
     v_pred v_cst;
   |]
 
-let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|]
+let v_template_arity =
+  v_tuple "template_arity" [|v_univ|]
+
+let v_template_universes =
+  v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
 
 let v_primitive =
   v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
@@ -265,7 +268,7 @@ let v_mono_ind_arity =
   v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|]
 
 let v_ind_arity = v_sum "inductive_arity" 0
-  [|[|v_mono_ind_arity|];[|v_pol_arity|]|]
+  [|[|v_mono_ind_arity|];[|v_template_arity|]|]
 
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;
@@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     v_rctxt;
     v_univs; (* universes *)
+    Opt v_template_universes;
     Opt (Array v_variance);
     Opt (Array v_variance);
     Opt v_bool;
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31dd26d2ba..13ee353c6b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t =
   t
 
 let cook_one_ind ~ntypes
-    (section_decls,_ as hyps) expmod mip =
+    hyps expmod mip =
   let mind_arity = match mip.mind_arity with
     | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
       let arity = abstract_as_type (expmod arity) hyps in
       let sort = destSort (expmod (mkSort sort)) in
       RegularArity {mind_user_arity=arity; mind_sort=sort}
-    | TemplateArity {template_param_levels=levels;template_level;template_context} ->
-      let sec_levels = CList.map_filter (fun d ->
-          if RelDecl.is_local_assum d then Some None
-          else None)
-          section_decls
-      in
-      let levels = List.rev_append sec_levels levels in
-      TemplateArity {template_param_levels=levels;template_level;template_context}
+    | TemplateArity {template_level} ->
+      TemplateArity {template_level}
   in
   let mind_arity_ctxt =
     let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
@@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
       in
       Some (Array.append newvariance variance), Some sec_variance
   in
+  let mind_template = match mib.mind_template with
+  | None -> None
+  | Some {template_param_levels=levels; template_context} ->
+      let sec_levels = CList.map_filter (fun d ->
+          if RelDecl.is_local_assum d then Some None
+          else None)
+          section_decls
+      in
+      let levels = List.rev_append sec_levels levels in
+      Some {template_param_levels=levels; template_context}
+  in
   {
     mind_packets;
     mind_record;
@@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
     mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
     mind_params_ctxt;
     mind_universes;
+    mind_template;
     mind_variance;
     mind_sec_variance;
     mind_private = mib.mind_private;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ac130d018d..11a07ee5cf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -30,8 +30,11 @@ type engagement = set_predicativity
 *)
 
 type template_arity = {
-  template_param_levels : Univ.Level.t option list;
   template_level : Univ.Universe.t;
+}
+
+type template_universes = {
+  template_param_levels : Univ.Level.t option list;
   template_context : Univ.ContextSet.t;
 }
 
@@ -218,6 +221,8 @@ type mutual_inductive_body = {
 
     mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
+    mind_template : template_universes option;
+
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
     mind_sec_variance : Univ.Variance.t array option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a3adac7a11..a1122d1279 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -46,9 +46,10 @@ let map_decl_arity f g = function
   | TemplateArity a -> TemplateArity (g a)
 
 let hcons_template_arity ar =
+  { template_level = Univ.hcons_univ ar.template_level; }
+
+let hcons_template_universe ar =
   { template_param_levels = ar.template_param_levels;
-      (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
-    template_level = Univ.hcons_univ ar.template_level;
     template_context = Univ.hcons_universe_context_set ar.template_context }
 
 let universes_context = function
@@ -247,6 +248,7 @@ let subst_mind_body sub mib =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
+    mind_template = mib.mind_template;
     mind_variance = mib.mind_variance;
     mind_sec_variance = mib.mind_sec_variance;
     mind_private = mib.mind_private;
@@ -323,6 +325,7 @@ let hcons_mind mib =
   { mib with
     mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
+    mind_template = Option.Smart.map hcons_template_universe mib.mind_template;
     mind_universes = hcons_universes mib.mind_universes }
 
 (** Hashconsing of modules *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 501ac99ff3..1b5a77cc96 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env =
   | TemplateArity _ -> true
   | RegularArity _ -> false
 
-let template_polymorphic_variables (mind,i) env =
-  match (lookup_mind mind env).mind_packets.(i).mind_arity with
-  | TemplateArity { Declarations.template_param_levels = l; _ } ->
+let template_polymorphic_variables (mind, _) env =
+  match (lookup_mind mind env).mind_template with
+  | Some { Declarations.template_param_levels = l; _ } ->
     List.map_filter (fun level -> level) l
-  | RegularArity _ -> []
+  | None -> []
 
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 1d72d1bd6e..d5aadd0c02 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -222,7 +222,66 @@ let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
   else if not @@ Univ.LSet.is_empty univs then Some (univs, params)
   else None
 
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let get_param_levels ctx params arity splayed_lc =
+  let min_univ = match arity with
+  | RegularArity _ ->
+    CErrors.user_err
+      Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.")
+  | TemplateArity ar -> ar.template_level
+  in
+  let ctor_levels =
+    let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+    let param_levels =
+      List.fold_left (fun levels d -> match d with
+          | LocalAssum _ -> levels
+          | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+        Univ.LSet.empty params
+    in
+    Array.fold_left
+      (fun levels (d,c) ->
+          let levels =
+            List.fold_left (fun levels d ->
+                Context.Rel.Declaration.fold_constr add_levels d levels)
+              levels d
+          in
+          add_levels c levels)
+      param_levels
+      splayed_lc
+  in
+  match template_polymorphic_univs ~ctor_levels ctx params min_univ with
+  | None ->
+    CErrors.user_err
+      Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+  | Some (_, param_levels) ->
+    param_levels
+
+let get_template univs params data =
+  let ctx = match univs with
+      | Monomorphic ctx -> ctx
+      | Polymorphic _ ->
+        CErrors.anomaly ~label:"polymorphic_template_ind"
+          Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+  (* For each type in the block, compute potential template parameters *)
+  let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in
+  (* Pick the lower bound of template parameters. Note that in particular, if
+     one of the the inductive types from the block is Prop-valued, then no
+     parameters are template. *)
+  let fold min params =
+    let map u v = match u, v with
+    | (None, _) | (_, None) -> None
+    | Some u, Some v ->
+      let () = assert (Univ.Level.equal u v) in
+      Some u
+    in
+    List.map2 map min params
+  in
+  let params = match params with
+  | [] -> assert false
+  | hd :: rem -> List.fold_left fold hd rem
+  in
+  { template_param_levels = params; template_context = ctx }
+
+let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
   if not (Universe.Set.is_empty univ_info.missing)
   then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
   let arity = Vars.subst_univs_level_constr usubst arity in
@@ -238,37 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
 
   let arity = match univ_info.ind_min_univ with
     | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
-    | Some min_univ ->
-      let ctx = match univs with
-          | Monomorphic ctx -> ctx
-          | Polymorphic _ ->
-            CErrors.anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
-      let ctor_levels =
-        let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
-        let param_levels =
-          List.fold_left (fun levels d -> match d with
-              | LocalAssum _ -> levels
-              | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
-            Univ.LSet.empty params
-        in
-        Array.fold_left
-          (fun levels (d,c) ->
-             let levels =
-               List.fold_left (fun levels d ->
-                   Context.Rel.Declaration.fold_constr add_levels d levels)
-                 levels d
-             in
-             add_levels c levels)
-          param_levels
-          splayed_lc
-      in
-      match template_polymorphic_univs ~ctor_levels ctx params min_univ with
-      | None ->
-        CErrors.user_err
-          Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
-      | Some (_, param_levels) ->
-        TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
+    | Some min_univ -> TemplateArity { template_level = min_univ; }
   in
 
   let kelim = allowed_sorts univ_info in
@@ -350,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
-  let data = List.map (abstract_packets univs usubst params) data in
+  let data = List.map (abstract_packets usubst) data in
+  let template =
+    let check ((arity, _), _, _) = match arity with
+    | TemplateArity _ -> true
+    | RegularArity _ -> false
+    in
+    if List.exists check data then Some (get_template univs params data) else None
+  in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
@@ -359,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, variance, record, params, Array.of_list data
+  env_ar_par, univs, template, variance, record, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index a625caec83..babb82c39e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
   -> mutual_inductive_entry
   -> env
   * universes
+  * template_universes option
   * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b6b8e5265c..58e5e76b61 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib =
   Array.of_list (List.rev rs),
   Array.of_list (List.rev pbs)
 
-let build_inductive env ~sec_univs names prv univs variance
+let build_inductive env ~sec_univs names prv univs template variance
     paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
@@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_universes = univs;
+      mind_template = template;
       mind_variance = variance;
       mind_sec_variance = sec_variance;
       mind_private = prv;
@@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance
 
 let check_inductive env ~sec_univs kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+  let (env_ar_par, univs, template, variance, record, paramsctxt, inds) =
     IndTyping.typecheck_inductive env ~sec_univs mie
   in
   (* Then check positivity conditions *)
@@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie =
       (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
   in
   (* Build the inductive packets *)
-    build_inductive env ~sec_univs names mie.mind_entry_private univs variance
+    build_inductive env ~sec_univs names mie.mind_entry_private univs template variance
       paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1be86f2bf8..6325779675 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -185,8 +185,8 @@ let make_subst =
 
 exception SingletonInductiveBecomesProp of Id.t
 
-let instantiate_universes ctx ar args =
-  let subst = make_subst (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx (templ, ar) args =
+  let subst = make_subst (ctx,templ.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes ctx ar paramtyps in
+    let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b690fe1157..90571844b9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : Sorts.t array -> Universe.t
 
-val instantiate_universes : Constr.rel_context ->
-  template_arity -> param_univs -> Constr.rel_context * Sorts.t
-
 (** {6 Debug} *)
 
 type size = Large | Strict
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aafd662f7d..c9ccd668ca 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) | Construct ((ind, _), u) ->
     let mib,oib = Inductive.lookup_mind_specif env ind in
-      (match oib.mind_arity with
-      | RegularArity _ -> assert false
-      | TemplateArity templ -> templ.template_param_levels)
+      (match mib.mind_template with
+      | None -> assert false
+      | Some templ -> templ.template_param_levels)
   | _ -> assert false
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a4406aeba1..01994a35c7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
   | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let _,scl = splay_arity env sigma conclty in
     let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
       instantiate_universes
-        env evdref scl ar.template_level (ctx,ar.template_param_levels) in
+        env evdref scl ar.template_level (ctx,templ.template_param_levels) in
       !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_constant env (p,u) =