4 files changed, 50 insertions, 3 deletions
diff --git a/test/typecheck/pass/execute_decode_hard.sail b/test/typecheck/pass/execute_decode_hard.sail
new file mode 100644
index 00000000..d5e91b79
--- /dev/null
+++ b/test/typecheck/pass/execute_decode_hard.sail
@@ -0,0 +1,26 @@
+default Order dec
+
+$include <prelude.sail>
+
+union ast('D: Int), 'D in {32, 64, 128} = {
+  Instr1 : {'R, 'R in {32, 64}. (int('R), bits('D))}
+}
+
+val execute : forall 'd, 'd in {32, 64, 128}. ast('d) -> unit
+
+function clause execute(Instr1(r as int('R), d)) = {
+  _prove(constraint('R in {32, 64}));
+  if length(d) == 64 then {
+    let _ = d[r - 1 .. 0];
+    ()
+  }
+}
+
+function clause execute(Instr1((r as int('R), d))) = {
+  _prove(constraint('R in {32, 64}));
+  if length(d) == 64 then {
+    let _ = d[r - 1 .. 0];
+    ()
+  }
+}
+
diff --git a/test/typecheck/fpthreesimp.sail b/test/typecheck/pass/fpthreesimp.sail
index 3f759ba4..d0f44119 100644
--- a/test/typecheck/fpthreesimp.sail
+++ b/test/typecheck/pass/fpthreesimp.sail
@@ -4,11 +4,11 @@ $include <prelude.sail>
 
 val Zeros : forall 'N, 'N >= 0. int('N) -> bits('N)
 
-type FPExponent ('N : Int) = {'E, ('N = 16 & 'E = 5) | ('N = 32 & 'E = 8) | ('N = 64 & 'E = 11). int('E)}
+type FPExponent ('N : Int) = {'E, ('N == 16 & 'E == 5) | ('N == 32 & 'E == 8) | ('N == 64 & 'E == 11). int('E)}
 
-val FPThree : forall 'N, 'N in {16, 32, 64}. bits(1) -> bits('N)
+val FPThree : forall 'N, 'N in {16, 32, 64}. (implicit('N), bits(1)) -> bits('N)
 
-function FPThree(sign) = {
+function FPThree(N, sign) = {
   let E : FPExponent('N) = if 'N == 16 then 5 else if 'N == 32 then 8 else 11;
   sign @ 0b1 @ Zeros(E - 1) @ 0b1 @ Zeros('N - E - 2)
 }
 \ No newline at end of file
diff --git a/test/typecheck/pass/plus_one_unify.sail b/test/typecheck/pass/plus_one_unify.sail
new file mode 100644
index 00000000..0dceaa4c
--- /dev/null
+++ b/test/typecheck/pass/plus_one_unify.sail
@@ -0,0 +1,6 @@
+
+val f2 : forall 'm, 'm in {0,1}. (int('m+1)) -> int
+
+function f2(_) = 3
+
+let x = f2(1)
+\ No newline at end of file
diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail
new file mode 100644
index 00000000..5ca85f53
--- /dev/null
+++ b/test/typecheck/pass/recursion.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+val log2 : int -> int
+
+function log2(n) =
+  if n <= 1 then 0 else 1 + log2(n/2)
+
+termination_measure log2(n) = n
+
+val testlog2 : unit -> unit effect {escape}
+
+function testlog2() =
+  assert(log2(64) == 6)