From e0bcbccf437ebee4157fdfdd5cba7b42019ead27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Mar 2020 10:57:19 +0100
Subject: Ensure that template parameters are shared in the same inductive
 block.

This could have been at the root of strange behaviours (read unsoundness).
---
 kernel/indTyping.ml | 104 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 70 insertions(+), 34 deletions(-)

(limited to 'kernel/indTyping.ml')

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
-- 
cgit v1.2.3