Prototype Bi-directional type checking algorithm for sail

Started work on a bi-directional type checking algorithm for sail
based on Mark and Neel's typechecker for minisail in idl
repository. It's a bit different though, because we are working with
the unmodified sail AST, and not in let normal-form.

Currently, we can check a fragment of sail that includes pattern
matching (in both function clauses and switch statements), numeric
constraints (but not set constraints), function application, casts
between numeric types, assignments to local mutable variables,
sequential blocks, and (implicit) let expressions.

For example, we can correctly typecheck the following program:

val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus

val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id

val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id

val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch

function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
{
  switch x {
    case ([|10:30|]) y -> y
    case ([:31:]) _ -> sizeof 'N
    case ([|31:40|]) _ -> plus(60,3)
  }
}
and branch (([|51:63|]) _) = ten_id(sizeof 'N)

The typechecker has been set up so it can produce derivation trees for
the typing judgements and constraints, so for the above program we
have:

Checking function branch
Adding local binding x :: range<10, 'N>
|   Check { switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} } <= range<10, 'N>
|   |   Check switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} <= range<10, 'N>
|   |   |   Infer x => range<10, 'N>
|   |   Subset 'N >= 63 |- {'fv1 | 10 <= 'fv1 & 'fv1 <= 30} {'fv0 | 10 <= 'fv0 & 'fv0 <= 'N}
|   |   Adding local binding y :: range<10, 30>
|   |   |   Check y <= range<10, 'N>
|   |   |   |   Infer y => range<10, 30>
|   |   |   Subset 'N >= 63 |- {'fv4 | 10 <= 'fv4 & 'fv4 <= 30} {'fv3 | 10 <= 'fv3 & 'fv3 <= 'N}
|   |   Subset 'N >= 63 |- {'fv7 | 31 <= 'fv7 & 'fv7 <= 31} {'fv6 | 10 <= 'fv6 & 'fv6 <= 'N}
|   |   |   Check sizeof 'N <= range<10, 'N>
|   |   |   |   Infer sizeof 'N => atom<'N>
|   |   |   Subset 'N >= 63 |- {'fv10 | 'N <= 'fv10 & 'fv10 <= 'N} {'fv9 | 10 <= 'fv9 & 'fv9 <= 'N}
|   |   Subset 'N >= 63 |- {'fv13 | 31 <= 'fv13 & 'fv13 <= 40} {'fv12 | 10 <= 'fv12 & 'fv12 <= 'N}
|   |   |   Check plus(60, 3) <= range<10, 'N>
|   |   |   |   |   Infer 60 => atom<60>
|   |   |   |   |   Infer 3 => atom<3>
|   |   |   |   Infer plus(60, 3) => atom<((60 - 20) + (20 + 3))>
|   |   |   Subset 'N >= 63 |- {'fv20 | ((60 - 20) + (20 + 3)) <= 'fv20 & 'fv20 <= ((60 - 20) + (20 + 3))} {'fv19 | 10 <= 'fv19 & 'fv19 <= 'N}
Subset 'N >= 63 |- {'fv23 | 51 <= 'fv23 & 'fv23 <= 63} {'fv22 | 10 <= 'fv22 & 'fv22 <= 'N}
|   Check ten_id(sizeof 'N) <= range<10, 'N>
|   |   |   Infer sizeof 'N => atom<'N>
|   |   Prove 'N >= 63 |- 'N >= 10
|   |   Infer ten_id(sizeof 'N) => atom<'N>
|   Subset 'N >= 63 |- {'fv28 | 'N <= 'fv28 & 'fv28 <= 'N} {'fv27 | 10 <= 'fv27 & 'fv27 <= 'N}

Judgements are displayed in the order they occur - inference steps go
inwards bottom up, while checking steps go outwards top-down. The
subtyping rules from Mark and Neel's check_sub rule all are verified
using the Z3 constraint solver.

I have been a set of tests in test/typecheck which aim to exhaustively
test all the code paths in the typechecker, adding new tests everytime
I add support for a new construct.

The new checker is turned on using the -new_typecheck option, and can
be tested (from the toplevel sail directory) by running:

test/typecheck/run_tests.sh -new_typecheck
(currently passes 32/32)

and compared to the old typechecker by

test/typecheck/run_tests.sh
(currently passes 21/32)

33 files changed, 428 insertions, 0 deletions

diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail
new file mode 100644
index 00000000..1ad9f8bf
--- /dev/null
+++ b/test/typecheck/fail/assignment_simple1.sail
@@ -0,0 +1,16 @@
+
+val ([:10:], unit) -> [:10:] effect pure f
+
+function [:10:] f (x, y) = x
+
+val unit -> [:10:] effect pure test
+
+function [:10:] test () =
+{
+  z := 9;
+  z
+}
+
+val unit -> unit effect pure test2
+
+function unit test2 () = x := 10
diff --git a/test/typecheck/fail/assignment_simple2.sail b/test/typecheck/fail/assignment_simple2.sail
new file mode 100644
index 00000000..db45bbcf
--- /dev/null
+++ b/test/typecheck/fail/assignment_simple2.sail
@@ -0,0 +1,15 @@
+
+val ([:10:], unit) -> [:10:] effect pure f
+
+function [:10:] f (x, y) = x
+
+val unit -> [:10:] effect pure test
+
+function [:10:] test () =
+{
+  f(z, z := 10)
+}
+
+val unit -> unit effect pure test2
+
+function unit test2 () = x := 10
diff --git a/test/typecheck/fail/assignment_simple3.sail b/test/typecheck/fail/assignment_simple3.sail
new file mode 100644
index 00000000..2a596c29
--- /dev/null
+++ b/test/typecheck/fail/assignment_simple3.sail
@@ -0,0 +1,15 @@
+
+val (unit, [:10:]) -> [:10:] effect pure f
+
+function [:10:] f (x, y) = y
+
+val unit -> [:10:] effect pure test
+
+function [:10:] test () =
+{
+  f(z := 10, z)
+}
+
+val unit -> unit effect pure test2
+
+function unit test2 () = x := 10
diff --git a/test/typecheck/fail/case_simple1.sail b/test/typecheck/fail/case_simple1.sail
new file mode 100644
index 00000000..471c3565
--- /dev/null
+++ b/test/typecheck/fail/case_simple1.sail
@@ -0,0 +1,9 @@
+
+val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test
+
+function forall Nat 'N. [|10:'N|] case_test (x, y) =
+{
+  switch (x, y) {
+    case _ -> x
+  }
+}
diff --git a/test/typecheck/fail/cast_lexp1.sail b/test/typecheck/fail/cast_lexp1.sail
new file mode 100644
index 00000000..dad4c84c
--- /dev/null
+++ b/test/typecheck/fail/cast_lexp1.sail
@@ -0,0 +1,7 @@
+
+val unit -> nat effect pure test
+
+function nat test () = {
+  (int) y := 10;
+  y
+}
diff --git a/test/typecheck/fail/cast_simple.sail b/test/typecheck/fail/cast_simple.sail
new file mode 100644
index 00000000..19768fbe
--- /dev/null
+++ b/test/typecheck/fail/cast_simple.sail
@@ -0,0 +1,7 @@
+
+val unit -> nat effect pure test
+
+function nat test () = {
+  (int) y := ([|0:10|]) 10;
+  (nat) y
+}
diff --git a/test/typecheck/fail/fun_simple_constraints1.sail b/test/typecheck/fail/fun_simple_constraints1.sail
new file mode 100644
index 00000000..979e0cdf
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints1.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:64|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/fun_simple_constraints2.sail b/test/typecheck/fail/fun_simple_constraints2.sail
new file mode 100644
index 00000000..43a0b6d7
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints2.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(9)
diff --git a/test/typecheck/fail/fun_simple_constraints3.sail b/test/typecheck/fail/fun_simple_constraints3.sail
new file mode 100644
index 00000000..098054e4
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints3.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(plus(sizeof 'N, 1))
diff --git a/test/typecheck/fail/fun_simple_constraints4.sail b/test/typecheck/fail/fun_simple_constraints4.sail
new file mode 100644
index 00000000..07b8c596
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints4.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-54))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/fun_simple_constraints5.sail b/test/typecheck/fail/fun_simple_constraints5.sail
new file mode 100644
index 00000000..7e28db85
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints5.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-9))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/fun_simple_constraints6.sail b/test/typecheck/fail/fun_simple_constraints6.sail
new file mode 100644
index 00000000..6dc5e0e6
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints6.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'k, Nat 'm. ([:'n + 'k:], [:'m:]) -> [:'n + 'k + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/fun_simple_constraints7.sail b/test/typecheck/fail/fun_simple_constraints7.sail
new file mode 100644
index 00000000..00d2a172
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints7.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|11:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/fun_simple_constraints8.sail b/test/typecheck/fail/fun_simple_constraints8.sail
new file mode 100644
index 00000000..e4c02da0
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints8.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|11:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/fail/return_simple1.sail b/test/typecheck/fail/return_simple1.sail
new file mode 100644
index 00000000..1bbc0e73
--- /dev/null
+++ b/test/typecheck/fail/return_simple1.sail
@@ -0,0 +1,7 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return x
+}
diff --git a/test/typecheck/fail/return_simple2.sail b/test/typecheck/fail/return_simple2.sail
new file mode 100644
index 00000000..f212a945
--- /dev/null
+++ b/test/typecheck/fail/return_simple2.sail
@@ -0,0 +1,9 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  x;
+  return x;
+  x
+}
diff --git a/test/typecheck/fail/return_simple3.sail b/test/typecheck/fail/return_simple3.sail
new file mode 100644
index 00000000..df75c5bd
--- /dev/null
+++ b/test/typecheck/fail/return_simple3.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return 9;
+  x
+}
diff --git a/test/typecheck/fail/return_simple4.sail b/test/typecheck/fail/return_simple4.sail
new file mode 100644
index 00000000..aa7c3010
--- /dev/null
+++ b/test/typecheck/fail/return_simple4.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return x;
+  9
+}
diff --git a/test/typecheck/fail/return_simple5.sail b/test/typecheck/fail/return_simple5.sail
new file mode 100644
index 00000000..d6947d91
--- /dev/null
+++ b/test/typecheck/fail/return_simple5.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N. [|10:'N - 1|] -> [|10:'N - 1|] effect pure return_test
+
+function forall Nat 'N. [|10:'N - 1|] return_test x =
+{
+  return x;
+  sizeof 'N
+}
diff --git a/test/typecheck/fail/return_simple6.sail b/test/typecheck/fail/return_simple6.sail
new file mode 100644
index 00000000..0e118632
--- /dev/null
+++ b/test/typecheck/fail/return_simple6.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return x;
+  sizeof 'N
+}
diff --git a/test/typecheck/pass/assignment_simple.sail b/test/typecheck/pass/assignment_simple.sail
new file mode 100644
index 00000000..dc0c78d8
--- /dev/null
+++ b/test/typecheck/pass/assignment_simple.sail
@@ -0,0 +1,16 @@
+
+val ([:10:], unit) -> [:10:] effect pure f
+
+function [:10:] f (x, y) = x
+
+val unit -> [:10:] effect pure test
+
+function [:10:] test () =
+{
+  z := 10;
+  z
+}
+
+val unit -> unit effect pure test2
+
+function unit test2 () = x := 10
\ No newline at end of file
diff --git a/test/typecheck/pass/case_simple1.sail b/test/typecheck/pass/case_simple1.sail
new file mode 100644
index 00000000..e4a81a36
--- /dev/null
+++ b/test/typecheck/pass/case_simple1.sail
@@ -0,0 +1,9 @@
+
+val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test
+
+function forall Nat 'N. [|10:'N|] case_test (x, y) =
+{
+  switch (x, y) {
+    case _ -> y
+  }
+}
diff --git a/test/typecheck/pass/case_simple2.sail b/test/typecheck/pass/case_simple2.sail
new file mode 100644
index 00000000..0ffba780
--- /dev/null
+++ b/test/typecheck/pass/case_simple2.sail
@@ -0,0 +1,9 @@
+
+val forall Nat 'N, 'N >= 10. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test
+
+function forall Nat 'N. [|10:'N|] case_test (x, y) =
+{
+  switch (x, y) {
+    case _ -> x
+  }
+}
diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail
new file mode 100644
index 00000000..f1b87235
--- /dev/null
+++ b/test/typecheck/pass/case_simple_constraints.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  switch x {
+    case ([|10:30|]) y -> y
+    case ([:31:]) _ -> sizeof 'N
+    case ([|31:40|]) _ -> plus(60,3)
+  }
+}
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/pass/cast_lexp1.sail b/test/typecheck/pass/cast_lexp1.sail
new file mode 100644
index 00000000..b8b29b87
--- /dev/null
+++ b/test/typecheck/pass/cast_lexp1.sail
@@ -0,0 +1,7 @@
+
+val unit -> int effect pure test
+
+function int test () = {
+  (int) y := 10;
+  y
+}
diff --git a/test/typecheck/pass/cast_lexp2].sail b/test/typecheck/pass/cast_lexp2].sail
new file mode 100644
index 00000000..a6f6d299
--- /dev/null
+++ b/test/typecheck/pass/cast_lexp2].sail
@@ -0,0 +1,7 @@
+
+val unit -> int effect pure test
+
+function int test () = {
+  (nat) y := 10;
+  y
+}
diff --git a/test/typecheck/pass/cast_simple.sail b/test/typecheck/pass/cast_simple.sail
new file mode 100644
index 00000000..c1507f26
--- /dev/null
+++ b/test/typecheck/pass/cast_simple.sail
@@ -0,0 +1,7 @@
+
+val unit -> int effect pure test
+
+function int test () = {
+  (nat) y := ([|0:10|]) 10;
+  (int) y
+}
diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail
new file mode 100644
index 00000000..7fd502b0
--- /dev/null
+++ b/test/typecheck/pass/fun_simple_constraints1.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
\ No newline at end of file
diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail
new file mode 100644
index 00000000..338ef8e8
--- /dev/null
+++ b/test/typecheck/pass/fun_simple_constraints2.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n <= -10. [|'n:'n|] -> [:'n:] effect pure minus_ten_id 
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
+{
+  x
+}
+and branch (([|10:30|]) y) = y
+and branch (([:31:]) _) = sizeof 'N
+and branch (([|31:40|]) _) = plus(60,3)
+and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53))
+and branch (([|51:63|]) _) = ten_id(sizeof 'N)
diff --git a/test/typecheck/pass/return_simple1.sail b/test/typecheck/pass/return_simple1.sail
new file mode 100644
index 00000000..26e6fc1d
--- /dev/null
+++ b/test/typecheck/pass/return_simple1.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return x;
+  x
+}
diff --git a/test/typecheck/pass/return_simple2.sail b/test/typecheck/pass/return_simple2.sail
new file mode 100644
index 00000000..06ce9757
--- /dev/null
+++ b/test/typecheck/pass/return_simple2.sail
@@ -0,0 +1,11 @@
+
+val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N. [|10:'N|] return_test x =
+{
+  return x;
+  return x;
+  return x;
+  return x;
+  x
+}
diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail
new file mode 100644
index 00000000..7e81b5b2
--- /dev/null
+++ b/test/typecheck/pass/return_simple3.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'N, 'N >= 10. [|10:'N|] -> [|10:'N|] effect pure return_test
+
+function forall Nat 'N, 'N >= 10. [|10:'N|] return_test x =
+{
+  return x;
+  sizeof 'N
+}
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
new file mode 100755
index 00000000..49739b5a
--- /dev/null
+++ b/test/typecheck/run_tests.sh
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[0;33m'
+NC='\033[0m'
+
+for i in `ls $DIR/pass/`;
+do
+  printf "testing $i expecting pass: "
+  if $DIR/../../sail $1 $DIR/pass/$i 2> /dev/null;
+  then
+    printf "${GREEN}pass${NC}\n"
+  else
+    printf "${RED}fail${NC}\n"
+  fi
+done
+
+for i in `ls $DIR/fail/`;
+do
+  printf "testing $i expecting fail: "
+  if $DIR/../../sail $1 $DIR/fail/$i 2> /dev/null;
+  then
+    printf "${RED}pass${NC}\n"
+  else
+    printf "${GREEN}fail${NC}\n"
+  fi
+done