diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index be45137f4..4360ef7f4 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -3599,6 +3599,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = (* Try to infer the type of the condition - in some cases it may be a constant `true` or `false`, e.g. `xlen == 32`. If that fails check it is a bool without inference. *) let cond' = try irule infer_exp env cond with Type_error _ -> crule check_exp env cond bool_typ in + subtyp (exp_loc cond) env (typ_of cond') bool_typ; (* Constraints to apply when reasoning about the branch types. The condition must be true when evaluating the type of the `then` branch, and false for `else`. *) diff --git a/test/typecheck/fail/non_bool_if.expect b/test/typecheck/fail/non_bool_if.expect new file mode 100644 index 000000000..fa46e5926 --- /dev/null +++ b/test/typecheck/fail/non_bool_if.expect @@ -0,0 +1,5 @@ +Type error: +fail/non_bool_if.sail:2.11-17: +2 |let _ = if "test" then 1 else 2 +  | ^----^ +  | Type mismatch between bool('ex1#) and string diff --git a/test/typecheck/fail/non_bool_if.sail b/test/typecheck/fail/non_bool_if.sail new file mode 100644 index 000000000..125acae44 --- /dev/null +++ b/test/typecheck/fail/non_bool_if.sail @@ -0,0 +1,2 @@ + +let _ = if "test" then 1 else 2