19 files changed, 28 insertions, 318 deletions

diff --git a/test/c/enum_match.sail b/test/c/enum_match.sail
index 591e2695..6c04d9dc 100644
--- a/test/c/enum_match.sail
+++ b/test/c/enum_match.sail
@@ -1,7 +1,8 @@
 
 val "eq_anything" : forall ('a : Type). ('a, 'a) -> bool
+val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
-overload operator == = {eq_anything}
+overload operator == = {eq_atom, eq_anything}
 
 val print = "print_endline" : string -> unit
 
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
index 930c5bc8..e85881f5 100755
--- a/test/c/run_tests.sh
+++ b/test/c/run_tests.sh
@@ -75,7 +75,7 @@ do
 	red "compiling $file" "fail"
     fi;
     rm -f ${file%.sail}.c
-    rm -r ${file%.sail}.result
+    rm -f ${file%.sail}.result
 done
 
 finish_suite "C testing"
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}