diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index edfb6e4d4..725dabcc7 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -54,20 +54,20 @@ $include <vector_dec.sail>
 
 /* External definitions not in the usual asl prelude */
 
-val extzv = {lem: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv = pure {lem: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extzv(m, v) = {
   if m < 'n then truncate(v, m) else sail_zero_extend(v, m)
 }
 
-val extsv = {lem: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extsv = pure {lem: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extsv(m, v) = {
   if m < 'n then truncate(v, m) else sail_sign_extend(v, m)
 }
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
-val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_in = pure "zeroExtend" : forall 'n. bits('n) -> bits('n)
+val bitvector_cast_out = pure "zeroExtend" : forall 'n. bits('n) -> bits('n)
 
 /* Builtins for the rewrites */
 val string_of_bits_subrange = pure "string_of_bits_subrange" : forall 'n. (bits('n), int, int) -> string
@@ -75,21 +75,21 @@ val string_of_bits_subrange = pure "string_of_bits_subrange" : forall 'n. (bits(
 /* Definitions for the rewrites */
 
 val is_zero_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
+  (bits('n), int, int) -> bool
 
 function is_zero_subrange (xs, i, j) = {
   (xs & slice_mask(j, i-j+1)) == extzv([bitzero] : bits(1))
 }
 
 val is_zeros_slice : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
+  (bits('n), int, int) -> bool
 
 function is_zeros_slice (xs, i, l) = {
   (xs & slice_mask(i, l)) == extzv([bitzero] : bits(1))
 }
 
 val is_ones_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
+  (bits('n), int, int) -> bool
 
 function is_ones_subrange (xs, i, j) = {
   let m : bits('n) = slice_mask(j,i-j+1) in
@@ -97,7 +97,7 @@ function is_ones_subrange (xs, i, j) = {
 }
 
 val is_ones_slice : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
+  (bits('n), int, int) -> bool
 
 function is_ones_slice (xs, i, j) = {
   let m : bits('n) = slice_mask(i,j) in
@@ -105,7 +105,7 @@ function is_ones_slice (xs, i, j) = {
 }
 
 val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
-  (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
+  (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r)
 
 function slice_slice_concat (r, xs, i, l, ys, i', l') = {
   let xs = sail_shiftright(xs & slice_mask(i,l), i) in
@@ -114,7 +114,7 @@ function slice_slice_concat (r, xs, i, l, ys, i', l') = {
 }
 
 val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0.
-  (bits('n), int, atom('p), atom('q)) -> bits('p + 'q) effect pure
+  (bits('n), int, atom('p), atom('q)) -> bits('p + 'q)
 
 function slice_zeros_concat (xs, i, l, l') = {
   let xs = sail_shiftright(xs & slice_mask(i,l), i) in
@@ -122,7 +122,7 @@ function slice_zeros_concat (xs, i, l, l') = {
 }
 
 val subrange_zeros_concat : forall 'n 'hi 'lo 'q, 'n >= 0 & 'hi - 'lo + 1 + 'q >= 0.
-  (bits('n), atom('hi), atom('lo), atom('q)) -> bits('hi - 'lo + 1 + 'q) effect pure
+  (bits('n), atom('hi), atom('lo), atom('q)) -> bits('hi - 'lo + 1 + 'q)
 
 function subrange_zeros_concat (xs, hi, lo, l') =
   slice_zeros_concat(xs, lo, hi - lo + 1, l')
@@ -130,7 +130,7 @@ function subrange_zeros_concat (xs, hi, lo, l') =
 /* Assumes initial vectors are of equal size */
 
 val subrange_subrange_eq : forall 'n, 'n >= 0.
-  (bits('n), int, int, bits('n), int, int) -> bool effect pure
+  (bits('n), int, int, bits('n), int, int) -> bool
 
 function subrange_subrange_eq (xs, i, j, ys, i', j') = {
   let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
@@ -139,7 +139,7 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = {
 }
 
 val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0.
-  (implicit('s), bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
+  (implicit('s), bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s)
 
 function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
   let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
@@ -148,7 +148,7 @@ function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m)
 
 function place_subrange(m,xs,i,j,shift) = {
   let xs = sail_shiftright(xs & slice_mask(j,i-j+1), j) in
@@ -156,7 +156,7 @@ function place_subrange(m,xs,i,j,shift) = {
 }
 
 val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m)
 
 function place_slice(m,xs,i,l,shift) = {
   let xs = sail_shiftright(xs & slice_mask(i,l), i) in
@@ -164,7 +164,7 @@ function place_slice(m,xs,i,l,shift) = {
 }
 
 val set_slice_zeros : forall 'n, 'n >= 0.
-  (implicit('n), bits('n), int, int) -> bits('n) effect pure
+  (implicit('n), bits('n), int, int) -> bits('n)
 
 function set_slice_zeros(n, xs, i, l) = {
   let ys : bits('n) = slice_mask(n, i, l) in
@@ -172,13 +172,13 @@ function set_slice_zeros(n, xs, i, l) = {
 }
 
 val set_subrange_zeros : forall 'n, 'n >= 0.
-  (implicit('n), bits('n), int, int) -> bits('n) effect pure
+  (implicit('n), bits('n), int, int) -> bits('n)
 
 function set_subrange_zeros(n, xs, hi, lo) =
   set_slice_zeros(n, xs, lo, hi - lo + 1)
 
 val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m)
 
 function zext_slice(m,xs,i,l) = {
   let xs = sail_shiftright(xs & slice_mask(i,l), i) in
@@ -186,12 +186,12 @@ function zext_slice(m,xs,i,l) = {
 }
 
 val zext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m)
 
 function zext_subrange(m, xs, i, j) = zext_slice(m, xs, j, i - j + 1)
 
 val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m)
 
 function sext_slice(m,xs,i,l) = {
   let xs = sail_arith_shiftright(sail_shiftleft((xs & slice_mask(i,l)), ('n - i - l)), 'n - l) in
@@ -199,19 +199,19 @@ function sext_slice(m,xs,i,l) = {
 }
 
 val sext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m)
 
 function sext_subrange(m, xs, i, j) = sext_slice(m, xs, j, i - j + 1)
 
 val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m)
 
 function place_slice_signed(m,xs,i,l,shift) = {
   sail_shiftleft(sext_slice(m, xs, i, l), shift)
 }
 
 val place_subrange_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m)
 
 function place_subrange_signed(m,xs,i,j,shift) = {
   place_slice_signed(m, xs, j, i-j+1, shift)
@@ -220,7 +220,7 @@ function place_subrange_signed(m,xs,i,j,shift) = {
 /* This has different names in the aarch64 prelude (UInt) and the other
    preludes (unsigned).  To avoid variable name clashes, we redeclare it
    here with a suitably awkward name. */
-val _builtin_unsigned = {
+val _builtin_unsigned = pure {
   ocaml: "uint",
   lem: "uint",
   interpreter: "uint",
@@ -232,7 +232,7 @@ val _builtin_unsigned = {
    they agree on positive values.  We use this here to give more precise return
    types for unsigned_slice and unsigned_subrange. */
 
-val _builtin_mod_nat = {
+val _builtin_mod_nat = pure {
   smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
@@ -242,10 +242,10 @@ val _builtin_mod_nat = {
 
 /* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return
    type of pow2, as SMT solvers tend to have problems with exponentiation. */
-val _builtin_pow2 = "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}
+val _builtin_pow2 = pure "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}
 
 val unsigned_slice : forall 'n 'l, 'n >= 0 & 'l >= 0.
-  (bits('n), int, int('l)) -> {'m, 0 <= 'm < 2 ^ 'l. int('m)} effect pure
+  (bits('n), int, int('l)) -> {'m, 0 <= 'm < 2 ^ 'l. int('m)}
 
 function unsigned_slice(xs,i,l) = {
   let xs = sail_shiftright(xs & slice_mask(i,l), i) in
@@ -253,7 +253,7 @@ function unsigned_slice(xs,i,l) = {
 }
 
 val unsigned_subrange : forall 'n 'i 'j, 'n >= 0 & ('i - 'j) >= 0.
-  (bits('n), int('i), int('j)) -> {'m, 0 <= 'm < 2 ^ ('i - 'j + 1). int('m)} effect pure
+  (bits('n), int('i), int('j)) -> {'m, 0 <= 'm < 2 ^ ('i - 'j + 1). int('m)}
 
 function unsigned_subrange(xs,i,j) = {
   let xs = sail_shiftright(xs & slice_mask(j,i-j+1), i) in
@@ -261,7 +261,7 @@ function unsigned_subrange(xs,i,j) = {
 }
 
 
-val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n) effect pure
+val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n)
 
 function zext_ones(n, m) = {
   let v : bits('n) = extsv([bitone] : bits(1)) in
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index 6e1759814..d3be70220 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -5,10 +5,10 @@ $include <arith.sail>
 $include <flow.sail>
 $include <vector_dec.sail>
 
-val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val neq_vec = pure {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 function neq_vec (x, y) = not_bool(x == y)
 overload operator != = {neq_vec}
-val UInt = {
+val UInt = pure {
   ocaml: "uint",
   lem: "uint",
   interpreter: "uint",
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 05eccc994..e4febb6d5 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -2,13 +2,13 @@ default Order dec
 $include <prelude.sail>
 $include <smt.sail>
 
-val extzv : forall 'n 'm, 'm >= 0 & 'n >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm, 'm >= 0 & 'n >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extzv(m, v) = sail_mask(m, v)
 
 
 /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
 
-val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n)
 
 function foo(n, x) =
   let y : bits(16) = extzv(x) in
@@ -17,7 +17,7 @@ function foo(n, x) =
     64 => let z = y@y@y@y in let dfsf = 4 in z
   }
 
-val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n)
 
 function foo_if(n, x) =
   let y : bits(16) = extzv(x) in
@@ -25,11 +25,11 @@ function foo_if(n, x) =
   then y@y
   else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z
 
-val use : bits(16) -> unit effect pure
+val use : bits(16) -> unit
 
 function use(x) = ()
 
-val bar : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+val bar : forall 'n, 'n in {8,16}. bits('n) -> unit
 
 function bar(x) =
   match 'n {
@@ -37,7 +37,7 @@ function bar(x) =
    16 => use(x)
   }
 
-val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit
 
 function bar_if(x) =
   if 'n == 8
@@ -146,7 +146,7 @@ function refine_mutable_exp2(n, x) = {
 
 /* Adding casts for top-level pattern matches */
 
-val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (int('n), bits('m)) -> bits('n) effect pure
+val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (int('n), bits('m)) -> bits('n)
 
 function foo2(32,x) =
   let y : bits(16) = extzv(x) in
@@ -155,7 +155,7 @@ and foo2(64,x) =
   let y : bits(16) = extzv(x) in
   let z = y@y@y@y in let dfsf = 4 in z
 
-val foo3 : forall 'm 'n, 'm >= 0 & 'n in {4,8}. (int('n), bits('m)) -> bits(8 * 'n) effect pure
+val foo3 : forall 'm 'n, 'm >= 0 & 'n in {4,8}. (int('n), bits('m)) -> bits(8 * 'n)
 
 function foo3(4,x) =
   let y : bits(16) = extzv(x) in
@@ -165,7 +165,7 @@ and foo3(8,x) =
   let z = y@y@y@y in let dfsf = 4 in z
 
 /* Casting an argument isn't supported yet 
-val bar2 : forall 'n, 'n in {8,16}. (int('n),bits('n)) -> unit effect pure
+val bar2 : forall 'n, 'n in {8,16}. (int('n),bits('n)) -> unit
 
 function bar2(8,x) =
   use(x@x)
diff --git a/test/mono/castrequnion.sail b/test/mono/castrequnion.sail
index fa7a98acf..f0a327049 100644
--- a/test/mono/castrequnion.sail
+++ b/test/mono/castrequnion.sail
@@ -2,7 +2,7 @@ default Order dec
 $include <prelude.sail>
 $include <mono_rewrites.sail>
 
-val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. (implicit('n), bits('m)) -> option(bits('n)) effect pure
+val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. (implicit('n), bits('m)) -> option(bits('n))
 
 function foo(n, x) =
   let y : bits(16) = sail_zero_extend(x,16) in
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
index d7f0266cc..3b4b4247e 100644
--- a/test/mono/exint.sail
+++ b/test/mono/exint.sail
@@ -1,7 +1,7 @@
 default Order dec
 $include <prelude.sail>
 
-val cast ex_int : int -> {'n, true. int('n)}
+val ex_int : int -> {'n, true. int('n)}
 function ex_int 'n = n
 
 
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index c24cfc2db..3c1a0f6f2 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -5,7 +5,7 @@ $include <prelude.sail>
    added in the right places, but it's also worth running in case that gets
    broken. */
 
-val needs_size_in_guard : forall 'n. int('n) -> unit
+val needs_size_in_guard : forall 'n, 'n >= 0. int('n) -> unit
 
 function needs_size_in_guard(n if n > 8) = {
   let x : bits('n) = replicate_bits(0b0,n);
@@ -16,7 +16,7 @@ and needs_size_in_guard(n) = {
   ()
 }
 
-val no_size_in_guard : forall 'n. (int('n), int) -> unit
+val no_size_in_guard : forall 'n, 'n >= 0. (int('n), int) -> unit
 
 function no_size_in_guard((n,m) if m > 8) = {
   let x : bits('n) = replicate_bits(0b0,n);
@@ -27,7 +27,7 @@ and no_size_in_guard(n,m) = {
   ()
 }
 
-val shadowed : forall 'n. int('n) -> unit
+val shadowed : forall 'n, 'n >= 0. int('n) -> unit
 
 function shadowed(n) = {
   let n = 8;
@@ -38,13 +38,13 @@ function shadowed(n) = {
 val willsplit : bool -> unit
 
 function willsplit(x) = {
-  let 'n : int = if x then 8 else 16;
+  let 'n : nat = if x then 8 else 16;
   needs_size_in_guard(n);
   no_size_in_guard(n,n);
   shadowed(n);
 }
 
-val execute : forall 'datasize. int('datasize) -> unit
+val execute : forall 'datasize, 'datasize >= 0. int('datasize) -> unit
 
 function execute(datasize) = {
   let x : bits('datasize) = replicate_bits(0b1, datasize);
@@ -56,10 +56,11 @@ val test_execute : unit -> unit
 function test_execute() = {
   let exp = 4;
   let 'datasize = shl_int(1, exp);
+  assert('datasize >= 0);
   execute(datasize)
 }
 
-val transitive_itself : forall 'n. int('n) -> unit
+val transitive_itself : forall 'n, 'n >= 0. int('n) -> unit
 
 function transitive_itself(n) = {
   needs_size_in_guard(n);
diff --git a/test/mono/letsplit.sail b/test/mono/letsplit.sail
index 50bc1b345..b66b9156b 100644
--- a/test/mono/letsplit.sail
+++ b/test/mono/letsplit.sail
@@ -7,7 +7,7 @@ $include <smt.sail>
 
 register size : bits(2)
 
-function get_size() -> {|8,16,32,64|} = {
+function get_size() -> {8,16,32,64} = {
   shl_int(8, unsigned(size))
 }
 
diff --git a/test/mono/mutrecmono.sail b/test/mono/mutrecmono.sail
index d78bff0cf..37d194cd6 100644
--- a/test/mono/mutrecmono.sail
+++ b/test/mono/mutrecmono.sail
@@ -1,9 +1,9 @@
 default Order dec
 $include <prelude.sail>
 
-val extz : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extz : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extz(m,v) = sail_mask(m,v)
-val UInt = {
+val UInt = pure {
   ocaml: "uint",
   lem: "uint",
   interpreter: "uint",
diff --git a/test/mono/set.sail b/test/mono/set.sail
index 27cc5a3a0..50371e787 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,10 +1,10 @@
 default Order dec
 $include <prelude.sail>
 
-val extz : forall 'n 'm, 'n >= 0 & 'm >= 'n. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extz : forall 'n 'm, 'n >= 0 & 'm >= 'n. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extz(m,v) = sail_zero_extend(v, m)
 
-val exts : forall 'n 'm, 'n >= 0 & 'm >= 'n. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val exts : forall 'n 'm, 'n >= 0 & 'm >= 'n. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function exts(m,v) = sail_sign_extend(v, m)
 
 /* A function which is merely parametrised by a size does not need to be
diff --git a/test/mono/times8.sail b/test/mono/times8.sail
index 64b4c8d87..df33979b6 100644
--- a/test/mono/times8.sail
+++ b/test/mono/times8.sail
@@ -3,7 +3,7 @@ $include <prelude.sail>
 
 /* Another byte/bit size conversion */
 
-val bar : forall 'n. int('n) -> bits(8 * 'n)
+val bar : forall 'n, 'n >= 0. int('n) -> bits(8 * 'n)
 
 function bar (n) = replicate_bits(0x12,n)
 
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
index 8f6a3e4f8..c5a775b42 100644
--- a/test/mono/times8div8.sail
+++ b/test/mono/times8div8.sail
@@ -5,9 +5,9 @@ $include <smt.sail>
 val extzv : forall 'n 'm, 'n >= 0 & 'm >= 'n. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec)
 function extzv(m,v) = sail_zero_extend(v, m)
 
-val cast ex_int : int -> {'n, true. int('n)}
+val ex_int : int -> {'n, true. int('n)}
 function ex_int 'n = n
-val quotient = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int
+val quotient = pure {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int
 overload operator / = {quotient}
 
 /* Byte/bits size conversions are a pain */
@@ -39,6 +39,7 @@ function g(m,n,v) = {
   assert(constraint('m >= 0 & 'n >= 0));
   let 'o : {'p, true. int('p)} = ex_int(m / n) in {
     assert(constraint('o * 'n == 'm));
+    assert(o >= 0);
     accept2(replicate_bits(v,o))
   }
 }
diff --git a/test/mono/union_split.sail b/test/mono/union_split.sail
index 2403e644c..595015476 100644
--- a/test/mono/union_split.sail
+++ b/test/mono/union_split.sail
@@ -15,7 +15,7 @@ function execute(SomeOp(n as int('n),v)) = {
   sail_zero_extend(b,32)
 }
 
-val run : unit -> unit effect {escape}
+val run : unit -> unit
 
 function run () = {
   assert(execute(SomeOp(8,0x11)) == 0x00000010);
diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail
index 4d0d7d8ff..458139e43 100644
--- a/test/mono/varmatch.sail
+++ b/test/mono/varmatch.sail
@@ -1,6 +1,6 @@
 $include <flow.sail>
 
-val eq_all = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_all = pure {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
 overload operator == = {eq_all}
 
 
diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail
index 3d5b74853..4ae032ec8 100644
--- a/test/mono/varpatterns.sail
+++ b/test/mono/varpatterns.sail
@@ -6,7 +6,7 @@ $include <prelude.sail>
 val test : bool -> unit
 
 function test(b) = {
-    let 'n : {|8,16|} = if b then 8 else 16;
+    let 'n : {8,16} = if b then 8 else 16;
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
     assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
 }
@@ -14,12 +14,12 @@ function test(b) = {
 val test2 : bool -> unit
 
 function test2(b) = {
-    let 'n = (if b then 8 else 16) : {|8,16|};
+    let 'n = (if b then 8 else 16) : {8,16};
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
     assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
 }
 
-val test_mult : {|4,8|} -> unit
+val test_mult : {4,8} -> unit
 
 function test_mult('m) = {
     let 'n = 2 * 'm;
diff --git a/test/mono/vectorsize.sail b/test/mono/vectorsize.sail
index 7b4f2423f..40f58f68a 100644
--- a/test/mono/vectorsize.sail
+++ b/test/mono/vectorsize.sail
@@ -8,7 +8,7 @@ type vmax : Int = 64
 
 register vsize : bits(2)
 
-function get_vector_size() -> {|8,16,32,64|} = {
+function get_vector_size() -> {8,16,32,64} = {
   shl_int(8, unsigned(vsize))
 }