4 files changed, 103 insertions, 3 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index d44fd493..05ace284 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2786,6 +2786,25 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
          end
      in
      try_overload ([], Env.get_overloads f env)
+  | E_app (f, [x; y]), _ when string_of_id f = "and_bool" || string_of_id f = "or_bool" ->
+     (* We have to ensure that the type of y in (x || y) and (x && y)
+        is non-empty, otherwise it could force the entire type of the
+        expression to become empty even when unevaluted due to
+        short-circuiting. *)
+     begin match destruct_exist (typ_of (irule infer_exp env y)) with
+     | None | Some (_, NC_aux (NC_true, _), _) ->
+        let inferred_exp = infer_funapp l env f [x; y] (Some typ) in
+        type_coercion env inferred_exp typ
+     | Some _ ->
+        let inferred_exp = infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] (Some typ) in
+        type_coercion env inferred_exp typ
+     | exception Type_error _ ->
+        let inferred_exp = infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] (Some typ) in
+        type_coercion env inferred_exp typ
+     end
+  | E_app (f, xs), _ ->
+     let inferred_exp = infer_funapp l env f xs (Some typ) in
+     type_coercion env inferred_exp typ
   | E_return exp, _ ->
      let checked_exp = match Env.get_ret_typ env with
        | Some ret_typ -> crule check_exp env exp ret_typ
@@ -2795,9 +2814,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_tuple exps, Typ_tup typs when List.length exps = List.length typs ->
      let checked_exps = List.map2 (fun exp typ -> crule check_exp env exp typ) exps typs in
      annot_exp (E_tuple checked_exps) typ
-  | E_app (f, xs), _ ->
-     let inferred_exp = infer_funapp l env f xs (Some typ) in
-     type_coercion env inferred_exp typ
   | E_if (cond, then_branch, else_branch), _ ->
      let cond' = try irule infer_exp env cond with Type_error _ -> crule check_exp env cond bool_typ in
      begin match destruct_exist (typ_of cond') with
@@ -3686,6 +3702,12 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
          end
      in
      try_overload ([], Env.get_overloads f env)
+  | E_app (f, [x; y]) when string_of_id f = "and_bool" || string_of_id f = "or_bool" ->
+     begin match destruct_exist (typ_of (irule infer_exp env y)) with
+     | None | Some (_, NC_aux (NC_true, _), _) -> infer_funapp l env f [x; y] None
+     | Some _ -> infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] None
+     | exception Type_error _ -> infer_funapp l env f [x; mk_exp (E_cast (bool_typ, y))] None
+     end
   | E_app (f, xs) -> infer_funapp l env f xs None
   | E_loop (loop_type, measure, cond, body) ->
      let checked_cond = crule check_exp env cond bool_typ in
diff --git a/test/typecheck/pass/short_circuit_bool_ex.sail b/test/typecheck/pass/short_circuit_bool_ex.sail
new file mode 100644
index 00000000..5cfdc1dc
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex.sail
@@ -0,0 +1,36 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+/*
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+*/
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if ok() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.expect b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
new file mode 100644
index 00000000..fc98db1b
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[short_circuit_bool_ex/v1.sail]:25:36-40
+25 |  if (true | assertive(n) > 0) then true else true
+   |                                    ^--^
+   | Tried performing type coercion from bool(true) to bool(0 == 1) on true
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.sail b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
new file mode 100644
index 00000000..2faf12af
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if bad() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file