Fix a warning in sail-riscv

Make sure we bind existential type variables introduced by
match head expressions before checking completeness, otherwise
we can miss some obvious cases

src/lib/type_check.ml

@@ -1855,8 +1855,9 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
         if Option.is_some (get_attribute "complete" uannot) || Option.is_some (get_attribute "incomplete" uannot) then
           (checked_cases, fun attrs -> attrs)
         else (
+          let completeness_typ, env = bind_existential (exp_loc exp) None inferred_typ env in
           let ctx = pattern_completeness_ctx env in
-          match PC.is_complete_wildcarded l ctx checked_cases inferred_typ with
+          match PC.is_complete_wildcarded l ctx checked_cases completeness_typ with
           | Some wildcarded -> (wildcarded, add_attribute (gen_loc l) "complete" "")
           | None -> (checked_cases, add_attribute (gen_loc l) "incomplete" "")
         )

test/c/struct_fn_arg.expect

@@ -0,0 +1 @@
+f1 = 3

test/c/struct_fn_arg.sail

@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct S = {
+  f1 : int,
+  f2 : int,
+}
+
+function foo(struct { f1, _ } : S, x : nat) -> unit = {
+  print_int("f1 = ", f1);
+}
+
+function main() -> unit = {
+  foo(struct { f1 = 3, f2 = 4 }, 5);
+}

test/pattern_completeness/set_match.sail

@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+val foo : unit -> {1, 2, 3}
+
+function bar() -> unit = {
+  match foo() {
+    1 => (),
+    2 => (),
+    3 => (),
+  }
+}

test/typecheck/struct_fn_arg.sail

@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct S = {
+  f1 : int,
+  f2 : int,
+}
+
+function foo(struct { f1, _ } : S, x : nat) -> unit = {
+  print_int("f1 = ", f1);
+}
+
+function main() -> unit = {
+  foo(struct { f1 = 3, f2 = 4 }, 5);
+}