Report check_eliminations bypasses in Print Assumptions and rocqchk

checker/check_stat.ml

@@ -45,6 +45,14 @@ let pr_type_in_type env =
   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
 
+(* Kept out of the report when empty: this flag has no vernacular setter and
+   should stay obscure (see #22294 discussion). *)
+let pr_unchecked_eliminations env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_eliminations 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_eliminations then MutInd.to_string c :: acc else acc) env csts in
+  if csts = [] then mt ()
+  else str "* " ++ hov 0 (pr_assumptions "Constants/Inductives relying on unchecked sort eliminations" csts ++ fnl()) ++ fnl()
+
 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
@@ -73,6 +81,7 @@ let print_context env opac = match opac with
     str "* " ++ hov 0 (pr_rewrite_rules env ++ fnl()) ++ fnl() ++
     str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++
     str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
+    pr_unchecked_eliminations env ++
     str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
     str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++
     str "* " ++ hov 0 (pr_indices_matter env ++ fnl()))

doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst

@@ -0,0 +1,10 @@
+- **Added:**
+  :cmd:`Print Assumptions` and the checker (``rocqchk``) now report
+  inductive types and constants whose sort elimination constraints were
+  not checked (typing flag ``check_eliminations = false``), which was
+  previously silently ignored, and :cmd:`Print Typing Flags` now also
+  displays that flag when it has been disabled. The flag has no vernacular setter by design; it can
+  only be disabled from a plugin (via ``Global.set_typing_flags``), as
+  done for instance by ``rocq-lean-import``
+  (`#22294 <https://github.com/rocq-prover/rocq/pull/22294>`_,
+  by Jason Gross).

printing/printer.ml

@@ -621,6 +621,7 @@ type axiom =
   | Positive of MutInd.t
   | Guarded of GlobRef.t
   | TypeInType of GlobRef.t
+  | UncheckedEliminations of GlobRef.t
   | UIP of MutInd.t
   | IndicesNotMattering of MutInd.t
 
@@ -644,7 +645,8 @@ struct
     | IndicesNotMattering m1, IndicesNotMattering m2 ->
       MutInd.UserOrd.compare m1 m2
     | Guarded k1 , Guarded k2
-    | TypeInType k1, TypeInType k2 ->
+    | TypeInType k1, TypeInType k2
+    | UncheckedEliminations k1, UncheckedEliminations k2 ->
       GlobRef.UserOrd.compare k1 k2
     | Constant _, _ -> -1
     | _, Constant _ -> 1
@@ -654,6 +656,8 @@ struct
     | _, Guarded _ -> 1
     | TypeInType _, _ -> -1
     | _, TypeInType _ -> 1
+    | UncheckedEliminations _, _ -> -1
+    | _, UncheckedEliminations _ -> 1
     | UIP _, _ -> -1
     | _, UIP _ -> 1
 
@@ -678,6 +682,7 @@ type theory_assumptions = {
   has_impredicative_set : bool;
   has_rewrite_rules : bool;
   has_type_in_type : bool;
+  has_unchecked_eliminations : bool;
 }
 
 let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s =
@@ -694,6 +699,7 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s =
   let show_theory_impredicative_set = (print_all && theory_info.has_impredicative_set) || is_impredicative_set env in
   let show_theory_rewrite_rules = (print_all && theory_info.has_rewrite_rules) || rewrite_rules_allowed env in
   let show_theory_type_in_type = (print_all && theory_info.has_type_in_type) || type_in_type env in
+  let show_theory_unchecked_eliminations = (print_all && theory_info.has_unchecked_eliminations) || ignore_elim_constraints env in
   if ContextObjectMap.is_empty s &&
        not show_theory_rewrite_rules &&
        not show_theory_impredicative_set then
@@ -737,6 +743,8 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s =
           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.")
+      | UncheckedEliminations gr ->
+          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on unchecked sort eliminations.")
       | UIP mind ->
           hov 2 (safe_pr_inductive env mind ++ spc () ++ strbrk"relies on definitional UIP.")
       | IndicesNotMattering mind ->
@@ -790,6 +798,11 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s =
         str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
       else theory
     in
+    let theory =
+      if show_theory_unchecked_eliminations then
+        str "Sort elimination constraints are not checked (logic is inconsistent)" :: theory
+      else theory
+    in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -811,6 +824,10 @@ 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 ()
+  (* shown only when disabled: this flag has no vernacular setter and should
+     stay obscure (see #22294 discussion) *)
+  ++ (if flags.check_eliminations then mt ()
+      else str "check_eliminations: " ++ bool flags.check_eliminations ++ fnl ())
   ++ str "definitional uip: " ++ bool flags.allow_uip
 
 module Debug =

printing/printer.mli

@@ -234,6 +234,7 @@ type axiom =
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | 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 *)
+  | UncheckedEliminations of GlobRef.t (* a constant or inductive whose sort elimination constraints were not checked *)
   | UIP of MutInd.t (* An inductive using the special reduction rule. *)
   | IndicesNotMattering of MutInd.t (* An inductive relying on indices not mattering. *)
 
@@ -251,6 +252,7 @@ type theory_assumptions = {
   has_impredicative_set : bool;
   has_rewrite_rules : bool;
   has_type_in_type : bool;
+  has_unchecked_eliminations : bool;
 }
 
 val pr_assumptionset : ?flags:PrintingFlags.t ->

test-suite/misc/unchecked-eliminations.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+
+# There is intentionally no vernacular setter for the [check_eliminations]
+# typing flag. This test builds a tiny plugin that toggles it via
+# [Global.set_typing_flags] (the way rocq-lean-import does), declares a
+# squashed Prop inductive with a large elimination while the flag is off, and
+# checks that both [Print Assumptions] and [rocq check] report it.
+
+set -ex
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+export LC_ALL=C
+
+cd misc/unchecked-eliminations/
+
+rocq makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/elim_flag_plugin.cmxs
+
+# Compile the .v, capturing the Print Assumptions / Print Typing Flags output.
+rocq c -I src -Q theories UncheckedElim theories/unchecked.v 2>&1 | tee log
+
+# checked_or (declared with the flag on) must NOT be reported.
+# Anchor at line start so this does not match "unchecked_or".
+grep -q "^checked_or relies on unchecked sort eliminations" log && {
+  >&2 echo "checked_or should not rely on unchecked eliminations"
+  exit 1
+}
+
+# unchecked_or and its constructors (declared with the flag off) must be
+# reported as relying on unchecked sort eliminations.
+grep -q "^unchecked_or relies on unchecked sort eliminations" log
+grep -q "^unchecked_l relies on unchecked sort eliminations" log
+grep -q "^unchecked_r relies on unchecked sort eliminations" log
+
+# The theory summary line appears under Set Printing All Assumptions.
+grep -q "Sort elimination constraints are not checked (logic is inconsistent)" log
+
+# Print Typing Flags reports the flag only while it is disabled; the final
+# Print Typing Flags (flag restored) must not mention it.
+grep -q "check_eliminations: false" log
+grep -q "check_eliminations: true" log && {
+  >&2 echo "check_eliminations should not be shown when at its default"
+  exit 1
+}
+
+# rocq check must report the inductive in its context summary.
+rocq check -Q theories UncheckedElim -o -silent -norec UncheckedElim.unchecked 2>&1 | tee chklog
+
+grep -q "Constants/Inductives relying on unchecked sort eliminations" chklog
+grep -q "UncheckedElim.unchecked.unchecked_or" chklog

test-suite/misc/unchecked-eliminations/.gitignore

@@ -0,0 +1,4 @@
+/Makefile*
+/log
+/chklog
+/src/elimFlag.ml

test-suite/misc/unchecked-eliminations/_CoqProject

@@ -0,0 +1,9 @@
+src/META.coq-test-suite
+-Q theories UncheckedElim
+-I src
+
+src/elimFlag.mlg
+src/elimFlagImpl.ml
+src/elimFlagImpl.mli
+src/elim_flag_plugin.mlpack
+theories/unchecked.v

test-suite/misc/unchecked-eliminations/src/META.coq-test-suite

@@ -0,0 +1,11 @@
+package "elim_flag" (
+    directory = "."
+    version = "dev"
+    description = "A test plugin toggling the check_eliminations typing flag"
+    requires = "rocq-runtime.plugins.ltac"
+    archive(byte) = "elim_flag_plugin.cma"
+    archive(native) = "elim_flag_plugin.cmxa"
+    plugin(byte) = "elim_flag_plugin.cma"
+    plugin(native) = "elim_flag_plugin.cmxs"
+)
+directory = "."

test-suite/misc/unchecked-eliminations/src/elimFlag.mlg

@@ -0,0 +1,10 @@
+{
+open ElimFlagImpl
+}
+
+DECLARE PLUGIN "coq-test-suite.elim_flag"
+
+VERNAC COMMAND EXTEND ElimChecking CLASSIFIED AS SIDEFF
+| [ "Unset" "Test" "Elimination" "Checking" ] -> { set_elimination_checking false }
+| [ "Set" "Test" "Elimination" "Checking" ] -> { set_elimination_checking true }
+END

test-suite/misc/unchecked-eliminations/src/elimFlagImpl.ml

@@ -0,0 +1,8 @@
+(* There is intentionally no vernacular setter for [check_eliminations]:
+   this test plugin toggles it directly, the way plugins such as
+   rocq-lean-import do, so that the reporting of unchecked sort eliminations
+   by Print Assumptions and rocqchk can be exercised. *)
+
+let set_elimination_checking b =
+  let flags = Global.typing_flags () in
+  Global.set_typing_flags { flags with Declarations.check_eliminations = b }

test-suite/misc/unchecked-eliminations/src/elimFlagImpl.mli

@@ -0,0 +1,2 @@
+
+val set_elimination_checking : bool -> unit

test-suite/misc/unchecked-eliminations/src/elim_flag_plugin.mlpack

@@ -0,0 +1,2 @@
+ElimFlagImpl
+ElimFlag

test-suite/misc/unchecked-eliminations/theories/unchecked.v

@@ -0,0 +1,42 @@
+Declare ML Module "coq-test-suite.elim_flag".
+
+(* With elimination checking on, the large elimination below is squashed. *)
+Inductive checked_or (A B : Prop) : Prop :=
+| checked_l : A -> checked_or A B
+| checked_r : B -> checked_or A B.
+
+Fail Definition checked_large (A B : Prop) (H : checked_or A B) : Type :=
+  match H with
+  | checked_l _ _ _ => nat
+  | checked_r _ _ _ => bool
+  end.
+
+Print Assumptions checked_or.
+
+(* The plugin disables check_eliminations directly, the way rocq-lean-import
+   does; there is intentionally no vernacular setter for this flag. *)
+Unset Test Elimination Checking.
+
+(* While disabled, Print Typing Flags shows the flag; when it is at its
+   default (true) the line is omitted entirely. *)
+Print Typing Flags.
+
+Inductive unchecked_or (A B : Prop) : Prop :=
+| unchecked_l : A -> unchecked_or A B
+| unchecked_r : B -> unchecked_or A B.
+
+Definition unchecked_large (A B : Prop) (H : unchecked_or A B) : Type :=
+  match H with
+  | unchecked_l _ _ _ => nat
+  | unchecked_r _ _ _ => bool
+  end.
+
+Set Test Elimination Checking.
+
+Print Assumptions unchecked_large.
+
+Set Printing All Assumptions.
+Print Assumptions unchecked_large.
+Unset Printing All Assumptions.
+
+Print Typing Flags.

vernac/assumptions.ml

@@ -377,9 +377,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
   let has_impredicative_set = ref false in
   let has_rewrite_rules = ref false in
   let has_type_in_type = ref false in
+  let has_unchecked_eliminations = ref false in
   let collect_theory_flags (tf : Declarations.typing_flags) =
     if tf.impredicative_set then has_impredicative_set := true;
-    if not tf.check_universes then has_type_in_type := true
+    if not tf.check_universes then has_type_in_type := true;
+    if not tf.check_eliminations then has_unchecked_eliminations := true
   in
   let fold obj contents accu = match obj with
   | VarRef id ->
@@ -407,6 +409,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
+      let accu =
+        if cb.const_typing_flags.check_eliminations then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (UncheckedEliminations obj, l)) Constr.mkProp accu
+      in
     if not (Option.has_some contents) then
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
@@ -440,6 +448,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
+      let accu =
+        if mind.mind_typing_flags.check_eliminations then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (UncheckedEliminations obj, l)) Constr.mkProp accu
+      in
       let accu =
         if not (uses_uip mind) then accu
         else
@@ -459,5 +473,6 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs =
     has_impredicative_set = !has_impredicative_set;
     has_rewrite_rules = !has_rewrite_rules;
     has_type_in_type = !has_type_in_type;
+    has_unchecked_eliminations = !has_unchecked_eliminations;
   } in
   (theory, map)