Merge branch 'sail2' into rmem_interpreter

63 files changed, 772 insertions, 249 deletions

diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
new file mode 100644
index 00000000..03954a9f
--- /dev/null
+++ b/test/typecheck/pass/Replicate.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
new file mode 100644
index 00000000..92c6d7cd
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v1.sail]:11:4-30
+11 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
new file mode 100644
index 00000000..69f2bb6f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
new file mode 100644
index 00000000..0dec309f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v2.sail]:10:4-30
+10 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from {('ex42# : Int), true. vector(('M * 'ex42#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
new file mode 100644
index 00000000..e54b0af4
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bitvector_param.sail b/test/typecheck/pass/bitvector_param.sail
new file mode 100644
index 00000000..ffebeb6e
--- /dev/null
+++ b/test/typecheck/pass/bitvector_param.sail
@@ -0,0 +1,42 @@
+/* from prelude */
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+
+val vector_subrange = {
+  ocaml: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange",
+  coq: "subrange_vec_dec"
+} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
+
+val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
+  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
+
+overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
+
+val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+
+val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
+
+overload append = {bitvector_concat, vector_concat}
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+type xlen : Int = 64
+type ylen : Int = 1
+
+type xlenbits = bits(xlen)
+
+bitfield Mstatus : xlenbits = {
+  SD  : xlen - ylen,
+  SXL : xlen - ylen - 1 .. xlen - ylen - 3
+}
+register mstatus : Mstatus
diff --git a/test/typecheck/pass/bool_bits_mapping.sail b/test/typecheck/pass/bool_bits_mapping.sail
new file mode 100644
index 00000000..7fd2bae3
--- /dev/null
+++ b/test/typecheck/pass/bool_bits_mapping.sail
@@ -0,0 +1,8 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0
+}
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index 3e2c7bde..b1597759 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -1,27 +1,20 @@
-Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
-
-  if b then n else 4
-
-Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm == 3). int('m)} on 4
-Coercion failed because:
-  int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
-  in context
-  * 4 == 'ex41#m
-  * not('b)
-  where
-  * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
-
-function foo(b, n) = {
-  if b then n else 4
-}
-
-  * 'ex41#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
-
-  if b then n else 4
-
-  * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
-
-function foo(b, n) = {
-  if b then n else 4
-}
-
+Type error:
+[bool_constraint/v1.sail]:12:19-20
+12 |  if b then n else 4
+   |                   ^
+   | Tried performing type coercion from int(4) to {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} on 4
+   | Coercion failed because:
+   | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
+   | [bool_constraint/v1.sail]:11:0-13:1
+   | 11 |function foo(b, n) = {
+   |    |^---------------------
+   | 13 |}
+   |    |^
+   |    | 'b bound here
+   | [bool_constraint/v1.sail]:11:0-13:1
+   | 11 |function foo(b, n) = {
+   |    |^---------------------
+   | 13 |}
+   |    |^
+   |    | 'n bound here
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
index 847ef329..c7a355e1 100644
--- a/test/typecheck/pass/bool_constraint/v2.expect
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -1,5 +1,6 @@
-Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32
-
-    _prove(constraint('n <= 14))
-
-Cannot prove 'n <= 14
+Type error:
+[bool_constraint/v2.sail]:38:4-32
+38 |    _prove(constraint('n <= 14))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 14
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
index ca87fac1..63791a70 100644
--- a/test/typecheck/pass/bool_constraint/v3.expect
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -1,5 +1,6 @@
-Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32
-
-    _prove(constraint('n <= 14))
-
-Cannot prove 'n <= 14
+Type error:
+[bool_constraint/v3.sail]:46:4-32
+46 |    _prove(constraint('n <= 14))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 14
+   | 
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
index 07363175..420909bf 100644
--- a/test/typecheck/pass/bool_constraint/v4.expect
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -1,5 +1,6 @@
-Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32
-
-    _prove(constraint('n <= 13))
-
-Cannot prove 'n <= 13
+Type error:
+[bool_constraint/v4.sail]:46:4-32
+46 |    _prove(constraint('n <= 13))
+   |    ^--------------------------^
+   | Cannot prove 'n <= 13
+   | 
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index ab25cbc4..8c95193d 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -1,5 +1,6 @@
-Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26
-
-type MyStruct64 = MyStruct(65)
-
-Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+Type error:
+[constrained_struct/v1.sail]:10:18-26
+10 |type MyStruct64 = MyStruct(65)
+   |                  ^------^
+   | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect
index c3886af8..cf3b9399 100644
--- a/test/typecheck/pass/constraint_ctor/v1.expect
+++ b/test/typecheck/pass/constraint_ctor/v1.expect
@@ -1,5 +1,6 @@
-Type error at file "constraint_ctor/v1.sail", line 10, character 3 to line 10, character 29
-
-  _prove(constraint('x >= 4));
-
-Cannot prove 'x >= 4
+Type error:
+[constraint_ctor/v1.sail]:10:2-29
+10 |  _prove(constraint('x >= 4));
+   |  ^-------------------------^
+   | Cannot prove 'x >= 4
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect
index a315b3b7..0e56f0a4 100644
--- a/test/typecheck/pass/constraint_ctor/v2.expect
+++ b/test/typecheck/pass/constraint_ctor/v2.expect
@@ -1,5 +1,6 @@
-Type error at file "constraint_ctor/v2.sail", line 18, character 3 to line 18, character 30
-
-  _prove(constraint('x >= 24));
-
-Cannot prove 'x >= 24
+Type error:
+[constraint_ctor/v2.sail]:18:2-30
+18 |  _prove(constraint('x >= 24));
+   |  ^--------------------------^
+   | Cannot prove 'x >= 24
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect
index e0edd01a..37d1dff2 100644
--- a/test/typecheck/pass/constraint_ctor/v3.expect
+++ b/test/typecheck/pass/constraint_ctor/v3.expect
@@ -1,5 +1,6 @@
-Type error at file "constraint_ctor/v3.sail", line 18, character 3 to line 18, character 30
-
-  _prove(constraint('x >= 23));
-
-Cannot prove 'x >= 23
+Type error:
+[constraint_ctor/v3.sail]:18:2-30
+18 |  _prove(constraint('x >= 23));
+   |  ^--------------------------^
+   | Cannot prove 'x >= 23
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
index 06eb9d22..64893e4d 100644
--- a/test/typecheck/pass/constraint_ctor/v4.expect
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -1,5 +1,6 @@
-Type error at file "constraint_ctor/v4.sail", line 17, character 34 to line 17, character 36
-
-function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
-
-Could not prove 23 <= 22 for type constructor Bar
+Type error:
+[constraint_ctor/v4.sail]:17:33-36
+17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+   |                                 ^-^
+   | Could not prove 23 <= 22 for type constructor Bar
+   | 
diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect
index b6df0222..fc2ef615 100644
--- a/test/typecheck/pass/constraint_ctor/v5.expect
+++ b/test/typecheck/pass/constraint_ctor/v5.expect
@@ -1,5 +1,6 @@
-Type error at file "constraint_ctor/v5.sail", line 27, character 3 to line 27, character 29
-
-  _prove(constraint('x >= 4));
-
-Cannot prove 'x >= 4
+Type error:
+[constraint_ctor/v5.sail]:27:2-29
+27 |  _prove(constraint('x >= 4));
+   |  ^-------------------------^
+   | Cannot prove 'x >= 4
+   | 
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index fb1b2619..cc8b874f 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -1,6 +1,8 @@
-Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42
-
-let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
-
-Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
-Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
+Type error:
+[exist_synonym/v1.sail]:6:41-42
+6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
+  |                                         ^
+  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4
+  | Coercion failed because:
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('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 5bde04ba..c01d8359 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -1,6 +1,8 @@
-Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41
-
-let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
-
-Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
-Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
+Type error:
+[exist_synonym/v2.sail]:6:40-41
+6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+  |                                        ^
+  | Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4
+  | Coercion failed because:
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('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 a647ef00..c237ae2d 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
+Type error:
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index d8bad777..abb232cb 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
+Type error:
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail
index 7813cb16..347a9b3a 100644
--- a/test/typecheck/pass/foreach_var_updates.sail
+++ b/test/typecheck/pass/foreach_var_updates.sail
@@ -1,3 +1,5 @@
+$include <flow.sail>
+
 val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int
 
 overload operator + = {add_int}
diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect
index 6e40adc0..2bb734aa 100644
--- a/test/typecheck/pass/function_namespace/v1.expect
+++ b/test/typecheck/pass/function_namespace/v1.expect
@@ -1,5 +1,6 @@
-Type error at file "function_namespace/v1.sail", line 9, character 7 to line 9, character 10
-
-  let test = true;
-
-Local variable test is already bound as a function name
+Type error:
+[function_namespace/v1.sail]:9:6-10
+9 |  let test = true;
+  |      ^--^
+  | Local variable test is already bound as a function name
+  | 
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index e81c467e..ac4428c6 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -1,24 +1,12 @@
-Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15
-
-let _ = test(32)
-
-Tried performing type coercion from int(32) to int('size) on 32
-Coercion failed because:
-  int(32) is not a subtype of int('size)
-  in context
-  * 'size == 'ex14#
-  * ('ex14# == 32 | 'ex14# == 64)
-  * ('ex13# == 32 | 'ex13# == 64)
-  where
-  * 'ex13# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'ex14# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
+Type error:
+[global_type_var/v1.sail]:23:13-15
+23 |let _ = test(32)
+   |             ^^
+   | Tried performing type coercion from int(32) to int('size) on 32
+   | Coercion failed because:
+   | int(32) is not a subtype of int('size)
+   | [global_type_var/v1.sail]:5:13-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |             ^---^
+   |   | 'size bound here
+   | 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 21c4b348..93eb628b 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -1,24 +1,12 @@
-Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15
-
-let _ = test(64)
-
-Tried performing type coercion from int(64) to int('size) on 64
-Coercion failed because:
-  int(64) is not a subtype of int('size)
-  in context
-  * 'size == 'ex14#
-  * ('ex14# == 32 | 'ex14# == 64)
-  * ('ex13# == 32 | 'ex13# == 64)
-  where
-  * 'ex13# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'ex14# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
-  * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
-
-let (size as 'size) : {|32, 64|} = 32
-
+Type error:
+[global_type_var/v2.sail]:23:13-15
+23 |let _ = test(64)
+   |             ^^
+   | Tried performing type coercion from int(64) to int('size) on 64
+   | Coercion failed because:
+   | int(64) is not a subtype of int('size)
+   | [global_type_var/v2.sail]:5:13-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |             ^---^
+   |   | 'size bound here
+   | 
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 43096686..6def5172 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -1,5 +1,12 @@
-Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23
-
-val test : forall 'size. atom('size) -> unit
-
-type variable ('size : Int) is already bound
+Type error:
+[global_type_var/v3.sail]:15:23-27
+15 |    let y : atom(64) = size in
+   |                       ^--^
+   | Tried performing type coercion from int('_size) to int(64) on size
+   | Coercion failed because:
+   | int('_size) is not a subtype of int(64)
+   | [global_type_var/v3.sail]:5:5-18
+   | 5 |let (size as 'size) : {|32, 64|} = 32
+   |   |     ^-----------^
+   |   | '_size bound here
+   | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 95073799..c8217478 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -1,17 +1,12 @@
-Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, character 37
-
-  let _ = 0b100[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3)
-    
-    Try adding named type variables for 
-    
-    
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3)
-    
-    Try adding named type variables for 
-    
-    
+Type error:
+[if_infer/v1.sail]:10:10-37
+10 |  let _ = 0b100[if R then 0 else f()];
+   |          ^-------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Could not resolve quantifiers for bitvector_access
+   |    * (0 <= 'ex40# & ('ex40# + 1) <= 3)
+   | * plain_vector_access
+   |    Could not resolve quantifiers for plain_vector_access
+   |    * (0 <= 'ex43# & ('ex43# + 1) <= 3)
+   | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index afa04343..f0c2fab3 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -1,17 +1,12 @@
-Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, character 38
-
-  let _ = 0b1001[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4)
-    
-    Try adding named type variables for 
-    
-    
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4)
-    
-    Try adding named type variables for 
-    
-    
+Type error:
+[if_infer/v2.sail]:10:10-38
+10 |  let _ = 0b1001[if R then 0 else f()];
+   |          ^--------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Could not resolve quantifiers for bitvector_access
+   |    * (0 <= 'ex40# & ('ex40# + 1) <= 4)
+   | * plain_vector_access
+   |    Could not resolve quantifiers for plain_vector_access
+   |    * (0 <= 'ex43# & ('ex43# + 1) <= 4)
+   | 
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
index 8b149bc8..7e0e74bb 100644
--- a/test/typecheck/pass/if_infer/v3.expect
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -1,7 +1,10 @@
-Type error at file "if_infer/v3.sail", line 10, character 11 to line 10, character 38
-
-  let _ = 0b1001[if R then 0 else f()];
-
-No overloadings for vector_access, tried:
-  bitvector_access: Numeric type is non-simple
-  plain_vector_access: Numeric type is non-simple
+Type error:
+[if_infer/v3.sail]:10:10-38
+10 |  let _ = 0b1001[if R then 0 else f()];
+   |          ^--------------------------^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Numeric type is non-simple
+   | * plain_vector_access
+   |    Numeric type is non-simple
+   | 
diff --git a/test/typecheck/pass/implicits.sail b/test/typecheck/pass/implicits.sail
new file mode 100644
index 00000000..2923fab4
--- /dev/null
+++ b/test/typecheck/pass/implicits.sail
@@ -0,0 +1,45 @@
+default Order dec
+
+$include <prelude.sail>
+
+val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTZ(m, x) = sail_zero_extend(x, m)
+
+val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTS(m, x) = sail_sign_extend(x, m)
+
+val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n)
+
+function zeros(n) = replicate_bits(0b0, n)
+
+val dzeros : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m)) -> (bits('n), bits('m))
+
+function dzeros(n, m) = (zeros(n), zeros(m))
+
+val dzeros2 : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m), unit) -> (bits('n), bits('m))
+
+function dzeros2(n, m, _) = (zeros(n), zeros(m))
+
+function main((): unit) -> unit = {
+  let a: bits(64) = EXTZ(0xFF);
+  let b: bits(64) = EXTS(0xFF);
+  let c: bits(64) = EXTS(64, 0xFF);
+  let d: bits(64) = zeros();
+  let e: bits(64) = zeros(64);
+  let (f, g): (bits(64), bits(32)) = dzeros();
+  let (h, i) = dzeros(16, 8);
+  let (j, k): (bits(4), bits(2)) = dzeros2();
+  print_bits("a = ", a);
+  print_bits("b = ", b);
+  print_bits("c = ", c);
+  print_bits("d = ", d);
+  print_bits("e = ", e);
+  print_bits("f = ", f);
+  print_bits("g = ", g);
+  print_bits("h = ", h);
+  print_bits("i = ", i);
+  print_bits("j = ", j);
+  print_bits("k = ", k)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/implicits/v1.expect b/test/typecheck/pass/implicits/v1.expect
new file mode 100644
index 00000000..f1711d54
--- /dev/null
+++ b/test/typecheck/pass/implicits/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[implicits/v1.sail]:9:51-63
+9 |val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (bits('n), implicit('m)) -> bits('m)
+  |                                                   ^----------^
+  | Arguments are invalid, implicit arguments must come before all other arguments
+  | 
diff --git a/test/typecheck/pass/implicits/v1.sail b/test/typecheck/pass/implicits/v1.sail
new file mode 100644
index 00000000..661ff309
--- /dev/null
+++ b/test/typecheck/pass/implicits/v1.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <prelude.sail>
+
+val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTZ(m, x) = sail_zero_extend(x, m)
+
+val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (bits('n), implicit('m)) -> bits('m)
+
+function EXTS(x, m) = sail_sign_extend(x, m)
+
+val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n)
+
+function zeros(n) = replicate_bits(0b0, n)
+
+function main((): unit) -> unit = {
+  let a: bits(64) = EXTZ(0xFF);
+  let b: bits(64) = EXTS(0xFF);
+  let c: bits(64) = EXTS(0xFF, 64);
+  let d: bits(64) = zeros();
+  let e: bits(64) = zeros(64);
+  print_bits("a = ", a);
+  print_bits("b = ", b);
+  print_bits("c = ", c);
+  print_bits("d = ", d);
+  print_bits("e = ", e);
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/implicits/v2.expect b/test/typecheck/pass/implicits/v2.expect
new file mode 100644
index 00000000..11ffeace
--- /dev/null
+++ b/test/typecheck/pass/implicits/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[implicits/v2.sail]:5:50-56
+5 |val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m - 1), bits('n)) -> bits('m)
+  |                                                  ^----^
+  | Implicit argument must contain a single type variable
+  | 
diff --git a/test/typecheck/pass/implicits/v2.sail b/test/typecheck/pass/implicits/v2.sail
new file mode 100644
index 00000000..4040aa0c
--- /dev/null
+++ b/test/typecheck/pass/implicits/v2.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m - 1), bits('n)) -> bits('m)
+
+function EXTZ(m, x) = sail_zero_extend(x, m)
+
+val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTS(m, x) = sail_sign_extend(x, m)
+
+function main((): unit) -> unit = {
+  let a: bits(64) = EXTZ(0xFF);
+  let b: bits(64) = EXTS(0xFF);
+  print_bits("a = ", a);
+  print_bits("b = ", b)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/lt_flow.sail b/test/typecheck/pass/lt_flow.sail
new file mode 100644
index 00000000..4e7572da
--- /dev/null
+++ b/test/typecheck/pass/lt_flow.sail
@@ -0,0 +1,5 @@
+val lt_flow : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+val test : unit -> bool(true)
+
+function test() = lt_flow(1,10)
diff --git a/test/typecheck/pass/mutrec.sail b/test/typecheck/pass/mutrec.sail
new file mode 100644
index 00000000..26dbf729
--- /dev/null
+++ b/test/typecheck/pass/mutrec.sail
@@ -0,0 +1,12 @@
+$include <prelude.sail>
+
+val f : list(int) -> int
+val g : list(int) -> int
+
+function f([| |]) = 0
+and f(h::t) = h + g(t)
+function g([||]) = 0
+and g(h::t) = f(t) - h
+
+val test : unit -> int
+function test() = f([|1,2,3|])
diff --git a/test/typecheck/pass/nexp_synonym.sail b/test/typecheck/pass/nexp_synonym.sail
new file mode 100644
index 00000000..b908b265
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+type LEN : Int = 32
+
+let v : bits(LEN) = 0xFFFF_FFFF
+
+function main((): unit) -> unit = {
+  print_bits("v = ", v)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/nexp_synonym/v1.expect b/test/typecheck/pass/nexp_synonym/v1.expect
new file mode 100644
index 00000000..9ba21c2c
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[nexp_synonym/v1.sail]:7:20-31
+7 |let v : bits(LEN) = 0xFFFF_FFFF
+  |                    ^---------^
+  | Tried performing type coercion from vector(32, dec, bit) to bits(LEN) on 0xFFFFFFFF
+  | Coercion failed because:
+  | Mismatched argument types in subtype check
+  | 
diff --git a/test/typecheck/pass/nexp_synonym/v1.sail b/test/typecheck/pass/nexp_synonym/v1.sail
new file mode 100644
index 00000000..96690e00
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym/v1.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+type LEN : Int = 33
+
+let v : bits(LEN) = 0xFFFF_FFFF
+
+function main((): unit) -> unit = {
+  print_bits("v = ", v)
+}
diff --git a/test/typecheck/pass/nexp_synonym/v2.expect b/test/typecheck/pass/nexp_synonym/v2.expect
new file mode 100644
index 00000000..68d664f7
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym/v2.expect
@@ -0,0 +1,8 @@
+Type error:
+[nexp_synonym/v2.sail]:7:20-32
+7 |let v : bits(LEN) = 0xFFFF_FFFFF
+  |                    ^----------^
+  | Tried performing type coercion from vector(36, dec, bit) to bits(LEN) on 0xFFFFFFFFF
+  | Coercion failed because:
+  | Mismatched argument types in subtype check
+  | 
diff --git a/test/typecheck/pass/nexp_synonym/v2.sail b/test/typecheck/pass/nexp_synonym/v2.sail
new file mode 100644
index 00000000..0c1b5b5b
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym/v2.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+type LEN : Int = 32
+
+let v : bits(LEN) = 0xFFFF_FFFFF
+
+function main((): unit) -> unit = {
+  print_bits("v = ", v)
+}
diff --git a/test/typecheck/pass/nexp_synonym2.sail b/test/typecheck/pass/nexp_synonym2.sail
new file mode 100644
index 00000000..9e9bd7b8
--- /dev/null
+++ b/test/typecheck/pass/nexp_synonym2.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+type LEN : Int = 30 + 2
+
+type V : Type = bits(LEN)
+
+type V2('n: Int) -> Type = bits('n)
+
+let v : V = 0xFFFF_FFFF
+
+function main((): unit) -> unit = {
+  print_bits("v = ", v : V2(LEN))
+}
diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect
index 9de82d1f..aeefb901 100644
--- a/test/typecheck/pass/not_pattern/v1.expect
+++ b/test/typecheck/pass/not_pattern/v1.expect
@@ -1,5 +1,6 @@
-Type error at file "not_pattern/v1.sail", line 12, character 7 to line 12, character 7
-
-    ~(y) => (),
-
-Bindings are not allowed in this context
+Type error:
+[not_pattern/v1.sail]:12:6-7
+12 |    ~(y) => (),
+   |      ^
+   | Bindings are not allowed in this context
+   | 
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index 86294543..4433a2c3 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -12,7 +12,7 @@ val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order).
   (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool
 
 val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
-  (int('n), int('m)) -> bool
+  (int('n), int('m)) -> bool('n == 'm)
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool
 
diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail
index 96663073..6be3533f 100644
--- a/test/typecheck/pass/phantom_num.sail
+++ b/test/typecheck/pass/phantom_num.sail
@@ -1,9 +1,13 @@
+function __id forall 'n. (x: int('n)) -> int('n) = x
+
+overload __size = {__id}
+
 val gt_int = {ocaml: "gt", lem: "gt"}: (int, int) -> bool
 
 overload operator > = {gt_int}
 
 register z : int
 
-val test : forall ('n : Int). unit -> unit effect {wreg}
+val test : forall ('n : Int). (implicit('n), unit) -> unit effect {wreg}
 
-function test () = if 'n > 3 then z = 0 else z = 1
+function test(n, _) = if 'n > 3 then z = 0 else z = 1
diff --git a/test/typecheck/pass/reg_32_64.sail b/test/typecheck/pass/reg_32_64.sail
new file mode 100644
index 00000000..79dfc862
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect
new file mode 100644
index 00000000..eb398991
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v1.expect
@@ -0,0 +1,11 @@
+Type error:
+[reg_32_64/v1.sail]:35:9-28
+35 |  R(0) = 0xCAFE_CAFE_0000_00;
+   |         ^-----------------^
+   | No overloading for R, tried:
+   | * set_R
+   |    Could not resolve quantifiers for set_R
+   |    * (regno(0) & (56 == 32 | 56 == 64))
+   | * get_R
+   |    No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v1.sail b/test/typecheck/pass/reg_32_64/v1.sail
new file mode 100644
index 00000000..8c0e980b
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v1.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_00;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
new file mode 100644
index 00000000..f007c917
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -0,0 +1,13 @@
+Type error:
+[reg_32_64/v2.sail]:21:18-22
+21 |  (*R)['d .. 0] = data
+   |                  ^--^
+   | Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | This error occured because of a previous error:
+   | [reg_32_64/v2.sail]:21:2-15
+   | 21 |  (*R)['d .. 0] = data
+   |    |  ^-----------^
+   |    | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v2.sail b/test/typecheck/pass/reg_32_64/v2.sail
new file mode 100644
index 00000000..64daea4a
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v2.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect
new file mode 100644
index 00000000..cea45127
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v3.expect
@@ -0,0 +1,10 @@
+Type error:
+[reg_32_64/v3.sail]:29:15-21
+29 |  reg_deref(R)['d - 1 .. 0]
+   |               ^----^
+   | No overloading for (operator -), tried:
+   | * sub_atom
+   |    Cannot re-write sizeof('d)
+   | * sub_int
+   |    Cannot re-write sizeof('d)
+   | 
diff --git a/test/typecheck/pass/reg_32_64/v3.sail b/test/typecheck/pass/reg_32_64/v3.sail
new file mode 100644
index 00000000..dda787ab
--- /dev/null
+++ b/test/typecheck/pass/reg_32_64/v3.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(_, r) = {
+  let R = GPRs[r];
+  reg_deref(R)['d - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail
index fdda96dc..5653cb51 100644
--- a/test/typecheck/pass/return_simple3.sail
+++ b/test/typecheck/pass/return_simple3.sail
@@ -1,6 +1,10 @@
-val return_test : forall ('N : Int), 'N >= 10. range(10, 'N) -> range(10, 'N)
+function __id forall 'n. (x: int('n)) -> int('n) = x
 
-function return_test x = {
+overload __size = {__id}
+
+val return_test : forall ('N : Int), 'N >= 10. (implicit('N), range(10, 'N)) -> range(10, 'N)
+
+function return_test(N, x) = {
   return(x);
   'N
 }
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
index f1c8bade..43c7ddc9 100644
--- a/test/typecheck/pass/tautology.sail
+++ b/test/typecheck/pass/tautology.sail
@@ -1,3 +1,4 @@
+$include <flow.sail>
 
 type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
 
diff --git a/test/typecheck/pass/true_false.sail b/test/typecheck/pass/true_false.sail
new file mode 100644
index 00000000..42b175d8
--- /dev/null
+++ b/test/typecheck/pass/true_false.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main((): unit) -> unit = {
+  let x: bool(false) = false;
+  let y: bool(true) = true;
+  _check(x : bool);
+  _check(x : bool(false));
+  _not_check(x : bool(true))
+}
diff --git a/test/typecheck/pass/tyvar_shadow.sail b/test/typecheck/pass/tyvar_shadow.sail
new file mode 100644
index 00000000..973aa916
--- /dev/null
+++ b/test/typecheck/pass/tyvar_shadow.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main((): unit) -> unit = {
+  let x as int('x) = 3;
+  let x as int('x) = 4;
+  _prove(constraint('x + 'x == 8));
+  _not_prove(constraint('x + 'x == 6 | 'x + 'x == 7));
+
+  let y : {'n, 'n == 3. int('n)} = 3;
+  _prove(constraint('_y == 3))
+}
+
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
index 68a4ca70..ce61cf2a 100644
--- a/test/typecheck/pass/vec_length/v1.expect
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -1,13 +1,12 @@
-Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15
-
-  let y = x[10];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+Type error:
+[vec_length/v1.sail]:6:10-15
+6 |  let y = x[10];
+  |          ^---^
+  | No overloading for vector_access, tried:
+  | * bitvector_access
+  |    Could not resolve quantifiers for bitvector_access
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | * plain_vector_access
+  |    Could not resolve quantifiers for plain_vector_access
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | 
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
index 7ce8fd99..3d40cdb0 100644
--- a/test/typecheck/pass/vec_length/v1_inc.expect
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -1,13 +1,12 @@
-Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15
-
-  let y = x[10];
-
-No overloadings for vector_access, tried:
-  bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+Type error:
+[vec_length/v1_inc.sail]:6:10-15
+6 |  let y = x[10];
+  |          ^---^
+  | No overloading for vector_access, tried:
+  | * bitvector_access
+  |    Could not resolve quantifiers for bitvector_access
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | * plain_vector_access
+  |    Could not resolve quantifiers for plain_vector_access
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | 
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
index d123cabd..c77ecaa7 100644
--- a/test/typecheck/pass/vec_length/v2.expect
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -1,13 +1,12 @@
-Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25
-
-  let z = [x with 10 = y];
-
-No overloadings for vector_update, tried:
-  bitvector_update:
-    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_update:
-    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+Type error:
+[vec_length/v2.sail]:7:10-25
+7 |  let z = [x with 10 = y];
+  |          ^-------------^
+  | No overloading for vector_update, tried:
+  | * bitvector_update
+  |    Could not resolve quantifiers for bitvector_update
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | * plain_vector_update
+  |    Could not resolve quantifiers for plain_vector_update
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | 
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
index e7d2b52f..cff65f62 100644
--- a/test/typecheck/pass/vec_length/v2_inc.expect
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -1,13 +1,12 @@
-Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25
-
-  let z = [x with 10 = y];
-
-No overloadings for vector_update, tried:
-  bitvector_update:
-    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
-  plain_vector_update:
-    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
-    
-    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+Type error:
+[vec_length/v2_inc.sail]:7:10-25
+7 |  let z = [x with 10 = y];
+  |          ^-------------^
+  | No overloading for vector_update, tried:
+  | * bitvector_update
+  |    Could not resolve quantifiers for bitvector_update
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | * plain_vector_update
+  |    Could not resolve quantifiers for plain_vector_update
+  |    * (0 <= 10 & (10 + 1) <= 8)
+  | 
diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect
new file mode 100644
index 00000000..e3afecee
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v3.expect
@@ -0,0 +1,14 @@
+Type error:
+[vec_length/v3.sail]:6:10-12:3
+6  |  let y = x[
+   |          ^-
+12 |  ];
+   |--^
+   | No overloading for vector_access, tried:
+   | * bitvector_access
+   |    Could not resolve quantifiers for bitvector_access
+   |    * (0 <= 10 & (10 + 1) <= 8)
+   | * plain_vector_access
+   |    Could not resolve quantifiers for plain_vector_access
+   |    * (0 <= 10 & (10 + 1) <= 8)
+   | 
diff --git a/test/typecheck/pass/vec_length/v3.sail b/test/typecheck/pass/vec_length/v3.sail
new file mode 100644
index 00000000..8736278e
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v3.sail
@@ -0,0 +1,14 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[
+
+
+
+
+    10
+  ];
+  ()
+}
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index 50a93cff..b82d6c8c 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -1,3 +1,4 @@
+
 val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0.
   (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a
 
@@ -11,6 +12,8 @@ val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm)
 
 val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n)
 
+overload __size = {length}
+
 default Order inc
 
 val test : forall 'n 'm, 'n >= 5.