From 0f1d10dc4afab04a8ec679320105c64d0f33cfb3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 25 Oct 2023 14:58:55 +0200
Subject: [PATCH] Revert "Stop catching anomalies from conversion"

This reverts commit 89b0356d99596113d80ca7e9908ca3afada40515.
---
 pretyping/pretype_errors.ml |  1 +
 pretyping/reductionops.ml   | 32 ++++++++++++++++++++++++++++++++
 pretyping/reductionops.mli  |  2 ++
 3 files changed, 35 insertions(+)

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 4d3f24e20763..e984644492eb 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -69,6 +69,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | CErrors.UserError _ | TypeError _ | PretypeError _
+  | Reductionops.AnomalyInConversion _
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fbb720b1c30c..fa20d16eb639 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1050,6 +1050,29 @@ let is_transparent e k =
 
 type conversion_test = Constraints.t -> Constraints.t
 
+(* NOTE: We absorb anomalies happening in the conversion tactic, which
+   is a bit ugly. This is mostly due to efficiency both in tactics and
+   in the conversion machinery itself. It is not uncommon for a tactic
+   to send some ill-typed term to the engine.
+
+   We would usually say that a tactic that converts ill-typed terms is
+   buggy, but fixing the tactic could have a very large runtime cost
+   *)
+exception AnomalyInConversion of exn
+
+let _ = CErrors.register_handler (function
+    | AnomalyInConversion e ->
+      Some Pp.(str "Conversion test raised an anomaly:" ++
+               spc () ++ CErrors.print e)
+    | _ -> None)
+
+let report_anomaly (e, info) =
+  let e =
+    if is_anomaly e then AnomalyInConversion e
+    else e
+  in
+  Exninfo.iraise (e, info)
+
 module CheckUnivs =
 struct
 
@@ -1107,6 +1130,9 @@ let is_fconv ?(reds=TransparentState.full) pb env sigma t1 t2 =
       let _ = Conversion.generic_conv ~l2r:false pb evars reds env (sigma, CheckUnivs.checked_universes) t1 t2 in
       true
     with Conversion.NotConvertible -> false
+    | e ->
+      let e = Exninfo.capture e in
+      report_anomaly e
 
 let is_conv ?(reds=TransparentState.full) env sigma x y =
   is_fconv ~reds Conversion.CONV env sigma x y
@@ -1193,6 +1219,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
   with
   | Conversion.NotConvertible -> None
   | UGraph.UniverseInconsistency _ when catch_incon -> None
+  | e ->
+    let e = Exninfo.capture e in
+    report_anomaly e
 
 let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
       Conversion.generic_conv pb ~l2r (Evd.evar_handler sigma))
@@ -1219,6 +1248,9 @@ let infer_conv_ustate ?(catch_incon=true) ?(pb=Conversion.CUMUL)
   with
   | Conversion.NotConvertible -> None
   | UGraph.UniverseInconsistency _ when catch_incon -> None
+  | e ->
+    let e = Exninfo.capture e in
+    report_anomaly e
 
 let evars_of_evar_map sigma =
   { Genlambda.evars_val = Evd.evar_handler sigma }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ebd57a601484..d77b0cae7e1c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -277,6 +277,8 @@ val is_head_evar : env -> evar_map -> constr -> bool
 (** {6 Meta-related reduction functions } *)
 val meta_instance : env -> evar_map -> constr freelisted -> constr
 
+exception AnomalyInConversion of exn
+
 (* inferred_universes just gathers the constraints. *)
 val inferred_universes : (UGraph.t * Univ.Constraints.t) Conversion.universe_compare