Flag to disable cumulativity of Prop

checker/checkFlags.ml

@@ -27,6 +27,7 @@ let set_local_flags flags env =
     indices_matter = envflags.indices_matter;
     impredicative_set = envflags.impredicative_set;
     sprop_allowed = envflags.sprop_allowed;
+    cumulative_prop = envflags.cumulative_prop;
   }
   in
   Environ.set_typing_flags flags env

checker/values.ml

@@ -249,7 +249,7 @@ let v_typing_flags =
   v_tuple "typing_flags"
     [|v_bool; v_bool; v_bool;
       v_oracle; v_bool; v_bool;
-      v_bool; v_bool; v_bool; v_bool; v_bool|]
+      v_bool; v_bool; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 1 [|[|v_abs_context|]|]
 

doc/changelog/01-kernel/18828-prop-cumul.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  :flag:`Cumulative Prop` may be used to disable cumulativity of `Prop`
+  (`#18828 <https://github.com/coq/coq/pull/18828>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1097,6 +1097,12 @@ Controlling Typing Flags
    This :term:`boolean attribute` is similar to the :flag:`Universe Checking` flag, but on a per-declaration basis.
    Disable universe checking locally with ``bypass_check(universes)``.
 
+.. flag:: Cumulative Prop
+
+   This :term:`flag` can be used to control whether `Prop` is in
+   cumulativity with the predicative universes (`Set` and instantiations of `Type`).
+   It is on by default.
+
 .. cmd:: Print Typing Flags
 
    Print the status of the three typing flags: guard checking, positivity checking

doc/tools/docgram/common.edit_mlg

@@ -719,6 +719,11 @@ is_module_type: [
 | WITH ":=" LIST1 module_type_inl SEP "<+"
 ]
 
+setting_name: [
+| REPLACE LIST1 [ IDENT | "Prop" ]
+| WITH LIST1 IDENT
+]
+
 gallina_ext: [
 | REPLACE "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | WITH "Arguments" smart_global LIST0 arg_specs    LIST0 [  "," LIST0 implicits_alt ]                OPT [ ":" LIST1 args_modifier SEP "," ]

doc/tools/docgram/fullGrammar

@@ -1469,7 +1469,7 @@ table_value: [
 ]
 
 setting_name: [
-| LIST1 IDENT
+| LIST1 [ IDENT | "Prop" ]
 ]
 
 ne_in_or_out_modules: [

engine/uState.ml

@@ -41,7 +41,7 @@ module QState : sig
   val union : fail:(t -> Quality.t -> Quality.t -> t) -> t -> t -> t
   val add : check_fresh:bool -> named:bool -> elt -> t -> t
   val repr : elt -> t -> Quality.t
-  val unify_quality : fail:(unit -> t) -> Conversion.conv_pb -> Quality.t -> Quality.t -> t -> t
+  val unify_quality : fail:(unit -> t) -> cumulative_prop:bool -> Conversion.conv_pb -> Quality.t -> Quality.t -> t -> t
   val is_above_prop : elt -> t -> bool
   val undefined : t -> QVar.Set.t
   val collapse : t -> t
@@ -104,11 +104,11 @@ let set_above_prop q m =
   if QSet.mem q m.named then None
   else Some { named = m.named; qmap = m.qmap; above = QSet.add q m.above }
 
-let unify_quality ~fail c q1 q2 local = match q1, q2 with
+let unify_quality ~fail ~cumulative_prop c q1 q2 local = match q1, q2 with
 | QConstant QType, QConstant QType
 | QConstant QProp, QConstant QProp
 | QConstant QSProp, QConstant QSProp -> local
-| QConstant QProp, QVar q when c == Conversion.CUMUL ->
+| QConstant QProp, QVar q when c == Conversion.CUMUL && cumulative_prop ->
   begin match set_above_prop q local with
   | Some local -> local
   | None -> fail ()
@@ -129,7 +129,7 @@ let unify_quality ~fail c q1 q2 local = match q1, q2 with
 | (QConstant QProp, QConstant QType) ->
   begin match c with
   | CONV -> fail ()
-  | CUMUL -> local
+  | CUMUL -> if cumulative_prop then local else fail ()
   end
 | (QConstant QSProp, QConstant (QType | QProp)) -> fail ()
 | (QConstant QProp, QConstant QSProp) -> fail ()
@@ -159,7 +159,8 @@ let union ~fail s1 s2 =
   let s = { named = QSet.union s1.named s2.named; qmap; above } in
   List.fold_left (fun s (q1,q2) ->
       let q1 = nf_quality s q1 and q2 = nf_quality s q2 in
-      unify_quality ~fail:(fun () -> fail s q1 q2) CONV q1 q2 s)
+      (* cumulative_prop doesn't matter with CONV *)
+      unify_quality ~fail:(fun () -> fail s q1 q2) CONV ~cumulative_prop:false q1 q2 s)
     s
     extra
 
@@ -500,7 +501,7 @@ let unify_quality univs c s1 s2 l =
     else sort_inconsistency (get_constraint c) s1 s2
   in
   { l with
-    local_sorts  = QState.unify_quality ~fail
+    local_sorts  = QState.unify_quality ~fail ~cumulative_prop:(UGraph.cumulative_prop univs)
         c (Sorts.quality s1) (Sorts.quality s2) l.local_sorts;
   }
 

kernel/declarations.mli

@@ -95,6 +95,8 @@ type typing_flags = {
   sprop_allowed: bool;
   (** If [false], error when encountering [SProp]. *)
 
+  cumulative_prop: bool;
+
   allow_uip: bool;
   (** Allow definitional UIP (breaks termination) *)
 

kernel/declareops.ml

@@ -28,6 +28,7 @@ let safe_flags oracle = {
   indices_matter = true;
   impredicative_set = false;
   sprop_allowed = true;
+  cumulative_prop = true;
   allow_uip = false;
 }
 

kernel/environ.ml

@@ -504,6 +504,7 @@ let same_flags {
      enable_native_compiler;
      impredicative_set;
      sprop_allowed;
+     cumulative_prop;
      allow_uip;
   } alt =
   check_guarded == alt.check_guarded &&
@@ -516,16 +517,20 @@ let same_flags {
   enable_native_compiler == alt.enable_native_compiler &&
   impredicative_set == alt.impredicative_set &&
   sprop_allowed == alt.sprop_allowed &&
+  cumulative_prop == alt.cumulative_prop &&
   allow_uip == alt.allow_uip
 [@warning "+9"]
 
 let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
+let set_cumulative_prop b = map_universes (UGraph.set_cumulative_prop b)
+
 let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
   else
     let env = { env with env_typing_flags = c } in
     let env = set_type_in_type (not c.check_universes) env in
+    let env = set_cumulative_prop c.cumulative_prop env in
     env
 
 let update_typing_flags ?typing_flags env =

kernel/indTyping.ml

@@ -358,9 +358,10 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   let env_univs =
     match mie.mind_entry_universes with
     | Template_ind_entry ctx ->
-        (* 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
+      (* For that particular case, we typecheck the inductive in an environment
+         where the universes introduced by the definition are only [>= Prop] *)
+      if env.env_typing_flags.cumulative_prop then Environ.push_floating_context_set ctx env
+      else push_context_set ~strict:false ctx env
     | Monomorphic_ind_entry -> env
     | Polymorphic_ind_entry ctx -> push_context ctx env
   in

kernel/uGraph.ml

@@ -28,6 +28,7 @@ module G = AcyclicGraph.Make(struct
 type t = {
   graph: G.t;
   type_in_type : bool;
+  cumulative_prop : bool;
 }
 
 (* Universe inconsistency: error raised when trying to enforce a relation
@@ -50,6 +51,10 @@ let set_type_in_type b g = {g with type_in_type=b}
 
 let type_in_type g = g.type_in_type
 
+let set_cumulative_prop b g = {g with cumulative_prop=b}
+
+let cumulative_prop g = g.cumulative_prop
+
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -75,7 +80,7 @@ let check_eq g u v =
 let check_eq_level g u v =
   u == v || type_in_type g || G.check_eq g.graph u v
 
-let empty_universes = {graph=G.empty; type_in_type=false}
+let empty_universes = {graph=G.empty; type_in_type=false; cumulative_prop=true}
 
 let initial_universes =
   let big_rank = 1000000 in
@@ -109,7 +114,7 @@ let enforce_constraint cst g = match enforce_constraint0 cst g with
 
 let merge_constraints csts g = Constraints.fold enforce_constraint csts g
 
-let check_constraint { graph = g; type_in_type } (u,d,v) =
+let check_constraint { graph = g; type_in_type; cumulative_prop=__; } (u,d,v) =
   type_in_type
   || match d with
   | Le -> G.check_leq g u v
@@ -168,6 +173,8 @@ let add_universe u ~lbound ~strict g = match lbound with
   let d = if strict then Lt else Le in
   enforce_constraint (Level.set, d, u) { g with graph }
 | Bound.Prop ->
+  if not g.cumulative_prop
+  then CErrors.anomaly Pp.(str "add_universe lbound=Prop when not cumulative Prop");
   (* Do not actually add any constraint. This is a hack for template. *)
   { g with graph = G.add u g.graph }
 
@@ -237,7 +244,7 @@ let check_leq_sort ugraph s1 s2 = match s1, s2 with
 | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> true
 | (SProp, _) -> type_in_type ugraph
 | (Prop, SProp) -> type_in_type ugraph
-| (Prop, (Set | Type _)) -> true
+| (Prop, (Set | Type _)) -> type_in_type ugraph || cumulative_prop ugraph
 | (Prop, QSort _) -> false
 | (_, (SProp | Prop)) -> type_in_type ugraph
 | (Type _ | Set), (Type _ | Set) ->

kernel/uGraph.mli

@@ -16,13 +16,17 @@ type t
 
 val set_type_in_type : bool -> t -> t
 
+val set_cumulative_prop : bool -> t -> t
+
 (** When [type_in_type], functions adding constraints do not fail and
    may instead ignore inconsistent constraints.
 
     Checking functions such as [check_leq] always return [true].
 *)
 val type_in_type : t -> bool
 
+val cumulative_prop : t -> bool
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 val check_leq : Universe.t check_function

library/global.ml

@@ -86,13 +86,16 @@ let push_section_context c = globalize0 (Safe_typing.push_section_context c)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set ~strict c = globalize0 (Safe_typing.push_context_set ~strict c)
 
+let typing_flags () = Environ.typing_flags (env ())
+
 let set_impredicative_set c = globalize0 (Safe_typing.set_impredicative_set c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
 let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
 let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
-let typing_flags () = Environ.typing_flags (env ())
+let set_cumulative_prop c =
+  globalize0 (Safe_typing.set_typing_flags {(typing_flags()) with cumulative_prop = c})
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let set_rewrite_rules_allowed b = globalize0 (Safe_typing.set_rewrite_rules_allowed b)

library/global.mli

@@ -34,6 +34,7 @@ val set_typing_flags : typing_flags -> unit
 val set_check_guarded : bool -> unit
 val set_check_positive : bool -> unit
 val set_check_universes : bool -> unit
+val set_cumulative_prop : bool -> unit
 val typing_flags : unit -> typing_flags
 val set_allow_sprop : bool -> unit
 val sprop_allowed : unit -> bool

pretyping/coercion.ml

@@ -216,7 +216,8 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
     | Sort s, Sort s' ->
       (match ESorts.kind sigma s, ESorts.kind sigma s' with
        | Prop, Prop | Set, Set -> sigma, None
-       | (Prop | Set), Type _ -> sigma, None
+       | Prop, Type _ when UGraph.cumulative_prop (Evd.universes sigma) -> sigma, None
+       | Set, Type _ -> sigma, None
        | Type x, Type y when Univ.Universe.equal x y -> sigma, None (* false *)
        | _ -> subco sigma)
     | Prod (name, a, b), Prod (name', a', b') ->

printing/printer.ml

@@ -1184,6 +1184,7 @@ let pr_typing_flags flags =
   str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
   ++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
   ++ str "check_universes: " ++ bool flags.check_universes ++ fnl ()
+  ++ str "cumulative Prop:" ++ bool flags.cumulative_prop ++ fnl ()
   ++ str "definitional uip: " ++ bool flags.allow_uip
 
 module Debug =

test-suite/success/NonCumulativeProp.v

@@ -0,0 +1,16 @@
+Unset Cumulative Prop.
+
+Fail Check fun P:Prop => P:Set.
+
+Inductive Box (A:Prop) : Set := box (_:A).
+
+Check Box True.
+
+(* template can't be instantiated with Prop *)
+Inductive TBox (A:Type) : Type := tbox (_:A).
+
+Check TBox nat : Set.
+
+Check TBox Set.
+
+Fail Check TBox True.

vernac/comInductive.ml

@@ -620,7 +620,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let ninds = List.length indl in
 
   (* In case of template polymorphism, we need to compute more constraints *)
-  let unconstrained_sorts = not poly in
+  let unconstrained_sorts = not poly && env0.env_typing_flags.cumulative_prop in
 
   let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
     interp_params ~unconstrained_sorts env0 udecl uparamsl paramsl

vernac/g_vernac.mlg

@@ -1204,7 +1204,7 @@ GRAMMAR EXTEND Gram
       | s  = STRING   -> { Goptions.StringRefValue s } ] ]
   ;
   setting_name:
-    [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
+    [ [ fl = LIST1 [ x = IDENT -> { x } | "Prop" -> { "Prop" } ] -> { fl } ]]
   ;
   ne_in_or_out_modules:
     [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }

vernac/record.ml

@@ -217,7 +217,7 @@ let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
     List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
-  let unconstrained_sorts = not poly && not def && is_template in
+  let unconstrained_sorts = not poly && not def && is_template && env0.env_typing_flags.cumulative_prop in
   let sigma, decl, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl in
   let () = List.iter check_parameters_must_be_named ps in
   let sigma, (impls_env, ((_env1,newps), imps)) =

vernac/vernacentries.ml

@@ -1842,6 +1842,14 @@ let () =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
       optwrite = (fun b -> Global.set_check_universes b) }
 
+let () =
+  declare_bool_option
+    { optstage = Summary.Stage.Interp;
+      optdepr  = None;
+      optkey   = ["Cumulative"; "Prop"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.cumulative_prop);
+      optwrite = (fun b -> Global.set_cumulative_prop b) }
+
 let () =
   declare_bool_option
     { optstage = Summary.Stage.Interp;