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)

42 files changed, 1843 insertions, 3 deletions

diff --git a/src/_tags b/src/_tags
index 8ec7acb9..83ca12e0 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,7 +1,7 @@
 true: -traverse, debug
 <**/*.ml>: bin_annot, annot
 <lem_interp> or <test>:  include
-<sail.{byte,native}>: use_pprint, use_nums
+<sail.{byte,native}>: use_pprint, use_nums, use_unix
 <pprint> or <pprint/src>: include
 
 # see http://caml.inria.fr/mantis/view.php?id=4943
diff --git a/src/ast.ml b/src/ast.ml
index c923ae3f..476c40b7 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -486,7 +486,7 @@ type
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
+val_spec_aux =  (* Value type specification *)
    VS_val_spec of typschm * id
  | VS_extern_no_rename of typschm * id
  | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
@@ -536,7 +536,7 @@ type
 
 type 
 'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+   VS_aux of val_spec_aux * 'a annot
 
 
 type 
diff --git a/src/constraint.ml b/src/constraint.ml
new file mode 100644
index 00000000..8b28fa4a
--- /dev/null
+++ b/src/constraint.ml
@@ -0,0 +1,306 @@
+open Big_int
+open Util
+
+(* ===== Integer Constraints ===== *)
+       
+type nexp_op = Plus | Minus | Mult
+
+type nexp =
+  | NFun of (nexp_op * nexp * nexp)
+  | N2n of nexp
+  | NConstant of big_int
+  | NVar of int
+
+let big_int_op : nexp_op -> big_int -> big_int -> big_int = function
+  | Plus -> add_big_int
+  | Minus -> sub_big_int
+  | Mult -> mult_big_int 
+              
+let rec arith constr =
+  let constr' = match constr with
+    | NFun (op, x, y) -> NFun (op, arith x, arith y)
+    | N2n c -> arith c
+    | c -> c
+  in                  
+  match constr' with
+  | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y)
+  | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x)
+  | c -> c
+
+(* ===== Boolean Constraints ===== *)
+ 
+type constraint_bool_op = And | Or
+
+type constraint_compare_op = Gt | Lt | GtEq | LtEq | Eq | NEq 
+
+let negate_comparison = function
+  | Gt -> LtEq
+  | Lt -> GtEq
+  | GtEq -> Lt
+  | LtEq -> Gt
+  | Eq -> NEq
+  | NEq -> Eq
+                                                            
+type 'a constraint_bool =
+  | BFun of (constraint_bool_op * 'a constraint_bool * 'a constraint_bool)
+  | Not of 'a constraint_bool
+  | CFun of (constraint_compare_op * 'a * 'a)
+  | Branch of ('a constraint_bool list)
+  | Boolean of bool
+       
+let rec pairs (xs : 'a list) (ys : 'a list) : ('a * 'b) list =
+  match xs with
+  | [] -> []
+  | (x :: xs) -> List.map (fun y -> (x, y)) ys @ pairs xs ys
+
+let rec unbranch : 'a constraint_bool -> 'a constraint_bool list = function
+  | Branch xs -> List.map unbranch xs |> List.concat
+  | Not x -> unbranch x |> List.map (fun y -> Not y)
+  | BFun (op, x, y) ->
+     let xs, ys = unbranch x, unbranch y in
+     List.map (fun (z, w) -> BFun (op, z, w)) (pairs xs ys)
+  | c -> [c]
+       
+(* Apply De Morgan's laws to push all negations to just before integer
+   constraints *)
+let rec de_morgan : 'a constraint_bool -> 'a constraint_bool = function
+  | Not (Not x) -> de_morgan x
+  | Not (BFun (And, x, y)) -> BFun (Or, de_morgan (Not x), de_morgan (Not y))
+  | Not (BFun (Or, x, y)) -> BFun (And, de_morgan (Not x), de_morgan (Not y))
+  | Not (Boolean b) -> Boolean (not b)
+  | BFun (op, x, y) -> BFun (op, de_morgan x, de_morgan y)
+  | c -> c
+
+(* Once De Morgan's laws are applied we can push all the Nots into
+   comparison constraints *)
+let rec remove_nots : 'a constraint_bool -> 'a constraint_bool = function
+  | BFun (op, x, y) -> BFun (op, remove_nots x, remove_nots y)
+  | Not (CFun (c, x, y)) -> CFun (negate_comparison c, x, y)
+  | c -> c
+           
+(* Apply distributivity so all Or clauses are within And clauses *)
+let rec distrib_step : 'a constraint_bool -> ('a constraint_bool * int) = function
+  | BFun (Or, x, BFun (And, y, z)) ->
+     let (xy, n) = distrib_step (BFun (Or, x, y)) in
+     let (xz, m) = distrib_step (BFun (Or, x, z)) in
+     BFun (And, xy, xz), n + m + 1
+  | BFun (Or, BFun (And, x, y), z) ->
+     let (xz, n) = distrib_step (BFun (Or, x, z)) in
+     let (yz, m) = distrib_step (BFun (Or, y, z)) in
+     BFun (And, xz, yz), n + m + 1
+  | BFun (op, x, y) ->
+     let (x', n) = distrib_step x in
+     let (y', m) = distrib_step y in
+     BFun (op, x', y'), n + m 
+  | c -> (c, 0)
+
+let rec distrib (c : 'a constraint_bool) : 'a constraint_bool =
+  let (c', n) = distrib_step c in
+  if n = 0 then c else distrib c'
+
+(* Once these steps have been applied, the constraint language is a
+   list of And clauses, each a list of Or clauses, with either
+   explicit booleans (LBool) or integer comparisons LFun. The flatten
+   function coverts from a constraint_bool to this representation. *)
+type 'a constraint_leaf =
+  | LFun of (constraint_compare_op * 'a * 'a)
+  | LBoolean of bool
+
+let rec flatten_or : 'a constraint_bool -> 'a constraint_leaf list = function
+  | BFun (Or, x, y) -> flatten_or x @ flatten_or y
+  | CFun comparison -> [LFun comparison]
+  | Boolean b -> [LBoolean b]
+  | _ -> assert false
+  
+let rec flatten : 'a constraint_bool -> 'a constraint_leaf list list = function
+  | BFun (And, x, y) -> flatten x @ flatten y
+  | Boolean b -> [[LBoolean b]]
+  | c -> [flatten_or c]
+
+let normalize (constr : 'a constraint_bool) : 'a constraint_leaf list list =
+  constr
+  |> de_morgan
+  |> remove_nots
+  |> distrib
+  |> flatten
+
+(* Get a set of variables from a constraint *)
+module IntSet = Set.Make(
+  struct
+    let compare = Pervasives.compare
+    type t = int
+  end)
+                    
+let rec int_expr_vars : nexp -> IntSet.t = function
+  | NConstant _ -> IntSet.empty
+  | NVar v -> IntSet.singleton v
+  | NFun (_, x, y) -> IntSet.union (int_expr_vars x) (int_expr_vars y)
+  | N2n x -> int_expr_vars x
+
+let leaf_expr_vars : nexp constraint_leaf -> IntSet .t = function
+  | LBoolean _ -> IntSet.empty
+  | LFun (_, x, y) -> IntSet.union (int_expr_vars x) (int_expr_vars y)
+
+let constraint_vars constr : IntSet.t =
+  constr
+  |> List.map (List.map leaf_expr_vars)
+  |> List.map (List.fold_left IntSet.union IntSet.empty)
+  |> List.fold_left IntSet.union IntSet.empty
+
+(* SMTLIB v2.0 format is based on S-expressions so we have a
+   lightweight representation of those here. *)
+type sexpr = List of (sexpr list) | Atom of string
+
+let sfun (fn : string) (xs : sexpr list) : sexpr = List (Atom fn :: xs) 
+                                              
+let rec pp_sexpr : sexpr -> string = function
+  | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")"
+  | Atom x -> x
+                   
+let var_decs constr =
+  constraint_vars constr
+  |> IntSet.elements
+  |> List.map (fun var -> sfun "declare-const" [Atom ("v" ^ string_of_int var); Atom "Int"])
+  |> string_of_list "\n" pp_sexpr
+
+let cop_sexpr op x y =
+  match op with
+  | Gt -> sfun ">" [x; y]
+  | Lt -> sfun "<" [x; y]
+  | GtEq -> sfun ">=" [x; y]
+  | LtEq -> sfun "<=" [x; y]
+  | Eq -> sfun "=" [x; y]
+  | NEq -> sfun "not" [sfun "=" [x; y]]
+
+let iop_sexpr op x y =
+  match op with
+  | Plus -> sfun "+" [x; y]
+  | Minus -> sfun "-" [x; y]
+  | Mult -> sfun "*" [x; y]
+
+let rec sexpr_of_nexp = function
+  | NFun (op, x, y) -> iop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y)
+  | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x]
+  | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *)
+  | NVar var -> Atom ("v" ^ string_of_int var)
+              
+let rec sexpr_of_cbool = function
+  | BFun (And, x, y) -> sfun "and" [sexpr_of_cbool x; sexpr_of_cbool y]
+  | BFun (Or, x, y) -> sfun "or" [sexpr_of_cbool x; sexpr_of_cbool y]
+  | Not x -> sfun "not" [sexpr_of_cbool x]
+  | CFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y)
+  | Branch xs -> sfun "BRANCH" (List.map sexpr_of_cbool xs)
+  | Boolean true -> Atom "true"
+  | Boolean false -> Atom "false"
+                     
+let sexpr_of_constraint_leaf = function
+  | LFun (op, x, y) -> cop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y)
+  | LBoolean true -> Atom "true"
+  | LBoolean false -> Atom "false"
+
+let sexpr_of_constraint constr : sexpr =
+  constr
+  |> List.map (List.map sexpr_of_constraint_leaf)
+  |> List.map (fun xs -> match xs with [x] -> x | _ -> (sfun "or" xs))
+  |> sfun "and"
+
+let smtlib_of_constraint constr : string =
+  "(push)\n"
+  ^ var_decs constr ^ "\n"
+  ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; sexpr_of_constraint constr])
+  ^ "\n(assert constraint)\n(check-sat)\n(pop)"
+
+type t = nexp constraint_bool
+
+type smt_result = Unknown of t list | Unsat of t
+                    
+let rec call_z3 constraints : smt_result =
+  let problems = unbranch constraints in
+  let z3_file =
+    problems
+    |> List.map normalize
+    |> List.map smtlib_of_constraint
+    |> string_of_list "\n" (fun x -> x)
+  in
+  
+  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
+  
+  let rec input_lines chan = function
+    | 0 -> []
+    | n ->
+       begin
+         let l = input_line chan in
+         let ls = input_lines chan (n - 1) in
+         l :: ls
+       end
+  in
+  
+  begin
+    let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
+    output_string tmp_chan z3_file;
+    close_out tmp_chan;
+    let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+    let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
+    let _ = Unix.close_process_in z3_chan in
+    Sys.remove input_file;
+    try
+      let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+      Unsat problem
+    with
+    | Not_found ->
+       z3_output
+       |> List.filter (fun (_, result) -> result = "unknown")
+       |> List.map fst
+       |> (fun unsolved -> Unknown unsolved)
+  end
+
+let string_of constr =
+  constr
+  |> unbranch
+  |> List.map normalize
+  |> List.map (fun c -> smtlib_of_constraint c)
+  |> string_of_list "\n" (fun x -> x)
+    
+(* ===== Abstract API for building constraints ===== *)
+
+(* These functions are exported from constraint.mli, and ensure that
+   the internal representation of constraints remains opaque. *)
+                    
+let implies (x : t) (y : t) : t =
+  BFun (Or, Not x, y)
+
+let conj (x : t) (y : t) : t =
+  BFun (And, x, y)
+
+let disj (x : t) (y : t) : t =
+  BFun (Or, x, y)
+
+let negate (x : t) : t = Not x
+
+let branch (xs : t list) : t = Branch xs
+
+let literal (b : bool) : t = Boolean b
+
+let lt x y : t = CFun (Lt, x, y)
+
+let lteq x y : t = CFun (LtEq, x, y)
+
+let gt x y : t = CFun (Gt, x, y)
+
+let gteq x y : t = CFun (GtEq, x, y)
+
+let eq x y : t = CFun (Eq, x, y)
+
+let neq x y : t = CFun (NEq, x, y)
+
+let pow2 x : nexp = N2n x
+
+let add x y : nexp = NFun (Plus, x, y)
+                                     
+let sub x y : nexp = NFun (Minus, x, y)
+                                     
+let mult x y : nexp = NFun (Mult, x, y)
+
+let constant (x : big_int) : nexp = NConstant x
+
+let variable (v : int) : nexp = NVar v
diff --git a/src/constraint.mli b/src/constraint.mli
new file mode 100644
index 00000000..3fb3d2f6
--- /dev/null
+++ b/src/constraint.mli
@@ -0,0 +1,30 @@
+type nexp
+type t
+
+type smt_result = Unknown of t list | Unsat of t
+       
+val call_z3 : t -> smt_result
+
+val string_of : t -> string
+                                           
+val implies : t -> t -> t
+val conj : t -> t -> t
+val disj : t -> t -> t
+val negate : t -> t
+val branch : t list -> t
+val literal : bool -> t
+
+val lt : nexp -> nexp -> t
+val lteq : nexp -> nexp -> t
+val gt : nexp -> nexp -> t
+val gteq : nexp -> nexp -> t
+val eq : nexp -> nexp -> t
+val neq : nexp -> nexp -> t
+
+val pow2 : nexp -> nexp
+val add : nexp -> nexp -> nexp
+val sub : nexp -> nexp -> nexp
+val mult : nexp -> nexp -> nexp
+
+val constant : Big_int.big_int -> nexp
+val variable : int -> nexp
diff --git a/src/process_file.ml b/src/process_file.ml
index 273979cf..12a067e1 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -88,6 +88,8 @@ let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind
 let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
   Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
+let opt_new_typecheck = ref false
+                                        
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs =
   let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
                 Type_internal.nabbrevs = Envmap.empty;
@@ -97,6 +99,9 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
                 {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc 
 		                                     | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec
 						     | _ -> Type_internal.Oinc)};} in
+  if !opt_new_typecheck
+  then let _ = Type_check_new.check Type_check_new.initial_env defs in ()
+  else ();
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs 
 
 let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
diff --git a/src/process_file.mli b/src/process_file.mli
index 2c18b830..bfc719cc 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,6 +48,8 @@ val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
+val opt_new_typecheck : bool ref
+                                                                              
 type out_type =
   | Lem_ast_out
   | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
diff --git a/src/sail.ml b/src/sail.ml
index 4e76551f..343a677c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -86,6 +86,9 @@ let options = Arg.align ([
   ( "-skip_constraints",
     Arg.Clear Type_internal.do_resolve_constraints,
     " (debug) skip constraint resolution in type-checking");
+  ( "-new_typecheck",
+    Arg.Set opt_new_typecheck,
+    " use new typechecker with Z3 constraint solving (experimental)");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
new file mode 100644
index 00000000..175586ed
--- /dev/null
+++ b/src/type_check_new.ml
@@ -0,0 +1,997 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Util
+open Big_int
+
+let debug = ref 1
+let depth = ref 0
+
+let typ_debug m = if !debug > 1 then prerr_endline m else ()
+
+let rec indent n = match n with
+  | 0 -> ""
+  | n -> "|   " ^ indent (n - 1)
+                                                            
+let typ_print m = if !debug > 0 then (prerr_endline (indent !depth ^ m)) else ()
+                                                                                
+let typ_error l m = raise (Reporting_basic.err_typ l m)
+
+let string_of_id = function
+  | Id_aux (Id v, _) -> v
+  | Id_aux (DeIid v, _) -> v
+
+let string_of_kid = function
+  | Kid_aux (Var v, _) -> v
+                             
+let id_loc = function
+  | Id_aux (_, l) -> l
+
+let kid_loc = function
+  | Kid_aux (_, l) -> l
+                       
+let string_of_base_effect_aux = function
+  | BE_rreg -> "rreg"  
+  | BE_wreg -> "wreg"  
+  | BE_rmem -> "rmem" 
+  | BE_rmemt -> "rmemt" 
+  | BE_wmem -> "wmem" 
+  | BE_eamem -> "eamem" 
+  | BE_exmem -> "exmem" 
+  | BE_wmv -> "wmv" 
+  | BE_wmvt -> "wmvt" 
+  | BE_barr -> "barr" 
+  | BE_depend -> "depend" 
+  | BE_undef -> "undef" 
+  | BE_unspec -> "unspec" 
+  | BE_nondet -> "nondet" 
+  | BE_escape -> "escape" 
+  | BE_lset -> "lset"
+  | BE_lret -> "lret"
+
+let string_of_base_kind_aux = function
+  | BK_type -> "Type"
+  | BK_nat -> "Nat"
+  | BK_order -> "Order"
+  | BK_effect -> "Effect"
+                 
+let string_of_base_effect = function
+  | BE_aux (beff, _) -> string_of_base_effect_aux beff
+
+let string_of_effect = function
+  | Effect_aux (Effect_var kid, _) ->
+     typ_debug "kid effect occured"; string_of_kid kid
+  | Effect_aux (Effect_set [], _) -> "pure"
+  | Effect_aux (Effect_set beffs, _) ->
+     "{" ^ string_of_list ", " string_of_base_effect beffs ^ "}" 
+
+let string_of_order = function
+  | Ord_aux (Ord_var kid, _) -> string_of_kid kid
+  | Ord_aux (Ord_inc, _) -> "inc"
+  | Ord_aux (Ord_dec, _) -> "dec"
+                                              
+let rec string_of_nexp = function
+  | Nexp_aux (nexp, _) -> string_of_nexp_aux nexp
+and string_of_nexp_aux = function
+  | Nexp_id id -> string_of_id id
+  | Nexp_var kid -> string_of_kid kid
+  | Nexp_constant c -> string_of_int c
+  | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")"
+  | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")"
+  | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")"
+  | Nexp_exp n -> "2 ^ " ^ string_of_nexp n
+  | Nexp_neg n -> "- " ^ string_of_nexp n
+ 
+let rec string_of_typ = function
+  | Typ_aux (typ, l) -> string_of_typ_aux typ
+and string_of_typ_aux = function
+  | Typ_wild -> "_"
+  | Typ_id id -> string_of_id id
+  | Typ_var kid -> string_of_kid kid
+  | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")"
+  | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">"
+  | Typ_fn (typ_arg, typ_ret, eff) ->
+     string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+and string_of_typ_arg = function
+  | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
+and string_of_typ_arg_aux = function
+  | Typ_arg_nexp n -> string_of_nexp n 
+  | Typ_arg_typ typ -> string_of_typ typ
+  | Typ_arg_order o -> string_of_order o
+  | Typ_arg_effect eff -> string_of_effect eff
+
+let string_of_n_constraint = function
+  | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
+  | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
+  | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
+  | NC_aux (NC_nat_set_bounded (kid, ns), _) ->
+     string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
+                                           
+let string_of_quant_item_aux = function
+  | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
+  | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "KIND " ^ string_of_kid kid
+  | QI_const constr -> string_of_n_constraint constr
+     
+let string_of_quant_item = function
+  | QI_aux (qi, _) -> string_of_quant_item_aux qi
+                                           
+let string_of_typquant_aux = function
+  | TypQ_tq quants -> "forall " ^ string_of_list ", " string_of_quant_item quants
+  | TypQ_no_forall -> ""
+    
+let string_of_typquant = function
+  | TypQ_aux (quant, _) -> string_of_typquant_aux quant
+
+let string_of_typschm (TypSchm_aux (TypSchm_ts (quant, typ), _)) =
+  string_of_typquant quant ^ ". " ^ string_of_typ typ
+                                                  
+let string_of_bind (typquant, typ) = string_of_typquant typquant ^ ". " ^ string_of_typ typ
+
+let string_of_lit (L_aux (lit, _)) =
+  match lit with
+  | L_unit -> "()"
+  | L_zero -> "bitzero" (* FIXME: Check *)
+  | L_one -> "bitone"
+  | L_true -> "true"
+  | L_false -> "false"
+  | L_num n -> string_of_int n
+  | L_hex n -> "0x" ^ n
+  | L_bin n -> "0b" ^ n
+  | L_undef -> "undefined"
+  | L_string str -> "\"" ^ str ^ "\""
+                                                                                        
+let rec string_of_exp (E_aux (exp, _)) =
+  match exp with
+  | E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }"
+  | E_id v -> string_of_id v
+  | E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp 
+  | E_lit lit -> string_of_lit lit
+  | E_return exp -> "return " ^ string_of_exp exp
+  | E_app (f, args) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp args ^ ")"
+  | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")"
+  | E_case (exp, cases) ->
+     "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
+  | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp
+  | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind
+  | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
+  | _ -> "INTERNAL"
+and string_of_pexp (Pat_aux (Pat_exp (pat, exp), _)) = string_of_pat pat ^ " -> " ^ string_of_exp exp
+and string_of_pat (P_aux (pat, l)) =
+  match pat with
+  | P_lit lit -> string_of_lit lit
+  | P_wild -> "_"
+  | P_id v -> string_of_id v
+  | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
+  | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
+  | _ -> "PAT"
+and string_of_lexp (LEXP_aux (lexp, _)) =
+  match lexp with
+  | LEXP_id v -> string_of_id v
+  | LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v
+  | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")"
+  | _ -> "LEXP"
+and string_of_letbind (LB_aux (lb, l)) =
+  match lb with
+  | LB_val_implicit (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
+  | LB_val_explicit (typschm, pat, exp) ->
+     string_of_typschm typschm ^ " " ^ string_of_pat pat ^ " = " ^ string_of_exp exp
+                           
+module Id = struct
+  type t = id
+  let compare id1 id2 =
+    match (id1, id2) with
+    | Id_aux (Id x, _), Id_aux (Id y, _) -> String.compare x y
+    | Id_aux (DeIid x, _), Id_aux (DeIid y, _) -> String.compare x y
+    | Id_aux (Id _, _), Id_aux (DeIid _, _) -> -1
+    | Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1
+end
+
+module Kid = struct
+  type t = kid
+  let compare kid1 kid2 = String.compare (string_of_kid kid1) (string_of_kid kid2)
+end
+
+module Bindings = Map.Make(Id)
+module KBindings = Map.Make(Kid)
+module KidSet = Set.Make(Kid)
+              
+module Env : sig
+  type t
+  val get_val_spec : id -> t -> typquant * typ
+  val add_val_spec : id -> typquant * typ -> t -> t
+  val get_local : id -> t -> typ
+  val add_local : id -> typ -> t -> t
+  val get_constraints : t -> n_constraint list
+  val add_constraint : n_constraint -> t -> t
+  val get_typ_var : kid -> t -> base_kind_aux
+  val add_typ_var : kid -> base_kind_aux -> t -> t
+  val get_ret_typ : t -> typ option
+  val add_ret_typ : typ -> t -> t
+  val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t
+  val get_typ_synonym : id -> t -> typ_arg list -> typ
+  val fresh_kid : t -> kid
+  val expand_synonyms : t -> typ -> typ
+  val empty : t                                   
+end = struct
+  type t =
+    { top_val_specs : (typquant * typ) Bindings.t;
+      locals : typ Bindings.t;
+      typ_vars : base_kind_aux KBindings.t;
+      typ_synonyms : (typ_arg list -> typ) Bindings.t;
+      constraints : n_constraint list;
+      ret_typ : typ option
+    }
+  
+  let empty =
+    { top_val_specs = Bindings.empty;
+      locals = Bindings.empty;
+      typ_vars = KBindings.empty;
+      typ_synonyms = Bindings.empty;
+      constraints = [];
+      ret_typ = None;
+    }
+
+  let counter = ref 0
+                           
+  let get_val_spec id env =
+    try Bindings.find id env.top_val_specs with
+    | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+
+  let add_val_spec id bind env =
+    if Bindings.mem id env.top_val_specs
+    then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound")
+    else
+      begin
+        typ_debug ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind);
+        { env with top_val_specs = Bindings.add id bind env.top_val_specs }
+      end                     
+
+  let get_local id env =
+    try Bindings.find id env.locals with
+    | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+
+  let add_local id typ env =
+    begin
+      typ_print ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ);
+      { env with locals = Bindings.add id typ env.locals }
+    end
+
+  let get_typ_var kid env =
+    try KBindings.find kid env.typ_vars with
+    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+
+  let add_typ_var kid k env =
+    if KBindings.mem kid env.typ_vars
+    then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
+    else
+      begin
+        typ_debug ("Adding kind identifier binding " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k);
+        { env with typ_vars = KBindings.add kid k env.typ_vars }
+      end
+
+  let rec wf_nexp env (Nexp_aux (nexp, l)) =
+    match nexp with
+    | Nexp_id _ -> typ_error l "Unimplemented: Nexp_id"
+    | Nexp_var kid ->
+       begin
+         match get_typ_var kid env with
+         | BK_nat -> ()
+         | kind -> typ_error l ("Constraint is badly formed, "
+                                ^ string_of_kid kid ^ " has kind "
+                                ^ string_of_base_kind_aux kind ^ " but should have kind Nat")
+       end
+    | Nexp_constant _ -> ()
+    | Nexp_times (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2
+    | Nexp_sum (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2
+    | Nexp_minus (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2
+    | Nexp_exp nexp -> wf_nexp env nexp (* MAYBE: Could put restrictions on what is allowed here *)
+    | Nexp_neg nexp -> wf_nexp env nexp
+
+  let wf_constraint env (NC_aux (nc, _)) =
+    match nc with
+    | NC_fixed (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+    | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+    | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+    | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
+      
+  let get_constraints env = env.constraints
+        
+  let add_constraint (NC_aux (_, l) as constr) env =
+    wf_constraint env constr;
+    begin
+      typ_debug ("Adding constraint " ^ string_of_n_constraint constr);
+      { env with constraints = constr :: env.constraints }
+    end
+
+  let fresh_kid env =
+    let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter), Parse_ast.Unknown) in
+    incr counter; fresh
+
+  let get_ret_typ env = env.ret_typ
+
+  let add_ret_typ typ env = { env with ret_typ = Some typ }
+
+  let add_typ_synonym id synonym env =
+    if Bindings.mem id env.typ_synonyms
+    then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
+    else
+      begin
+        typ_debug ("Adding typ synonym " ^ string_of_id id);
+        { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
+      end
+
+  let get_typ_synonym id env =
+    try Bindings.find id env.typ_synonyms with
+    | Not_found -> typ_error (id_loc id) ("No type synonym " ^ string_of_id id)
+
+  let rec expand_synonyms env (Typ_aux (typ, l)) =
+    match typ with
+    | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
+    | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
+    | Typ_app (id, args) ->
+       begin
+         try
+           let synonym = Bindings.find id env.typ_synonyms in
+           expand_synonyms env (synonym args)
+         with
+       | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l)
+       end
+    | typ -> Typ_aux (typ, l)
+  and expand_synonyms_arg env (Typ_arg_aux (typ_arg, l)) =
+    match typ_arg with
+    | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l)
+    | arg -> Typ_arg_aux (arg, l)
+
+end
+
+type tannot = (Env.t * typ) option
+ 
+let add_typquant (quant : typquant) (env : Env.t) : Env.t =
+  let rec add_quant_item env = function
+    | QI_aux (qi, _) -> add_quant_item_aux env qi
+  and add_quant_item_aux env = function
+    | QI_const constr -> Env.add_constraint constr env
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_nat env
+    | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var kid k env
+    | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!"
+  in
+  match quant with
+  | TypQ_aux (TypQ_no_forall, _) -> env
+  | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants
+
+let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
+let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
+let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
+ 
+let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
+let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
+let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
+
+type index_sort =
+  | IS_int
+  | IS_prop of kid * (nexp * nexp) list
+                         
+type tnf =
+  | Tnf_wild
+  | Tnf_id of id
+  | Tnf_var of kid
+  | Tnf_tup of tnf list
+  | Tnf_index_sort of index_sort
+  | Tnf_app of id * tnf_arg list
+and tnf_arg =
+  | Tnf_arg_nexp of nexp
+  | Tnf_arg_typ of tnf
+  | Tnf_arg_order of order
+  | Tnf_arg_effect of effect
+
+let rec string_of_tnf = function
+  | Tnf_wild -> "_"
+  | Tnf_id id -> string_of_id id
+  | Tnf_var kid -> string_of_kid kid
+  | Tnf_tup tnfs -> "(" ^ string_of_list ", " string_of_tnf tnfs ^ ")"
+  | Tnf_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_tnf_arg args ^ ">"
+  | Tnf_index_sort IS_int -> "INT"
+  | Tnf_index_sort (IS_prop (kid, props)) ->
+     "{" ^ string_of_kid kid ^ " | " ^ string_of_list " & " (fun (n1, n2) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2) props ^ "}"
+and string_of_tnf_arg = function
+  | Tnf_arg_nexp n -> string_of_nexp n 
+  | Tnf_arg_typ tnf -> string_of_tnf tnf
+  | Tnf_arg_order o -> string_of_order o
+  | Tnf_arg_effect eff -> string_of_effect eff
+                        
+let rec normalize_typ env (Typ_aux (typ, l)) =
+  match typ with
+  | Typ_wild -> Tnf_wild
+  | Typ_id (Id_aux (Id "int", _)) -> Tnf_index_sort IS_int
+  | Typ_id (Id_aux (Id "nat", _)) ->
+     let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nconstant 0, nvar kid)]))
+  | Typ_id v -> Tnf_id v
+  | Typ_var kid -> Tnf_var kid
+  | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs)
+  | Typ_app (Id_aux (Id "range", _), [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) ->
+     let kid = Env.fresh_kid env in
+     Tnf_index_sort (IS_prop (kid, [(n1, nvar kid); (nvar kid, n2)]))
+  | Typ_app (id, args) -> normalize_typ env (Env.get_typ_synonym id env args) 
+  | Typ_fn _ -> typ_error l ("Cannot normalize function type " ^ string_of_typ (Typ_aux (typ, l)))
+and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) =
+  match typ_arg with
+  | Typ_arg_nexp n -> Tnf_arg_nexp n
+  | Typ_arg_typ typ -> Tnf_arg_typ (normalize_typ env typ)
+  | Typ_arg_order o -> Tnf_arg_order o
+  | Typ_arg_effect e -> Tnf_arg_effect e
+
+(* Here's how the constraint generation works for subtyping
+
+X(b,c...) --> {a. Y(a,b,c...)} \subseteq {a. Z(a,b,c...)}
+
+this is equivalent to
+
+\forall b c. X(b,c) --> \forall a. Y(a,b,c) --> Z(a,b,c)
+
+\forall b c. X(b,c) --> \forall a. !Y(a,b,c) \/ !Z^-1(a,b,c)
+
+\forall b c. X(b,c) --> !\exists a. Y(a,b,c) /\ Z^-1(a,b,c)
+
+\forall b c. !X(b,c) \/ !\exists a. Y(a,b,c) /\ Z^-1(a,b,c)
+
+!\exists b c. X(b,c) /\ \exists a. Y(a,b,c) /\ Z^-1(a,b,c)
+
+!\exists a b c. X(b,c) /\ Y(a,b,c) /\ Z^-1(a,b,c)
+
+which is then a problem we can feed to the constraint solver expecting unsat.
+ *)
+
+let unaux_nexp (Nexp_aux (nexp, _)) = nexp
+                                       
+let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
+and nexp_subst_aux sv subst = function
+  | Nexp_id v -> Nexp_id v
+  | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid
+  | Nexp_constant c -> Nexp_constant c
+  | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
+  | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
+  | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
+
+let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
+and nc_subst_nexp_aux l sv subst = function
+  | NC_fixed (n1, n2) -> NC_fixed (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
+  | NC_nat_set_bounded (kid, ints) as set_nc ->
+      if compare kid sv = 0
+      then typ_error l ("Cannot substitute " ^ string_of_kid sv ^ " into set constraint " ^ string_of_n_constraint (NC_aux (set_nc, l)))
+      else set_nc
+                                           
+let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
+and typ_subst_nexp_aux sv subst = function
+  | Typ_wild -> Typ_wild
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> Typ_var kid
+  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
+and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l)
+and typ_subst_arg_nexp_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ)
+  | Typ_arg_order o -> Typ_arg_order o
+  | Typ_arg_effect eff -> Typ_arg_effect eff
+                              
+let rec props_subst sv subst props =
+  match props with
+  | [] -> []
+  | ((nexp1, nexp2) :: props) -> (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) :: props_subst sv subst props
+
+let rec nexp_constraint var_of (Nexp_aux (nexp, l)) =
+  match nexp with
+  | Nexp_id v -> typ_error l "Unimplemented: Cannot generate constraint from Nexp_id"
+  | Nexp_var kid -> Constraint.variable (var_of kid)
+  | Nexp_constant c -> Constraint.constant (big_int_of_int c)
+  | Nexp_times (nexp1, nexp2) -> Constraint.mult (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | Nexp_sum (nexp1, nexp2) -> Constraint.add (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint var_of nexp)
+  | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint var_of nexp)
+                                                                                                      
+let nc_constraint var_of (NC_aux (nc, _)) =
+  match nc with
+  | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | NC_nat_set_bounded (_, []) -> Constraint.literal false
+  | NC_nat_set_bounded (kid, (int :: ints)) ->
+     List.fold_left Constraint.disj
+                    (Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int int)))
+                    (List.map (fun i -> Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int i))) ints)
+
+let rec nc_constraints var_of ncs =
+  match ncs with
+  | [] -> Constraint.literal true
+  | [nc] -> nc_constraint var_of nc
+  | (nc :: ncs) ->
+     Constraint.conj (nc_constraint var_of nc) (nc_constraints var_of ncs)
+
+let prove env nc =
+  typ_print ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc);
+  let module Bindings = Map.Make(Kid) in
+  let bindings = ref Bindings.empty  in
+  let fresh_var kid =
+    let n = Bindings.cardinal !bindings in
+    bindings := Bindings.add kid n !bindings;
+    n
+  in
+  let var_of kid =
+    try Bindings.find kid !bindings with
+    | Not_found -> fresh_var kid
+  in
+  let constr = Constraint.conj (nc_constraints var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint var_of nc)) in
+  match Constraint.call_z3 constr with
+  | Constraint.Unsat _ -> typ_debug "unsat"; true
+  | Constraint.Unknown [] -> typ_debug "sat"; false
+  | Constraint.Unknown _ -> typ_debug "unknown"; false
+                                                   
+let rec subtyp_tnf env tnf1 tnf2 =
+  typ_print ("Subset " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_tnf tnf1 ^ " " ^ string_of_tnf tnf2);
+  let module Bindings = Map.Make(Kid) in
+  let bindings = ref Bindings.empty  in
+  let fresh_var kid =
+    let n = Bindings.cardinal !bindings in
+    bindings := Bindings.add kid n !bindings;
+    n
+  in
+  let var_of kid =
+    try Bindings.find kid !bindings with
+    | Not_found -> fresh_var kid
+  in
+  let rec neg_props props =
+    match props with
+    | [] -> Constraint.literal false
+    | [(nexp1, nexp2)] -> Constraint.gt (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+    | ((nexp1, nexp2) :: props) ->
+       Constraint.disj (Constraint.gt (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)) (neg_props props)
+  in
+  let rec pos_props props =
+    match props with
+    | [] -> Constraint.literal true
+    | [(nexp1, nexp2)] -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+    | ((nexp1, nexp2) :: props) ->
+       Constraint.conj (Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)) (pos_props props)
+  in
+  match (tnf1, tnf2) with
+  | Tnf_wild, Tnf_wild -> true
+  | Tnf_id v1, Tnf_id v2 -> Id.compare v1 v2 = 0
+  | Tnf_var kid1, Tnf_var kid2 -> Kid.compare kid1 kid2 = 0
+  | Tnf_tup tnfs1, Tnf_tup tnfs2 ->
+     begin
+       try List.for_all2 (subtyp_tnf env) tnfs1 tnfs2 with
+       | Invalid_argument _ -> false
+     end
+  | Tnf_app (v1, args1), Tnf_app (v2, args2) -> Id.compare v1 v2 = 0 && List.for_all2 (tnf_args_eq env) args1 args2
+  | Tnf_index_sort IS_int, Tnf_index_sort IS_int -> true
+  | Tnf_index_sort (IS_prop _), Tnf_index_sort IS_int -> true
+  | Tnf_index_sort (IS_prop (kid1, prop1)), Tnf_index_sort (IS_prop (kid2, prop2)) ->
+     begin
+       let kid3 = Env.fresh_kid env in
+       let (prop1, prop2) = props_subst kid1 (Nexp_var kid3) prop1, props_subst kid2 (Nexp_var kid3) prop2 in
+       let constr = Constraint.conj (nc_constraints var_of (Env.get_constraints env)) (Constraint.conj (pos_props prop1) (neg_props prop2)) in
+       match Constraint.call_z3 constr with
+       | Constraint.Unsat _ -> typ_debug "unsat"; true
+       | Constraint.Unknown [] -> typ_debug "sat"; false
+       | Constraint.Unknown _ -> typ_debug "unknown"; false
+     end
+  | _, _ -> false
+
+and tnf_args_eq env arg1 arg2 = true
+
+let subtyp l env typ1 typ2 =
+  if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2)
+  then ()
+  else typ_error l (string_of_typ typ1
+                    ^ " is not a subtype of " ^ string_of_typ typ2
+                    ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
+
+let rec nexp_frees (Nexp_aux (nexp, l)) =
+  match nexp with
+  | Nexp_id _ -> typ_error l "Unimplemented Nexp_id in nexp_frees"
+  | Nexp_var kid -> KidSet.singleton kid
+  | Nexp_constant _ -> KidSet.empty
+  | Nexp_times (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2)
+  | Nexp_sum (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2)
+  | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2)
+  | Nexp_exp n -> nexp_frees n
+  | Nexp_neg n -> nexp_frees n
+
+let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
+  match nexp1, nexp2 with
+  | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0
+  | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 = 0
+  | Nexp_constant c1, Nexp_constant c2 -> c1 = c2
+  | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+  | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+  | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b
+  | Nexp_exp n1, Nexp_exp n2 -> nexp_identical n1 n2
+  | Nexp_neg n1, Nexp_neg n2 -> nexp_identical n1 n2
+  | _, _ -> false
+                                               
+let rec unify_nexps l (Nexp_aux (nexp_aux1, _) as nexp1) nexp2 =
+  typ_debug ("UNIFYING NEXPS " ^ string_of_nexp nexp1 ^ " AND " ^ string_of_nexp nexp2);
+  match nexp_aux1 with
+  | Nexp_id v -> typ_error l "Unimplemented Nexp_id in unify nexp"
+  | Nexp_var kid -> (kid, nexp2)
+  | Nexp_sum (n1a, n1b) ->
+     if KidSet.is_empty (nexp_frees n1b)
+     then unify_nexps l n1a (nminus nexp2 n1b)
+     else
+       if KidSet.is_empty (nexp_frees n1a)
+       then unify_nexps l n1b (nminus nexp2 n1a)
+       else typ_error l ("Both sides of Nat expression " ^ string_of_nexp nexp1
+                         ^ " contain free type variables so it cannot be unified with " ^ string_of_nexp nexp2)
+  | _ -> typ_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
+
+let unify l env typ1 typ2 =
+  let merge_unifiers l kid nexp1 nexp2 =
+    match nexp1, nexp2 with
+    | Some n1, Some n2 ->
+       if nexp_identical n1 n2 then Some n1
+       else typ_error l ("Multiple non-identical unifiers for " ^ string_of_kid kid
+                         ^ ": " ^ string_of_nexp n1 ^ " and " ^ string_of_nexp n2)
+    | None, Some n2 -> Some n2
+    | Some n1, None -> Some n1
+    | None, None -> None
+  in
+  let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) =
+    typ_debug ("UNIFYING: " ^ string_of_typ typ1 ^ " AND " ^ string_of_typ typ2);
+    match typ1_aux, typ2_aux with
+    | Typ_wild, Typ_wild -> KBindings.empty
+    | Typ_id v1, Typ_id v2 ->
+       if compare v1 v2 = 0 then KBindings.empty
+       else typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
+    | Typ_var _, Typ_var _ -> typ_error l "Raw identifiers during unification"
+    | Typ_tup typs1, Typ_tup typs2 ->
+       begin
+         try List.fold_left (KBindings.merge (merge_unifiers l)) KBindings.empty (List.map2 (unify_typ l) typs1 typs2) with
+         | Invalid_argument _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2
+                                              ^ " tuple type is of different length")
+       end
+    | Typ_app (f1, args1), Typ_app (f2, args2) ->
+       begin
+         if Id.compare f1 f2 = 0
+         then
+           try List.fold_left (KBindings.merge (merge_unifiers l)) KBindings.empty (List.map2 (unify_typ_args l) args1 args2) with
+           | Invalid_argument _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2
+                                                ^ " functions applied to different number of arguments")
+         else typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
+       end
+    | _, _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) 
+  and unify_typ_args l (Typ_arg_aux (typ_arg_aux1, _) as typ_arg1) (Typ_arg_aux (typ_arg_aux2, _) as typ_arg2) =
+    match typ_arg_aux1, typ_arg_aux2 with
+    | Typ_arg_nexp n1, Typ_arg_nexp n2 -> let (kid, unifier) = unify_nexps l n1 n2 in KBindings.singleton kid unifier
+    | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2
+    | Typ_arg_order _, Typ_arg_order _ -> assert false (* FIXME *)
+    | Typ_arg_effect _, Typ_arg_effect _ -> assert false
+    | _, _ -> typ_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2)
+  in
+  let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in
+  unify_typ l typ1 typ2
+
+let infer_lit env (L_aux (lit_aux, l) as lit) =
+  match lit_aux with
+  | L_unit -> mk_typ (Typ_id (mk_id "unit"))
+  | L_zero -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant 0))]))
+  | L_one -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant 1))]))
+  | L_num n -> mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nconstant n))]))
+  | _ -> typ_error l ("Unimplemented literal " ^ string_of_lit lit)
+            
+let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as typ) =
+  let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in
+  match pat_aux with
+  | P_id v -> annot_pat (P_id v) typ, Env.add_local v typ env
+  | P_wild -> annot_pat P_wild typ, env
+  | P_typ (typ_annot, pat) ->
+     begin
+       subtyp l env typ_annot typ;
+       let (typed_pat, env) = bind_pat env pat typ_annot in
+       annot_pat (P_typ (typ_annot, typed_pat)) typ, env
+     end
+  | P_tup pats ->
+     begin
+       match typ_aux with
+       | Typ_tup typs ->
+          let bind_tuple_pat (tpats, env) pat typ =
+            let tpat, env = bind_pat env pat typ in tpat :: tpats, env
+          in
+          let tpats, env =
+            try List.fold_left2 bind_tuple_pat ([], env) pats typs with
+            | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length"
+          in
+          annot_pat (P_tup tpats) typ, env
+       | _ -> typ_error l "Cannot bind tuple pattern against non tuple type"
+     end
+  | P_lit lit ->
+     begin
+       let lit_typ = infer_lit env lit in
+       subtyp l env lit_typ typ;
+       annot_pat (P_lit lit) typ, env
+     end
+  | _ -> typ_error l ("Unhandled pat " ^ string_of_pat pat)
+
+and bind_lexp env (LEXP_aux (lexp_aux, (l, _))) typ =
+  let annot_lexp lexp typ = LEXP_aux (lexp, (l, Some (env, typ))) in
+  match lexp_aux with
+  | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v typ env
+  | LEXP_cast (typ_annot, v) ->
+     begin
+       subtyp l env typ typ_annot;
+       annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v typ_annot env
+     end
+  | LEXP_tup lexps ->
+     begin
+       let (Typ_aux (typ_aux, _)) = typ in
+       match typ_aux with
+       | Typ_tup typs ->
+          let bind_tuple_lexp (tlexps, env) lexp typ =
+            let tlexp, env = bind_lexp env lexp typ in tlexp :: tlexps, env
+          in
+          let tlexps, env =
+            try List.fold_left2 bind_tuple_lexp ([], env) lexps typs with
+            | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length"
+          in
+          annot_lexp (LEXP_tup tlexps) typ, env
+       | _ -> typ_error l "Cannot bind tuple l-expression against non tuple type"
+     end
+  | _ -> typ_error l ("Unhandled l-expression")
+                   
+let quant_items = function
+  | TypQ_aux (TypQ_tq qis, _) -> qis
+  | TypQ_aux (TypQ_no_forall, _) -> []
+                                      
+let is_nat_kid kid = function
+  | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | _ -> false
+
+let typ_of (E_aux (_, (_, tannot))) = match tannot with
+  | Some (_, typ) -> typ
+  | None -> assert false
+
+let crule r env exp typ =
+  incr depth;
+  typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ);  
+  let checked_exp = r env exp typ in
+  decr depth; checked_exp
+
+let irule r env exp =
+  incr depth;
+  let inferred_exp = r env exp in
+  typ_print ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp));
+  decr depth;
+  inferred_exp
+                   
+let rec check_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
+  let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
+  match (exp_aux, typ_aux) with
+  | E_block exps, _ ->
+     begin
+       let rec check_block l env exps typ = match exps with
+         | [] -> typ_error l "Empty block found"
+         | [exp] -> [crule check_exp env exp typ]
+         | (E_aux (E_assign (lexp, bind), _) :: exps) ->
+            let texp, env = bind_assignment env lexp bind in
+            texp :: check_block l env exps typ
+         | (exp :: exps) ->
+            let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
+            texp :: check_block l env exps typ
+       in
+       annot_exp (E_block (check_block l env exps typ)) typ
+     end
+  | E_case (exp, cases), _ ->
+     let inferred_exp = irule infer_exp env exp in
+     let check_case (Pat_aux (Pat_exp (pat, case), (l, _))) typ =
+       let tpat, env = bind_pat env pat (typ_of inferred_exp) in
+       Pat_aux (Pat_exp (tpat, crule check_exp env case typ), (l, None))
+     in
+     annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ
+  | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
+     begin
+       match letbind with
+       | LB_val_explicit (typschm, pat, bind) -> assert false
+       | LB_val_implicit (pat, bind) ->
+          let inferred_bind = irule infer_exp env bind in
+          let tpat, env = bind_pat env pat (typ_of inferred_bind) in
+          annot_exp (E_let (LB_aux (LB_val_implicit (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+     end
+  | _, _ -> 
+     let inferred_exp = irule infer_exp env exp
+     in (subtyp l env (typ_of inferred_exp) typ; inferred_exp)
+
+and bind_assignment env lexp (E_aux (_, (l, _)) as exp) =
+  let inferred_exp = irule infer_exp env exp in
+  let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
+  E_aux (E_assign (tlexp, inferred_exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit"))))), env'
+          
+and infer_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) : tannot exp =
+  let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
+  match exp_aux with
+  | E_id v -> annot_exp (E_id v) (Env.get_local v env)
+  | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
+  | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
+  | E_return exp ->
+     begin
+       match Env.get_ret_typ env with
+       | Some typ -> annot_exp (E_return (crule check_exp env exp typ)) (mk_typ (Typ_id (mk_id "unit")))
+       | None -> typ_error l "Return found in non-function environment"
+     end
+  | E_tuple exps ->
+     let inferred_exps = List.map (irule infer_exp env) exps in
+     annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps)))
+  | E_assign (lexp, bind) ->
+     fst (bind_assignment env lexp bind)
+  | E_cast (typ, exp) ->
+     let checked_exp = check_exp env exp typ in
+     annot_exp (E_cast (typ, checked_exp)) typ
+  | E_app (f, xs) ->
+     begin
+       let rec instantiate_quants quants kid nexp = match quants with
+         | [] -> []
+         | ((QI_aux (QI_id kinded_id, _) as quant) :: quants) ->
+            if is_nat_kid kid kinded_id then instantiate_quants quants kid nexp else quant :: instantiate_quants quants kid nexp
+         | ((QI_aux (QI_const nc, l)) :: quants) ->
+            QI_aux (QI_const (nc_subst_nexp kid (unaux_nexp nexp) nc), l) :: quants
+       in
+       let solve_quant = function
+         | QI_aux (QI_id _, _) -> false
+         | QI_aux (QI_const nc, _) -> prove env nc
+       in
+       let rec instantiate quants typs ret_typ args =
+         match quants, typs, args with
+         | [], [], [] -> ([], ret_typ)
+         | _, [], [] ->
+            if List.for_all solve_quant quants
+            then ([], ret_typ)
+            else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
+                              ^ " not resolved during function application of " ^ string_of_id f)
+         | _, [], _ -> typ_error l ("Function " ^ string_of_id f ^ " applied to too many arguments")
+         | _, _, [] -> typ_error l ("Function " ^ string_of_id f ^ " not applied to not enough arguments")
+         | _, (typ :: typs), (arg :: args) ->
+            begin
+              typ_debug ("INSTANTIATE: " ^ string_of_exp arg ^ " with " ^ string_of_typ typ ^ " NF " ^ string_of_tnf (normalize_typ env typ));
+              let iarg = irule infer_exp env arg in
+              typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg) ^ " NF " ^ string_of_tnf (normalize_typ env (typ_of iarg)));
+              let unifiers = unify l env typ (typ_of iarg) in
+              typ_debug (string_of_list ", " (fun (kid, nexp) -> string_of_kid kid ^ " => " ^ string_of_nexp nexp) (KBindings.bindings unifiers));
+              let typs' = List.map (fun typ -> List.fold_left (fun typ (kid, nexp) -> typ_subst_nexp kid (unaux_nexp nexp) typ)
+                                                              typ
+                                                              (KBindings.bindings unifiers)) typs in
+              let quants' = List.fold_left (fun qs (kid, nexp) -> instantiate_quants qs kid nexp) quants (KBindings.bindings unifiers) in
+              let ret_typ' = List.fold_left (fun typ (kid, nexp) -> typ_subst_nexp kid (unaux_nexp nexp) typ) ret_typ (KBindings.bindings unifiers) in
+              let (iargs, ret_typ'') = instantiate quants' typs' ret_typ' args in
+              (iarg :: iargs, ret_typ'')
+            end
+       in
+       let (typq, f_typ) = Env.get_val_spec f env in
+       match f_typ with
+       | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, effs), _) ->
+          let (xs, typ_ret) = instantiate (quant_items typq) typ_args typ_ret xs in
+          annot_exp (E_app (f, xs)) typ_ret
+       | Typ_aux (Typ_fn (typ_arg, typ_ret, effs), _) ->
+          let (xs, typ_ret) = instantiate (quant_items typq) [typ_arg] typ_ret xs in
+          annot_exp (E_app (f, xs)) typ_ret
+       | _ -> typ_error l (string_of_id f ^ " is not a function")
+     end         
+  | _ -> typ_error l "Unimplemented"
+
+let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ =
+  match typ with
+  | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
+     begin
+       let typed_pat, env = bind_pat env pat typ_arg in
+       let env = Env.add_ret_typ typ_ret env in
+       let exp = crule check_exp env exp typ_ret in
+       FCL_aux (FCL_Funcl (id, typed_pat, exp), (l, Some (env, typ)))
+     end
+  | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
+               
+let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux : 'a fundef) : tannot def =
+  let (Typ_annot_opt_aux (Typ_annot_opt_some (annot_quant, annot_typ1), _)) = tannotopt in
+  let id =
+    match (List.fold_right
+             (fun (FCL_aux (FCL_Funcl (id, _, _), _)) id' ->
+               match id' with
+               | Some id' -> if string_of_id id' = string_of_id id then Some id' 
+                             else typ_error l ("Function declaration expects all definitions to have the same name, " 
+                                               ^ string_of_id id ^ " differs from other definitions of " ^ string_of_id id')
+               | None -> Some id) funcls None)
+    with
+    | Some id -> id 
+    | None -> typ_error l "funcl list is empty"
+  in
+  typ_print ("\nChecking function " ^ string_of_id id);
+  let (quant, typ) = Env.get_val_spec id env in
+  typ_debug ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ));
+  typ_debug ("Annotation typ " ^ string_of_bind (annot_quant, annot_typ1));
+  let funcl_env = add_typquant quant env in
+  let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
+  DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None)))
+
+(* Checking a val spec simply adds the type as a binding in the
+   context. We have to destructure the various kinds of val specs, but
+   the difference is irrelvant for the typechecker. *)
+let check_val_spec env (VS_aux (vs, (l, _))) =
+  let (id, quants, typ) = match vs with
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ) 
+    | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ)
+    | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, _) -> (id, quants, typ) in
+  DEF_spec (VS_aux (vs, (l, None))), Env.add_val_spec id (quants, typ) env
+
+let rec check_def env def =
+  let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Case") in
+  match def with
+  | DEF_kind kdef -> cd_err ()
+  | DEF_type tdef -> cd_err ()
+  | DEF_fundef fdef -> check_fundef env fdef, env
+  | DEF_val letdef -> cd_err ()
+  | DEF_spec vs -> check_val_spec env vs
+  | DEF_default default -> cd_err ()
+  | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> cd_err ()
+  | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> cd_err ()
+  | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) -> cd_err ()
+  | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
+  | DEF_comm (DC_comm str) -> DEF_comm (DC_comm str), env
+  | DEF_comm (DC_comm_struct def) ->
+     let def, env = check_def env def
+     in DEF_comm (DC_comm_struct def), env
+
+let rec check env (Defs defs) = 
+  match defs with
+  | [] -> (Defs []), env
+  | def :: defs ->
+     let (def, env) = check_def env def in
+     let (Defs defs, env) = check env (Defs defs) in
+     (Defs (def::defs)), env
+
+let initial_env =
+  Env.empty
+  |> Env.add_typ_synonym (mk_id "atom") (fun args -> mk_typ (Typ_app (mk_id "range", args @ args)))
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
new file mode 100644
index 00000000..98e1171e
--- /dev/null
+++ b/src/type_check_new.mli
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+
+module Env : sig
+  type t
+  val get_val_spec : id -> t -> typquant * typ
+  val add_val_spec : id -> typquant * typ -> t -> t
+  val get_local : id -> t -> typ
+  val add_local : id -> typ -> t -> t
+  val get_constraints : t -> n_constraint list
+  val add_constraint : n_constraint -> t -> t
+  val get_typ_var : kid -> t -> base_kind_aux
+  val add_typ_var : kid -> base_kind_aux -> t -> t
+  val get_ret_typ : t -> typ option
+  val add_ret_typ : typ -> t -> t
+  val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t
+  val get_typ_synonym : id -> t -> typ_arg list -> typ
+  val fresh_kid : t -> kid
+  val expand_synonyms : t -> typ -> typ
+  val empty : t                                   
+end
+
+type tannot = (Env.t * typ) option
+               
+val check : Env.t -> 'a defs -> tannot defs * Env.t
+
+val initial_env : Env.t
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