Revert "Stop catching anomalies from conversion"

This reverts commit 89b0356.

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
 

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 }

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