7 files changed, 67 insertions, 52 deletions

diff --git a/test/builtins/get_slice_int.sail b/test/builtins/get_slice_int.sail
index b64526d2..ef673daf 100644
--- a/test/builtins/get_slice_int.sail
+++ b/test/builtins/get_slice_int.sail
@@ -199,7 +199,8 @@ function main (() : unit) -> unit = {
   assert(get_slice_int(4, 6, 0) == 4^0x6, "get_slice_int(4, 6, 0) == 4^0x6");
   assert(get_slice_int(4, 7, 0) == 4^0x7, "get_slice_int(4, 7, 0) == 4^0x7");
   assert(get_slice_int(4, 8, 0) == 4^0x8, "get_slice_int(4, 8, 0) == 4^0x8");
-  assert(get_slice_int(4, undefined, 0) == 4^0x0, "get_slice_int(4, undefined, 0) == 4^0x0");
+  // Not sure we want this property!
+  // assert(get_slice_int(4, undefined, 0) == 4^0x0, "get_slice_int(4, undefined, 0) == 4^0x0");
   assert(get_slice_int(5, 0, 0) == 5^0x0, "get_slice_int(5, 0, 0) == 5^0x0");
   assert(get_slice_int(5, 1, 0) == 5^0x1, "get_slice_int(5, 1, 0) == 5^0x1");
   assert(get_slice_int(5, 17, 0) == 5^0x11, "get_slice_int(5, 17, 0) == 5^0x11");
diff --git a/test/c/list_test.sail b/test/c/list_test.sail
index c315d3bf..b89e0f47 100644
--- a/test/c/list_test.sail
+++ b/test/c/list_test.sail
@@ -20,8 +20,8 @@ val main : unit -> unit
 
 function main () = {
   let x : list(int) = [|1, 2, 3|];
-  let y = hd(0 : int, x);
+  let y : int = hd(0, x);
   print_int("y = ", y);
-  print_int("hd(tl(x)) = ", hd(0, tl(x)));
-  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))));
+  print_int("hd(tl(x)) = ", hd(0, tl(x)) : int);
+  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))) : int);
 }
\ No newline at end of file
diff --git a/test/typecheck/pass/constraint_ctor.sail b/test/typecheck/pass/constraint_ctor.sail
index 2b4a5746..17ec74ce 100644
--- a/test/typecheck/pass/constraint_ctor.sail
+++ b/test/typecheck/pass/constraint_ctor.sail
@@ -18,3 +18,12 @@ 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/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/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/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|]);
+  ()
+}