Porting some minisail changes to sail2 branch

This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in

```
val f : nat -> nat

let x = f(3)
```

whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.

Also:

- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
  pass didn't add type paramemters for newly added type variables in
  generated function parameters.

- Updated string_of_ functions in ast_util to reflect syntax changes

- Fixed a C compilation issue where elements of union type
  constructors were not being coerced between big integers and 64-bit
  integers where appropriate

- Type annotations in patterns now generalise, rather than restrict
  the type of the pattern. This should be safer and easier to handle
  in the various backends. I don't think any code we had was relying
  on this behaviour anyway.

- Add inequality operator to lib/flow.sail

- Fix an issue whereby top-level let bindings with annotations were
  checked incorrectly

17 files changed, 25 insertions, 316 deletions

diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail
deleted file mode 100644
index 66fc0025..00000000
--- a/test/typecheck/pass/case_simple_constraints.sail
+++ /dev/null
@@ -1,17 +0,0 @@
-val plus = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int).
-  (atom('n + 20), atom('m)) -> atom('n + 20 + 'm)
-
-val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10.
-  atom('n) -> atom('n)
-
-val ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n >= 10.
-  atom('n) -> atom('n)
-
-val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N)
-
-function branch x = match x {
-  y : range(10, 30) => y,
-  _ : atom(31) => 'N,
-  _ : range(31, 40) => plus(60, 3)
-}
-and branch _ : range(51, 63) = ten_id('N)
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 178f8003..47343e02 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -41,9 +41,9 @@ function main () = {
     }
   };
   match word {
-    8 : range(0, 8) => x = 32,
-    16 : range(0, 16) => x = 64,
-    32 : range(0, 32) => x = 128
+    8  => x = 32,
+    16 => x = 64,
+    32 => x = 128
   };
   match 0b010101 {
     0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42,
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 8ecba308..c2f05f5c 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -3,4 +3,4 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
 let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
 
 Tried performing type coercion on 4
-Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 33)
+Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index 09bba469..5926bcdb 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -3,4 +3,4 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
 
 Tried performing type coercion on 4
-Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom<'n> with (0 <= 'n & 'n <= 8)
+Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index be1a92a1..c41f2c4b 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 100)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index 13edc200..a17ed112 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 2 & 2 <= 4)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail
index 47b26261..19336fd5 100644
--- a/test/typecheck/pass/flow_gt1.sail
+++ b/test/typecheck/pass/flow_gt1.sail
@@ -1,46 +1,6 @@
-default Order inc
+default Order dec
 
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
-
-overload operator <= = {lteq_atom_range, lteq_range_atom}
-
-overload operator > = {gt_atom_range, gt_range_atom}
-
-overload operator >= = {gteq_atom_range, gteq_range_atom}
+$include <prelude.sail>
 
 val branch : range(0, 63) -> range(0, 63)
 
diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail
index 3ea9d69b..f985cc09 100644
--- a/test/typecheck/pass/flow_gteq1.sail
+++ b/test/typecheck/pass/flow_gteq1.sail
@@ -1,46 +1,6 @@
-default Order inc
+default Order dec
 
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
-
-overload operator <= = {lteq_atom_range, lteq_range_atom}
-
-overload operator > = {gt_atom_range, gt_range_atom}
-
-overload operator >= = {gteq_atom_range, gteq_range_atom}
+$include <prelude.sail>
 
 val branch : range(0, 63) -> range(0, 63)
 
diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail
index e29424be..0dc6dc98 100644
--- a/test/typecheck/pass/flow_lt1.sail
+++ b/test/typecheck/pass/flow_lt1.sail
@@ -1,40 +1,6 @@
-default Order inc
+default Order dec
 
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
+$include <prelude.sail>
 
 val branch : range(0, 63) -> range(0, 63)
 
diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail
index 2c1ad667..3101c608 100644
--- a/test/typecheck/pass/flow_lt2.sail
+++ b/test/typecheck/pass/flow_lt2.sail
@@ -1,40 +1,6 @@
-default Order inc
+default Order dec
 
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
+$include <prelude.sail>
 
 val branch : range(0, 63) -> range(0, 63)
 
diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail
deleted file mode 100644
index afc620b6..00000000
--- a/test/typecheck/pass/flow_lt_assign.sail
+++ /dev/null
@@ -1,47 +0,0 @@
-default Order inc
-
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
-
-val branch : range(0, 63) -> range(0, 63)
-
-function branch x = {
-  y = x;
-  if y < 32 then {
-    y = 31;
-    y + 32
-  } else y - 32
-}
diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail
index c61f93e2..30486c7e 100644
--- a/test/typecheck/pass/flow_lteq1.sail
+++ b/test/typecheck/pass/flow_lteq1.sail
@@ -1,45 +1,5 @@
-default Order inc
+default Order dec
 
-val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (range('n, 'm), atom('o)) -> bool
-
-val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int).
-  (atom('n), range('m, 'o)) -> bool
-
-overload operator + = {add_range}
-
-overload operator - = {sub_range}
-
-overload operator < = {lt_atom_range, lt_range_atom}
-
-overload operator <= = {lteq_atom_range, lteq_range_atom}
-
-overload operator > = {gt_atom_range, gt_range_atom}
-
-overload operator >= = {gteq_atom_range, gteq_range_atom}
+$include <prelude.sail>
 
 function branch x : range(0, 63) -> range(0, 63) = if x <= 32 then x + 31 else x - 33
diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail
deleted file mode 100644
index 2731c2b9..00000000
--- a/test/typecheck/pass/fun_simple_constraints1.sail
+++ /dev/null
@@ -1,15 +0,0 @@
-val plus : forall ('n : Int) ('m : Int).
-  (atom('n + 20), atom('m)) -> atom('n + 20 + 'm)
-
-val minus_ten_id : forall ('n : Int), 'n <= -10. atom('n) -> atom('n)
-
-val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n)
-
-val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N)
-
-function branch x = x
-and branch y : range(10, 30) = y
-and branch _ : atom(31) = 'N
-and branch _ : range(31, 40) = plus(60, 3)
-and branch _ : range(41, 50) = plus('N, minus_ten_id(-53))
-and branch _ : range(51, 63) = ten_id('N)
diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail
deleted file mode 100644
index b6c4eef5..00000000
--- a/test/typecheck/pass/fun_simple_constraints2.sail
+++ /dev/null
@@ -1,15 +0,0 @@
-val plus : forall ('n : Int) ('m : Int).
-  (atom('n + 20), atom('m)) -> atom('n + 20 + 'm)
-
-val minus_ten_id : forall ('n : Int), 'n <= -10. range('n, 'n) -> atom('n)
-
-val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n)
-
-val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N)
-
-function branch x = x
-and branch y : range(10, 30) = y
-and branch _ : atom(31) = 'N
-and branch _ : range(31, 40) = plus(60, 3)
-and branch _ : range(41, 50) = plus('N, minus_ten_id(-53))
-and branch _ : range(51, 63) = ten_id('N)
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index c421cada..d80cb349 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -3,4 +3,6 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 let _ = test(32)
 
 Tried performing type coercion on 32
-Failed because atom<32> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)
+Failed because
+  atom(32) is not a subtype of atom('size)
+  in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 8539ea0f..740c1e2e 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -3,4 +3,6 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 let _ = test(64)
 
 Tried performing type coercion on 64
-Failed because atom<64> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)
+Failed because
+  atom(64) is not a subtype of atom('size)
+  in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64)
diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail
index 9fc753e6..4aac2bed 100644
--- a/test/typecheck/pass/guards.sail
+++ b/test/typecheck/pass/guards.sail
@@ -1,19 +1,6 @@
-infix 4 ==
-infixl 6 /
+default Order dec
 
-val add_int : (int, int) -> int
-
-overload operator + = {add_int}
-
-val eq : forall ('a : Type). ('a, 'a) -> bool
-
-val neq : forall ('a : Type). ('a, 'a) -> bool
-
-overload operator == = {eq}
-
-overload operator != = {neq}
-
-val quotient : (int, int) -> int
+$include <prelude.sail>
 
 overload operator / = {quotient}