diff --git a/.gitignore b/.gitignore
index ed56e0546..0bdd47e8a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,7 +6,7 @@ __pycache__
 *.pyc
 
 /_build
-*/_build
+**/_build
 /_opam
 /_docker_build
 /docs/_build
diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml
index 4af3fab57..587a0ed3c 100644
--- a/src/ligo/ast_simplified.ml
+++ b/src/ligo/ast_simplified.ml
@@ -81,6 +81,7 @@ and instruction =
   | Loop of ae * b
   | Skip
   | Fail of ae
+  | Record_patch of ae * (string * ae) list
 
 and matching =
   | Match_bool of {
@@ -106,22 +107,38 @@ module Simplify = struct
 
   let nseq_to_list (hd, tl) = hd :: tl
   let npseq_to_list (hd, tl) = hd :: (List.map snd tl)
+  let npseq_to_nelist (hd, tl) = hd, (List.map snd tl)
+  let pseq_to_list = function
+    | None -> []
+    | Some lst -> npseq_to_list lst
+
+  let type_constants = [
+    ("nat", 0) ;
+    ("int", 0) ;
+  ]
 
   let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
     match t with
     | TPar x -> simpl_type_expression x.value.inside
-    | TAlias v -> ok @@ Type_variable v.value
+    | TAlias v -> (
+        match List.assoc_opt v.value type_constants with
+        | Some 0 -> ok @@ Type_constant (v.value, [])
+        | Some _ -> simple_fail "type constructor with wrong number of args"
+        | None -> ok @@ Type_variable v.value
+      )
     | TApp x ->
         let (name, tuple) = x.value in
-        let%bind lst = bind_list
-          @@ List.map simpl_type_expression
-          @@ npseq_to_list tuple.value.inside in
-        ok @@ Type_constant (name.value, lst)
+        let lst = npseq_to_list tuple.value.inside in
+        let%bind _ = match List.assoc_opt name.value type_constants with
+        | Some n when n = List.length lst -> ok ()
+        | Some _ -> simple_fail "type constructor with wrong number of args"
+        | None -> simple_fail "unrecognized type constants" in
+        let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
+        ok @@ Type_constant (name.value, lst')
     | TProd p ->
-        let%bind lst = bind_list
-          @@ List.map simpl_type_expression
+        let%bind tpl = simpl_list_type_expression
           @@ npseq_to_list p.value in
-        ok @@ Type_tuple lst
+        ok tpl
     | TRecord r ->
         let aux = fun (x, y) -> let%bind y = simpl_type_expression y in ok (x, y) in
         let%bind lst = bind_list
@@ -161,16 +178,32 @@ module Simplify = struct
         ok @@ ae @@ Application (ae @@ Variable f, arg)
     | EPar x -> simpl_expression x.value.inside
     | EUnit _ -> ok @@ ae @@ Literal Unit
-    | EBytes x -> ok @@ ae @@ Literal (Bytes (fst x.value))
+    | EBytes x -> ok @@ ae @@ Literal (Bytes (Bytes.of_string @@ fst x.value))
     | ETuple tpl ->
         simpl_list_expression
         @@ npseq_to_list tpl.value.inside
+    | ERecord (RecordInj r) ->
+        let%bind fields = bind_list
+          @@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
+          @@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
+          @@ npseq_to_list r.value.fields in
+        let aux prev (k, v) = SMap.add k v prev in
+        ok @@ ae @@ Record (List.fold_left aux SMap.empty fields)
+    | ERecord (RecordProj p) ->
+        let record = p.value.record_name.value in
+        let lst = List.map (fun (x:_ Raw.reg) -> x.value) @@ npseq_to_list p.value.field_path in
+        let aux prev cur =
+          ae @@ Record_accessor (prev, cur)
+        in
+        let init = ae @@ Variable record in
+        ok @@ List.fold_left aux init lst
     | EConstr (ConstrApp c) ->
         let (c, args) = c.value in
         let%bind arg =
           simpl_list_expression
           @@ npseq_to_list args.value.inside in
         ok @@ ae @@ Constructor (c.value, arg)
+    | EConstr _ -> simple_fail "econstr: not supported yet"
     | EArith (Add c) ->
         let%bind (a, b) = simpl_binop c.value in
         ok @@ ae @@ Constant ("ADD", [a;b])
@@ -181,7 +214,15 @@ module Simplify = struct
     | EString (String s) ->
         ok @@ ae @@ Literal (String s.value)
     | EString _ -> simple_fail "string: not supported yet"
-    | _ -> simple_fail "todo"
+    | ELogic (BoolExpr (False _)) ->
+        ok @@ ae @@ Literal (Bool false)
+    | ELogic (BoolExpr (True _)) ->
+        ok @@ ae @@ Literal (Bool true)
+    | ELogic _ -> simple_fail "logic: not supported yet"
+    | EList _ -> simple_fail "list: not supported yet"
+    | ESet _ -> simple_fail "set: not supported yet"
+    | EMap _ -> simple_fail "map: not supported yet"
+
 
   and simpl_binop (t:_ Raw.bin_op) : (ae * ae) result =
     let%bind a = simpl_expression t.arg1 in
@@ -196,7 +237,36 @@ module Simplify = struct
         let%bind lst = bind_list @@ List.map simpl_expression lst in
         ok @@ ae @@ Tuple lst
 
-  and simpl_lambda (t:Raw.lambda_decl) : lambda result = simple_fail "todo"
+  and simpl_local_declaration (t:Raw.local_decl) : instruction result =
+    match t with
+    | LocalVar x ->
+        let x = x.value in
+        let name = x.name.value in
+        let%bind t = simpl_type_expression x.var_type in
+        let type_annotation = Some t in
+        let%bind expression = simpl_expression x.init in
+        ok @@ Assignment {name;annotated_expression={expression with type_annotation}}
+    | LocalConst x ->
+        let x = x.value in
+        let name = x.name.value in
+        let%bind t = simpl_type_expression x.const_type in
+        let type_annotation = Some t in
+        let%bind expression = simpl_expression x.init in
+        ok @@ Assignment {name;annotated_expression={expression with type_annotation}}
+    | _ -> simple_fail "todo"
+
+  and simpl_param (t:Raw.param_decl) : named_type_expression result =
+    match t with
+    | ParamConst c ->
+        let c = c.value in
+        let type_name = c.var.value in
+        let%bind type_expression = simpl_type_expression c.param_type in
+        ok { type_name ; type_expression }
+    | ParamVar v ->
+        let c = v.value in
+        let type_name = c.var.value in
+        let%bind type_expression = simpl_type_expression c.param_type in
+        ok { type_name ; type_expression }
 
   and simpl_declaration (t:Raw.declaration) : declaration result =
     let open! Raw in
@@ -213,8 +283,130 @@ module Simplify = struct
         ok @@ Constant_declaration {name=name.value;annotated_expression={expression with type_annotation}}
     | LambdaDecl (FunDecl x) ->
         let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
-        simple_fail "todo"
-    | _ -> simple_fail "todo"
+        let%bind param = match npseq_to_list param.value.inside with
+          | [a] -> ok a
+          | _ -> simple_fail "only one param allowed" in
+        let%bind input = simpl_param param in
+        let name = name.value in
+        let binder = input.type_name in
+        let input_type = input.type_expression in
+        let%bind local_declarations = bind_list @@ List.map simpl_local_declaration local_decls in
+        let%bind instructions = bind_list
+          @@ List.map simpl_instruction
+          @@ npseq_to_list block.value.instr in
+        let%bind result = simpl_expression return in
+        let%bind output_type = simpl_type_expression ret_type in
+        let body = local_declarations @ instructions in
+        let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
+        let type_annotation = Some (Type_function (input_type, output_type)) in
+        ok @@ Constant_declaration {name;annotated_expression = {expression;type_annotation}}
+    | LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
+    | LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
+
+
+  and simpl_single_instruction (t:Raw.single_instr) : instruction result =
+    match t with
+    | ProcCall _ -> simple_fail "no proc call"
+    | Fail e ->
+        let%bind expr = simpl_expression e.value.fail_expr in
+        ok @@ Fail expr
+    | Skip _ -> ok @@ Skip
+    | Loop (While l) ->
+        let l = l.value in
+        let%bind cond = simpl_expression l.cond in
+        let%bind body = simpl_block l.block.value in
+        ok @@ Loop (cond, body)
+    | Loop (For _) ->
+        simple_fail "no for yet"
+    | Cond c ->
+        let c = c.value in
+        let%bind expr = simpl_expression c.test in
+        let%bind match_true = simpl_instruction_block c.ifso in
+        let%bind match_false = simpl_instruction_block c.ifnot in
+        ok @@ Matching (expr, (Match_bool {match_true; match_false}))
+    | Assign a ->
+        let a = a.value in
+        let%bind name = match a.lhs with
+          | Path (Name v) -> ok v.value
+          | _ -> simple_fail "no complex assignments yet"
+        in
+        let%bind annotated_expression = match a.rhs with
+          | Expr e -> simpl_expression e
+          | _ -> simple_fail "no weird assignments yet"
+        in
+        ok @@ Assignment {name ; annotated_expression}
+    | Case c ->
+        let c = c.value in
+        let%bind expr = simpl_expression c.expr in
+        let%bind cases = bind_list
+          @@ List.map (fun (x:Raw.case) -> let%bind i = simpl_instruction_block x.instr in ok (x.pattern, i))
+          @@ List.map (fun (x:_ Raw.reg) -> x.value)
+          @@ npseq_to_list c.cases.value in
+        let%bind m = simpl_cases cases in
+        ok @@ Matching (expr, m)
+    | RecordPatch r ->
+        let r = r.value in
+        let%bind record = match r.path with
+          | Name v -> ok v.value
+          | _ -> simple_fail "no complex assignments yet"
+        in
+        let%bind inj = bind_list
+          @@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
+          @@ List.map (fun (x:_ Raw.reg) -> x.value)
+          @@ npseq_to_list r.record_inj.value.fields in
+        ok @@ Record_patch ({expression=Variable record;type_annotation=None}, inj)
+    | MapPatch _ -> simple_fail "no map patch yet"
+
+  and simpl_cases (t:(Raw.pattern * block) list) : matching result =
+    let open Raw in
+    let get_var (t:Raw.pattern) = match t with
+      | PVar v -> ok v.value
+      | _ -> simple_fail "not a var"
+    in
+    match t with
+    | [(PFalse _, f) ; (PTrue _, t)]
+    | [(PTrue _, f) ; (PFalse _, t)] -> ok @@ Match_bool {match_true = t ; match_false = f}
+    | [(PSome v, some) ; (PNone _, none)]
+    | [(PNone _, none) ; (PSome v, some)] -> (
+        let (_, v) = v.value in
+        let%bind v = match v.value.inside with
+        | PVar v -> ok v.value
+        | _ -> simple_fail "complex patterns not supported yet" in
+        ok @@ Match_option {match_none = none ; match_some = (v, some) }
+      )
+    | [(PCons c, cons) ; (PList n, nil)]
+    | [(PList n, nil) ; (PCons c, cons)] ->
+        let%bind _ = match n with
+          | Sugar c -> (
+              match pseq_to_list c.value.inside with
+              | [] -> ok ()
+              | _ -> simple_fail "complex patterns not supported yet"
+            )
+          | Raw _ -> simple_fail "complex patterns not supported yet"
+        in
+        let%bind (a, b) =
+          match c.value with
+          | a, [(_, b)] ->
+              let%bind a = get_var a in
+              let%bind b = get_var b in
+              ok (a, b)
+          | _ -> simple_fail "complex patterns not supported yet"
+        in
+        ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil}
+    | _ -> simple_fail "complex patterns not supported yet"
+
+  and simpl_instruction_block (t:Raw.instruction) : block result =
+    match t with
+    | Single s -> let%bind i = simpl_single_instruction s in ok [ i ]
+    | Block b -> simpl_block b.value
+
+  and simpl_instruction (t:Raw.instruction) : instruction result =
+    match t with
+    | Single s -> simpl_single_instruction s
+    | Block _ -> simple_fail "no block instruction yet"
+
+  and simpl_block (t:Raw.block) : block result =
+    bind_list @@ List.map simpl_instruction (npseq_to_list t.instr)
 
   let simpl_program (t:Raw.ast) : program result =
     bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl
diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml
index 5a5397c56..84dd88845 100644
--- a/src/ligo/ast_typed.ml
+++ b/src/ligo/ast_typed.ml
@@ -42,6 +42,7 @@ and expression =
   | Literal of literal
   | Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
   | Variable of name
+  | Application of ae * ae
   | Lambda of {
       binder: name ;
       input_type: tv ;
@@ -60,6 +61,7 @@ and expression =
 
 
 and literal =
+  | Unit
   | Bool of bool
   | Int of int
   | Nat of int
@@ -91,22 +93,59 @@ and matching =
     }
   | Match_tuple of (name * b) list
 
+module PP = struct
+  open Format
+  open Ligo_helpers.PP
+
+  let rec type_value ppf (tv:type_value) : unit =
+    match tv with
+    | Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst
+    | Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m
+    | Type_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m
+    | Type_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
+    | Type_constant (c, []) -> fprintf ppf "%s" c
+    | Type_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n
+end
+
 open Ligo_helpers.Trace
 
+module Errors = struct
+  let different_kinds a b =
+    let title = "different kinds" in
+    let full = Format.asprintf "(%a) VS (%a)" PP.type_value a PP.type_value b in
+    error title full
+
+  let different_constants a b =
+    let title = "different constants" in
+    let full = Format.asprintf "%s VS %s" a b in
+    error title full
+
+  let different_size_constants a b =
+    let title = "constants have different sizes" in
+    let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
+    error title full
+
+  let different_size_tuples a b =
+    let title = "tuple have different sizes" in
+    let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
+    error title full
+end
+open Errors
+
 let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab with
-  | Type_tuple a, Type_tuple b -> (
+  | Type_tuple a as ta, (Type_tuple b as tb) -> (
       let%bind _ =
-        Assert.assert_true ~msg:"tuples with different sizes"
-        @@ List.(length a = length b) in
+        trace_strong (different_size_tuples ta tb)
+        @@ Assert.assert_true List.(length a = length b) in
       bind_list_iter type_value_eq (List.combine a b)
     )
-  | Type_constant (a, a'), Type_constant (b, b') -> (
+  | Type_constant (a, a') as ca, (Type_constant (b, b') as cb) -> (
       let%bind _ =
-        Assert.assert_true ~msg:"constants with different sizes"
-        @@ List.(length a' = length b') in
+        trace_strong (different_size_constants ca cb)
+        @@ Assert.assert_true List.(length a' = length b') in
       let%bind _ =
-        Assert.assert_true ~msg:"constants with different names"
-        @@ (a = b) in
+        trace_strong (different_constants a b)
+        @@ Assert.assert_true (a = b) in
       trace (simple_error "constant sub-expression")
       @@ bind_list_iter type_value_eq (List.combine a' b')
     )
@@ -136,7 +175,7 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w
       @@ bind_list_iter aux (List.combine a' b')
 
     )
-  | _ -> simple_fail "Different kinds of types"
+  | a, b -> fail @@ different_kinds a b
 
 let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
   match a, b with
@@ -151,6 +190,7 @@ let t_bool : type_value = Type_constant ("bool", [])
 let t_string : type_value = Type_constant ("string", [])
 let t_bytes : type_value = Type_constant ("bytes", [])
 let t_int : type_value = Type_constant ("int", [])
+let t_unit : type_value = Type_constant ("unit", [])
 
 let get_annotation (x:annotated_expression) = x.type_annotation
 
diff --git a/src/ligo/contracts/toto.ligo b/src/ligo/contracts/toto.ligo
new file mode 100644
index 000000000..84b965857
--- /dev/null
+++ b/src/ligo/contracts/toto.ligo
@@ -0,0 +1,8 @@
+type toto is record
+  a : nat ;
+  b : nat
+end
+
+const foo : int = 3
+
+
diff --git a/src/ligo/dune b/src/ligo/dune
index e96ee8c92..df889af1b 100644
--- a/src/ligo/dune
+++ b/src/ligo/dune
@@ -13,3 +13,10 @@
   )
   (flags (:standard -w +1..62-4-9-44-40-42-48@39@33 ))
 )
+
+(alias
+  (name runtest)
+  (action (run test/test.exe))
+  (deps (glob_files contracts/*))
+
+)
diff --git a/src/ligo/ligo-helpers/PP.ml b/src/ligo/ligo-helpers/PP.ml
new file mode 100644
index 000000000..15252672a
--- /dev/null
+++ b/src/ligo/ligo-helpers/PP.ml
@@ -0,0 +1,12 @@
+open Format
+module SMap = X_map.String
+
+let const s ppf () = pp_print_string ppf s
+
+let list_sep pp = pp_print_list ~pp_sep:(const " ; ") pp
+let pair_sep pp ppf (a, b) = fprintf ppf "(%a, %a)" pp a pp b
+let smap_sep pp ppf m =
+  let aux k v prev = (k, v) :: prev in
+  let new_pp ppf (k, v) = fprintf ppf "%s -> %a" k pp v in
+  let lst = List.rev @@ SMap.fold aux m [] in
+  fprintf ppf "%a" (list_sep new_pp) lst
diff --git a/src/ligo/ligo-helpers/trace.ml b/src/ligo/ligo-helpers/trace.ml
index 8fefe7910..47485c223 100644
--- a/src/ligo/ligo-helpers/trace.ml
+++ b/src/ligo/ligo-helpers/trace.ml
@@ -34,6 +34,10 @@ module Let_syntax = struct
   let bind m ~f = m >>? f
 end
 
+let trace_strong err = function
+  | Ok _ as o -> o
+  | Errors _ -> Errors [err]
+
 let trace err = function
   | Ok _ as o -> o
   | Errors errs -> Errors (err :: errs)
@@ -151,9 +155,9 @@ let pp_to_string pp () x =
 let errors_to_string = pp_to_string errors_pp
 
 module Assert = struct
-  let assert_true ~msg = function
+  let assert_true ?msg = function
     | true -> ok ()
-    | false -> simple_fail msg
+    | false -> simple_fail @@ Option.unopt ~default:"not true" msg
 
   let assert_equal_int ?msg a b =
     let msg = Option.unopt ~default:"not equal int" msg in
diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml
index 385b61c52..91186eac6 100644
--- a/src/ligo/ligo.ml
+++ b/src/ligo/ligo.ml
@@ -48,8 +48,8 @@ let parse (s:string) : AST_Raw.t result =
   ok program_cst
 
 
-let abstract (p:AST_Raw.t) : AST_Simplified.program result = AST_Simplified.Simplify.program p
+let simplify (p:AST_Raw.t) : Ast_simplified.program result = AST_Simplified.Simplify.simpl_program p
 
-let annotate_types (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p
+let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p
 
 let transpile (p:AST_Typed.program) : Mini_c.program result = Transpiler.translate_program p
diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml
index 48a0304bb..dd5da1b13 100644
--- a/src/ligo/test/test.ml
+++ b/src/ligo/test/test.ml
@@ -11,159 +11,43 @@ let test name f =
       Format.printf "Errors : {\n%a}\n%!" errors_pp errs ;
       raise Alcotest.Test_error
 
-open Mini_c
-open Combinators
-
-module Mini_c = struct
-
-  let simple_int_program body : program = [
-    Fun("main", function_int body)
-  ]
-
-  let run_int program n =
-    Run.run program (`Int n) >>? function
-    | `Int n -> ok n
-    | _ -> simple_fail "run_int : output not int"
-
-  let neg () =
-    let program : program = simple_int_program [
-        assign_variable "output" @@ neg_int (var_int "input") ;
-        assign_variable "output" @@ neg_int (var_int "output") ;
-        assign_variable "output" @@ neg_int (var_int "output") ;
-      ] in
-    run_int program 42 >>? fun output ->
-    Assert.assert_equal_int (-42) output >>? fun () ->
-    ok ()
-
-  let multiple_variables () =
-    let program = simple_int_program [
-        assign_variable "a" @@ neg_int (var_int "input") ;
-        assign_variable "b" @@ neg_int (var_int "a") ;
-        assign_variable "c" @@ neg_int (var_int "b") ;
-        assign_variable "d" @@ neg_int (var_int "c") ;
-        assign_variable "output" @@ neg_int (var_int "d") ;
-      ] in
-    run_int program 42 >>? fun output ->
-    Assert.assert_equal_int (-42) output >>? fun () ->
-    ok ()
-
-  let arithmetic () =
-    let expression = add_int (var_int "input") (neg_int (var_int "input")) in
-    let program = simple_int_program [
-        Assignment (Variable ("a", expression)) ;
-        Assignment (Variable ("b", var_int "a")) ;
-        Assignment (Variable ("output", var_int "b")) ;
-      ] in
-    let test n =
-      run_int program n >>? fun output ->
-      Assert.assert_equal_int 0 output >>? fun () ->
-      ok ()
-    in
-    let%bind _assert = bind_list @@ List.map test [42 ; 150 ; 0 ; -42] in
-    ok ()
-
-  let quote_ () =
-    let program = simple_int_program [
-        assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "input") (int 42)] ;
-        assign_function "g" @@ function_int [assign_variable "output" @@ neg_int (var_int "input")] ;
-        assign_variable "output" @@ apply_int (type_f_int @@ var "g") @@ apply_int (type_f_int @@ var "f") (var_int "input") ;
-      ] in
-    let%bind output = run_int program 42 in
-    let%bind _ = Assert.assert_equal_int (-84) output in
-    ok ()
-
-  let function_ () =
-    let program = simple_int_program [
-        assign_variable "a" @@ int 42 ;
-        assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "input") (var_int "a")] ;
-        let env = Environment.Small.of_list ["a", t_int] in
-        assign_variable "output" @@ apply_int (type_closure_int env @@ var "f") (var_int "input") ;
-      ] in
-    let%bind output = run_int program 100 in
-    let%bind _ = Assert.assert_equal_int 142 output in
-    ok ()
-
-  let functions_ () =
-    let program = simple_int_program [
-        assign_variable "a" @@ int 42 ;
-        assign_variable "b" @@ int 144 ;
-        assign_function "f" @@ function_int [
-          assign_variable "output" @@ add_int (var_int "input") (var_int "a")
-        ] ;
-        assign_function "g" @@ function_int [
-          assign_variable "output" @@ add_int (var_int "input") (var_int "b")
-        ] ;
-        let env_f = Environment.Small.of_list ["a", t_int] in
-        let env_g = Environment.Small.of_list ["b", t_int] in
-        assign_variable "output" @@ add_int
-          (apply_int (type_closure_int env_f @@ var "f") (var_int "input"))
-          (apply_int (type_closure_int env_g @@ var "g") (var_int "input"))
-      ] in
-    let%bind output = run_int program 100 in
-    let%bind _ = Assert.assert_equal_int 386 output in
-    ok ()
-
-  let rich_function () =
-    let program = simple_int_program [
-        assign_variable "a" @@ int 42 ;
-        assign_variable "b" @@ int 144 ;
-        assign_function "f" @@ function_int [assign_variable "output" @@ add_int (var_int "a") (var_int "b")] ;
-        let env = Environment.Small.of_list [("a", t_int) ; ("b", t_int)] in
-        assign_variable "output" @@ apply_int (type_closure_int env @@ var "f") (var_int "input") ;
-      ] in
-    let test n =
-      let%bind output = run_int program n in
-      let%bind _ = Assert.assert_equal_int 186 output in
-      ok () in
-    let%bind _assert = bind_list @@ List.map test [42 ; 150 ; 0 ; -42] in
-    ok ()
-
-  let main = "Mini_c", [
-      test "basic.neg" neg ;
-      test "basic.variables" multiple_variables ;
-      test "basic.arithmetic" arithmetic ;
-      test "basic.quote" quote_ ;
-      test "basic.function" function_ ;
-      test "basic.functions" functions_ ;
-      test "basic.rich_function" rich_function ;
-    ]
-end
-
 module Ligo = struct
-  let run (source:string) (input:Ligo.Typed.O.value) : Ligo.Typed.Value.value result =
-    parse_file source >>? fun program_ast ->
-    Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program ->
-    Ligo.Run.run typed_program input >>? fun output ->
-    ok output
-
-  let assert_value_int : Ligo.Typed.Value.value -> int result = function
-    | `Constant (`Int n) -> ok n
-    | _ -> simple_fail "not an int"
+  let pass (source:string) : unit result =
+    let%bind raw =
+      trace (simple_error "parsing") @@
+      parse_file source in
+    let%bind simplified =
+      trace (simple_error "simplifying") @@
+      simplify raw in
+    let%bind typed =
+      trace (simple_error "typing") @@
+      type_ simplified in
+    let%bind _mini_c =
+      trace (simple_error "transpiling") @@
+      transpile typed in
+    ok ()
 
   let basic () : unit result =
-    run "./contracts/toto.ligo" (Ligo.Typed.Value.int 42) >>? fun output ->
-    assert_value_int output >>? fun output ->
-    Assert.assert_equal_int 42 output >>? fun () ->
-    ok ()
+    Format.printf "basic test" ;
+    pass "./contracts/toto.ligo"
 
-  let display_basic () : unit result =
-    parse_file "./contracts/toto.ligo" >>? fun program_ast ->
-    Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program ->
-    Ligo.Transpile.program_to_michelson typed_program >>? fun node ->
-    let node = Tezos_utils.Cast.flatten_node node in
-    let str = Tezos_utils.Cast.node_to_string node in
-    Format.printf "Program:\n%s\n%!" str ;
-    ok ()
+  (* let display_basic () : unit result =
+   *   parse_file "./contracts/toto.ligo" >>? fun program_ast ->
+   *   Ligo.Typecheck.typecheck_program program_ast >>? fun typed_program ->
+   *   Ligo.Transpile.program_to_michelson typed_program >>? fun node ->
+   *   let node = Tezos_utils.Cast.flatten_node node in
+   *   let str = Tezos_utils.Cast.node_to_string node in
+   *   Format.printf "Program:\n%s\n%!" str ;
+   *   ok () *)
 
   let main = "Ligo", [
       test "basic" basic ;
-      test "basic.display" display_basic ;
     ]
 end
 
 let () =
   (* Printexc.record_backtrace true ; *)
   Alcotest.run "LIGO" [
-    main ;
+    Ligo.main ;
   ] ;
   ()
diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml
index a73aa7698..33f427066 100644
--- a/src/ligo/transpiler.ml
+++ b/src/ligo/transpiler.ml
@@ -66,7 +66,12 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
   | Literal (Nat n) -> ok (Literal (`Nat n), tv, env)
   | Literal (Bytes s) -> ok (Literal (`Bytes s), tv, env)
   | Literal (String s) -> ok (Literal (`String s), tv, env)
+  | Literal Unit -> ok (Literal `Unit, tv, env)
   | Variable name -> ok (Var name, tv, env)
+  | Application (a, b) ->
+      let%bind a = translate_annotated_expression env a in
+      let%bind b = translate_annotated_expression env b in
+      ok (Apply (a, b), tv, env)
   | Constructor (m, param) ->
       let%bind (param'_expr, param'_tv, _) = translate_annotated_expression env ae in
       let%bind map_tv = AST.get_t_sum ae.type_annotation in
diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml
index 496b8941e..af3700759 100644
--- a/src/ligo/typer.ml
+++ b/src/ligo/typer.ml
@@ -32,10 +32,39 @@ module Environment = struct
     List.assoc_opt s e.type_environment
   let add_type (e:t) (s:string) (tv:ele) : t =
     {e with type_environment = (s, tv) :: e.type_environment}
+
+  module PP = struct
+    open Format
+    open Ligo_helpers.PP
+
+    let value ppf (e:t) =
+      let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in
+      fprintf ppf "ValueEnv[%a]" (list_sep pp) e.environment
+
+    let type_ ppf e =
+      let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in
+      fprintf ppf "TypeEnv[%a]" (list_sep pp) e.type_environment
+
+    let full ppf e =
+      fprintf ppf "%a\n%a" value e type_ e
+  end
 end
 
 type environment = Environment.t
 
+module Errors = struct
+  let unbound_type_variable (e:environment) (n:string) =
+    let title = "unbound type variable" in
+    let full = Format.asprintf "%s in %a" n Environment.PP.type_ e in
+    error title full
+
+  let unrecognized_constant (n:string) =
+    let title = "unrecognized constant" in
+    let full = n in
+    error title full
+end
+open Errors
+
 let rec type_program (p:I.program) : O.program result =
   let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) =
     let%bind (e', d') = type_declaration e d in
@@ -99,6 +128,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
       let%bind m' = type_match e m in
       let%bind ex' = type_annotated_expression e ex in
       ok (e, O.Matching (ex', m'))
+  | Record_patch _ -> simple_fail "no record_patch yet"
 
 and type_match (e:environment) : I.matching -> O.matching result = function
   | Match_bool {match_true ; match_false} ->
@@ -148,7 +178,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
       ok (O.Type_record m)
   | Type_variable name ->
       let%bind tv =
-        trace_option (simple_error "unbound type variable")
+        trace_option (unbound_type_variable e name)
         @@ Environment.get_type e name in
       ok tv
   | Type_constant (cst, lst) ->
@@ -171,6 +201,9 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
   | Literal (Bool b) ->
       let%bind type_annotation = check O.t_bool in
       ok O.{expression = Literal (Bool b) ; type_annotation }
+  | Literal Unit ->
+      let%bind type_annotation = check O.t_unit in
+      ok O.{expression = Literal (Unit) ; type_annotation }
   | Literal (String s) ->
       let%bind type_annotation = check O.t_string in
       ok O.{expression = Literal (String s) ; type_annotation }
@@ -241,13 +274,23 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
       let%bind (name', tv) = type_constant name tv_lst in
       let%bind type_annotation = check tv in
       ok O.{expression = O.Constant (name', lst') ; type_annotation}
+  | Application (f, arg) ->
+      let%bind f = type_annotated_expression e f in
+      let%bind arg = type_annotated_expression e arg in
+      let%bind type_annotation = match f.type_annotation with
+        | Type_function (param, result) ->
+            let%bind _ = O.type_value_eq (param, arg.type_annotation) in
+            ok result
+        | _ -> simple_fail "applying to not-a-function"
+      in
+      ok O.{expression = Application (f, arg) ; type_annotation}
 
 and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value) result =
   (* Constant poorman's polymorphism *)
   let open O in
   match (name, lst) with
-  | "add", [a ; b] when a = t_int && b = t_int -> ok ("add_int", t_int)
-  | "add", [a ; b] when a = t_string && b = t_string -> ok ("concat_string", t_string)
-  | "add", [_ ; _] -> simple_fail "bad types to add"
-  | "add", _ -> simple_fail "bad number of params to add"
-  | _ -> simple_fail "unrecognized constant"
+  | "ADD", [a ; b] when a = t_int && b = t_int -> ok ("ADD_INT", t_int)
+  | "ADD", [a ; b] when a = t_string && b = t_string -> ok ("CONCAT", t_string)
+  | "ADD", [_ ; _] -> simple_fail "bad types to add"
+  | "ADD", _ -> simple_fail "bad number of params to add"
+  | name, _ -> fail @@ unrecognized_constant name