Be more careful when flow-typing loops

Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.

3 files changed, 24 insertions, 0 deletions

diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail
new file mode 100644
index 00000000..6d63f2e8
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _not_prove(constraint(false));
+  } until (false);
+}
diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect
new file mode 100644
index 00000000..9d561e11
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[repeat_constraint/v1.sail]:7:4-29
+7 |    _prove(constraint(false));
+  |    ^-----------------------^
+  | Cannot prove false
+  | 
diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail
new file mode 100644
index 00000000..5dd2f513
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _prove(constraint(false));
+  } until (false);
+}