Controlling typing flags with commands (no attribute)

checker/checkInductive.ml

@@ -142,8 +142,12 @@ let check_inductive env mind mb =
         mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
-    (* Locally set the oracle for further typechecking *)
-    let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+    (* Locally set typing flags for further typechecking *)
+    let mb_flags = mb.mind_typing_flags in
+    let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
+                                                                  check_positive = mb_flags.check_positive;
+                                                                  check_universes = mb_flags.check_universes;
+                                                                  conv_oracle = mb_flags.conv_oracle} env in
     Indtypes.check_inductive env mind entry
   in
   let check = check mind in

checker/check_stat.ml

@@ -31,14 +31,31 @@ let pr_engagement env =
     | PredicativeSet -> str "Theory: Set is predicative"
   end
 
-let is_ax _ cb = not (Declareops.constant_has_body cb)
 
-let pr_ax env =
-  let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
+let pr_assumptions ass axs =
   if axs = [] then
-    str "Axioms: <none>"
+    str ass ++ str ": <none>"
   else
-    hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
+    hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
+
+let pr_axioms env =
+  let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
+  pr_assumptions "Axioms" csts
+
+let pr_type_in_type env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on type-in-type" csts
+
+let pr_unguarded env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
+
+let pr_nonpositive env =
+  let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
+  pr_assumptions "Inductives whose positivity is assumed" inds
+
 
 let print_context env =
   if !output_context then begin
@@ -47,7 +64,10 @@ let print_context env =
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax env)));
+      str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_nonpositive env)))
   end
 
 let stats env =

checker/mod_checking.ml

@@ -17,9 +17,12 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  (* Locally set the oracle for further typechecking *)
-  let oracle = env.env_typing_flags.conv_oracle in
-  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;
+                                                      check_universes = cb_flags.check_universes;
+                                                      conv_oracle = cb_flags.conv_oracle} env in
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
@@ -57,8 +60,8 @@ let check_constant_declaration env kn cb =
     if poly then add_constant kn cb env
     else add_constant kn cb env'
   in
-  (* Reset the value of the oracle *)
-  Environ.set_oracle env oracle
+  (* Reset the value of the typing flags *)
+  Environ.set_typing_flags orig_flags env
 
 (** {6 Checking modules } *)
 

checker/values.ml

@@ -219,7 +219,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 

doc/changelog/07-commands-and-options/10291-typing-flags.rst

@@ -0,0 +1,4 @@
+- Adding unsafe commands to enable/disable guard checking, positivity checking
+  and universes checking (providing a local `-type-in-type`).
+  See :ref:`controlling-typing-flags`.
+  (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier).

doc/sphinx/language/gallina-specification-language.rst

@@ -778,7 +778,8 @@ Simple inductive types
 
       The types of the constructors have to satisfy a *positivity condition*
       (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition.
+      the inductive definition. The positivity checking can be disabled using
+      the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 

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

@@ -1204,6 +1204,79 @@ Controlling the locality of commands
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
+.. _controlling-typing-flags:
+
+Controlling Typing Flags
+----------------------------
+
+.. flag:: Guard Checking
+
+   This option can be used to enable/disable the guard checking of
+   fixpoints. Warning: this can break the consistency of the system, use at your
+   own risk. Decreasing argument can still be specified: the decrease is not checked
+   anymore but it still affects the reduction of the term. Unchecked fixpoints are
+   printed by :cmd:`Print Assumptions`.
+
+.. flag:: Positivity Checking
+
+   This option can be used to enable/disable the positivity checking of inductive
+   types and the productivity checking of coinductive types. Warning: this can
+   break the consistency of the system, use at your own risk. Unchecked
+   (co)inductive types are printed by :cmd:`Print Assumptions`.
+
+.. flag:: Universe Checking
+
+   This option can be used to enable/disable the checking of universes, providing a
+   form of "type in type".  Warning: this breaks the consistency of the system, use
+   at your own risk.  Constants relying on "type in type" are printed by
+   :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
+   argument (see :ref:`command-line-options`).
+
+.. cmd:: Print Typing Flags
+
+   Print the status of the three typing flags: guard checking, positivity checking
+   and universe checking.
+
+.. example::
+
+   .. coqtop:: all reset
+
+        Unset Guard Checking.
+
+        Print Typing Flags.
+
+        Fixpoint f (n : nat) : False
+          := f n.
+
+        Fixpoint ackermann (m n : nat) {struct m} : nat :=
+          match m with
+          | 0 => S n
+          | S m =>
+            match n with
+            | 0 => ackermann m 1
+            | S n => ackermann m (ackermann (S m) n)
+            end
+          end.
+
+        Print Assumptions ackermann.
+
+   Note that the proper way to define the Ackermann function is to use
+   an inner fixpoint:
+
+   .. coqtop:: all reset
+
+        Fixpoint ack m :=
+          fix ackm n :=
+          match m with
+          | 0 => S n
+          | S m' =>
+            match n with
+            | 0 => ack m' 1
+            | S n' => ack m' (ackm n')
+            end
+          end.
+
+
 .. _internal-registration-commands:
 
 Internal registration commands

kernel/declarations.ml

@@ -66,6 +66,10 @@ type typing_flags = {
   (** If [false] then fixed points and co-fixed points are assumed to
       be total. *)
 
+  check_positive : bool;
+  (** If [false] then inductive types are assumed positive and co-inductive
+      types are assumed productive. *)
+
   check_universes : bool;
   (** If [false] universe constraints are not checked *)
 

kernel/declareops.ml

@@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration
 
 let safe_flags oracle = {
   check_guarded = true;
+  check_positive = true;
   check_universes = true;
   conv_oracle = oracle;
   share_reduction = true;

kernel/environ.ml

@@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt =
 let fold_constants f env acc =
   Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
 
+let fold_inductives f env acc =
+  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
@@ -418,6 +421,7 @@ let set_engagement c env = (* Unsafe *)
 (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
 let same_flags {
      check_guarded;
+     check_positive;
      check_universes;
      conv_oracle;
      indices_matter;
@@ -426,6 +430,7 @@ let same_flags {
      enable_native_compiler;
   } alt =
   check_guarded == alt.check_guarded &&
+  check_positive == alt.check_positive &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
   indices_matter == alt.indices_matter &&

kernel/environ.mli

@@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
 val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)

kernel/indtypes.ml

@@ -546,7 +546,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let chkpos = (Environ.typing_flags env).check_guarded in
+  let chkpos = (Environ.typing_flags env).check_positive in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
       mie.mind_entry_inds
   in

kernel/safe_typing.ml

@@ -194,6 +194,18 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_check_guarded b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_guarded = b } senv
+
+let set_check_positive b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_positive = b } senv
+
+let set_check_universes b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_universes = b } senv
+
 let set_indices_matter indices_matter senv =
   set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
 

kernel/safe_typing.mli

@@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0
 val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
+val set_check_guarded : bool -> safe_transformer0
+val set_check_positive : bool -> safe_transformer0
+val set_check_universes : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
 val make_sprop_cumulative : safe_transformer0

library/global.ml

@@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let set_engagement c = globalize0 (Safe_typing.set_engagement 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 make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)

library/global.mli

@@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context
 val set_engagement : Declarations.engagement -> unit
 val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val set_check_guarded : bool -> unit
+val set_check_positive : bool -> unit
+val set_check_universes : bool -> unit
 val typing_flags : unit -> Declarations.typing_flags
 val make_sprop_cumulative : unit -> unit
 val set_allow_sprop : bool -> unit

printing/printer.ml

@@ -853,7 +853,8 @@ let pr_goal_emacs ~proof gid sid =
 type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -873,7 +874,7 @@ struct
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
-        Constant.CanOrd.compare k1 k2
+        GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
     | _ -> -1
@@ -903,14 +904,20 @@ let pr_assumptionset env sigma s =
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
-        (* FIXME? *)
-        let mp,lab = Constant.repr2 kn in
-        str (ModPath.to_string mp) ++ str "." ++ Label.print lab
+        Names.Constant.print kn
+    in
+    let safe_pr_global env gr =
+      try pr_global_env (Termops.vars_of_env env) gr
+      with Not_found ->
+        let open GlobRef in match gr with
+        | VarRef id -> Id.print id
+        | ConstRef con -> Constant.print con
+        | IndRef (mind,_) -> MutInd.print mind
+        | ConstructRef _ -> assert false
     in
     let safe_pr_inductive env kn =
       try pr_inductive env (kn,0)
       with Not_found ->
-        (* FIXME? *)
         MutInd.print kn
     in
     let safe_pr_ltype env sigma typ =
@@ -927,9 +934,11 @@ let pr_assumptionset env sigma s =
       | Constant kn ->
           safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
-          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
-      | Guarded kn ->
-          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
+      | Guarded gr ->
+          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TypeInType gr ->
+         hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
@@ -1003,3 +1012,8 @@ let print_and_diff oldp newp =
         pr_open_subgoals ~proof
     in
     Feedback.msg_notice output;;
+
+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

printing/printer.mli

@@ -191,7 +191,8 @@ val print_and_diff : Proof.t option -> Proof.t option -> unit
 type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -207,3 +208,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
+
+val pr_typing_flags : Declarations.typing_flags -> Pp.t

tactics/declare.ml

@@ -246,7 +246,7 @@ let get_roles export eff =
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
-  not (flags.check_universes && flags.check_guarded)
+  not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 let define_constant ~side_effect ~name cd =
   let open Proof_global in