Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

11 files changed, 138 insertions, 35 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8d32684b09..44676c9da5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,6 +87,11 @@ type typing_flags = {
 
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
+
+  check_template : bool;
+  (* If [false] then we don't check that the universes template-polymorphic
+     inductive parameterize on are necessarily local and unbounded from below.
+     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 391b139496..7225671a1e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
+  check_template = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 655094e88b..4a2aeea22d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,8 +59,9 @@ type globals = {
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -119,9 +120,9 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet;
     env_sprop_allowed = false;
-  };
+    env_universes_lbound = Univ.Level.set;
+    env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab;
@@ -262,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
 let indices_matter env = env.env_typing_flags.indices_matter
+let check_template env = env.env_typing_flags.check_template
 
 let universes env = env.env_stratification.env_universes
+let universes_lbound env = env.env_stratification.env_universes_lbound
+
+let set_universes_lbound env lbound =
+  let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
+  { env with env_stratification }
+
 let named_context env = env.env_named_context.env_named_ctx
 let named_context_val env = env.env_named_context
 let rel_context env = env.env_rel_context.env_rel_ctx
@@ -382,29 +390,30 @@ let check_constraints c env =
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let add_universes strict ctx g =
+let add_universes ~lbound ~strict ctx g =
   let g = Array.fold_left
-            (fun g v -> UGraph.add_universe v strict g)
+            (fun g v -> UGraph.add_universe ~lbound ~strict v g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
 			   
 let push_context ?(strict=false) ctx env =
-  map_universes (add_universes strict ctx) env
+  map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
 
-let add_universes_set strict ctx g =
+let add_universes_set ~lbound ~strict ctx g =
   let g = Univ.LSet.fold
             (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
-  map_universes (add_universes_set strict ctx) env
+  map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env
 
 let push_subgraph (levels,csts) env =
+  let lbound = universes_lbound env in
   let add_subgraph g =
-    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in
     let newg = UGraph.merge_constraints csts newg in
     (if not (Univ.Constraint.is_empty csts) then
        let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
@@ -428,6 +437,7 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
+     check_template;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -436,7 +446,8 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler
+  enable_native_compiler == alt.enable_native_compiler &&
+  check_template == alt.check_template
 [@warning "+9"]
 
 let set_typing_flags c env = (* Unsafe *)
@@ -568,11 +579,20 @@ let polymorphic_pind (ind,u) env =
 let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
+let template_checked_ind (mind,_i) env =
+  (lookup_mind mind env).mind_typing_flags.check_template
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | 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; _ } ->
+    List.map_filter (fun level -> level) l
+  | RegularArity _ -> []
+
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
@@ -762,6 +782,22 @@ let is_template_polymorphic env r =
   | IndRef ind -> template_polymorphic_ind ind env
   | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
 
+let get_template_polymorphic_variables env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> []
+  | ConstRef _c -> []
+  | IndRef ind -> template_polymorphic_variables ind env
+  | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
+
+let is_template_checked env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef _c -> false
+  | IndRef ind -> template_checked_ind ind env
+  | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
+
 let is_type_in_type env r =
   let open Names.GlobRef in
   match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index e6d814ac7d..f7de98dcfb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,8 +51,9 @@ type globals
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type named_context_val = private {
@@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
+val universes_lbound : env -> Univ.Level.t
+val set_universes_lbound : env -> Univ.Level.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
@@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
+val check_template : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
+val template_checked_ind : inductive -> env -> bool
 
 (** {5 Modules } *)
 
@@ -346,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
+val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
+val is_template_checked : env -> GlobRef.t -> bool
 val is_type_in_type : env -> GlobRef.t -> bool
 
 (** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c8e04b9fee..06d2e1bb21 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_}
   if not ind_squashed then InType
   else Sorts.family (Sorts.sort_of_univ ind_univ)
 
+(* For a level to be template polymorphic, it must be introduced
+   by the definition (so have no constraint except lbound <= l)
+   and not to be constrained from below, so any universe l' <= l
+   can be used as an instance of l. All bounds from above, i.e.
+   l <=/< r will be valid for any l' <= l. *)
+let unbounded_from_below u cstrs =
+  Univ.Constraint.for_all (fun (l, d, r) ->
+      match d with
+      | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+      | Lt | Le -> not (Univ.Level.equal r u))
+    cstrs
+
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
-   polymorphism. The elements x_k is None if the k-th parameter (starting
-   from the most recent and ignoring let-definitions) is not contributing
-   or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
+   polymorphism. The elements x_k is None if the k-th parameter
+   (starting from the most recent and ignoring let-definitions) is not
+   contributing to the inductive type's sort or is Some u_k if its level
+   is u_k and is contributing. *)
+let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+  let check_level l =
+    if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+       unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+      Some l
+    else None
+  in
+  let univs = Univ.Universe.levels concl in
+  let univs =
+    if template_check then
+      Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+    else univs (* Doesn't check the universes can be generalized *)
+  in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
-        | Sort (Type u) -> Univ.Universe.level u
+        | Sort (Type u) ->
+          if template_check then
+            (match Univ.Universe.level u with
+             | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+             | None -> None)
+          else Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
-  List.fold_left fold [] paramsctxt
+  let params = List.fold_left fold [] paramsctxt in
+  params, univs
 
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
   let arity = Vars.subst_univs_level_constr usubst arity in
   let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
   let indices = Vars.subst_univs_level_context usubst indices in
@@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
   let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
 
   let arity = match univ_info.ind_min_univ with
-    | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+    | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
     | Some min_univ ->
-      ((match univs with
-          | Monomorphic _ -> ()
+      let ctx = match univs with
+          | Monomorphic ctx -> ctx
           | Polymorphic _ ->
             CErrors.anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
-       TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+      let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+      if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+         && Univ.LSet.is_empty concl_levels then
+        CErrors.anomaly ~label:"polymorphic_template_ind"
+          Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+      else
+        TemplateArity {template_param_levels = param_levels; template_level = min_univ}
   in
 
   let kelim = allowed_sorts univ_info in
@@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   mind_check_names mie;
   assert (List.is_empty (Environ.rel_context env));
 
+  let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+
   (* universes *)
   let env_univs =
     match mie.mind_entry_universes with
-    | Monomorphic_entry ctx -> push_context_set ctx env
+    | Monomorphic_entry ctx ->
+      let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
+      push_context_set ctx env
     | Polymorphic_entry (_, ctx) -> push_context ctx env
   in
 
@@ -335,7 +376,8 @@ let typecheck_inductive env (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 template_check = Environ.check_template env in
+  let data = List.map (abstract_packets ~template_check univs usubst params) data in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index aaa0d6a149..8da4e2885c 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
      Sorts.family)
     array
+
+(* Utility function to compute the actual universe parameters
+   of a template polymorphic inductive *)
+val template_polymorphic_univs :
+  template_check:bool ->
+  Univ.ContextSet.t ->
+  Constr.rel_context ->
+  Univ.Universe.t ->
+  Univ.Level.t option list * Univ.LSet.t
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9305a91731..ccc218771a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           c', Monomorphic Univ.ContextSet.empty, cst
         | Polymorphic uctx, Some ctx ->
           let () =
-            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+            if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env)
+                      (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
           (** Terms are compared in a context with De Bruijn universe indices *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 53f228c618..327cb2efeb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs =
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> infer_pb Univ.type0_univ u
-    | Type _u, Prop -> raise NotConvertible
+    | Type u, Prop -> infer_pb u Univ.type0m_univ
     | Type u, Set -> infer_pb u Univ.type0_univ
     | Type u0, Type u1 -> infer_pb u0 u1
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d47dc0c6e1..d22ec3b7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -97,7 +97,8 @@ let check_universes error env u1 u2 =
   match u1, u2 with
   | Monomorphic _, Monomorphic _ -> env
   | Polymorphic auctx1, Polymorphic auctx2 ->
-    if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    let lbound = Environ.universes_lbound env in
+    if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then
       error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
     else
       Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6fde6e9c5f..33336079bb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -149,10 +149,10 @@ let enforce_leq_alg u v g =
   cg
 
 exception AlreadyDeclared = G.AlreadyDeclared
-let add_universe u strict g =
+let add_universe u ~lbound ~strict g =
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
-  enforce_constraint (Level.set,d,u) {g with graph}
+  enforce_constraint (lbound,d,u) {g with graph}
 
 let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
 
@@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k
 
 (** Subtyping of polymorphic contexts *)
 
-let check_subtype univs ctxT ctx =
+let check_subtype ~lbound univs ctxT ctx =
   if AUContext.size ctxT == AUContext.size ctx then
     let (inst, cst) = UContext.dest (AUContext.repr ctx) in
     let cstT = UContext.constraints (AUContext.repr ctxT) in
-    let push accu v = add_universe v false accu in
+    let push accu v = add_universe v ~lbound ~strict:false accu in
     let univs = Array.fold_left push univs (Instance.to_array inst) in
     let univs = merge_constraints cstT univs in
     check_constraints cst univs
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1b5868d55..d90f01d8d1 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> bool -> t -> t
+val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : AUContext.t check_function
+val check_subtype : lbound:Level.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)