Stop using lbound:Prop in higher layers

checker/checkInductive.ml

@@ -42,7 +42,9 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
         mechanism for template inductive types. *)
       begin match mb.mind_template with
       | None -> Monomorphic_ind_entry
-      | Some ctx -> Template_ind_entry ctx.template_context
+      | Some ctx ->
+        let pseudo_sort_poly = ctx.template_pseudo_sort_poly in
+        Template_ind_entry {univs=ctx.template_context; pseudo_sort_poly}
       end
     | Polymorphic auctx -> Polymorphic_ind_entry (AbstractContext.repr auctx)
   in
@@ -91,11 +93,18 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> assert false
 
+let check_template_pseudo_sort_poly a b =
+  match a, b with
+  | TemplatePseudoSortPoly, TemplatePseudoSortPoly
+  | TemplateUnivOnly, TemplateUnivOnly -> true
+  | (TemplatePseudoSortPoly | TemplateUnivOnly), _ -> false
+
 let check_template ar1 ar2 = match ar1, ar2 with
 | None, None -> true
-| Some ar, Some {template_context; template_param_arguments} ->
+| Some ar, Some {template_context; template_param_arguments; template_pseudo_sort_poly} ->
   List.equal Bool.equal ar.template_param_arguments template_param_arguments &&
-  ContextSet.equal template_context ar.template_context
+  ContextSet.equal template_context ar.template_context &&
+  check_template_pseudo_sort_poly template_pseudo_sort_poly ar.template_pseudo_sort_poly
 | None, Some _ | Some _, None -> false
 
 (* if the generated inductive is squashed the original one must be squashed *)

checker/values.ml

@@ -327,7 +327,7 @@ let v_template_arity =
   v_tuple "template_arity" [|v_sort|]
 
 let v_template_universes =
-  v_tuple "template_universes" [|v_list v_bool;v_context_set|]
+  v_tuple "template_universes" [|v_list v_bool;v_context_set; v_bool|]
 
 let v_primitive =
   v_enum "primitive" 63 (* Number of constructors of the CPrimitives.t type *)

engine/evd.ml

@@ -1211,10 +1211,13 @@ let collapse_sort_variables evd =
   let universes = UState.collapse_sort_variables evd.universes in
   { evd with universes }
 
-let minimize_universes ?lbound evd =
-  let uctx' = UState.collapse_sort_variables evd.universes in
+let minimize_universes ?(collapse_sort_variables=true) evd =
+  let uctx' = if collapse_sort_variables
+    then UState.collapse_sort_variables evd.universes
+    else evd.universes
+  in
   let uctx' = UState.normalize_variables uctx' in
-  let uctx' = UState.minimize ?lbound uctx' in
+  let uctx' = UState.minimize uctx' in
   {evd with universes = uctx'}
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s

engine/evd.mli

@@ -616,8 +616,8 @@ val collapse_sort_variables : evar_map -> evar_map
 
 val fix_undefined_variables : evar_map -> evar_map
 
-(** Universe minimization *)
-val minimize_universes : ?lbound:UGraph.Bound.t -> evar_map -> evar_map
+(** Universe minimization (collapse_sort_variables is true by default) *)
+val minimize_universes : ?collapse_sort_variables:bool -> evar_map -> evar_map
 
 (** Lift [UState.update_sigma_univs] *)
 val update_sigma_univs : UGraph.t -> evar_map -> evar_map

kernel/declarations.mli

@@ -25,13 +25,16 @@ open Constr
     In truly universe polymorphic mode, we always use RegularArity.
 *)
 
+type template_pseudo_sort_poly = TemplatePseudoSortPoly | TemplateUnivOnly
+
 type template_arity = {
   template_level : Sorts.t;
 }
 
 type template_universes = {
   template_param_arguments : bool list;
   template_context : Univ.ContextSet.t;
+  template_pseudo_sort_poly : template_pseudo_sort_poly;
 }
 
 type ('a, 'b) declaration_arity =

kernel/declareops.ml

@@ -49,11 +49,14 @@ let map_decl_arity f g = function
   | TemplateArity a -> TemplateArity (g a)
 
 let hcons_template_arity ar =
-  { template_level = Sorts.hcons ar.template_level; }
+  { template_level = Sorts.hcons ar.template_level;
+  }
 
 let hcons_template_universe ar =
   { template_param_arguments = ar.template_param_arguments;
-    template_context = Univ.hcons_universe_context_set ar.template_context }
+    template_context = Univ.hcons_universe_context_set ar.template_context;
+    template_pseudo_sort_poly = ar.template_pseudo_sort_poly;
+  }
 
 let universes_context = function
   | Monomorphic -> UVars.AbstractContext.empty

kernel/discharge.ml

@@ -183,10 +183,10 @@ let cook_inductive info mib =
   in
   let mind_template = match mib.mind_template with
   | None -> None
-  | Some {template_param_arguments=levels; template_context} ->
+  | Some {template_param_arguments=levels; template_context; template_pseudo_sort_poly} ->
       let sec_levels = List.make (Context.Rel.nhyps (rel_context_of_cooking_cache cache)) false in
       let levels = List.rev_append sec_levels levels in
-      Some {template_param_arguments=levels; template_context}
+      Some {template_param_arguments=levels; template_context; template_pseudo_sort_poly}
   in
   {
     mind_packets;

kernel/entries.mli

@@ -23,7 +23,10 @@ type universes_entry =
 type inductive_universes_entry =
   | Monomorphic_ind_entry
   | Polymorphic_ind_entry of UVars.UContext.t
-  | Template_ind_entry of Univ.ContextSet.t
+  | Template_ind_entry of {
+      univs : Univ.ContextSet.t;
+      pseudo_sort_poly : Declarations.template_pseudo_sort_poly;
+    }
 
 type variance_entry = UVars.Variance.t option array
 

kernel/indTyping.ml

@@ -297,7 +297,7 @@ let get_arity c =
 let get_template univs ~env_params ~env_ar_par ~params entries data =
   match univs with
   | Polymorphic_ind_entry _ | Monomorphic_ind_entry -> None
-  | Template_ind_entry ctx ->
+  | Template_ind_entry {univs=ctx; pseudo_sort_poly} ->
     let entry, sort = match entries, data with
       | [entry], [(_, _, info)] -> entry, info.ind_univ
       | _ -> CErrors.user_err Pp.(str "Template-polymorphism not allowed with mutual inductives.")
@@ -379,7 +379,7 @@ let get_template univs ~env_params ~env_ar_par ~params entries data =
         ~ctors:[entry.mind_entry_lc]
     in
     let params = List.rev_map Option.has_some params in
-    Some { template_param_arguments = params; template_context = ctx }
+    Some { template_param_arguments = params; template_context = ctx; template_pseudo_sort_poly=pseudo_sort_poly }
 
 let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
   if not (List.is_empty univ_info.missing)
@@ -428,10 +428,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   (* universes *)
   let env_univs =
     match mie.mind_entry_universes with
-    | Template_ind_entry ctx ->
+    | Template_ind_entry {univs=ctx; pseudo_sort_poly} ->
+      begin match pseudo_sort_poly with
+      | TemplatePseudoSortPoly ->
         (* For that particular case, we typecheck the inductive in an environment
            where the universes introduced by the definition are only [>= Prop] *)
         Environ.push_floating_context_set ctx env
+      | TemplateUnivOnly -> Environ.push_context_set ~strict:false ctx env
+      end
     | Monomorphic_ind_entry -> env
     | Polymorphic_ind_entry ctx -> push_context ctx env
   in

kernel/inductive.ml

@@ -183,7 +183,7 @@ let make_subst =
   in
   make Univ.Level.Map.empty
 
-let subst_univs_sort subs = function
+let subst_univs_sort (subs, pseudo_sort_poly) = function
 | Sorts.QSort _ -> no_sort_variable ()
 | Sorts.Prop | Sorts.Set | Sorts.SProp as s -> s
 | Sorts.Type u ->
@@ -192,15 +192,18 @@ let subst_univs_sort subs = function
   let supern u n = iterate Universe.super n u in
   let map (u, n) =
     if Level.is_set u then Some (Universe.type0, n)
-    else match Level.Map.find u subs with
-    | TemplateProp ->
+    else match Level.Map.find u subs, pseudo_sort_poly with
+    | TemplateProp, TemplatePseudoSortPoly ->
       if Int.equal n 0 then
         (* This is an instantiation of a template universe by Prop, ignore it *)
         None
       else
         (* Prop + S n actually means Set + S n *)
         Some (Universe.type0, n)
-    | TemplateUniv v -> Some (v,n)
+    | TemplateProp, TemplateUnivOnly ->
+      (* exploit Prop <= Set *)
+      Some (Universe.type0, n)
+    | TemplateUniv v, _ -> Some (v,n)
     | exception Not_found ->
       (* Either an unbound template universe due to missing arguments, or a
          global one appearing in the inductive arity. *)
@@ -242,7 +245,7 @@ let instantiate_template_constraints subst templ =
   let _, cstrs = templ.template_context in
   let fold (u, cst, v) accu =
     (* v is not a local universe by the unbounded from below property *)
-    let u = subst_univs_sort subst (Sorts.sort_of_univ (Universe.make u)) in
+    let u = subst_univs_sort (subst, templ.template_pseudo_sort_poly) (Sorts.sort_of_univ (Universe.make u)) in
     match u with
     | Sorts.QSort _ | Sorts.SProp -> assert false
     | Sorts.Prop -> accu
@@ -264,9 +267,10 @@ let instantiate_template_universes (mib, _mip) args =
   | Some t -> t
   in
   let ctx = List.rev mib.mind_params_ctxt in
-  let subst = make_subst (ctx,templ.template_param_arguments,args) in
+  let subst0 = make_subst (ctx,templ.template_param_arguments,args) in
+  let subst = (subst0,templ.template_pseudo_sort_poly) in
   let ctx = subst_univs_ctx [] subst ctx templ.template_param_arguments in
-  let cstrs = instantiate_template_constraints subst templ in
+  let cstrs = instantiate_template_constraints subst0 templ in
   (cstrs, ctx, subst)
 
 (* Type of an inductive type *)

kernel/inductive.mli

@@ -58,7 +58,7 @@ val instantiate_template_constraints
   -> Univ.Constraints.t
 
 val instantiate_template_universes : mind_specif -> param_univs ->
-  Constraints.t * rel_context * template_univ Univ.Level.Map.t
+  Constraints.t * rel_context * (template_univ Univ.Level.Map.t * template_pseudo_sort_poly)
 
 val constrained_type_of_inductive : mind_specif puniverses -> types constrained
 

pretyping/templateArity.ml

@@ -37,23 +37,29 @@ let get_template_arity env ind ~ctoropt =
       let ctx = List.rev @@ List.skipn (List.length mib.mind_params_ctxt) @@
         List.rev mip.mind_arity_ctxt
       in
-      let template_can_be_prop = match s with
-        | SProp | Prop | Set -> None
-        | QSort _ -> assert false
-        | Type u ->
-          (* if all template levels are instantiated to Prop, do we get Prop? *)
-          let template_levels = Univ.ContextSet.levels template.template_context in
-          if List.exists (fun (u,n) -> n > 0 || not (Univ.Level.Set.mem u template_levels))
-              (Univ.Universe.repr u)
-          then None
-          else
-            (* don't use the qvar for non used univs
-               eg with "Ind (A:Type@{u}) (B:Type@{v}) : Type@{u}"
-               "Ind True nat" should be Prop *)
-            let used_template_levels =
-              Univ.Level.Set.inter template_levels (Univ.Universe.levels u)
-            in
-            Some used_template_levels
+      let template_can_be_prop = match template.template_pseudo_sort_poly with
+        | TemplateUnivOnly -> None
+        | TemplatePseudoSortPoly ->
+          (* we still need to check which levels are used in the conclusion *)
+          match s with
+          | SProp | Prop | Set -> None
+          | QSort _ -> assert false
+          | Type u ->
+            (* if all template levels are instantiated to Prop, do we get Prop?
+               XXX skip this check and trust that only actually pseudo sort poly inductives
+               are declared pseudo sort poly? *)
+            let template_levels = Univ.ContextSet.levels template.template_context in
+            if List.exists (fun (u,n) -> n > 0 || not (Univ.Level.Set.mem u template_levels))
+                (Univ.Universe.repr u)
+            then None
+            else
+              (* don't use the qvar for non used univs
+                 eg with "Ind (A:Type@{u}) (B:Type@{v}) : Type@{u}"
+                 "Ind True nat" should be Prop *)
+              let used_template_levels =
+                Univ.Level.Set.inter template_levels (Univ.Universe.levels u)
+              in
+              Some used_template_levels
       in
       { template_can_be_prop }, IndType (template, EConstr.of_rel_context ctx, s)
     | Some ctor ->

test-suite/output/Inductive.out

@@ -20,7 +20,7 @@ Expands to: Inductive Corelib.Init.Datatypes.option
 Declared in library Corelib.Init.Datatypes, line 202, characters 10-16
 option : Type@{option.u0} -> Type@{max(Set,option.u0)}
 
-option is template universe polymorphic on option.u0
+option is template universe polymorphic on option.u0 (cannot be instantiated to Prop)
 Arguments option A%type_scope
 Expands to: Inductive Corelib.Init.Datatypes.option
 Declared in library Corelib.Init.Datatypes, line 202, characters 10-16

test-suite/output/UnivBinders.out

@@ -256,7 +256,7 @@ Universe inconsistency. Cannot enforce a < a because a = a.
 JMeq :
 forall [A : Type@{JMeq.u0}], A -> forall [B : Type@{JMeq.u1}], B -> Prop
 
-JMeq is template universe polymorphic on JMeq.u0
+JMeq is template universe polymorphic on JMeq.u0 (cannot be instantiated to Prop)
 Arguments JMeq [A]%type_scope x [B]%type_scope _
 Expands to: Inductive UnivBinders.PartialTemplate.JMeq
 Declared in library UnivBinders, line 219, characters 10-14

test-suite/success/Template.v

@@ -231,3 +231,33 @@ Module TemplateNoExtraCsts.
   Polymorphic Definition some@{u|} (A:Type@{u}) (x:A) : opt' A := Some x.
 
 End TemplateNoExtraCsts.
+
+Module BoundedQuality.
+  Inductive dumb' (b:bool) (B : Type) := cons' : B -> (b = true -> dumb' false nat) -> dumb' b B.
+
+  (* dumb' true _ contains a nat *)
+  Fail Check dumb' true True : Prop.
+
+  Check dumb' true nat : Set.
+  Fail Check dumb' true Set : Set.
+  Check dumb' true Set.
+End BoundedQuality.
+
+Module UnminimizedOption.
+  Unset Universe Minimization ToSet.
+  Inductive option A := None | Some (_:A).
+
+  Fail Check option True : Prop.
+  Check option nat : Set.
+  Fail Check option Set : Set.
+  Check option Set : Type.
+End UnminimizedOption.
+
+Module ExplicitOption.
+  Inductive option@{u} (A:Type@{u}) : Type@{u} := None | Some (_:A).
+
+  Fail Check option True : Prop.
+  Check option nat : Set.
+  Fail Check option Set : Set.
+  Check option Set : Type.
+End ExplicitOption.