Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors

Ack-by: gares
Ack-by: ppedrot

6 files changed, 85 insertions, 39 deletions

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 81e745b714..35c90444b1 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -142,7 +142,9 @@ let progress_evars t =
         let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
         if eq_constr_mod_evars sigma concl newconcl
-        then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
+        then
+          let info = Exninfo.reify () in
+          Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)")
         else Proofview.tclUNIT ()
       end
     in t <*> check
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d6b2a17882..4bc8d61258 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1566,7 +1566,8 @@ let assert_replacing id newt tac =
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
 
 let newfail n s =
-  Proofview.tclZERO (Refiner.FailError (n, lazy s))
+  let info = Exninfo.reify () in
+  Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
@@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let treat sigma res =
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None -> if progress then newfail 0 (str"Failed to progress")
-                   else Proofview.tclUNIT ()
+    | Some None ->
+      if progress
+      then newfail 0 (str"Failed to progress")
+      else Proofview.tclUNIT ()
     | Some (Some res) ->
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 
 let tactic_init_setoid () =
   try init_setoid (); Proofview.tclUNIT ()
-  with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
+  with e when CErrors.noncritical e ->
+    let _, info = Exninfo.capture e in
+    Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded")
 
 let cl_rewrite_clause_strat progress strat clause =
   tactic_init_setoid () <*>
@@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause =
       (cl_rewrite_clause_newtac ~progress strat clause)
       (fun (e, info) -> match e with
        | RewriteFailure e ->
-         tclZEROMSG (str"setoid rewrite failed: " ++ e)
+         tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
        | Refiner.FailError (n, pp) ->
-          tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
-       | e -> Proofview.tclZERO ~info e))
+         tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
+       | e ->
+         Proofview.tclZERO ~info e))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause =
@@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
             (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
     (fun (e, info) -> match e with
     | RewriteFailure e ->
-      tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+      tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e)
     | e -> Proofview.tclZERO ~info e)
   end
 
@@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
-let not_declared env sigma ty rel =
-  tclFAIL 0
+let not_declared ~info env sigma ty rel =
+  tclFAIL ~info 0
     (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
@@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback =
           let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
             (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
-        with e -> Proofview.tclZERO e
+        with e ->
+          (* XXX what is the right test here as to whether e can be converted ? *)
+          let e, info = Exninfo.capture e in
+          Proofview.tclZERO ~info e
       end
       begin function
         | e ->
@@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback =
                 | Hipattern.NoEquationFound ->
                     begin match e with
                     | (Not_found, _) ->
-                        let rel, _, _ = decompose_app_rel env sigma concl in
-                        not_declared env sigma ty rel
-                    | (e, info) -> Proofview.tclZERO ~info e
+                      let rel, _, _ = decompose_app_rel env sigma concl in
+                      not_declared ~info env sigma ty rel
+                    | (e, info) ->
+                      Proofview.tclZERO ~info e
                     end
                 | e' -> Proofview.tclZERO ~info e'
               end
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6d350ade8d..5abe18e00c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -774,7 +774,9 @@ let interp_message_token ist = function
   | MsgIdent {loc;v=id} ->
     let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
     match v with
-    | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
+    | None -> Ftactic.lift (
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found."))
     | Some v -> message_of_value v
 
 let interp_message ist l =
@@ -1087,11 +1089,15 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       end
   | TacFail (g,n,s) ->
       let msg = interp_message ist s in
-      let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in
+      let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in
       let tac =
         match g with
-        | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l)
-        | TacGlobal -> tac
+        | TacLocal ->
+          let info = Exninfo.reify () in
+          fun l -> Proofview.tclINDEPENDENT (tac ~info l)
+        | TacGlobal ->
+          let info = Exninfo.reify () in
+          tac ~info
       in
       Ftactic.run msg tac
   | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
@@ -1174,8 +1180,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         let len1 = List.length alias.Tacenv.alias_args in
         let len2 = List.length l in
         if len1 = len2 then tac
-        else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
-          expected " ++ int len1 ++ str ", found " ++ int len2)
+        else
+          let info = Exninfo.reify () in
+          Tacticals.New.tclZEROMSG ~info
+            (str "Arguments length mismatch: \
+                  expected " ++ int len1 ++ str ", found " ++ int len2)
       in
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
@@ -1267,7 +1276,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 and interp_app loc ist fv largs : Val.t Ftactic.t =
   Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
-  let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
+  let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in
   if has_type fv (topwit wit_tacvalue) then
   match to_tacvalue fv with
      (* if var=[] and body has been delayed by val_interp, then body
@@ -1313,12 +1322,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
     | (VFun(appl,trace,olfun,[],body)) ->
       let extra_args = List.length largs in
-      Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
-                                str (string_of_int extra_args) ++
-                                str " extra " ++ str (String.plural extra_args "argument") ++
-                                str ".")
-    | VRec(_,_) -> fail
-  else fail
+      let info = Exninfo.reify () in
+      Tacticals.New.tclZEROMSG ~info
+        (str "Illegal tactic application: got " ++
+         str (string_of_int extra_args) ++
+         str " extra " ++ str (String.plural extra_args "argument") ++
+         str ".")
+    | VRec(_,_) ->
+      let info = Exninfo.reify () in
+      fail ~info
+  else
+    let info = Exninfo.reify () in
+    fail ~info
 
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value ist vle =
@@ -1346,7 +1361,8 @@ and tactic_of_value ist vle =
      let givenargs =
        List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
      let numgiven = List.length givenargs in
-     Tacticals.New.tclZEROMSG
+     let info = Exninfo.reify () in
+     Tacticals.New.tclZEROMSG ~info
        (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
           (match numargs with
             0 -> assert false
@@ -1364,11 +1380,15 @@ and tactic_of_value ist vle =
           | _ ->
              Pp.str "arguments were provided for variables " ++
                pr_enum Pp.str givenargs ++ Pp.str ".")
-  | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+  | VRec _ ->
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     tactic_of_value ist tac
-  else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
+  else
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1562,10 +1582,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
           pr_econstr_env env sigma cresult)
     end <*>
     Ftactic.return cresult
-  with CannotCoerceTo _ ->
+  with CannotCoerceTo _ as exn ->
+    let _, info = Exninfo.capture exn in
     let env = Proofview.Goal.env gl in
-    Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
-      str "offending expression: " ++ fnl() ++ pr_inspect env e result)
+    Tacticals.New.tclZEROMSG ~info
+      (str "Must evaluate to a closed term" ++ fnl() ++
+       str "offending expression: " ++ fnl() ++ pr_inspect env e result)
   end
 
 
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 525199735d..2b43b11fe1 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct
     { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
 
   (** Failure of the pattern-matching monad: no success. *)
-  let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+  let fail (type a) : a m = { stream = fun _ _ ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info matching_error }
 
   let run (m : 'a m) =
     let ctx = {
@@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct
   (** Declares a substitution, a context substitution and a term substitution. *)
   let put subst context terms : unit m =
     let s = { subst ; context ; terms ; lhs = () } in
-    { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+    { stream = fun k ctx -> match merge s ctx with
+          | None ->
+            let info = Exninfo.reify () in
+            Proofview.tclZERO ~info matching_error
+          | Some s -> k () s }
 
   (** Declares a substitution. *)
   let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 79d6c05e1d..3ba6365783 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1475,7 +1475,9 @@ let coq_omega =
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
       tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
+    with NO_CONTRADICTION as e ->
+      let _, info = Exninfo.capture e in
+      tclZEROMSG ~info (Pp.str"Omega can't solve this system")
   end
   end
 
@@ -1890,7 +1892,9 @@ let destructure_goal =
                                          end)
                 intro
             with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
-            | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+            | e when Proofview.V82.catchable_exception e ->
+              let e, info = Exninfo.capture e in
+              Proofview.tclZERO ~info e
           in
           tclTHEN goal_tac destructure_hyps
     in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 88a3e85211..ad0a31622c 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
       Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
     tclUNIT (env,sigma,term)
   with e ->
+    (* XXX this is another catch all! *)
+    let e, info = Exninfo.capture e in
     Ssrprinters.ppdebug (lazy
     Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
-     tclZERO e
+    tclZERO ~info e
 end
 
 (* Commits the term to the monad *)