Controlling typing flags

CHANGES.md

@@ -55,6 +55,9 @@ Vernacular commands
 - Binders for an `Instance` now act more like binders for a `Theorem`.
   Names may not be repeated, and may not overlap with section variable names.
 
+- New commands and attributes to enable/disable guard checking, positivity checking
+  and universes checking (providing a local `-type-in-type`).
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:

checker/values.ml

@@ -229,7 +229,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 

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

@@ -776,7 +776,9 @@ 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 disable using
+      the command :cmd:`Unset Positivity Checking` or the attribute
+      ``assume_positive`` (see :ref:`gallina-attributes`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -1500,7 +1502,7 @@ the following attributes names are recognized:
     (see :ref:`programs`).
 
 ``global``, ``local``
-    Take no value, analogous to the ``Global`` and ``Local`` flags
+    Takes no value, analogous to the ``Global`` and ``Local`` flags
     (see :ref:`controlling-locality-of-commands`).
 
 ``deprecated``
@@ -1533,6 +1535,29 @@ the following attributes names are recognized:
           now foo.
         Abort.
 
+``check_guarded``, ``assume_guarded``
+    Takes no value. Enable/disable the guard checking of fixpoints during a
+    definition (see also :ref:`controlling-typing-flags`). Works with
+    :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`CoFixpoint`, :cmd:`Theorem`
+    (and its variants).
+
+``check_positive``, ``assume_positive``
+    Takes no value. Enable/disable the positivity checking for the declaration
+    of an inductive type or the productivity checking for a coinductive type
+    (see also :ref:`controlling-typing-flags`).
+
+``check_universes``, ``type_in_type``
+    Takes no value. Enable/disable the checking of universes during a definition
+    or the declaration of a (co)inductive type.
+    (see also :ref:`controlling-typing-flags`).
+
+.. example::
+
+   .. coqtop:: all reset
+
+        #[assume_guarded] Fixpoint f (n : nat) : False
+          := f n.
+
 .. [1]
    This is similar to the expression “*entry* :math:`\{` sep *entry*
    :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*

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

@@ -1202,6 +1202,66 @@ scope of their effect. There are four kinds of commands:
   occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
   category.
 
+
+.. _controlling-typing-flags:
+
+Controlling Typing Flags
+----------------------------
+
+.. cmd:: Set Guard Checking
+.. cmd:: Unset Guard Checking
+
+   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 but the decrease is not checked anymore. Unchecked
+   fixpoint are printed by :cmd:`Print Assumptions`.
+
+.. cmd:: Set Positivity Checking
+.. cmd:: Unset Positivity Checking
+
+   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`.
+
+.. cmd:: Set Universes Checking
+.. cmd:: Unset Universes Checking
+
+   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`.
+
+.. cmd:: Print Typing Flags
+
+   Print the status of the three typing flags: check of guard, check of positivity
+   and check of universes.
+
+.. 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
+   well-founded recursion (see :cmd:`Program Fixpoint`).
+
 .. _exposing-constants-to-ocaml-libraries:
 
 Exposing constants to OCaml libraries

kernel/declarations.ml

@@ -63,6 +63,8 @@ type constant_universes =
 type typing_flags = {
   check_guarded : bool; (** 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 *)
   conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
   share_reduction : bool; (** Use by-need reduction algorithm *)

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

@@ -233,6 +233,13 @@ let set_oracle env o =
 let engagement env = env.env_stratification.env_engagement
 let typing_flags env = env.env_typing_flags
 
+let update_check_guarded flags opt =
+  Option.cata (fun b -> {flags with check_guarded = b}) flags opt
+let update_check_positive flags opt =
+  Option.cata (fun b -> {flags with check_positive = b}) flags opt
+let update_check_universes flags opt =
+  Option.cata (fun b -> {flags with check_universes = b}) flags opt
+
 let is_impredicative_set env = 
   match engagement env with
   | ImpredicativeSet -> true

kernel/environ.mli

@@ -93,6 +93,9 @@ val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 val engagement    : env -> engagement
 val typing_flags    : env -> typing_flags
+val update_check_guarded : typing_flags -> bool option -> typing_flags
+val update_check_positive : typing_flags -> bool option -> typing_flags
+val update_check_universes : typing_flags -> bool option -> typing_flags
 val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool

kernel/indtypes.ml

@@ -973,7 +973,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, paramsctxt, inds) = 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 (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_private mie.mind_entry_universes

library/global.ml

@@ -90,6 +90,16 @@ 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_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
+let update_check_guarded = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_guarded = b}
+  | None -> ()
+let update_check_positive = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_positive = b}
+  | None -> ()
+let update_check_universes = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_universes = b}
+  | None -> ()
+
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)

library/global.mli

@@ -32,6 +32,11 @@ val set_engagement : Declarations.engagement -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val typing_flags : unit -> Declarations.typing_flags
 
+(** Changing some typing flags (does nothing if None) *)
+val update_check_guarded : bool option -> unit
+val update_check_positive : bool option -> unit
+val update_check_universes : bool option -> unit
+
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit

printing/printer.ml

@@ -838,6 +838,7 @@ 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 *)
+  | TypeInType of Constant.t (* a which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -911,9 +912,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.")
+          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded kn ->
-          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TypeInType kn ->
+         hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
@@ -995,3 +998,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

@@ -193,6 +193,7 @@ 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 *)
+  | TypeInType of Constant.t (* a which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -208,3 +209,4 @@ 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_typing_flags : Declarations.typing_flags -> Pp.t

test-suite/success/typing_flags.v

@@ -0,0 +1,82 @@
+
+(* Print Typing Flags. *)
+#[type_in_type, assume_guarded] Fixpoint f' (n : nat) : nat := f' n.
+
+#[assume_guarded, local] Fixpoint f (n : nat) : nat.
+Proof.
+  exact (f n).
+(* Print Typing Flags. *)
+Defined.
+
+(* Print Typing Flags. *)
+
+Unset Universes Checking.
+
+(* Print Tables. *)
+(* Test Universes Checking. *)
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+(* Print Typing Flags. *)
+Set Universes Checking.
+
+#[type_in_type] Fixpoint g1 (n : nat) : T.
+Proof.
+  (* Print Typing Flags. *)
+  exact T.
+Defined.
+Set Universes Checking.
+
+Fail Definition g2 (n : nat) : T := T.
+#[type_in_type] Definition g2 (n : nat) : T := T.
+(* Print Typing Flags. *)
+
+Unset Guard Checking.
+Fail #[check_guarded] Definition e := fix e (n : nat) : nat := e n.
+Definition e := fix e (n : nat) : nat := e n.
+Set Guard Checking.
+
+#[assumed_positive] Inductive T :=
+y : (T -> T) -> T.
+
+Unset Positivity Checking.
+Inductive Cor :=
+| Over : Cor
+| Next : ((Cor -> list nat) -> list nat) -> Cor.
+Set Positivity Checking.
+(* Print Typing Flags. *)
+(* Print Assumptions Cor. *)
+
+
+
+#[check_universes, assume_guarded] Definition e2 : nat -> nat.
+Proof.
+  exact (fix e (n : nat) : nat := e n).
+Defined.
+(* Print Typing Flags. *)
+Section b.
+  Unset Universes Checking.
+  Variable T : let t := Type in (t : t).
+  Definition T' := T.
+  (* Print Assumptions T'. *)
+  (* Print Typing Flags. *)
+End b.
+(* Print Typing Flags. *)
+Set Universes Checking.
+(* Print Assumptions T'. *)
+
+(* Unset Universes Checking. *)
+#[type_in_type] Inductive T4  := a : let t := Type in (t : t) -> T4.
+Module b.
+  Unset Guard Checking.
+  Global Unset Universes Checking.
+  (* Disable Type In Type. *)
+  Definition T := let t := Type in (t : t).
+  (* Print Typing Flags. *)
+End b.
+(* Print Typing Flags. *)
+Import b.
+(* Print Typing Flags. *)
+(* About T. *)
+(* Print Assumptions T. *)

vernac/assumptions.ml

@@ -312,7 +312,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
       in
-    if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
+      let accu =
+        if cb.const_typing_flags.check_universes then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (TypeInType kn, l)) Constr.mkProp accu
+      in
+    if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu
@@ -326,7 +332,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
       let mind = lookup_mind m in
-      if mind.mind_typing_flags.check_guarded then
+      if mind.mind_typing_flags.check_positive then
         accu
       else
         let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in

vernac/attributes.ml

@@ -73,6 +73,9 @@ let mk_deprecation ?(since=None) ?(note=None) () =
 
 type t = {
   locality : bool option;
+  (* check_guard : bool option; *)
+  (* check_positivity : bool option; *)
+  (* check_universes : bool option; *)
   polymorphic : bool;
   template : bool option;
   program : bool;
@@ -134,6 +137,12 @@ let program = program_opt >>= function
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
+let check_guard = bool_attribute ~name:"Check Guard" ~on:"check_guarded" ~off:"assume_guarded"
+
+let check_positivity = bool_attribute ~name:"Check Positivity" ~on:"check_positive" ~off:"assume_positive"
+
+let check_universes = bool_attribute ~name:"Check Universes" ~on:"check_universes" ~off:"type_in_type"
+
 let warn_unqualified_univ_attr =
   CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated"
     (fun key -> Pp.(str "Attribute " ++ str key ++
@@ -205,6 +214,10 @@ let attributes_of_flags f =
     parse (locality ++ deprecation ++ universe_poly_template ++ program) f
   in
   { polymorphic; program; locality; template; deprecated }
+  (* let (((((locality, check_guard), check_positivity), check_universes), deprecated), (polymorphic, template)), program = *)
+  (*   parse (locality ++ check_guard ++ check_positivity ++ check_universes ++ deprecation ++ universe_poly_template ++ program) f *)
+  (* in *)
+  (* { locality; check_guard; check_positivity; check_universes; deprecated; polymorphic; template; program } *)
 
 let only_locality atts = parse locality atts