From 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 17:10:49 +0100
Subject: Do not hardcode specific handling of Prop levels in template poly.

We also factorize a few checks by returning an option when looking for
a potentially template universe.
---
 kernel/indTyping.ml  | 20 +++++++++-----------
 kernel/indTyping.mli |  2 +-
 2 files changed, 10 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index cc15109f06..d48422909f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -200,26 +200,27 @@ let unbounded_from_below u cstrs =
 let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
   let check_level l =
     Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+    (let () = assert (not @@ Univ.Level.is_small l) in true) &&
     unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
     not (Univ.LSet.mem l ctor_levels)
   in
   let univs = Univ.Universe.levels concl in
-  let univs =
-    Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
-  in
+  let univs = Univ.LSet.filter (fun l -> check_level l) univs in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
         | Sort (Type u) ->
             (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
+             | Some l -> if Univ.LSet.mem l univs then Some l else None
              | None -> None)
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
   let params = List.fold_left fold [] paramsctxt in
-  params, univs
+  if Universe.is_type0m concl then Some (univs, params)
+  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) =
   if not (Universe.Set.is_empty univ_info.missing)
@@ -262,14 +263,11 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
           param_levels
           splayed_lc
       in
-      let param_levels, concl_levels =
-        template_polymorphic_univs ~ctor_levels ctx params min_univ
-      in
-      if List.for_all (fun x -> Option.is_empty x) param_levels
-         && Univ.LSet.is_empty concl_levels then
+      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.")
-      else
+      | Some (_, param_levels) ->
         TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
   in
 
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 723ba5459e..a625caec83 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -44,4 +44,4 @@ val template_polymorphic_univs :
   Univ.ContextSet.t ->
   Constr.rel_context ->
   Univ.Universe.t ->
-  Univ.Level.t option list * Univ.LSet.t
+  (Univ.LSet.t * Univ.Level.t option list) option
-- 
cgit v1.2.3