Make kernel parametric on the lowest universe and fix #9294

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.

1 files changed, 56 insertions, 14 deletions

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