Merge branch 'sail2' into rmem_interpreter

81 files changed, 923 insertions, 202 deletions

diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
index c442d6a8..ae340941 100644
--- a/test/typecheck/pass/bind_typ_var.sail
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -1,7 +1,7 @@
 
 val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
 
-val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+val mk_square : unit -> {'n 'm, 'n == 'm. vector('n, dec, vector('m, dec, bit))}
 
 val test : unit -> unit
 
@@ -10,8 +10,8 @@ function test () = {
   // could still be
   let v2 as 'len2 = mk_vector ();
   let matrix as vector('width, _, 'height) = mk_square ();
-  _prove(constraint('width = 'height));
-  _prove(constraint('len = 32 | 'len = 64));
-  _prove(constraint('len2 = 32 | 'len2 = 64));
+  _prove(constraint('width == 'height));
+  _prove(constraint('len == 32 | 'len == 64));
+  _prove(constraint('len2 == 32 | 'len2 == 64));
   ()
 }
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint.sail b/test/typecheck/pass/bool_constraint.sail
new file mode 100644
index 00000000..de6bf4b7
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  };
+
+  if my_not(cond) then {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
new file mode 100644
index 00000000..3e2c7bde
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -0,0 +1,27 @@
+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
+}
+
diff --git a/test/typecheck/pass/bool_constraint/v1.sail b/test/typecheck/pass/bool_constraint/v1.sail
new file mode 100644
index 00000000..46badd52
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
new file mode 100644
index 00000000..847ef329
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/bool_constraint/v2.sail b/test/typecheck/pass/bool_constraint/v2.sail
new file mode 100644
index 00000000..1506bbbd
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 16 & implies('b, 'n <= 15).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
new file mode 100644
index 00000000..ca87fac1
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/bool_constraint/v3.sail b/test/typecheck/pass/bool_constraint/v3.sail
new file mode 100644
index 00000000..966ad2d5
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
new file mode 100644
index 00000000..07363175
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/bool_constraint/v4.sail b/test/typecheck/pass/bool_constraint/v4.sail
new file mode 100644
index 00000000..9f68bf91
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 13))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/commentfix.sail b/test/typecheck/pass/commentfix.sail
new file mode 100644
index 00000000..fd2cf0b2
--- /dev/null
+++ b/test/typecheck/pass/commentfix.sail
@@ -0,0 +1,7 @@
+/********/
+
+/*=====*/
+
+//////
+
+default Order inc
diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail
new file mode 100644
index 00000000..87d55b65
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct MyStruct('n), 'n in {32, 64} = {
+  field: bits('n)
+}
+
+type MyStruct32 = MyStruct(32)
+type MyStruct64 = MyStruct(64)
+
+let x : MyStruct64 = struct { field = 0xFFFF_FFFF_FFFF_FFFF }
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
new file mode 100644
index 00000000..ab25cbc4
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail
new file mode 100644
index 00000000..98daf59e
--- /dev/null
+++ b/test/typecheck/pass/constrained_struct/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct MyStruct('n), 'n in {32, 64} = {
+  field: bits('n)
+}
+
+type MyStruct32 = MyStruct(32)
+type MyStruct64 = MyStruct(65)
+
+let x : MyStruct64 = struct { field = 0b1 @ 0xFFFF_FFFF_FFFF_FFFF }
diff --git a/test/typecheck/pass/constraint_ctor.sail b/test/typecheck/pass/constraint_ctor.sail
new file mode 100644
index 00000000..17ec74ce
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
+
+union Quux('a : Type) = {
+  Quux : 'a
+}
+
+function quux(Quux(x as int('x)) : Quux({'n, 'n >= 3. int('n)})) -> unit = {
+  _prove(constraint('x >= 3));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect
new file mode 100644
index 00000000..c3886af8
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v1.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constraint_ctor/v1.sail b/test/typecheck/pass/constraint_ctor/v1.sail
new file mode 100644
index 00000000..20df5480
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v1.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 4));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect
new file mode 100644
index 00000000..a315b3b7
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v2.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constraint_ctor/v2.sail b/test/typecheck/pass/constraint_ctor/v2.sail
new file mode 100644
index 00000000..76d9793d
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v2.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 24));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect
new file mode 100644
index 00000000..e0edd01a
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v3.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constraint_ctor/v3.sail b/test/typecheck/pass/constraint_ctor/v3.sail
new file mode 100644
index 00000000..a8f5bd13
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v3.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(22)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
new file mode 100644
index 00000000..06eb9d22
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constraint_ctor/v4.sail b/test/typecheck/pass/constraint_ctor/v4.sail
new file mode 100644
index 00000000..d8dab178
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v4.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 22 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect
new file mode 100644
index 00000000..b6df0222
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v5.expect
@@ -0,0 +1,5 @@
+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
diff --git a/test/typecheck/pass/constraint_ctor/v5.sail b/test/typecheck/pass/constraint_ctor/v5.sail
new file mode 100644
index 00000000..855044a5
--- /dev/null
+++ b/test/typecheck/pass/constraint_ctor/v5.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+
+union Foo = {
+  Foo : {'n, 'n >= 3. int('n)}
+}
+
+function foo(Foo(x as int('x)): Foo) -> unit = {
+  _prove(constraint('x >= 3));
+}
+
+union Bar('m), 'm <= 100 = {
+  Bar : {'n, 'n >= 'm. int('n)}
+}
+
+function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+  _prove(constraint('x >= 23));
+  ()
+}
+
+union Quux('a : Type) = {
+  Quux : 'a
+}
+
+function quux(Quux(x as int('x)) : Quux({'n, 'n >= 3. int('n)})) -> unit = {
+  _prove(constraint('x >= 4));
+  ()
+}
diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail
deleted file mode 100644
index 6d212e40..00000000
--- a/test/typecheck/pass/constraint_sym.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-$option -Xconstraint_synonyms
-
-constraint Size('n) = 'n in {32, 64}
-
-constraint Nat('n) = 'n >= 0
-
-val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect
deleted file mode 100644
index 71fd6f30..00000000
--- a/test/typecheck/pass/constraint_sym/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24
-
-constraint Size('n) = 'm in {32, 64}
-
-No type variable 'm
diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail
deleted file mode 100644
index 4421ee77..00000000
--- a/test/typecheck/pass/constraint_sym/v1.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-$option -Xconstraint_synonyms
-
-constraint Size('n) = 'm in {32, 64}
-
-constraint Nat('n) = 'n >= 0
-
-val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect
deleted file mode 100644
index 58a0f416..00000000
--- a/test/typecheck/pass/constraint_sym/v2.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34
-
-val foo : forall 'n, where Siz('n). int('n) -> unit
-
-Constraint synonym Siz is not defined
diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail
deleted file mode 100644
index 1d98e3e4..00000000
--- a/test/typecheck/pass/constraint_sym/v2.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-$option -Xconstraint_synonyms
-
-constraint Size('n) = 'n in {32, 64}
-
-constraint Nat('n) = 'n >= 0
-
-val foo : forall 'n, where Siz('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect
deleted file mode 100644
index ab4526dc..00000000
--- a/test/typecheck/pass/constraint_sym/v3.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43
-
-val foo : forall ('n : Type), where Size('n). int('n) -> unit
-
-Constraint is badly formed, 'n has kind Type but should have kind Int
diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail
deleted file mode 100644
index 886acbe4..00000000
--- a/test/typecheck/pass/constraint_sym/v3.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-$option -Xconstraint_synonyms
-
-constraint Size('n) = 'n in {32, 64}
-
-constraint Nat('n) = 'n >= 0
-
-val foo : forall ('n : Type), where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect
deleted file mode 100644
index c8374baf..00000000
--- a/test/typecheck/pass/constraint_sym/v4.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15
-
-constraint Size('n) = 'n in {32, 64}
-
-Use -Xconstraint_synonyms to enable constraint synonyms
diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail
deleted file mode 100644
index 96bf5e82..00000000
--- a/test/typecheck/pass/constraint_sym/v4.sail
+++ /dev/null
@@ -1,6 +0,0 @@
-
-constraint Size('n) = 'n in {32, 64}
-
-constraint Nat('n) = 'n >= 0
-
-val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/custom_flow.sail b/test/typecheck/pass/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/typecheck/pass/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail
index ffa6d033..3e2acf28 100644
--- a/test/typecheck/pass/exint.sail
+++ b/test/typecheck/pass/exint.sail
@@ -1,8 +1,8 @@
 type MyInt = {'n, true. atom('n)}
 
-val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)}
+val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n + 'm. atom('o)}
 
-val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)}
+val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n * 'm. atom('o)}
 
 overload operator + = {add}
 
@@ -14,7 +14,7 @@ let y = x + x * x
 
 let z : atom(7 * 8) = y
 
-type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
+type Range('n: Int, 'm: Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
 
 let a : Range(3, 4) = 3
 
diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail
index f6c0c073..6db518e8 100644
--- a/test/typecheck/pass/exist1.sail
+++ b/test/typecheck/pass/exist1.sail
@@ -22,6 +22,6 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
 let v8 = s_add(v7, 4)
diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail
index 42ec8cb1..e518609d 100644
--- a/test/typecheck/pass/exist2.sail
+++ b/test/typecheck/pass/exist2.sail
@@ -22,13 +22,13 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
-let v9 : {'n, 0 = 0. atom('n)} = 100
+let v9 : {'n, 0 == 0. atom('n)} = 100
 
 let v10 : int = v9
 
-type MyInt = {'n, 0 = 0. atom('n)}
+type MyInt = {'n, 0 == 0. atom('n)}
 
 val existential_int : int -> MyInt
 
@@ -37,8 +37,8 @@ val existential_range : forall 'n 'm.
 
 overload existential = {existential_int, existential_range}
 
-let v11 : {'n, 0 = 0. atom('n)} = existential(v10)
+let v11 : {'n, 0 == 0. atom('n)} = existential(v10)
 
-let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3))
+let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = 2
 
 let v13 : MyInt = existential(v10)
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
deleted file mode 100644
index ac41114f..00000000
--- a/test/typecheck/pass/exist_pattern.sail
+++ /dev/null
@@ -1,48 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-register n : nat
-
-register x : nat
-
-register y : nat
-
-type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)}
-
-let word : wordsize = 8 : range(0, 8)
-
-val main : unit -> int effect {wreg, rreg}
-
-function main () = {
-  n = 1;
-  y = match n {
-    0 => {
-      x = 21;
-      x
-    },
-    1 => {
-      x = 42;
-      x
-    },
-    z => {
-      x = 99;
-      x
-    }
-  };
-  match word {
-    8  => x = 32,
-    16 => x = 64,
-    32 => x = 128
-  };
-  match 0b010101 {
-    0b01 @ _ : vector(1, dec, bit) @ 0b101 => n = 42,
-    _ => n = 0
-  };
-  n = 3;
-  match n {
-    0 => 21,
-    1 => 42,
-    u => 99
-  }
-}
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail
index 44382213..b251cbf8 100644
--- a/test/typecheck/pass/exist_synonym.sail
+++ b/test/typecheck/pass/exist_synonym.sail
@@ -1,6 +1,6 @@
 
 // Type synonym with a constraint.
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regno('n: Int), 0 <= 'n < 32 = atom('n)
 
 // Existential with constrained type synonym.
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 9ee4b202..fb1b2619 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -2,6 +2,5 @@ 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 from atom(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33)
+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)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index e3414034..5bde04ba 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -2,6 +2,5 @@ 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 from atom(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8)
+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)
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index c41f2c4b..a647ef00 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), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 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 a17ed112..d8bad777 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), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 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/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 33d6cbcd..e81c467e 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -2,23 +2,23 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 
 let _ = test(32)
 
-Tried performing type coercion from atom(32) to atom('size) on 32
-Failed because
-atom(32) is not a subtype of atom('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 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
 
-* 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+  * '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
+  * '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
 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 25304155..21c4b348 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -2,23 +2,23 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 
 let _ = test(64)
 
-Tried performing type coercion from atom(64) to atom('size) on 64
-Failed because
-atom(64) is not a subtype of atom('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+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
 
-* 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+  * '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
+  * '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
 
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index c7e06dc7..43096686 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-type variable 'size is already bound
+type variable ('size : Int) is already bound
diff --git a/test/typecheck/pass/if_infer.sail b/test/typecheck/pass/if_infer.sail
new file mode 100644
index 00000000..f3fec1c4
--- /dev/null
+++ b/test/typecheck/pass/if_infer.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 3. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
new file mode 100644
index 00000000..95073799
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -0,0 +1,17 @@
+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 
+    
+    
diff --git a/test/typecheck/pass/if_infer/v1.sail b/test/typecheck/pass/if_infer/v1.sail
new file mode 100644
index 00000000..0938aaed
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 3. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b100[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
new file mode 100644
index 00000000..afa04343
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -0,0 +1,17 @@
+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 
+    
+    
diff --git a/test/typecheck/pass/if_infer/v2.sail b/test/typecheck/pass/if_infer/v2.sail
new file mode 100644
index 00000000..a49e1ed7
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v2.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n, 1 <= 'n <= 4. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect
new file mode 100644
index 00000000..8b149bc8
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v3.expect
@@ -0,0 +1,7 @@
+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
diff --git a/test/typecheck/pass/if_infer/v3.sail b/test/typecheck/pass/if_infer/v3.sail
new file mode 100644
index 00000000..0c3dec21
--- /dev/null
+++ b/test/typecheck/pass/if_infer/v3.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bool
+
+val f : unit -> {'n 'm, 'm == 3 & 1 <= 'n <= 'm. int('n)}
+
+function main((): unit) -> unit = {
+  let _ = 0b1001[if R then 0 else f()];
+  ()
+}
diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail
index dd761b83..95be790c 100644
--- a/test/typecheck/pass/inline_typ.sail
+++ b/test/typecheck/pass/inline_typ.sail
@@ -1,2 +1,2 @@
 
-function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file
+function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined
\ No newline at end of file
diff --git a/test/typecheck/pass/lexp_vec.sail b/test/typecheck/pass/lexp_vec.sail
new file mode 100644
index 00000000..605c3855
--- /dev/null
+++ b/test/typecheck/pass/lexp_vec.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+register V : vector(1, dec, vector(32, dec, bit))
+
+val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
+
+function main() : unit -> unit = {
+  V[0] = zeros()
+}
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
index a12e81da..f171eb9b 100644
--- a/test/typecheck/pass/nat_set.sail
+++ b/test/typecheck/pass/nat_set.sail
@@ -1,4 +1,4 @@
-function test x : atom('n) -> forall 'n. bool = true
+function test forall 'n, 'n in {1, 3}. x : atom('n) -> bool = true
 
 let x = test(1)
 
diff --git a/test/typecheck/pass/nlflow.sail b/test/typecheck/pass/nlflow.sail
new file mode 100644
index 00000000..95d2d280
--- /dev/null
+++ b/test/typecheck/pass/nlflow.sail
@@ -0,0 +1,16 @@
+$option -non_lexical_flow
+
+default Order dec
+
+$include <prelude.sail>
+$include <exception_basic.sail>
+
+val foo : forall 'n, 'n != 8. int('n) -> unit
+
+function test(xs: vector(4, dec, bit)) -> unit = {
+  if xs == 0b1000 then {
+    throw(Exception())
+  };
+  let y = unsigned(xs);
+  foo(y)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index de4458ed..ec4e72db 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -1,17 +1,17 @@
 default Order inc
 
-union option ('a : Type) = {None : unit, Some : 'a}
+union option('a: Type) = {None : unit, Some : 'a}
 
-function none () -> forall ('a : Type). option('a) = None()
+function none forall ('a : Type). () -> option('a) = None()
 
-function some x : 'a -> forall ('a : Type). option('a) = Some(x)
+function some forall ('a : Type). x : 'a -> option('a) = Some(x)
 
-function test x : option('a) -> forall ('a : Type). range(0, 1) = match x {
+function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   None() => 0,
   Some(y) => 1
 }
 
-union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b}
+union either('a: Type, 'b: Type) = {Left : 'a, Right : 'b}
 
 val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int
 
diff --git a/test/typecheck/pass/or_pattern.sail b/test/typecheck/pass/or_pattern.sail
deleted file mode 100644
index a6e11ecd..00000000
--- a/test/typecheck/pass/or_pattern.sail
+++ /dev/null
@@ -1,16 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    3 | 4       => (),
-    (1 | 2) | 3 => (),
-    1 | (2 | 3) => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/or_pattern/v1.expect b/test/typecheck/pass/or_pattern/v1.expect
deleted file mode 100644
index edf07f03..00000000
--- a/test/typecheck/pass/or_pattern/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "or_pattern/v1.sail", line 11, character 5 to line 11, character 5
-
-    y | z       => (),
-
-Bindings are not allowed in this context
diff --git a/test/typecheck/pass/or_pattern/v1.sail b/test/typecheck/pass/or_pattern/v1.sail
deleted file mode 100644
index 21bc87e8..00000000
--- a/test/typecheck/pass/or_pattern/v1.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    y | z       => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index 94b40885..86294543 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -3,20 +3,20 @@ default Order dec
 infix 4 ==
 
 val extz = {ocaml: "extz", lem: "extz_vec"}: forall ('n : Int) ('m : Int) ('ord : Order).
-  (atom('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
+  (int('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
 
 val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type).
-  vector('m, 'ord, 'a) -> atom('m)
+  vector('m, 'ord, 'a) -> int('m)
 
 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_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
-  (atom('n), atom('m)) -> bool
+val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+  (int('n), int('m)) -> bool
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool
 
-overload operator == = {eq_vec, eq_atom, eq}
+overload operator == = {eq_vec, eq_int, eq}
 
 val test : forall 'n, 'n in {32, 64}.
   vector('n, dec, bit) -> vector(64, dec, bit)
diff --git a/test/typecheck/pass/poly_list.sail b/test/typecheck/pass/poly_list.sail
new file mode 100644
index 00000000..cb8e9b49
--- /dev/null
+++ b/test/typecheck/pass/poly_list.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+$include <prelude.sail>
+
+function cons(x: int, xs: list(int)) -> list(int) = {
+  x :: xs
+}
+
+function poly_cons forall ('a : Type). (x: 'a, xs: list('a)) -> list('a) = {
+  x :: xs
+}
+
+function main((): unit) -> unit = {
+  let _ = cons(1, [|2, 3, 4|]);
+  let _ : list(int) = poly_cons(1, [|2, 3, 4|]);
+  // TODO: This fails due to different order of instantiation
+  // let _ = poly_cons(1 : int, [|2, 3, 4|]);
+  ()
+}
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index cbdb2c9d..588fd324 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index cd3e849a..de388c3e 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/reg_ref.sail b/test/typecheck/pass/reg_ref.sail
new file mode 100644
index 00000000..a81f6abf
--- /dev/null
+++ b/test/typecheck/pass/reg_ref.sail
@@ -0,0 +1,13 @@
+register reg : range(0, 10)
+
+val modify : register(range(0,10)) -> unit effect {wreg}
+
+function modify (r) = {
+  (*r) = 9;
+  (*r) = 10;
+  (*r) = 8
+}
+
+val test : unit -> unit effect {wreg}
+
+function test () = modify(ref reg)
diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail
index bb4a1a14..01bf7ad8 100644
--- a/test/typecheck/pass/simple_scattered.sail
+++ b/test/typecheck/pass/simple_scattered.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-scattered union ast ('datasize : Int) ('destsize : Int) ('regsize : Int)
+scattered union ast('datasize : Int, 'destsize : Int, 'regsize : Int)
 
 val execute : forall ('datasize : Int) ('destsize : Int) ('regsize : Int).
   ast('datasize, 'destsize, 'regsize) -> unit
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
new file mode 100644
index 00000000..f1c8bade
--- /dev/null
+++ b/test/typecheck/pass/tautology.sail
@@ -0,0 +1,65 @@
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val tautologies :  forall ('p : Bool) ('q : Bool) ('r : Bool). (bool('p), bool('q), bool('r)) -> unit effect {escape}
+
+function tautologies(p, q, r) = {
+  _not_prove(constraint('p));
+  _not_prove(constraint('q));
+  _not_prove(constraint('r));
+
+  // implication definition
+  _prove(constraint(not('p) | 'q --> ('p --> 'q)));
+  _prove(constraint(('p --> 'q) --> not('p) | 'q));
+  _prove(constraint(('p --> 'q) <--> not('p) | 'q));
+
+  // implication properties
+  _prove(constraint('p --> 'p));
+  _prove(constraint(('p --> 'q) & ('q --> 'r) --> ('p --> 'r)));
+  _prove(constraint(('p --> 'q) & 'p --> 'q));
+
+  _prove(constraint('p & 'q <--> 'q & 'p));
+  _prove(constraint('p | 'q <--> 'q | 'p));
+  _prove(constraint(('p <--> 'q) <--> ('q <--> 'p)));
+
+  // excluded middle
+  _prove(constraint('p | not('p)));
+
+  // de Morgan
+  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
+  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));
+
+  // contradiction
+  _prove(constraint('p & not('p) --> false));
+  {
+    assert(constraint('p & not('p)));
+    _prove(constraint(false))
+  };
+  _not_prove(constraint(false));
+
+  _prove(constraint(('p <--> 'q) & ('p | 'q) --> ('p & 'q)));
+  _prove(constraint(('p & 'q --> 'r) <--> ('p --> 'q --> 'r)));
+
+  {
+    assert(constraint('p));
+    _prove(constraint('p))
+  };
+  _not_prove(constraint('p));
+
+  {
+    assert(constraint('p));
+    assert(constraint('p --> 'q));
+    _prove(constraint('q));
+    assert(constraint('q --> 'r));
+    _prove(constraint('r))
+  };
+  _not_prove(constraint('q));
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
new file mode 100644
index 00000000..21911b15
--- /dev/null
+++ b/test/typecheck/pass/vec_length.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
new file mode 100644
index 00000000..68a4ca70
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -0,0 +1,13 @@
+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)
diff --git a/test/typecheck/pass/vec_length/v1.sail b/test/typecheck/pass/vec_length/v1.sail
new file mode 100644
index 00000000..735da89c
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
new file mode 100644
index 00000000..7ce8fd99
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -0,0 +1,13 @@
+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)
diff --git a/test/typecheck/pass/vec_length/v1_inc.sail b/test/typecheck/pass/vec_length/v1_inc.sail
new file mode 100644
index 00000000..b72738d1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.sail
@@ -0,0 +1,8 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
new file mode 100644
index 00000000..d123cabd
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -0,0 +1,13 @@
+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)
diff --git a/test/typecheck/pass/vec_length/v2.sail b/test/typecheck/pass/vec_length/v2.sail
new file mode 100644
index 00000000..4df62e81
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
new file mode 100644
index 00000000..e7d2b52f
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -0,0 +1,13 @@
+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)
diff --git a/test/typecheck/pass/vec_length/v2_inc.sail b/test/typecheck/pass/vec_length/v2_inc.sail
new file mode 100644
index 00000000..3f75fee1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length_inc.sail b/test/typecheck/pass/vec_length_inc.sail
new file mode 100644
index 00000000..a8dd707f
--- /dev/null
+++ b/test/typecheck/pass/vec_length_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index ff70dc1b..ad2592df 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -4,9 +4,9 @@ set -e
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 SAILDIR="$DIR/../.."
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 mkdir -p $DIR/rtpass
@@ -50,9 +50,9 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 
 for i in `ls $DIR/pass/ | grep sail`;
 do
-    if $SAILDIR/sail -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
+    if $SAILDIR/sail -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i;
     then
-	if $SAILDIR/sail -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
+	if $SAILDIR/sail -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i;
 	then
 	    if diff $DIR/rtpass/$i $DIR/rtpass2/$i;
 	    then
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
new file mode 100755
index 00000000..ba436daf
--- /dev/null
+++ b/test/typecheck/update_errors.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+
+
+for i in `ls $DIR/pass/ | grep sail`;
+do
+    shopt -s nullglob;
+    for file in $DIR/pass/${i%.sail}/*.sail;
+    do
+	pushd $DIR/pass > /dev/null;
+	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+	popd > /dev/null
+    done
+done