diff options
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | test/typecheck/future/bool_constraint.sail | 10 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 5774a46f..cc0b9843 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1997,6 +1997,10 @@ let rec combine_constraint b f x y = match b, x, y with | _, _, _ -> None let rec assert_constraint env b (E_aux (exp_aux, _) as exp) = + match typ_of exp with + | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) -> + Some nc + | _ -> match exp_aux with | E_constraint nc -> Some nc diff --git a/test/typecheck/future/bool_constraint.sail b/test/typecheck/future/bool_constraint.sail new file mode 100644 index 00000000..53994630 --- /dev/null +++ b/test/typecheck/future/bool_constraint.sail @@ -0,0 +1,10 @@ +default Order dec + +$include <prelude.sail> + +val foo : forall ('n : Int) ('b : Bool). + (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)} + +function foo(b, n) = { + if b then n else 3 +}
\ No newline at end of file |