Merge PR #11566: [misc] Better preserve backtraces in several modules

Ack-by: SkySkimmer
Reviewed-by: ppedrot

5 files changed, 99 insertions, 67 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a8fb5a3f45..3d99e1d227 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -618,8 +618,9 @@ let interp_univ_constraints env evd cstrs =
     let cstrs' = Univ.Constraint.add cstr cstrs in
     try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
         evd, cstrs'
-    with Univ.UniverseInconsistency e ->
-      CErrors.user_err ~hdr:"interp_constraint"
+    with Univ.UniverseInconsistency e as exn ->
+      let _, info = Exninfo.capture exn in
+      CErrors.user_err ~hdr:"interp_constraint" ~info
         (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
   in
   List.fold_left interp (evd,Univ.Constraint.empty) cstrs
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5ad8af6d57..ee041ed088 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -115,7 +115,7 @@ type internalization_error =
   | NotAProjectionOf of qualid * qualid
   | ProjectionsOfDifferentRecords of qualid * qualid
 
-exception InternalizationError of internalization_error Loc.located
+exception InternalizationError of internalization_error
 
 let explain_variable_capture id id' =
   Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++
@@ -164,8 +164,13 @@ let explain_internalization_error e =
     explain_projections_of_diff_records inductive1_id inductive2_id
   in pp ++ str "."
 
-let error_bad_inductive_type ?loc =
-  user_err ?loc  (str
+let _ = CErrors.register_handler (function
+    | InternalizationError e ->
+      Some (explain_internalization_error e)
+    | _ -> None)
+
+let error_bad_inductive_type ?loc ?info () =
+  user_err ?loc ?info (str
     "This should be an inductive type applied to patterns.")
 
 let error_parameter_not_implicit ?loc =
@@ -368,7 +373,7 @@ let impls_term_list n ?(args = []) =
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
 let rec check_capture ty = let open CAst in function
   | { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
-      raise (InternalizationError (loc,VariableCapture (id,id')))
+    Loc.raise ?loc (InternalizationError (VariableCapture (id,id')))
   | _::nal ->
       check_capture ty nal
   | [] ->
@@ -1086,7 +1091,9 @@ let intern_extended_global_of_qualid qid =
 let intern_reference qid =
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> Nametab.error_global_not_found qid
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      Nametab.error_global_not_found ~info qid
   in
   Smartlocate.global_of_extended_global r
 
@@ -1170,16 +1177,20 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
         let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
         check_applied_projection isproj realref qid;
         find_appl_head_data r, args2
-      with Not_found ->
+      with Not_found as exn ->
         (* Extra allowance for non globalizing functions *)
         if !interning_grammar || env.unb then
           (* check_applied_projection ?? *)
           (gvar (loc,qualid_basename qid) us, [], []), args
-        else Nametab.error_global_not_found qid
+        else
+          let _, info = Exninfo.capture exn in
+          Nametab.error_global_not_found ~info qid
   else
     let r,realref,args2 =
       try intern_qualid qid intern env ntnvars us args
-      with Not_found -> Nametab.error_global_not_found qid
+      with Not_found as exn ->
+        let _, info = Exninfo.capture exn in
+        Nametab.error_global_not_found ~info qid
     in
     check_applied_projection isproj realref qid;
     find_appl_head_data r, args2
@@ -1253,14 +1264,16 @@ let loc_of_lhs lhs =
 let check_linearity lhs ids =
   match has_duplicate ids with
     | Some id ->
-        raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
+      let loc = loc_of_lhs lhs in
+      Loc.raise ?loc (InternalizationError (NonLinearPattern id))
     | None ->
         ()
 
 (* Match the number of pattern against the number of matched args *)
 let check_number_of_pattern loc n l =
   let p = List.length l in
-  if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
+  if not (Int.equal n p) then
+    Loc.raise ?loc (InternalizationError (BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
   let eq_id {v=id} {v=id'} = Id.equal id id' in
@@ -1392,7 +1405,7 @@ let find_constructor loc add_params ref =
 
 let find_pattern_variable qid =
   if qualid_is_ident qid then qualid_basename qid
-  else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
+  else Loc.raise ?loc:qid.CAst.loc (InternalizationError(NotAConstructor qid))
 
 let check_duplicate ?loc fields =
   let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
@@ -1429,8 +1442,10 @@ let sort_fields ~complete loc fields completer =
             let gr = locate_reference first_field_ref in
             Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
             (gr, Recordops.find_projection gr)
-          with Not_found ->
-            raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info loc in
+            Exninfo.iraise (InternalizationError(NotAProjection first_field_ref), info)
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1465,10 +1480,10 @@ let sort_fields ~complete loc fields completer =
                      try Recordops.find_projection field_glob_ref
                      with Not_found ->
                        let inductive_ref = inductive_of_record floc record in
-                       raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in
+                       Loc.raise ?loc:floc (InternalizationError(NotAProjectionOf (field_ref, inductive_ref))) in
                    let ind1 = inductive_of_record floc record in
                    let ind2 = inductive_of_record floc this_field_record in
-                   raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
+                   Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (ind1, ind2)))
                in
                if not regular && complete then
                  (* "regular" is false when the field is defined
@@ -1655,12 +1670,16 @@ let drop_notations_pattern looked_for genv =
       begin
         match drop_syndef top scopes head pl with
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
-          | None -> raise (InternalizationError (loc,NotAConstructor head))
+          | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
       end
     | CPatCstr (qid, Some expl_pl, pl) ->
-      let g = try Nametab.locate qid
-              with Not_found ->
-              raise (InternalizationError (loc,NotAConstructor qid)) in
+      let g =
+        try Nametab.locate qid
+        with Not_found as exn ->
+          let _, info = Exninfo.capture exn in
+          let info = Option.cata (Loc.add_loc info) info loc in
+          Exninfo.iraise (InternalizationError (NotAConstructor qid), info)
+      in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
         DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
@@ -1810,20 +1829,22 @@ let intern_ind_pattern genv ntnvars scopes pat =
   let no_not =
     try
       drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
-    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
+    with InternalizationError(NotAConstructor _) as exn ->
+      let _, info = Exninfo.capture exn in
+      error_bad_inductive_type ~info ()
   in
   let loc = no_not.CAst.loc in
   match DAst.get no_not with
     | RCPatCstr (head, expl_pl, pl) ->
-      let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
+      let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc ()) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
         (List.length expl_pl) pl in
       let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
       (with_letin,
        match product_of_cases_patterns empty_alias idslpl with
        | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
-       | _ -> error_bad_inductive_type ?loc)
-    | x -> error_bad_inductive_type ?loc
+       | _ -> error_bad_inductive_type ?loc ())
+    | x -> error_bad_inductive_type ?loc ()
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1899,8 +1920,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
-          with Not_found ->
-            raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info locid in
+            Exninfo.iraise (InternalizationError (UnboundFixName (false,iddef)),info)
         in
         let env = restart_lambda_binders env in
         let idl_temp = Array.map
@@ -1942,8 +1965,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let dl = Array.of_list dl in
         let n =
           try List.index0 Id.equal iddef lf
-          with Not_found ->
-            raise (InternalizationError (locid,UnboundFixName (true,iddef)))
+          with Not_found as exn ->
+            let _, info = Exninfo.capture exn in
+            let info = Option.cata (Loc.add_loc info) info locid in
+            Exninfo.iraise (InternalizationError (UnboundFixName (true,iddef)), info)
         in
         let env = restart_lambda_binders env in
         let idl_tmp = Array.map
@@ -2171,7 +2196,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         DAst.make ?loc @@
         GEvar (n, List.map (on_snd (intern_no_implicit env)) l)
     | CPatVar _ ->
-        raise (InternalizationError (loc,IllegalMetavariable))
+      Loc.raise ?loc (InternalizationError IllegalMetavariable)
     (* end *)
     | CSort s ->
         DAst.make ?loc @@
@@ -2337,12 +2362,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (intern_no_implicit enva a) :: (intern_args env subscopes args)
 
   in
-  try
-    intern env c
-  with
-      InternalizationError (loc,e) ->
-        user_err ?loc ~hdr:"internalize"
-          (explain_internalization_error e)
+  intern env c
 
 (**************************************************************************)
 (* Functions to translate constr_expr into glob_constr                    *)
@@ -2382,12 +2402,7 @@ let intern_gen kind env sigma
 let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
 let intern_type env sigma c = intern_gen IsType env sigma c
 let intern_pattern globalenv patt =
-  try
-    intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
-  with
-      InternalizationError (loc,e) ->
-        user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-
+  intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -2500,7 +2515,6 @@ let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
 let intern_context env impl_env binders =
-  try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let ids =
     (* We assume all ids around are parts of the prefix of the current
@@ -2514,8 +2528,6 @@ let intern_context env impl_env binders =
               tmp_scope = None; scopes = []; impls = impl_env;
               binder_block_names = Some (Some AbsPi,ids)}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
-  with InternalizationError (loc,e) ->
-    user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
 let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
   let open EConstr in
diff --git a/interp/modintern.ml b/interp/modintern.ml
index ae152e1c1c..50f90ebea7 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -22,14 +22,15 @@ exception ModuleInternalizationError of module_internalization_error
 
 type module_kind = Module | ModType | ModAny
 
-let error_not_a_module_loc kind loc qid =
+let error_not_a_module_loc ~info kind loc qid =
   let s = string_of_qualid qid in
   let e = match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
   in
-  Loc.raise ?loc e
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (e,info)
 
 let error_application_to_not_path loc me =
   Loc.raise ?loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
@@ -57,7 +58,9 @@ let lookup_module_or_modtype kind qid =
       if kind == Module then raise Not_found;
       let mp = Nametab.locate_modtype qid in
       Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
-    with Not_found -> error_not_a_module_loc kind loc qid
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      error_not_a_module_loc ~info kind loc qid
 
 let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 3f13476355..d4a44d9622 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -125,13 +125,14 @@ let declare_scope scope =
   with Not_found ->
     scope_map := String.Map.add scope empty_scope !scope_map
 
-let error_unknown_scope sc =
-  user_err ~hdr:"Notation"
+let error_unknown_scope ~info sc =
+  user_err ~hdr:"Notation" ~info
     (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope ?(tolerant=false) scope =
   try String.Map.find scope !scope_map
-  with Not_found ->
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
     if tolerant then
       (* tolerant mode to be turn off after deprecation phase *)
       begin
@@ -140,7 +141,7 @@ let find_scope ?(tolerant=false) scope =
         empty_scope
       end
     else
-      error_unknown_scope scope
+      error_unknown_scope ~info scope
 
 let check_scope ?(tolerant=false) scope =
   let _ = find_scope ~tolerant scope in ()
@@ -158,7 +159,9 @@ let normalize_scope sc =
     try
       let sc = String.Map.find sc !delimiters_map in
       let _ = String.Map.find sc !scope_map in sc
-    with Not_found -> error_unknown_scope sc
+    with Not_found as exn ->
+      let _, info = Exninfo.capture exn in
+      error_unknown_scope ~info sc
 
 (**********************************************************************)
 (* The global stack of scopes                                         *)
@@ -257,8 +260,10 @@ let remove_delimiters scope =
        try
          let _ = ignore (String.Map.find key !delimiters_map) in
          delimiters_map := String.Map.remove key !delimiters_map
-       with Not_found ->
-         assert false (* A delimiter for scope [scope] should exist *)
+       with Not_found as exn ->
+         let _, info = Exninfo.capture exn in
+         (* XXX info *)
+         CErrors.anomaly ~info (str "A delimiter for scope [scope] should exist")
 
 let find_delimiters_scope ?loc key =
   try String.Map.find key !delimiters_map
@@ -1123,12 +1128,17 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
 
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
-  with Not_found ->
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
     match d with
-    | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
-       (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
-    | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
-       (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    | [] ->
+      user_err ?loc ~info ~hdr:"prim_token_interpreter"
+        (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++
+         str " could not be found in the current environment.")
+    | _ ->
+      user_err ?loc ~info ~hdr:"prim_token_interpreter"
+        (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
+         str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -1250,8 +1260,9 @@ let interp_prim_token_gen ?loc g p local_scopes =
   try
     let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
     pat, (loc,sc)
-  with Not_found ->
-    user_err ?loc ~hdr:"interp_prim_token"
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    user_err ?loc ~info ~hdr:"interp_prim_token"
     ((match p with
       | Numeral _ ->
          str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
@@ -1284,9 +1295,10 @@ let interp_notation ?loc ntn local_scopes =
     let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
     Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
     n.not_interp, (n.not_location, sc)
-  with Not_found ->
-    user_err ?loc
-    (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    user_err ?loc ~info
+      (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 03977fcb4e..33d8aa6064 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -56,11 +56,15 @@ let global_inductive_with_alias qid  =
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type.")
-  with Not_found -> Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
-  with Not_found -> Nametab.error_global_not_found qid
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
 
 let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->