TC: Fix missing location on generated guards

src/lib/type_check.ml

@@ -2254,10 +2254,14 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
           let inferred_exp = infer_funapp l env f [x; y] uannot (Some typ) in
           expect_subtype env inferred_exp typ
       | Some _ ->
-          let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in
+          let inferred_exp =
+            infer_funapp l env f [x; mk_exp ~loc:(exp_loc y) (E_typ (bool_typ, y))] uannot (Some typ)
+          in
           expect_subtype env inferred_exp typ
       | exception Type_error _ ->
-          let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in
+          let inferred_exp =
+            infer_funapp l env f [x; mk_exp ~loc:(exp_loc y) (E_typ (bool_typ, y))] uannot (Some typ)
+          in
           expect_subtype env inferred_exp typ
     end
   | E_app (f, xs), _ ->
@@ -2550,12 +2554,22 @@ and check_case env pat_typ pexp typ =
   let env = bind_pattern_vector_subranges pat env in
   match bind_pat env pat pat_typ with
   | tpat, env, guards ->
+      let hint_loc l =
+        match guard with
+        | None -> Parse_ast.Hint ("guard created for this pattern", pat_loc pat, l)
+        | Some exp -> Parse_ast.Hint ("combining pattern with guard", exp_loc exp, l)
+      in
       let guard =
         match (guard, guards) with None, h :: t -> Some (h, t) | Some x, l -> Some (x, l) | None, [] -> None
       in
       let guard =
         match guard with
-        | Some (h, t) -> Some (List.fold_left (fun acc guard -> mk_exp (E_app_infix (acc, mk_id "&", guard))) h t)
+        | Some (h, t) ->
+            Some
+              (List.fold_left
+                 (fun acc guard -> mk_exp ~loc:(hint_loc (exp_loc guard)) (E_app_infix (acc, mk_id "&", guard)))
+                 h t
+              )
         | None -> None
       in
       let checked_guard, env' =

src/lib/type_error.ml

@@ -277,9 +277,12 @@ let message_of_type_error type_error =
           (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_function_arg (_, typ, err) -> (
+        let msg, hint = to_message err in
+        match hint with
+        | None -> (msg, Some ("checking function argument has type " ^ string_of_typ typ))
+        | Some _ -> (msg, hint)
+      )
     | 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

test/typecheck/pass/existential_ast/v1.expect

@@ -7,5 +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
+   |       ^------------^ checking function argument has type (range(0, 31), int('ex192#), bitvector(4))
    | range(0, 31) is not contained within range(0, 31)

test/typecheck/pass/existential_ast/v2.expect

@@ -7,5 +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
+   |       ^------------^ checking function argument has type (range(0, 30), int('ex192#), bitvector(4))
    | range(0, 30) is not contained within range(0, 30)

test/typecheck/pass/poly_vector/v1.expect

@@ -1,5 +1,5 @@
 Type error:
 pass/poly_vector/v1.sail:17.5-24:
 17 |  if my_length(xs) == 32 then {
-   |     ^-----------------^ checking function argument has type int('n)
+   |     ^-----------------^ checking function argument has type vector('n, 'a)
    | Type mismatch between vector('n, 'a) and bitvector(32)

test/typecheck/pass/reg_32_64/v3.expect

@@ -7,7 +7,7 @@ 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)
+   |  ^-----------------------^ (operator -)
    | No overloading for (operator -), tried:
    | * sub_atom
    |   pass/reg_32_64/v3.sail:29.15-17: