From d22c4ff57a27199c4fd26c58aba4f7e86349fec1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 6 Nov 2024 14:38:37 +0000 Subject: [PATCH] TC: Check that we haven't inferred a nonsensical type for if conditions --- src/lib/type_check.ml | 1 + test/typecheck/fail/non_bool_if.expect | 5 +++++ test/typecheck/fail/non_bool_if.sail | 2 ++ 3 files changed, 8 insertions(+) create mode 100644 test/typecheck/fail/non_bool_if.expect create mode 100644 test/typecheck/fail/non_bool_if.sail 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