diff --git a/src/bin/repl.ml b/src/bin/repl.ml
index 705be2007..7ed6569f5 100644
--- a/src/bin/repl.ml
+++ b/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;
diff --git a/src/lib/constant_fold.ml b/src/lib/constant_fold.ml
index 7c25d0e15..e2f910a64 100644
--- a/src/lib/constant_fold.ml
+++ b/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)
diff --git a/src/lib/error_format.ml b/src/lib/error_format.ml
index e836b40fc..7ffdefcff 100644
--- a/src/lib/error_format.ml
+++ b/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 }
diff --git a/src/lib/interpreter.ml b/src/lib/interpreter.ml
index e859ee940..53d4959f4 100644
--- a/src/lib/interpreter.ml
+++ b/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
diff --git a/src/lib/property.ml b/src/lib/property.ml
index d751c18d6..a2c6fc02d 100644
--- a/src/lib/property.ml
+++ b/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
diff --git a/src/lib/reporting.ml b/src/lib/reporting.ml
index 2c714350a..3aaed80ff 100644
--- a/src/lib/reporting.ml
+++ b/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 *)
 
diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml
index 73def7f1c..7a8baa002 100644
--- a/src/lib/rewrites.ml
+++ b/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
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index fd4adee67..913675a00 100644
--- a/src/lib/type_check.ml
+++ b/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
diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml
index c34d90b0b..a9ee853f2 100644
--- a/src/lib/type_env.ml
+++ b/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
diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml
index 551bc2df0..3470709d8 100644
--- a/src/lib/type_error.ml
+++ b/src/lib/type_error.ml
@@ -233,19 +233,27 @@ let simp_typ =
     | arg -> arg
   )
 
+(* If we have a sequence of overloading errors this function rates
+   them based on a heuristic score stored in the
+   [Err_instantiation_info] constructor. The aim of the heuristic is
+   to figure out which overloading is most likely intended by the
+   user. Any error not wrapped in [Err_instantiation_info] is treated
+   as likely. *)
 let rank_overload_errors errs =
-  let others, with_instantiation_info =
+  let with_heuristic, without_heuristic =
     Util.map_split
-      (function id, Err_instantiation_info (heuristic, err) -> Error (id, heuristic, err) | id, err -> Ok (id, err))
+      (function
+        | id, l, Err_instantiation_info (heuristic, err) -> Ok (id, heuristic, l, err) | id, l, err -> Error (id, l, err)
+        )
       errs
   in
-  match List.stable_sort (fun (_, h1, _) (_, h2, _) -> Int.compare h1 h2) with_instantiation_info with
-  | (id, heuristic, err) :: rest ->
-      let same, worse = Util.take_drop (fun (_, h, _) -> heuristic = h) rest in
-      ( others @ ((id, err) :: List.map (fun (id, _, err) -> (id, err)) same),
-        Some (List.map (fun (id, _, _) -> id) worse)
+  match List.stable_sort (fun (_, h1, _, _) (_, h2, _, _) -> Int.compare h1 h2) with_heuristic with
+  | (id, heuristic, l, err) :: rest ->
+      let same, worse = Util.take_drop (fun (_, h, _, _) -> heuristic = h) rest in
+      ( without_heuristic @ ((id, l, err) :: List.map (fun (id, _, l, err) -> (id, l, err)) same),
+        Some (List.map (fun (id, _, _, _) -> id) worse)
       )
-  | [] -> (others, None)
+  | [] -> (without_heuristic, None)
 
 let rec innermost_function_arg_error l typ err =
   match err with
@@ -253,48 +261,121 @@ let rec innermost_function_arg_error l typ err =
   | Err_function_arg (l, typ, err) -> innermost_function_arg_error l typ err
   | _ -> (l, typ, err)
 
-let message_of_type_error =
+let rec overload_messages_all_same = function
+  | (_, l1, m1) :: (id2, l2, m2) :: rest ->
+      if l1 = l2 && m1 = m2 then overload_messages_all_same ((id2, l2, m2) :: rest) else None
+  | [(_, l1, m1)] -> Some m1
+  | [] -> None
+
+let find_closest name f =
+  let closest = ref (Int.max_int, None) in
+  let distance_callback other_id =
+    let other_name = string_of_id other_id in
+    if abs (String.length name - String.length other_name) <= 2 then (
+      let distance = Util.levenshtein_distance ~osa:true name other_name in
+      let max_distance = min 4 (max 1 (String.length name - 3)) in
+      if distance <= max_distance && distance < fst !closest then closest := (distance, Some other_name)
+    )
+  in
+  f distance_callback;
+  snd !closest
+
+let message_of_type_error type_error =
   let open Error_format in
-  let rec msg = function
-    | Err_inner (err, l', prefix, hint, err') ->
+  let have_shown_overload_help = ref false in
+  let preserve var f x =
+    let preserved = !var in
+    var := true;
+    let result = f x in
+    var := preserved;
+    result
+  in
+  let rec to_message = function
+    | Err_hint h -> (Seq [], Some h)
+    | Err_inner (err, l', prefix, err') ->
         let prefix = if prefix = "" then "" else Util.(prefix ^ " " |> yellow |> clear) in
-        Seq [msg err; Line ""; Location (prefix, hint, l', msg err')]
-    | Err_other str -> if str = "" then Seq [] else Line str
-    | Err_function_arg (l, typ, err) ->
-        let l, typ, err = innermost_function_arg_error l typ err in
-        Seq [msg err; Location ("", Some ("when checking this argument has type " ^ string_of_typ typ), l, Seq [])]
+        let msg, hint = to_message err in
+        let msg', hint' = to_message err' in
+        (Seq [msg; Line ""; Location (prefix, hint', l', msg')], hint)
+    | Err_other str -> ((if str = "" then Seq [] else Line str), None)
+    | Err_function_arg (_, typ, err) ->
+        let msg, _ = to_message err in
+        (msg, Some ("checking function argument has type " ^ string_of_typ typ))
+    | Err_unbound_id { id; locals; have_function } ->
+        let name = string_of_id id in
+        let closest = find_closest name (fun callback -> Bindings.iter (fun other_id _ -> callback other_id) locals) in
+        let hint_msg = match closest with Some other_name -> ". Did you mean " ^ other_name ^ "?" | None -> "" in
+        if have_function then
+          ( Seq
+              [
+                Line ("Identifier " ^ name ^ " is unbound" ^ hint_msg);
+                Line "";
+                Line ("There is a also a function " ^ name ^ " in scope.");
+              ],
+            None
+          )
+        else (Line ("Identifier " ^ name ^ " is unbound" ^ hint_msg), None)
+    | Err_no_function_type { id; functions } ->
+        let name = string_of_id id in
+        let closest =
+          find_closest name (fun callback -> Bindings.iter (fun other_id _ -> callback other_id) functions)
+        in
+        let hint_msg = match closest with Some other_name -> ". Did you mean " ^ other_name ^ "?" | None -> "" in
+        (Line ("Function " ^ name ^ " not found" ^ hint_msg), None)
     | Err_no_overloading (id, errs) ->
-        let overload_errs = List.map (fun (id, err) -> (string_of_id id, msg err)) errs in
-        if messages_all_same overload_errs then snd (List.hd overload_errs)
-        else (
-          let likely, others = if !opt_explain_all_overloads then (errs, None) else rank_overload_errors errs in
-          let other_msg =
-            match others with
-            | None | Some [] -> []
-            | Some ids ->
-                [
-                  Line "";
-                  Line ("Also tried: " ^ Util.string_of_list ", " string_of_id ids);
-                  Line "These seem less likely, use --explain-all-overloads to see full details";
-                ]
-          in
-          Seq
-            ([
-               Line ("No overloading for " ^ string_of_id id ^ ", tried:");
-               List (List.map (fun (id, err) -> (string_of_id id, msg err)) likely);
-             ]
-            @ other_msg
-            )
-        )
-    | Err_instantiation_info (_, err) -> msg err
+        let overload_errs =
+          List.map (fun (id, l, err) -> (id, l, preserve have_shown_overload_help to_message err)) errs
+        in
+        let extra_help s =
+          if !have_shown_overload_help then []
+          else (
+            have_shown_overload_help := true;
+            [Line s]
+          )
+        in
+        begin
+          match overload_messages_all_same overload_errs with
+          | Some msg -> msg
+          | None ->
+              let likely, others = if !opt_explain_all_overloads then (errs, None) else rank_overload_errors errs in
+              let other_msg =
+                match others with
+                | None | Some [] -> []
+                | Some [id] ->
+                    [Line ""; Line ("Also tried " ^ string_of_id id)]
+                    @ extra_help "This seems less likely, use --explain-all-overloads to see full details"
+                | Some ids ->
+                    [Line ""; Line ("Also tried: " ^ Util.string_of_list ", " string_of_id ids)]
+                    @ extra_help "These seem less likely, use --explain-all-overloads to see full details"
+              in
+              ( Seq
+                  ([
+                     Line ("No overloading for " ^ string_of_id id ^ ", tried:");
+                     List
+                       (List.map
+                          (fun (id, l, err) ->
+                            let msg, hint = to_message err in
+                            (string_of_id id, Location ("", hint, l, msg))
+                          )
+                          likely
+                       );
+                   ]
+                  @ other_msg
+                  ),
+                Some (string_of_id id)
+              )
+        end
+    | Err_instantiation_info (_, err) -> to_message err
     | Err_unresolved_quants (id, quants, locals, tyvars, ncs) ->
-        Seq
-          [
-            Line ("Could not resolve quantifiers for " ^ string_of_id id);
-            Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants);
-          ]
+        ( Seq
+            [
+              Line ("Could not resolve quantifiers for " ^ string_of_id id);
+              Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants);
+            ],
+          None
+        )
     | Err_failed_constraint (check, locals, _, ncs) ->
-        Line ("Failed to prove constraint: " ^ string_of_n_constraint (constraint_simp check))
+        (Line ("Failed to prove constraint: " ^ string_of_n_constraint (constraint_simp check)), None)
     | Err_subtype (typ1, typ2, nc, all_constraints, tyvars) ->
         let nc = Option.map constraint_simp nc in
         let typ1, typ2 = (simp_typ typ1, simp_typ typ2) in
@@ -361,39 +442,30 @@ let message_of_type_error =
           | [info] -> format_var_constraint info
           | infos -> Seq (List.map format_var_constraint infos)
         in
-        Severity
-          ( Sev_warn,
-            Seq
-              (Line (error_string_of_typ substs typ1 ^ " is not a subtype of " ^ error_string_of_typ substs typ2)
-               ::
-               ( match nc with
-               | Some nc -> [Line ("as " ^ error_string_of_nc substs nc ^ " could not be proven")]
-               | None -> []
-               )
-              @ List.map
-                  (fun (v, l, ncs) ->
-                    Seq
-                      [
-                        Line "";
-                        Line ("type variable " ^ error_string_of_kid substs v ^ ":");
-                        Location ("", Some "bound here", l, format_var_constraints ncs);
-                      ]
-                  )
-                  var_constraints
-              )
-          )
-    | Err_no_num_ident id -> Line ("No num identifier " ^ string_of_id id)
-    | Err_no_casts (exp, typ_from, typ_to, trigger, reasons) ->
-        let coercion =
-          Line
-            ("Tried performing type coercion from " ^ string_of_typ typ_from ^ " to " ^ string_of_typ typ_to ^ " on "
-           ^ string_of_exp exp
-            )
-        in
-        Seq
-          ([coercion; Line "Coercion failed because:"; msg trigger]
-          @ if not (reasons = []) then Line "Possible reasons:" :: List.map msg reasons else []
-          )
+        ( Severity
+            ( Sev_warn,
+              Seq
+                (Line (error_string_of_typ substs typ1 ^ " is not a subtype of " ^ error_string_of_typ substs typ2)
+                 ::
+                 ( match nc with
+                 | Some nc -> [Line ("as " ^ error_string_of_nc substs nc ^ " could not be proven")]
+                 | None -> []
+                 )
+                @ List.map
+                    (fun (v, l, ncs) ->
+                      Seq
+                        [
+                          Line "";
+                          Line ("type variable " ^ error_string_of_kid substs v ^ ":");
+                          Location ("", Some "bound here", l, format_var_constraints ncs);
+                        ]
+                    )
+                    var_constraints
+                )
+            ),
+          None
+        )
+    | Err_no_num_ident id -> (Line ("No num identifier " ^ string_of_id id), None)
     | Err_not_in_scope (explanation, Some l, item_scope, into_scope, priv) ->
         let suggest, in_mod, add_requires_here =
           match (item_scope, into_scope) with
@@ -419,63 +491,43 @@ let message_of_type_error =
               )
         in
         if not priv then
-          Seq
-            ([
-               Line (Option.value ~default:"Not in scope" explanation);
-               Line "";
-               Line suggest;
-               Location ("", Some ("definition here" ^ in_mod), l, Seq []);
-             ]
-            @ add_requires_here
-            )
+          ( Seq
+              ([
+                 Line (Option.value ~default:"Not in scope" explanation);
+                 Line "";
+                 Line suggest;
+                 Location ("", Some ("definition here" ^ in_mod), l, Seq []);
+               ]
+              @ add_requires_here
+              ),
+            None
+          )
         else
-          Seq
-            [
-              Line (Option.value ~default:"Cannot use private definition" explanation);
-              Line "";
-              Location ("", Some ("private definition here" ^ in_mod), l, Seq []);
-            ]
-    | Err_not_in_scope (explanation, None, _, _, _) -> Line (Option.value ~default:"Not in scope" explanation)
+          ( Seq
+              [
+                Line (Option.value ~default:"Cannot use private definition" explanation);
+                Line "";
+                Location ("", Some ("private definition here" ^ in_mod), l, Seq []);
+              ],
+            None
+          )
+    | Err_not_in_scope (explanation, None, _, _, _) -> (Line (Option.value ~default:"Not in scope" explanation), None)
   in
-  msg
+  to_message type_error
 
 let string_of_type_error err =
   let open Error_format in
   let b = Buffer.create 20 in
-  format_message (message_of_type_error err) (buffer_formatter b);
-  Buffer.contents b
+  let msg, hint = message_of_type_error err in
+  format_message msg (buffer_formatter b);
+  (Buffer.contents b, hint)
 
-let rec collapse_errors = function
-  | Err_no_overloading (_, errs) as no_collapse ->
-      let errs = List.map (fun (_, err) -> collapse_errors err) errs in
-      let interesting = function Err_other _ -> false | Err_no_casts _ -> false | _ -> true in
-      begin
-        match List.filter interesting errs with
-        | err :: errs ->
-            let fold_equal msg err =
-              match (msg, err) with
-              | Some msg, Err_no_overloading _ -> Some msg
-              | Some msg, Err_no_casts _ -> Some msg
-              | Some msg, err when msg = string_of_type_error err -> Some msg
-              | _, _ -> None
-            in
-            begin
-              match List.fold_left fold_equal (Some (string_of_type_error err)) errs with
-              | Some _ -> err
-              | None -> no_collapse
-            end
-        | [] -> no_collapse
-      end
-  | Err_inner (err1, l, prefix, hint, err2) ->
-      let err1 = collapse_errors err1 in
-      let err2 = collapse_errors err2 in
-      if string_of_type_error err1 = string_of_type_error err2 then err1 else Err_inner (err1, l, prefix, hint, err2)
-  | err -> err
+let to_reporting_exn l err =
+  let str, hint = string_of_type_error err in
+  Reporting.err_typ ?hint l str
 
 let check_defs : Env.t -> uannot def list -> tannot def list * Env.t =
- fun env defs ->
-  try Type_check.check_defs env defs with Type_error (l, err) -> raise (Reporting.err_typ l (string_of_type_error err))
+ fun env defs -> try Type_check.check_defs env defs with Type_error (l, err) -> raise (to_reporting_exn l err)
 
 let check : Env.t -> uannot ast -> tannot ast * Env.t =
- fun env defs ->
-  try Type_check.check env defs with Type_error (l, err) -> raise (Reporting.err_typ l (string_of_type_error err))
+ fun env defs -> try Type_check.check env defs with Type_error (l, err) -> raise (to_reporting_exn l err)
diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli
index 79fcdc24b..e348892c1 100644
--- a/src/lib/type_error.mli
+++ b/src/lib/type_error.mli
@@ -91,18 +91,23 @@ val opt_explain_all_overloads : bool ref
 type constraint_reason = (l * string) option
 
 type type_error =
-  | Err_no_casts of uannot exp * typ * typ * type_error * type_error list
-  | Err_no_overloading of id * (id * type_error) list
+  | Err_no_overloading of id * (id * Parse_ast.l * type_error) list
   | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * type_variables * n_constraint list
   | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * type_variables * n_constraint list
   | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * type_variables
   | Err_no_num_ident of id
   | Err_other of string
-  | Err_inner of type_error * Parse_ast.l * string * string option * type_error
+  | Err_inner of type_error * Parse_ast.l * string * type_error
   | Err_not_in_scope of
       string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool
   | Err_instantiation_info of int * type_error
   | Err_function_arg of Parse_ast.l * typ * type_error
+  | Err_no_function_type of { id : id; functions : (typquant * typ) Bindings.t }
+      (** Takes the name of the function and the set of functions in scope *)
+  | Err_unbound_id of { id : id; locals : (mut * typ) Bindings.t; have_function : bool }
+      (** Takes the name of the identifier, the set of local bindings, and
+          whether we have a function of the same name in scope. *)
+  | Err_hint of string  (** A short error that only appears attached to a location *)
 
 exception Type_error of Parse_ast.l * type_error
 
@@ -112,9 +117,9 @@ type suggestion = Suggest_add_constraint of Ast.n_constraint | Suggest_none
 val analyze_unresolved_quant :
   (Ast_util.mut * Ast.typ) Ast_util.Bindings.t -> Ast.n_constraint list -> Ast.quant_item -> suggestion
 
-val collapse_errors : type_error -> type_error
+val string_of_type_error : type_error -> string * string option
 
-val string_of_type_error : type_error -> string
+val to_reporting_exn : Parse_ast.l -> type_error -> exn
 
 val check_defs : Type_check.Env.t -> uannot Ast.def list -> Type_check.tannot Ast.def list * Type_check.Env.t
 
diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml
index 0ac29e4aa..373fb0f71 100644
--- a/src/lib/type_internal.ml
+++ b/src/lib/type_internal.ml
@@ -98,23 +98,22 @@ type constraint_reason = (Ast.l * string) option
 type type_variables = { vars : (Ast.l * kind_aux) KBindings.t; shadows : int KBindings.t }
 
 type type_error =
-  (* First parameter is the error that caused us to start doing type
-     coercions, the second is the errors encountered by all possible
-     coercions *)
-  | Err_no_casts of uannot exp * typ * typ * type_error * type_error list
-  | Err_no_overloading of id * (id * type_error) list
+  | Err_no_overloading of id * (id * Parse_ast.l * type_error) list
   | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * type_variables * n_constraint list
   | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * type_variables * n_constraint list
   | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * type_variables
   | Err_no_num_ident of id
   | Err_other of string
-  | Err_inner of type_error * Parse_ast.l * string * string option * type_error
+  | Err_inner of type_error * Parse_ast.l * string * type_error
   | Err_not_in_scope of
       string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool
   | Err_instantiation_info of int * type_error
   | Err_function_arg of Parse_ast.l * typ * type_error
+  | Err_no_function_type of { id : id; functions : (typquant * typ) Bindings.t }
+  | Err_unbound_id of { id : id; locals : (mut * typ) Bindings.t; have_function : bool }
+  | Err_hint of string
 
-let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", None, error2)
+let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", error2)
 
 exception Type_error of l * type_error
 
diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml
index 00914b5e7..e1036d3c4 100644
--- a/src/sail_c_backend/c_backend.ml
+++ b/src/sail_c_backend/c_backend.ml
@@ -2201,7 +2201,7 @@ let compile_ast env effect_info output_chan c_includes ast =
       )
     |> output_string output_chan
   with Type_error.Type_error (l, err) ->
-    c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
+    c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ fst (Type_error.string_of_type_error err))
 
 let compile_ast_clib env effect_info ast codegen =
   let cdefs, ctx = jib_of_ast env effect_info ast in
diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml
index 4420400df..85151f1cf 100644
--- a/src/sail_coq_backend/pretty_print_coq.ml
+++ b/src/sail_coq_backend/pretty_print_coq.ml
@@ -3785,4 +3785,5 @@ let pp_ast_coq (types_file, types_modules) (defs_file, defs_modules) type_defs_m
       "\nError during Coq printing\n"
       ^ if Printexc.backtrace_status () then "\n" ^ Printexc.get_backtrace () else "(backtracing unavailable)"
     in
-    raise (Reporting.err_typ l (Type_error.string_of_type_error err ^ extra))
+    let msg, hint = Type_error.string_of_type_error err in
+    raise (Reporting.err_typ ?hint l (msg ^ extra))
diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml
index 5afd2a3c1..eda0473e9 100644
--- a/src/sail_smt_backend/jib_smt.ml
+++ b/src/sail_smt_backend/jib_smt.ml
@@ -2369,4 +2369,4 @@ let generate_smt props name_file env effect_info smt_includes ast =
   try
     let cdefs, _, ctx = compile env effect_info ast in
     smt_cdefs props [] name_file ctx cdefs smt_includes cdefs
-  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)
diff --git a/test/typecheck/fail/add_vec_lit_old.expect b/test/typecheck/fail/add_vec_lit_old.expect
index c45524dae..9d9e8c770 100644
--- a/test/typecheck/fail/add_vec_lit_old.expect
+++ b/test/typecheck/fail/add_vec_lit_old.expect
@@ -7,12 +7,15 @@ Cast annotations are deprecated. They will be removed in a future version of the
 Type error:
 fail/add_vec_lit_old.sail:14.23-32:
 14 |let x : range(0, 30) = 0xF + 0x2
-   |                       ^-------^
+   |                       ^-------^ (operator +)
    | No overloading for (operator +), tried:
    | * add_vec
-   |    Type mismatch between int('ex5#) and bitvector(4)
+   |   fail/add_vec_lit_old.sail:14.23-32:
+   |   14 |let x : range(0, 30) = 0xF + 0x2
+   |      |                       ^-------^
+   |      | Type mismatch between int('ex5#) and bitvector(4)
    | * add_range
-   |    Type mismatch between int('ex1#) and bitvector(4)
-   |    fail/add_vec_lit_old.sail:14.23-26:
-   |    14 |let x : range(0, 30) = 0xF + 0x2
-   |       |                       ^-^ when checking this argument has type int('ex1#)
+   |   fail/add_vec_lit_old.sail:14.23-26:
+   |   14 |let x : range(0, 30) = 0xF + 0x2
+   |      |                       ^-^ checking function argument has type int('ex1#)
+   |      | Type mismatch between int('ex1#) and bitvector(4)
diff --git a/test/typecheck/fail/and_let_bool.expect b/test/typecheck/fail/and_let_bool.expect
index e5e9e9e96..82770e21b 100644
--- a/test/typecheck/fail/and_let_bool.expect
+++ b/test/typecheck/fail/and_let_bool.expect
@@ -1,7 +1,7 @@
 Type error:
 fail/and_let_bool.sail:6.11-42:
 6 |  and_bool(let y : bool = x in not_bool(y), x)
-  |           ^-----------------------------^
+  |           ^-----------------------------^ checking function argument has type bool('p)
   | The type variable 'ex16# would leak into an outer scope.
   | 
   | Try adding a type annotation to this expression.
@@ -10,6 +10,3 @@
   | 6 |  and_bool(let y : bool = x in not_bool(y), x)
   |   |               ^
   |   | Type variable 'ex16# was introduced here
-  | fail/and_let_bool.sail:6.11-42:
-  | 6 |  and_bool(let y : bool = x in not_bool(y), x)
-  |   |           ^-----------------------------^ when checking this argument has type bool('p)
diff --git a/test/typecheck/fail/bv_update_error.expect b/test/typecheck/fail/bv_update_error.expect
index 7a0b87e55..6778abe8f 100644
--- a/test/typecheck/fail/bv_update_error.expect
+++ b/test/typecheck/fail/bv_update_error.expect
@@ -2,6 +2,4 @@
 fail/bv_update_error.sail:13.18-22:
 13 |  let _ = [v with FIEL = 0xFF];
    |                  ^--^
-   | No function type found for _update_b_FIEL
-   | 
-   | Did you mean _update_b_FIELD?
+   | Function _update_b_FIEL not found. Did you mean _update_b_FIELD?
diff --git a/test/typecheck/fail/issue277.expect b/test/typecheck/fail/issue277.expect
index 06da70169..87e74a14a 100644
--- a/test/typecheck/fail/issue277.expect
+++ b/test/typecheck/fail/issue277.expect
@@ -1,9 +1,6 @@
 Type error:
 fail/issue277.sail:12.8-20:
 12 |    foo(sizeof(xlen))
-   |        ^----------^
+   |        ^----------^ checking function argument has type int(32)
    | int(64) is not a subtype of int(32)
    | as 64 == 32 could not be proven
-   | fail/issue277.sail:12.8-20:
-   | 12 |    foo(sizeof(xlen))
-   |    |        ^----------^ when checking this argument has type int(32)
diff --git a/test/typecheck/fail/missing_tick.expect b/test/typecheck/fail/missing_tick.expect
index bac2ee3ea..5218dff5d 100644
--- a/test/typecheck/fail/missing_tick.expect
+++ b/test/typecheck/fail/missing_tick.expect
@@ -12,4 +12,4 @@
   |   | Caused by fail/missing_tick.sail:5.16-17:
   |   | 5 |type foo = bits(x)
   |   |   |                ^
-  |   | Undefined type synonym x
+  |   |   | Undefined type synonym x
diff --git a/test/typecheck/fail/no_function.expect b/test/typecheck/fail/no_function.expect
index c5ce20804..013cb0905 100644
--- a/test/typecheck/fail/no_function.expect
+++ b/test/typecheck/fail/no_function.expect
@@ -2,6 +2,4 @@
 fail/no_function.sail:10.10-17:
 10 |  let _ = foo_baz()
    |          ^-----^
-   | No function type found for foo_baz
-   | 
-   | Did you mean foo_bar?
+   | Function foo_baz not found. Did you mean foo_bar?
diff --git a/test/typecheck/fail/no_function2.expect b/test/typecheck/fail/no_function2.expect
index 73769c16f..df833d793 100644
--- a/test/typecheck/fail/no_function2.expect
+++ b/test/typecheck/fail/no_function2.expect
@@ -2,6 +2,4 @@
 fail/no_function2.sail:8.10-17:
 8 |  let _ = foo_baz()
   |          ^-----^
-  | No function type found for foo_baz
-  | 
-  | Did you mean foo_quux?
+  | Function foo_baz not found. Did you mean foo_quux?
diff --git a/test/typecheck/fail/no_function3.expect b/test/typecheck/fail/no_function3.expect
index 99218b2bf..bfbdad82c 100644
--- a/test/typecheck/fail/no_function3.expect
+++ b/test/typecheck/fail/no_function3.expect
@@ -2,4 +2,4 @@
 fail/no_function3.sail:6.10-17:
 6 |  let _ = foo_baz()
   |          ^-----^
-  | No function type found for foo_baz
+  | Function foo_baz not found
diff --git a/test/typecheck/fail/scattered_union_rec.expect b/test/typecheck/fail/scattered_union_rec.expect
index 48c65c511..b8972ef25 100644
--- a/test/typecheck/fail/scattered_union_rec.expect
+++ b/test/typecheck/fail/scattered_union_rec.expect
@@ -12,7 +12,7 @@
   |   | Caused by fail/scattered_union_rec.sail:6.24-25:
   |   | 6 |union clause U = Ctor : E
   |   |   |                        ^
-  |   | Undefined type E
+  |   |   | Undefined type E
   | 
   | Caused by fail/scattered_union_rec.sail:6.13-14:
   | 6 |union clause U = Ctor : E
diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect
index 1892581a9..3a7248c6a 100644
--- a/test/typecheck/fail/struct_rec.expect
+++ b/test/typecheck/fail/struct_rec.expect
@@ -14,4 +14,4 @@
   |   | Caused by fail/struct_rec.sail:3.10-11:
   |   | 3 |  field : S
   |   |   |          ^
-  |   | Undefined type S
+  |   |   | Undefined type S
diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect
index cfea8c001..acd37b41e 100644
--- a/test/typecheck/fail/synonym_rec.expect
+++ b/test/typecheck/fail/synonym_rec.expect
@@ -12,4 +12,4 @@
   |   | Caused by fail/synonym_rec.sail:2.9-10:
   |   | 2 |type T = T
   |   |   |         ^
-  |   | Undefined type T
+  |   |   | Undefined type T
diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect
index 2adc62056..348f8692f 100644
--- a/test/typecheck/fail/union_rec.expect
+++ b/test/typecheck/fail/union_rec.expect
@@ -14,4 +14,4 @@
   |   | Caused by fail/union_rec.sail:3.9-10:
   |   | 3 |  Ctor : U
   |   |   |         ^
-  |   | Undefined type U
+  |   |   | Undefined type U
diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect
index 77c7e0c77..99e767b1c 100644
--- a/test/typecheck/fail/union_recf.expect
+++ b/test/typecheck/fail/union_recf.expect
@@ -14,4 +14,4 @@
   |   | Caused by fail/union_recf.sail:3.9-10:
   |   | 3 |  Ctor : U -> U
   |   |   |         ^
-  |   | Undefined type U
+  |   |   | Undefined type U
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index c832f69b6..8303843a2 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -12,4 +12,4 @@
    |    | Caused by pass/constrained_struct/v1.sail:10.18-26:
    |    | 10 |type MyStruct64 = MyStruct(65)
    |    |    |                  ^------^
-   |    | Could not prove 65 in {32, 64} for type constructor MyStruct
+   |    |    | Could not prove 65 in {32, 64} for type constructor MyStruct
diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect
index a67d22fef..aa05a8d3c 100644
--- a/test/typecheck/pass/existential_ast/v1.expect
+++ b/test/typecheck/pass/existential_ast/v1.expect
@@ -7,8 +7,5 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 Type error:
 pass/existential_ast/v1.sail:46.7-21:
 46 |  Some(Ctor2(y, x, c))
-   |       ^------------^
+   |       ^------------^ checking function argument has type ast
    | range(0, 31) is not contained within range(0, 31)
-   | pass/existential_ast/v1.sail:46.7-21:
-   | 46 |  Some(Ctor2(y, x, c))
-   |    |       ^------------^ when checking this argument has type (range(0, 31), int('ex262#), bitvector(4))
diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect
index 901d3d04e..e768a5be3 100644
--- a/test/typecheck/pass/existential_ast/v2.expect
+++ b/test/typecheck/pass/existential_ast/v2.expect
@@ -7,8 +7,5 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 Type error:
 pass/existential_ast/v2.sail:39.7-21:
 39 |  Some(Ctor2(y, x, c))
-   |       ^------------^
+   |       ^------------^ checking function argument has type ast
    | range(0, 30) is not contained within range(0, 30)
-   | pass/existential_ast/v2.sail:39.7-21:
-   | 39 |  Some(Ctor2(y, x, c))
-   |    |       ^------------^ when checking this argument has type (range(0, 30), int('ex262#), bitvector(4))
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index f22f56380..c18c3802f 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -7,9 +7,6 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 Type error:
 pass/existential_ast/v3.sail:26.7-21:
 26 |  Some(Ctor1(a, x, c))
-   |       ^------------^
+   |       ^------------^ checking function argument has type ast
    | Could not resolve quantifiers for Ctor1
    | * 'ex343# in {32, 64}
-   | pass/existential_ast/v3.sail:26.7-21:
-   | 26 |  Some(Ctor1(a, x, c))
-   |    |       ^------------^ when checking this argument has type ast
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 4d6a90a04..1a0cef9c8 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -1,9 +1,6 @@
 Type error:
 pass/existential_ast3/v3.sail:25.9-40:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
-   |         ^-----------------------------^
+   |         ^-----------------------------^ checking function argument has type ast
    | Could not resolve quantifiers for Ctor
    | * (64 in {32, 64} & (0 <= 'ex330# & 'ex330# < 64))
-   | pass/existential_ast3/v3.sail:25.9-40:
-   | 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
-   |    |         ^-----------------------------^ when checking this argument has type ast
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 45a906069..e455150e9 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -7,9 +7,6 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 Type error:
 pass/global_type_var/v1.sail:21.13-15:
 21 |let _ = test(32)
-   |             ^^
+   |             ^^ checking function argument has type int('size)
    | int(32) is not a subtype of int('size)
    | as 32 == 'size could not be proven
-   | pass/global_type_var/v1.sail:21.13-15:
-   | 21 |let _ = test(32)
-   |    |             ^^ when checking this argument has type int('size)
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 4b9e58cb2..780d48a39 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -7,9 +7,6 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
 Type error:
 pass/global_type_var/v2.sail:21.13-15:
 21 |let _ = test(64)
-   |             ^^
+   |             ^^ checking function argument has type int('size)
    | int(64) is not a subtype of int('size)
    | as 64 == 'size could not be proven
-   | pass/global_type_var/v2.sail:21.13-15:
-   | 21 |let _ = test(64)
-   |    |             ^^ when checking this argument has type int('size)
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index ca0839e71..40c7e8932 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -1,16 +1,19 @@
 Type error:
 pass/if_infer/v1.sail:10.10-37:
 10 |  let _ = 0b100[if R then 0 else f()];
-   |          ^-------------------------^
+   |          ^-------------------------^ vector_access
    | No overloading for vector_access, tried:
    | * bitvector_access
-   |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex241# & 'ex241# < 3)
+   |   pass/if_infer/v1.sail:10.10-37:
+   |   10 |  let _ = 0b100[if R then 0 else f()];
+   |      |          ^-------------------------^
+   |      | Could not resolve quantifiers for bitvector_access
+   |      | * (0 <= 'ex241# & 'ex241# < 3)
    | * plain_vector_access
-   |    Type mismatch between vector('n, 'a) and bitvector(3)
-   |    pass/if_infer/v1.sail:10.10-15:
-   |    10 |  let _ = 0b100[if R then 0 else f()];
-   |       |          ^---^ when checking this argument has type vector('n, 'a)
+   |   pass/if_infer/v1.sail:10.10-15:
+   |   10 |  let _ = 0b100[if R then 0 else f()];
+   |      |          ^---^ checking function argument has type vector('n, 'a)
+   |      | Type mismatch between vector('n, 'a) and bitvector(3)
    | 
    | Caused by pass/if_infer/v1.sail:10.10-37:
    | 10 |  let _ = 0b100[if R then 0 else f()];
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index f157da429..60cc2915a 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -1,16 +1,19 @@
 Type error:
 pass/if_infer/v2.sail:10.10-38:
 10 |  let _ = 0b1001[if R then 0 else f()];
-   |          ^--------------------------^
+   |          ^--------------------------^ vector_access
    | No overloading for vector_access, tried:
    | * bitvector_access
-   |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex241# & 'ex241# < 4)
+   |   pass/if_infer/v2.sail:10.10-38:
+   |   10 |  let _ = 0b1001[if R then 0 else f()];
+   |      |          ^--------------------------^
+   |      | Could not resolve quantifiers for bitvector_access
+   |      | * (0 <= 'ex241# & 'ex241# < 4)
    | * plain_vector_access
-   |    Type mismatch between vector('n, 'a) and bitvector(4)
-   |    pass/if_infer/v2.sail:10.10-16:
-   |    10 |  let _ = 0b1001[if R then 0 else f()];
-   |       |          ^----^ when checking this argument has type vector('n, 'a)
+   |   pass/if_infer/v2.sail:10.10-16:
+   |   10 |  let _ = 0b1001[if R then 0 else f()];
+   |      |          ^----^ checking function argument has type vector('n, 'a)
+   |      | Type mismatch between vector('n, 'a) and bitvector(4)
    | 
    | Caused by pass/if_infer/v2.sail:10.10-38:
    | 10 |  let _ = 0b1001[if R then 0 else f()];
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index bda998104..da9901dc2 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -1,16 +1,16 @@
 Type error:
 pass/if_infer/v3.sail:10.10-38:
 10 |  let _ = 0b1001[if R then 0 else f()];
-   |          ^--------------------------^
+   |          ^--------------------------^ vector_access
    | No overloading for vector_access, tried:
    | * bitvector_access
-   |    Numeric type is non-simple
-   |    pass/if_infer/v3.sail:10.17-37:
-   |    10 |  let _ = 0b1001[if R then 0 else f()];
-   |       |                 ^------------------^ when checking this argument has type int('m)
+   |   pass/if_infer/v3.sail:10.17-37:
+   |   10 |  let _ = 0b1001[if R then 0 else f()];
+   |      |                 ^------------------^ checking function argument has type int('m)
+   |      | Numeric type is non-simple
    | 
-   | Also tried: plain_vector_access
-   | These seem less likely, use --explain-all-overloads to see full details
+   | Also tried plain_vector_access
+   | This seems less likely, use --explain-all-overloads to see full details
    | 
    | Caused by pass/if_infer/v3.sail:10.10-38:
    | 10 |  let _ = 0b1001[if R then 0 else f()];
diff --git a/test/typecheck/pass/poly_vector/v1.expect b/test/typecheck/pass/poly_vector/v1.expect
index cc7ef85ec..a3088aa6a 100644
--- a/test/typecheck/pass/poly_vector/v1.expect
+++ b/test/typecheck/pass/poly_vector/v1.expect
@@ -1,8 +1,13 @@
 Type error:
 pass/poly_vector/v1.sail:17.5-24:
 17 |  if my_length(xs) == 32 then {
-   |     ^-----------------^
-   | Type mismatch between vector('n, 'a) and bitvector(32)
-   | pass/poly_vector/v1.sail:17.15-17:
-   | 17 |  if my_length(xs) == 32 then {
-   |    |               ^^ when checking this argument has type vector('n, 'a)
+   |     ^-----------------^ (operator ==)
+   | No overloading for (operator ==), tried:
+   | * eq_int
+   |   pass/poly_vector/v1.sail:17.15-17:
+   |   17 |  if my_length(xs) == 32 then {
+   |      |               ^^ checking function argument has type int('n)
+   |      | Type mismatch between vector('n, 'a) and bitvector(32)
+   | 
+   | Also tried: eq_bit, eq_bool, eq_unit, eq_bit, eq_bits, eq_string
+   | These seem less likely, use --explain-all-overloads to see full details
diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect
index 0613847b2..543c09387 100644
--- a/test/typecheck/pass/reg_32_64/v1.expect
+++ b/test/typecheck/pass/reg_32_64/v1.expect
@@ -7,13 +7,16 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
 Type error:
 pass/reg_32_64/v1.sail:35.2-6:
 35 |  R(0) = 0xCAFE_CAFE_0000_00;
-   |  ^--^
+   |  ^--^ R
    | No overloading for R, tried:
    | * set_R
-   |    Could not resolve quantifiers for set_R
-   |    * (regno(0) & 56 in {32, 64})
+   |   pass/reg_32_64/v1.sail:35.2-6:
+   |   35 |  R(0) = 0xCAFE_CAFE_0000_00;
+   |      |  ^--^
+   |      | Could not resolve quantifiers for set_R
+   |      | * (regno(0) & 56 in {32, 64})
    | * get_R
-   |    Type mismatch between int('r) and bitvector(56)
-   |    pass/reg_32_64/v1.sail:35.9-28:
-   |    35 |  R(0) = 0xCAFE_CAFE_0000_00;
-   |       |         ^-----------------^ when checking this argument has type int('r)
+   |   pass/reg_32_64/v1.sail:35.9-28:
+   |   35 |  R(0) = 0xCAFE_CAFE_0000_00;
+   |      |         ^-----------------^ checking function argument has type int('r)
+   |      | Type mismatch between int('r) and bitvector(56)
diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect
index cc1045c7a..250c54dd3 100644
--- a/test/typecheck/pass/reg_32_64/v3.expect
+++ b/test/typecheck/pass/reg_32_64/v3.expect
@@ -7,18 +7,15 @@ Explicit effect annotations are deprecated. They are no longer used and can be r
 Type error:
 pass/reg_32_64/v3.sail:29.2-27:
 29 |  reg_deref(R)['d - 1 .. 0]
-   |  ^-----------------------^
+   |  ^-----------------------^ checking function argument has type int('m)
    | No overloading for (operator -), tried:
    | * sub_atom
-   |    Cannot re-write sizeof('d)
-   |    pass/reg_32_64/v3.sail:29.15-17:
-   |    29 |  reg_deref(R)['d - 1 .. 0]
-   |       |               ^^ when checking this argument has type int('n)
+   |   pass/reg_32_64/v3.sail:29.15-17:
+   |   29 |  reg_deref(R)['d - 1 .. 0]
+   |      |               ^^ checking function argument has type int('n)
+   |      | Cannot re-write sizeof('d)
    | * sub_int
-   |    Cannot re-write sizeof('d)
-   |    pass/reg_32_64/v3.sail:29.15-17:
-   |    29 |  reg_deref(R)['d - 1 .. 0]
-   |       |               ^^ when checking this argument has type int('ex174#)
-   | pass/reg_32_64/v3.sail:29.15-21:
-   | 29 |  reg_deref(R)['d - 1 .. 0]
-   |    |               ^----^ when checking this argument has type int('m)
+   |   pass/reg_32_64/v3.sail:29.15-17:
+   |   29 |  reg_deref(R)['d - 1 .. 0]
+   |      |               ^^ checking function argument has type int('ex174#)
+   |      | Cannot re-write sizeof('d)
diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect
index e069441b0..371ebf000 100644
--- a/test/typecheck/pass/shadow_let/v1.expect
+++ b/test/typecheck/pass/shadow_let/v1.expect
@@ -1,9 +1,6 @@
 Type error:
 pass/shadow_let/v1.sail:13.6-7:
 13 |  bar(y);
-   |      ^
+   |      ^ checking function argument has type int(2)
    | int('y) is not a subtype of int(2)
    | as 'y == 2 could not be proven
-   | pass/shadow_let/v1.sail:13.6-7:
-   | 13 |  bar(y);
-   |    |      ^ when checking this argument has type int(2)
diff --git a/test/typecheck/pass/string_literal_type/v1.expect b/test/typecheck/pass/string_literal_type/v1.expect
index c995bda5e..baf700bb7 100644
--- a/test/typecheck/pass/string_literal_type/v1.expect
+++ b/test/typecheck/pass/string_literal_type/v1.expect
@@ -1,8 +1,5 @@
 Type error:
 pass/string_literal_type/v1.sail:16.7-23:
 16 |  test(concat_str(x, z))
-   |       ^--------------^
+   |       ^--------------^ checking function argument has type string_literal
    | string is not a subtype of string_literal
-   | pass/string_literal_type/v1.sail:16.7-23:
-   | 16 |  test(concat_str(x, z))
-   |    |       ^--------------^ when checking this argument has type string_literal
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index 11c4b1386..f6ff7bce5 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -1,16 +1,19 @@
 Type error:
 pass/vec_length/v1.sail:6.10-15:
 6 |  let y = x[10];
-  |          ^---^
+  |          ^---^ vector_access
   | No overloading for vector_access, tried:
   | * bitvector_access
-  |    Could not resolve quantifiers for bitvector_access
-  |    * (0 <= 10 & 10 < 8)
+  |   pass/vec_length/v1.sail:6.10-15:
+  |   6 |  let y = x[10];
+  |     |          ^---^
+  |     | Could not resolve quantifiers for bitvector_access
+  |     | * (0 <= 10 & 10 < 8)
   | * plain_vector_access
-  |    Type mismatch between vector('n, 'a) and bitvector(8)
-  |    pass/vec_length/v1.sail:6.10-11:
-  |    6 |  let y = x[10];
-  |      |          ^ when checking this argument has type vector('n, 'a)
+  |   pass/vec_length/v1.sail:6.10-11:
+  |   6 |  let y = x[10];
+  |     |          ^ checking function argument has type vector('n, 'a)
+  |     | Type mismatch between vector('n, 'a) and bitvector(8)
   | 
   | Caused by pass/vec_length/v1.sail:6.10-15:
   | 6 |  let y = x[10];
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index 9a0bf9955..41dae45bc 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -1,16 +1,19 @@
 Type error:
 pass/vec_length/v1_inc.sail:6.10-15:
 6 |  let y = x[10];
-  |          ^---^
+  |          ^---^ vector_access
   | No overloading for vector_access, tried:
   | * bitvector_access
-  |    Could not resolve quantifiers for bitvector_access
-  |    * (0 <= 10 & 10 < 8)
+  |   pass/vec_length/v1_inc.sail:6.10-15:
+  |   6 |  let y = x[10];
+  |     |          ^---^
+  |     | Could not resolve quantifiers for bitvector_access
+  |     | * (0 <= 10 & 10 < 8)
   | * plain_vector_access
-  |    Type mismatch between vector('n, 'a) and bitvector(8)
-  |    pass/vec_length/v1_inc.sail:6.10-11:
-  |    6 |  let y = x[10];
-  |      |          ^ when checking this argument has type vector('n, 'a)
+  |   pass/vec_length/v1_inc.sail:6.10-11:
+  |   6 |  let y = x[10];
+  |     |          ^ checking function argument has type vector('n, 'a)
+  |     | Type mismatch between vector('n, 'a) and bitvector(8)
   | 
   | Caused by pass/vec_length/v1_inc.sail:6.10-15:
   | 6 |  let y = x[10];
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index c5fb2c3d5..989803e58 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -1,13 +1,16 @@
 Type error:
 pass/vec_length/v2.sail:7.10-25:
 7 |  let z = [x with 10 = y];
-  |          ^-------------^
+  |          ^-------------^ vector_update
   | No overloading for vector_update, tried:
   | * bitvector_update
-  |    Could not resolve quantifiers for bitvector_update
-  |    * (0 <= 10 & 10 < 8)
+  |   pass/vec_length/v2.sail:7.10-25:
+  |   7 |  let z = [x with 10 = y];
+  |     |          ^-------------^
+  |     | Could not resolve quantifiers for bitvector_update
+  |     | * (0 <= 10 & 10 < 8)
   | * plain_vector_update
-  |    Type mismatch between vector('n, 'a) and bitvector(8)
-  |    pass/vec_length/v2.sail:7.11-12:
-  |    7 |  let z = [x with 10 = y];
-  |      |           ^ when checking this argument has type vector('n, 'a)
+  |   pass/vec_length/v2.sail:7.11-12:
+  |   7 |  let z = [x with 10 = y];
+  |     |           ^ checking function argument has type vector('n, 'a)
+  |     | Type mismatch between vector('n, 'a) and bitvector(8)
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index 7ae810489..7c374624d 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -1,13 +1,16 @@
 Type error:
 pass/vec_length/v2_inc.sail:7.10-25:
 7 |  let z = [x with 10 = y];
-  |          ^-------------^
+  |          ^-------------^ vector_update
   | No overloading for vector_update, tried:
   | * bitvector_update
-  |    Could not resolve quantifiers for bitvector_update
-  |    * (0 <= 10 & 10 < 8)
+  |   pass/vec_length/v2_inc.sail:7.10-25:
+  |   7 |  let z = [x with 10 = y];
+  |     |          ^-------------^
+  |     | Could not resolve quantifiers for bitvector_update
+  |     | * (0 <= 10 & 10 < 8)
   | * plain_vector_update
-  |    Type mismatch between vector('n, 'a) and bitvector(8)
-  |    pass/vec_length/v2_inc.sail:7.11-12:
-  |    7 |  let z = [x with 10 = y];
-  |      |           ^ when checking this argument has type vector('n, 'a)
+  |   pass/vec_length/v2_inc.sail:7.11-12:
+  |   7 |  let z = [x with 10 = y];
+  |     |           ^ checking function argument has type vector('n, 'a)
+  |     | Type mismatch between vector('n, 'a) and bitvector(8)
diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect
index d7848bd7c..fe99575c5 100644
--- a/test/typecheck/pass/vec_length/v3.expect
+++ b/test/typecheck/pass/vec_length/v3.expect
@@ -6,13 +6,18 @@
    |--^
    | No overloading for vector_access, tried:
    | * bitvector_access
-   |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 10 & 10 < 8)
+   |   pass/vec_length/v3.sail:6.10-12.3:
+   |   6  |  let y = x[
+   |      |          ^-
+   |   12 |  ];
+   |      |--^
+   |      | Could not resolve quantifiers for bitvector_access
+   |      | * (0 <= 10 & 10 < 8)
    | * plain_vector_access
-   |    Type mismatch between vector('n, 'a) and bitvector(8)
-   |    pass/vec_length/v3.sail:6.10-11:
-   |    6 |  let y = x[
-   |      |          ^ when checking this argument has type vector('n, 'a)
+   |   pass/vec_length/v3.sail:6.10-11:
+   |   6 |  let y = x[
+   |     |          ^ checking function argument has type vector('n, 'a)
+   |     | Type mismatch between vector('n, 'a) and bitvector(8)
    | 
    | Caused by pass/vec_length/v3.sail:6.10-12.3:
    | 6  |  let y = x[