Further error message improvements

src/bin/repl.ml

@@ -664,7 +664,7 @@ let handle_input istate input =
       print_endline ("Error: " ^ str);
       istate
   | Type_error.Type_error (_, err) ->
-      print_endline (Type_error.string_of_type_error err);
+      print_endline (fst (Type_error.string_of_type_error err));
       istate
   | Reporting.Fatal_error err ->
       Reporting.print_error ~interactive:true err;

src/lib/constant_fold.ml

@@ -226,7 +226,8 @@ let rw_exp fixed target ok not_ok istate =
             Reporting.warn "" l
               ("Type error when folding constants in "
               ^ string_of_exp (E_aux (e_aux, annot))
-              ^ "\n" ^ Type_error.string_of_type_error err
+              ^ "\n"
+              ^ fst (Type_error.string_of_type_error err)
               );
             not_ok ();
             E_aux (e_aux, annot)

src/lib/error_format.ml

@@ -143,7 +143,7 @@ let format_code_single' prefix hint fname in_chan lnum cnum_from cnum_to content
   format_endline
     (blank_prefix ^ underline_single ppf.loc_color (adjust cnum_from) (adjust cnum_to) ^ format_hint ppf.loc_color hint)
     ppf;
-  contents { ppf with indent = blank_prefix ^ " " }
+  contents { ppf with indent = ppf.indent ^ blank_prefix ^ " " }
 
 let underline_double_from color cnum_from eol =
   Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (eol - cnum_from - 1) '-')))
@@ -172,12 +172,12 @@ let format_code_double' prefix fname in_chan lnum_from cnum_from lnum_to cnum_to
   let line_to, adjust = unprintable_escape ~color:Util.(fun e -> e |> magenta |> clear) line_to in
   format_endline (line_to_prefix ^ line_to) ppf;
   format_endline (blank_prefix ^ underline_double_to ppf.loc_color (adjust cnum_to)) ppf;
-  contents { ppf with indent = blank_prefix ^ " " }
+  contents { ppf with indent = ppf.indent ^ blank_prefix ^ " " }
 
 let format_code_single_fallback prefix fname lnum cnum_from cnum_to contents ppf =
   let blank_prefix = String.make (String.length (string_of_int lnum)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
   format_endline (Printf.sprintf "%s%s:%d.%d-%d:" prefix (format_filename fname) lnum cnum_from cnum_to) ppf;
-  contents { ppf with indent = blank_prefix ^ " " }
+  contents { ppf with indent = ppf.indent ^ blank_prefix ^ " " }
 
 let format_code_single prefix hint fname lnum cnum_from cnum_to contents ppf =
   try
@@ -197,7 +197,7 @@ let format_code_double_fallback prefix fname lnum_from cnum_from lnum_to cnum_to
   format_endline
     (Printf.sprintf "%s%s:%d.%d-%d.%d:" prefix (format_filename fname) lnum_from cnum_from lnum_to cnum_to)
     ppf;
-  contents { ppf with indent = blank_prefix ^ " " }
+  contents { ppf with indent = ppf.indent ^ blank_prefix ^ " " }
 
 let format_code_double prefix fname lnum_from cnum_from lnum_to cnum_to contents ppf =
   try
@@ -244,11 +244,6 @@ type message =
   | Seq of message list
   | Severity of severity * message
 
-let rec messages_all_same = function
-  | (_, m1) :: (id2, m2) :: rest -> m1 = m2 && messages_all_same ((id2, m2) :: rest)
-  | [(_, m1)] -> true
-  | [] -> false
-
 let bullet = Util.(clear (blue "*"))
 
 let rec format_message msg ppf =
@@ -259,7 +254,7 @@ let rec format_message msg ppf =
   | List list ->
       let format_list_item ppf (header, msg) =
         format_endline (Util.(clear (blue "*")) ^ " " ^ header) ppf;
-        format_message msg { ppf with indent = ppf.indent ^ "   " }
+        format_message msg { ppf with indent = ppf.indent ^ "  " }
       in
       List.iter (format_list_item ppf) list
   | Severity (Sev_error, msg) -> format_message msg { ppf with loc_color = Util.red }

src/lib/interpreter.ml

@@ -128,7 +128,7 @@ let fallthrough =
     check_case env exc_typ
       (mk_pexp (Pat_exp (mk_pat (P_id (mk_id "exn")), mk_exp (E_throw (mk_exp (E_id (mk_id "exn")))))))
       unit_typ
-  with Type_error (l, err) -> Reporting.unreachable l __POS__ (string_of_type_error err)
+  with Type_error (l, err) -> Reporting.unreachable l __POS__ (fst (string_of_type_error err))
 
 (**************************************************************************)
 (* 1. Interpreter Monad                                                   *)
@@ -864,8 +864,7 @@ let rec eval_frame' = function
     )
 
 let eval_frame frame =
-  try eval_frame' frame
-  with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  try eval_frame' frame with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err)
 
 let default_effect_interp state eff =
   let lstate, gstate = state in

src/lib/property.ml

@@ -124,7 +124,8 @@ let add_property_guards props ast =
                          would cause the runtime check x <= 100 to be added to the function body.\n\
                          To fix this error, ensure that all quantifiers have corresponding function arguments.\n"
                       in
-                      raise (Reporting.err_typ pragma_l (Type_error.string_of_type_error err ^ msg))
+                      let original_msg, hint = Type_error.string_of_type_error err in
+                      raise (Reporting.err_typ ?hint pragma_l (original_msg ^ msg))
                   in
                   let mk_funcl p = FCL_aux (FCL_funcl (id, Pat_aux (p, pexp_aux)), fcl_aux) in
                   match pexp with

src/lib/reporting.ml

@@ -119,13 +119,13 @@ type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
 
 let fix_endline str = if str.[String.length str - 1] = '\n' then String.sub str 0 (String.length str - 1) else str
 
-let print_err_internal p_l m1 m2 =
+let print_err_internal hint p_l m1 m2 =
   let open Error_format in
   prerr_endline (m1 ^ ":");
   begin
     match p_l with
-    | Loc l -> format_message (Location ("", None, l, Line (fix_endline m2))) err_formatter
-    | Pos p -> format_message (Location ("", None, Parse_ast.Range (p, p), Line (fix_endline m2))) err_formatter
+    | Loc l -> format_message (Location ("", hint, l, Line (fix_endline m2))) err_formatter
+    | Pos p -> format_message (Location ("", hint, Parse_ast.Range (p, p), Line (fix_endline m2))) err_formatter
   end
 
 let loc_to_string l =
@@ -174,7 +174,7 @@ let short_loc_to_string l =
       Printf.sprintf "%s:%d.%d-%d.%d" p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum
         (p2.pos_cnum - p2.pos_bol)
 
-let print_err l m1 m2 = print_err_internal (Loc l) m1 m2
+let print_err l m1 m2 = print_err_internal None (Loc l) m1 m2
 
 type error =
   | Err_general of Parse_ast.l * string
@@ -188,19 +188,20 @@ type error =
 let issues = "\nPlease report this as an issue on GitHub at https://github.com/rems-project/sail/issues"
 
 let dest_err ?(interactive = false) = function
-  | Err_general (l, m) -> (Util.("Error" |> yellow |> clear), Loc l, m)
+  | Err_general (l, m) -> (Util.("Error" |> yellow |> clear), None, Loc l, m)
   | Err_unreachable (l, (file, line, _, _), backtrace, m) ->
-      if interactive then ("Error", Loc l, m)
+      if interactive then ("Error", None, Loc l, m)
       else
         ( Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line,
+          None,
           Loc l,
           m ^ "\n\n" ^ Printexc.raw_backtrace_to_string backtrace ^ issues
         )
-  | Err_todo (l, m) -> ("Todo", Loc l, m)
-  | Err_syntax (p, m) -> (Util.("Syntax error" |> yellow |> clear), Pos p, m)
-  | Err_syntax_loc (l, m) -> (Util.("Syntax error" |> yellow |> clear), Loc l, m)
-  | Err_lex (p, s) -> (Util.("Lexical error" |> yellow |> clear), Pos p, s)
-  | Err_type (l, _, m) -> (Util.("Type error" |> yellow |> clear), Loc l, m)
+  | Err_todo (l, m) -> ("Todo", None, Loc l, m)
+  | Err_syntax (p, m) -> (Util.("Syntax error" |> yellow |> clear), None, Pos p, m)
+  | Err_syntax_loc (l, m) -> (Util.("Syntax error" |> yellow |> clear), None, Loc l, m)
+  | Err_lex (p, s) -> (Util.("Lexical error" |> yellow |> clear), None, Pos p, s)
+  | Err_type (l, hint, m) -> (Util.("Type error" |> yellow |> clear), hint, Loc l, m)
 
 exception Fatal_error of error
 
@@ -227,8 +228,8 @@ let forbid_errors ocaml_pos f x =
   | Fatal_error (Err_type (l, _, m)) -> raise (err_unreachable l ocaml_pos m)
 
 let print_error ?(interactive = false) e =
-  let m1, pos_l, m2 = dest_err ~interactive e in
-  print_err_internal pos_l m1 m2
+  let m1, hint, pos_l, m2 = dest_err ~interactive e in
+  print_err_internal hint pos_l m1 m2
 
 (* Warnings *)
 

src/lib/rewrites.ml

@@ -2149,7 +2149,7 @@ let rewrite_vector_concat_assignments env defs =
           in
           begin
             try check_exp env full_exp unit_typ
-            with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+            with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err)
           end
         )
         else E_aux (e_aux, annot)
@@ -2176,7 +2176,7 @@ let rewrite_tuple_assignments env defs =
         let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in
         begin
           try check_exp env let_exp unit_typ
-          with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+          with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err)
         end
     | _ -> E_aux (e_aux, annot)
   in
@@ -4576,7 +4576,7 @@ let rewrite effect_info env rewriters ast =
          (1, (ast, effect_info, env))
          rewriters
       )
-  with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err)
 
 let () =
   let open Interactive in

src/lib/type_check.ml

@@ -1542,7 +1542,7 @@ let check_function_instantiation l id env bind1 bind2 =
   try direction (fun check_env typ1 typ2 -> subtyp l check_env typ1 typ2) bind1 bind2
   with Type_error (l1, err1) -> (
     try direction (fun check_env typ1 typ2 -> subtyp l check_env typ2 typ1) bind2 bind1
-    with Type_error (l2, err2) -> typ_raise l2 (Err_inner (err2, l1, "Also tried", None, err1))
+    with Type_error (l2, err2) -> typ_raise l2 (Err_inner (err2, l1, "Also tried", err1))
   )
 
 type pattern_duplicate = Pattern_singleton of l | Pattern_duplicate of l * l
@@ -1752,8 +1752,7 @@ let rec lexp_assignment_type env (LE_aux (aux, (l, _))) =
                      ),
                    l_u,
                    "",
-                   Some "existing variable",
-                   Err_other ""
+                   Err_hint "existing variable"
                  )
               )
         | None, _ -> Declaration
@@ -1957,7 +1956,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
           );
       begin
         try crule check_exp env (E_aux (E_app (forwards_id, xs), (l, uannot))) typ
-        with Type_error (_, err1) ->
+        with Type_error (err1_loc, err1) ->
           typ_print
             ( lazy
               ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "("
@@ -1966,8 +1965,8 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
               );
           begin
             try crule check_exp env (E_aux (E_app (backwards_id, xs), (l, uannot))) typ
-            with Type_error (_, err2) ->
-              typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
+            with Type_error (err2_loc, err2) ->
+              typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1_loc, err1); (backwards_id, err2_loc, err2)]))
           end
       end
   | E_app (f, xs), _ when Env.is_overload f env ->
@@ -1978,9 +1977,9 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
         | errs, f :: fs -> begin
             typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
             try crule check_exp env (E_aux (E_app (f, xs), (l, uannot))) typ
-            with Type_error (_, err) ->
+            with Type_error (err_l, err) ->
               typ_debug (lazy "Error");
-              try_overload (errs @ [(f, err)], fs)
+              try_overload (errs @ [(f, err_l, err)], fs)
           end
       in
       try_overload ([], overloads)
@@ -3048,12 +3047,8 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
       | Register typ -> annot_exp (E_id v) typ
       | Unbound _ -> (
           match Bindings.find_opt v (Env.get_val_specs env) with
-          | Some _ ->
-              typ_error l
-                ("Identifier " ^ string_of_id v ^ " is unbound (Did you mean to call the " ^ string_of_id v
-               ^ " function?)"
-                )
-          | None -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
+          | Some _ -> typ_raise l (Err_unbound_id { id = v; locals = Env.get_locals env; have_function = true })
+          | None -> typ_raise l (Err_unbound_id { id = v; locals = Env.get_locals env; have_function = false })
         )
     end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
@@ -3140,7 +3135,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
           );
       begin
         try irule infer_exp env (E_aux (E_app (forwards_id, xs), (l, uannot)))
-        with Type_error (_, err1) ->
+        with Type_error (err1_loc, err1) ->
           (* typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); *)
           typ_print
             ( lazy
@@ -3150,9 +3145,9 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
               );
           begin
             try irule infer_exp env (E_aux (E_app (backwards_id, xs), (l, uannot)))
-            with Type_error (_, err2) ->
+            with Type_error (err2_loc, err2) ->
               (* typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); *)
-              typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
+              typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1_loc, err1); (backwards_id, err2_loc, err2)]))
           end
       end
   | E_app (f, xs) when Env.is_overload f env ->
@@ -3163,9 +3158,9 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
         | errs, f :: fs -> begin
             typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
             try irule infer_exp env (E_aux (E_app (f, xs), (l, uannot)))
-            with Type_error (_, err) ->
+            with Type_error (err_l, err) ->
               typ_debug (lazy "Error");
-              try_overload (errs @ [(f, err)], fs)
+              try_overload (errs @ [(f, err_l, err)], fs)
           end
       in
       try_overload ([], overloads)
@@ -4436,8 +4431,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list
                 let defs, env =
                   try check_defs env defs
                   with Type_error (inner_l, err) ->
-                    typ_raise l
-                      (Err_inner (Err_other "Error while checking bitfield", inner_l, "Bitfield error", None, err))
+                    typ_raise l (Err_inner (Err_other "Error while checking bitfield", inner_l, "Bitfield error", err))
                 in
                 let env = Env.add_bitfield id typ ranges env in
                 if !opt_no_bitfield_expansion then

src/lib/type_env.ml

@@ -406,8 +406,7 @@ let already_bound str id env =
            ( Err_other ("Cannot create " ^ str ^ " type " ^ string_of_id id ^ ", name is already bound"),
              l,
              "",
-             Some "previous binding",
-             Err_other ""
+             Err_hint "previous binding"
            )
         )
   | None ->
@@ -432,8 +431,7 @@ let already_bound_ctor_fn str id env =
                ),
              l,
              "",
-             Some "previous binding",
-             Err_other ""
+             Err_hint "previous binding"
            )
         )
   | None ->
@@ -984,9 +982,11 @@ let add_typ_synonym id typq arg env =
       env
   )
 
+let get_val_specs env = filter_items env env.global.val_specs
+
 let get_val_spec_orig id env =
   try get_item (id_loc id) env (Bindings.find id env.global.val_specs)
-  with Not_found -> typ_error (id_loc id) ("No function type found for " ^ string_of_id id)
+  with Not_found -> typ_raise (id_loc id) (Err_no_function_type { id; functions = get_val_specs env })
 
 let get_val_spec_opt id env =
   match Bindings.find_opt id env.global.val_specs with
@@ -1010,24 +1010,7 @@ let get_val_spec_opt id env =
 let get_val_spec id env =
   match get_val_spec_opt id env with
   | Some (bind, _) -> bind
-  | None ->
-      (* Try to find the most similar function name, within reason, to include in the error *)
-      let closest = ref (Int.max_int, None) in
-      Bindings.iter
-        (fun other_id item ->
-          let id_str = string_of_id id in
-          let other_str = string_of_id other_id in
-          if abs (String.length id_str - String.length other_str) <= 2 then (
-            let distance = Util.levenshtein_distance ~osa:true id_str other_str in
-            let max_distance = min 4 (max 1 (String.length id_str - 3)) in
-            if distance <= max_distance && distance < fst !closest then closest := (distance, Some other_str)
-          )
-        )
-        env.global.val_specs;
-      let hint_msg = match snd !closest with Some other_str -> "\n\nDid you mean " ^ other_str ^ "?" | None -> "" in
-      typ_error (id_loc id) ("No function type found for " ^ string_of_id id ^ hint_msg)
-
-let get_val_specs env = filter_items env env.global.val_specs
+  | None -> typ_raise (id_loc id) (Err_no_function_type { id; functions = get_val_specs env })
 
 let add_union_id ?in_module id bind env =
   if bound_ctor_fn env id then already_bound_ctor_fn "union constructor" id env