diff --git a/src/ligo/contracts/function-shared.ligo b/src/ligo/contracts/function-shared.ligo
index fb8009781..c84fec402 100644
--- a/src/ligo/contracts/function-shared.ligo
+++ b/src/ligo/contracts/function-shared.ligo
@@ -2,7 +2,7 @@ function inc ( const i : int ) : int is
  block { skip } with i + 1
 
 function double_inc ( const i : int ) : int is
- block { skip } with inc(inc(i))
+ block { skip } with inc(i + 1)
 
 function foo ( const i : int ) : int is
  block { skip } with inc(i) + double_inc(i)
diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml
index ac98222b2..b038b1c5c 100644
--- a/src/ligo/mini_c/PP.ml
+++ b/src/ligo/mini_c/PP.ml
@@ -73,7 +73,11 @@ and expression' ppf (e:expression') = match e with
   | E_make_none _ -> fprintf ppf "none"
   | E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
 
-and expression ppf (e', _, _) = expression' ppf e'
+and expression ppf (e' , _ , _) = expression' ppf e'
+
+and expression_with_type = fun ppf (e' , t , _) ->
+  fprintf ppf "%a : %a" expression' e' type_ t
+
 
 and function_ ppf ({binder ; input ; output ; body ; result ; capture_type}:anon_function_content) =
   fprintf ppf "fun[%s] (%s:%a) : %a %a return %a"
diff --git a/src/ligo/mini_c/compiler.ml b/src/ligo/mini_c/compiler.ml
index f93064db8..6955e3f07 100644
--- a/src/ligo/mini_c/compiler.ml
+++ b/src/ligo/mini_c/compiler.ml
@@ -115,164 +115,8 @@ and translate_function ({capture;content}:anon_function) : michelson result =
 
 and translate_expression ((expr', ty, env) as expr:expression) : michelson result =
   let error_message () = Format.asprintf  "%a" PP.expression expr in
-  let%bind (code : michelson) =
-    trace (error (thunk "compiling expression") error_message) @@
-    match expr' with
-    | E_literal v ->
-        let%bind v = translate_value v in
-        let%bind t = Compiler_type.type_ ty in
-        ok @@ seq [
-          prim ~children:[t;v] I_PUSH ;
-          prim I_PAIR ;
-        ]
-    | E_application((_, f_ty, _) as f, arg) -> (
-        match f_ty with
-        | T_function _ -> (
-            trace (simple_error "Compiling quote application") @@
-            let%bind f = translate_expression f in
-            let%bind arg = translate_expression arg in
-            ok @@ seq [
-              arg ;
-              i_unpair ;
-              dip f ;
-              dip i_unpair ;
-              prim I_EXEC ;
-              i_pair ;
-            ]
-          )
-        | T_deep_closure (small_env, _, _) -> (
-            let env' = Environment.of_small small_env in
-            let%bind add = Environment.to_michelson_anonymous_add env' in
-            let%bind f = translate_expression f in
-            let%bind arg = translate_expression arg in
-            ok @@ seq [
-              f ; i_unpair ; (* closure :: expr :: env *)
-              dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *)
-              i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *)
-              i_swap ; prim I_EXEC ;
-              i_pair ; (* expr :: env *)
-            ]
-          )
-        | T_shallow_closure (_, _, _) -> (
-            trace (simple_error "Compiling shallow closure application") @@
-            let%bind f = translate_expression f in
-            let%bind arg = translate_expression arg in
-            ok @@ seq [
-              i_comment "(* unit :: env *)" ;
-              i_comment "compute closure" ;
-              f ;
-              i_comment "(* (closure * unit) :: env *)" ;
-              i_comment "compute arg" ;
-              arg ;
-              i_comment "(* (arg * closure * unit) :: env *)" ;
-              i_comment "separate stuff" ;
-              i_unpair ; dip i_unpair ; dip i_unpair ;
-              i_comment "(* arg :: capture :: f :: unit :: env *)" ;
-              i_piar ;
-              i_exec ; (* output :: stack :: env *)
-              i_pair ; (* stack :: env *)
-            ]
-          )
-        | _ -> simple_fail "E_applicationing something not appliable"
-      )
-    | E_variable x ->
-        let%bind (get, _) = Environment.to_michelson_get env x in
-        ok @@ seq [
-          dip (seq [prim I_DUP ; get]) ;
-          i_piar ;
-        ]
-    | E_constant(str, lst) ->
-        let%bind lst' = bind_list @@ List.map translate_expression lst in
-        let%bind predicate = get_predicate str lst in
-        let%bind code = match (predicate, List.length lst) with
-          | Constant c, 0 -> ok (seq @@ lst' @ [c])
-          | Unary f, 1 -> ok (seq @@ lst' @ [f])
-          | Binary f, 2 -> ok (seq @@ lst' @ [f])
-          | Ternary f, 3 -> ok (seq @@ lst' @ [f])
-          | _ -> simple_fail "bad arity"
-        in
-        ok code
-    | E_empty_map sd ->
-        let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
-        let code = seq [
-            prim ~children:[src;dst] I_EMPTY_MAP ;
-            i_pair ;
-          ] in
-        ok code
-    | E_empty_list t ->
-        let%bind t' = Compiler_type.type_ t in
-        let code = seq [
-            prim ~children:[t'] I_NIL ;
-            i_pair ;
-          ] in
-        ok code
-    | E_make_none o ->
-        let%bind o' = Compiler_type.type_ o in
-        let code = seq [
-            prim ~children:[o'] I_NONE ;
-            i_pair ;
-          ] in
-        ok code
-    | E_function anon -> (
-        match anon.capture_type with
-        | No_capture ->
-            let%bind body = translate_quote_body anon in
-            let%bind input_type = Compiler_type.type_ anon.input in
-            let%bind output_type = Compiler_type.type_ anon.output in
-            let code = seq [
-                i_lambda input_type output_type body ;
-                i_pair ;
-              ] in
-            ok code
-        | Deep_capture small_env ->
-            (* Capture the variable bounds, assemble them. On call, append the input. *)
-            let senv_type = Compiler_environment.Small.to_mini_c_type small_env in
-            let%bind body = translate_closure_body anon senv_type in
-            let%bind capture = Environment.Small.to_mini_c_capture env small_env in
-            let%bind capture = translate_expression capture in
-            let%bind input_type = Compiler_type.type_ anon.input in
-            let%bind output_type = Compiler_type.type_ anon.output in
-            let code = seq [
-                capture ;
-                i_unpair ;
-                i_lambda input_type output_type body ;
-                i_piar ;
-                i_pair ;
-              ] in
-            ok code
-        | Shallow_capture env ->
-            (* Capture the whole environment. *)
-            let env_type = Compiler_environment.to_mini_c_type env in
-            let%bind body = translate_closure_body anon env_type in
-            let%bind input_type =
-              let input_type = Combinators.t_pair anon.input env_type in
-              Compiler_type.type_ input_type in
-            let%bind output_type = Compiler_type.type_ anon.output in
-            let code = seq [ (* stack :: env *)
-                i_comment "env on top" ;
-                dip i_dup ; i_swap ; (* env :: stack :: env *)
-                i_comment "lambda" ;
-                i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
-                i_comment "pair env + lambda" ;
-                i_piar ; (* (env * lambda) :: stack :: env *)
-                i_comment "new stack" ;
-                i_pair ; (* new_stack :: env *)
-              ] in
-            ok code
-      )
-    | E_Cond (c, a, b) -> (
-        let%bind c' = translate_expression c in
-        let%bind a' = translate_expression a in
-        let%bind b' = translate_expression b in
-        let%bind code = ok (seq [
-            c' ; i_unpair ;
-            i_if a' b' ;
-          ]) in
-        ok code
-      )
-  in
 
-  let%bind () =
+  let return code =
     let%bind (Ex_ty schema_ty) = Environment.to_ty env in
     let%bind output_type = Compiler_type.type_ ty in
     let%bind (Ex_ty output_ty) =
@@ -300,7 +144,176 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
       Tezos_utils.Memory_proto_alpha.parse_michelson code
         input_stack_ty output_stack_ty
     in
-    ok ()
+    ok code
+  in
+
+  let%bind (code : michelson) =
+    trace (error (thunk "compiling expression") error_message) @@
+    match expr' with
+    | E_literal v ->
+        let%bind v = translate_value v in
+        let%bind t = Compiler_type.type_ ty in
+        return @@ seq [
+          prim ~children:[t;v] I_PUSH ;
+          prim I_PAIR ;
+        ]
+    | E_application((_, f_ty, _) as f, arg) -> (
+        match f_ty with
+        | T_function _ -> (
+            trace (simple_error "Compiling quote application") @@
+            let%bind f = translate_expression f in
+            let%bind arg = translate_expression arg in
+            return @@ seq [
+              i_comment "quote application" ;
+              i_comment "get f" ;
+              f ;
+              i_comment "get arg" ;
+              arg ;
+              i_unpair ; dip i_unpair ;
+              prim I_EXEC ;
+              i_pair ;
+            ]
+          )
+        | T_deep_closure (_small_env, _, _) -> (
+            simple_fail "no compilation for deep closures app yet" ;
+          )
+        | T_shallow_closure (_, _, _) -> (
+            trace (simple_error "Compiling shallow closure application") @@
+            let%bind f' = translate_expression f in
+            let%bind arg' = translate_expression arg in
+            let error =
+              let error_title () = "michelson type-checking closure application" in
+              let error_content () =
+                Format.asprintf "Env : %a\nclosure : %a\narg : %a\n"
+                  PP.environment env
+                  PP.expression_with_type f
+                  PP.expression_with_type arg
+              in
+              error error_title error_content
+            in
+            trace error @@
+            return @@ seq [
+              i_comment "(* unit :: env *)" ;
+              i_comment "compute closure" ;
+              f' ;
+              i_comment "(* (closure * unit) :: env *)" ;
+              i_comment "compute arg" ;
+              arg' ;
+              i_comment "(* (arg * closure * unit) :: env *)" ;
+              i_comment "separate stuff" ;
+              i_unpair ; dip i_unpair ; dip i_unpair ;
+              i_comment "(* arg :: capture :: f :: unit :: env *)" ;
+              i_pair ;
+              i_exec ; (* output :: stack :: env *)
+              i_pair ; (* stack :: env *)
+            ]
+          )
+        | _ -> simple_fail "E_applicationing something not appliable"
+      )
+    | E_variable x ->
+        let%bind (get, _) = Environment.to_michelson_get env x in
+        return @@ seq [
+          dip (seq [prim I_DUP ; get]) ;
+          i_piar ;
+        ]
+    | E_constant(str, lst) ->
+        let%bind lst' = bind_list @@ List.map translate_expression lst in
+        let%bind predicate = get_predicate str lst in
+        let%bind code = match (predicate, List.length lst) with
+          | Constant c, 0 -> ok (seq @@ lst' @ [c])
+          | Unary f, 1 -> ok (seq @@ lst' @ [f])
+          | Binary f, 2 -> ok (seq @@ lst' @ [f])
+          | Ternary f, 3 -> ok (seq @@ lst' @ [f])
+          | _ -> simple_fail "bad arity"
+        in
+        return code
+    | E_empty_map sd ->
+        let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
+        let code = seq [
+            prim ~children:[src;dst] I_EMPTY_MAP ;
+            i_pair ;
+          ] in
+        return code
+    | E_empty_list t ->
+        let%bind t' = Compiler_type.type_ t in
+        let code = seq [
+            prim ~children:[t'] I_NIL ;
+            i_pair ;
+          ] in
+        return code
+    | E_make_none o ->
+        let%bind o' = Compiler_type.type_ o in
+        let code = seq [
+            prim ~children:[o'] I_NONE ;
+            i_pair ;
+          ] in
+        return code
+    | E_function anon -> (
+        match anon.capture_type with
+        | No_capture ->
+            let%bind body = translate_quote_body anon in
+            let%bind input_type = Compiler_type.type_ anon.input in
+            let%bind output_type = Compiler_type.type_ anon.output in
+            let code = seq [
+                i_lambda input_type output_type body ;
+                i_pair ;
+              ] in
+            return code
+        | Deep_capture small_env ->
+            (* Capture the variable bounds, assemble them. On call, append the input. *)
+            let senv_type = Compiler_environment.Small.to_mini_c_type small_env in
+            let%bind body = translate_closure_body anon senv_type in
+            let%bind capture = Environment.Small.to_mini_c_capture env small_env in
+            let%bind capture = translate_expression capture in
+            let%bind input_type = Compiler_type.type_ anon.input in
+            let%bind output_type = Compiler_type.type_ anon.output in
+            let code = seq [
+                capture ;
+                i_unpair ;
+                i_lambda input_type output_type body ;
+                i_piar ;
+                i_pair ;
+              ] in
+            return code
+        | Shallow_capture env ->
+            (* Capture the whole environment. *)
+            let env_type = Compiler_environment.to_mini_c_type env in
+            let%bind body = translate_closure_body anon env_type in
+            let%bind input_type =
+              let input_type = Combinators.t_pair anon.input env_type in
+              Compiler_type.type_ input_type in
+            let%bind output_type = Compiler_type.type_ anon.output in
+            let code = seq [ (* stack :: env *)
+                i_comment "env on top" ;
+                dip i_dup ; i_swap ; (* env :: stack :: env *)
+                i_comment "lambda" ;
+                i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
+                i_comment "pair env + lambda" ;
+                i_piar ; (* (env * lambda) :: stack :: env *)
+                i_comment "new stack" ;
+                i_pair ; (* new_stack :: env *)
+              ] in
+            let error =
+              let error_title () = "michelson type-checking trace" in
+              let error_content () =
+                Format.asprintf "Env : %a\n"
+                  PP.environment env
+              in
+              error error_title error_content
+            in
+            trace error @@
+            return code
+      )
+    | E_Cond (c, a, b) -> (
+        let%bind c' = translate_expression c in
+        let%bind a' = translate_expression a in
+        let%bind b' = translate_expression b in
+        let%bind code = ok (seq [
+            c' ; i_unpair ;
+            i_if a' b' ;
+          ]) in
+        return code
+      )
   in
 
   ok code
@@ -481,29 +494,32 @@ and translate_quote_body ({body;result} as f:anon_function_content) : michelson
   ok code
 
 and translate_closure_body ({body;result} as f:anon_function_content) (env_type:type_value) : michelson result =
-  let%bind body = translate_regular_block body in
+  let%bind body' = translate_regular_block body in
   let%bind expr = translate_expression result in
   let code = seq [
       i_comment "function body" ;
-      body ;
+      body' ;
       i_comment "function result" ;
       i_push_unit ; expr ; i_car ;
       dip i_drop ;
     ] in
 
   let%bind _assert_type =
-    let input = Combinators.t_pair env_type f.input in
+    let input = Combinators.t_pair f.input env_type in
     let output = f.output in
     let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ input in
     let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ output in
     let input_stack_ty = Stack.(input_ty @: nil) in
     let output_stack_ty = Stack.(output_ty @: nil) in
+    let body_env = (snd body).pre_environment in
     let error_message () =
       Format.asprintf
-        "\ncode : %a\ninput : %a\noutput : %a\n"
+        "\nmini_c code :%a\nmichelson code : %a\ninput : %a\noutput : %a\nenv : %a\n"
+        PP.function_ f
         Tezos_utils.Micheline.Michelson.pp code
         PP.type_ input
         PP.type_ output
+        PP.environment body_env
     in
     let%bind _ =
       Trace.trace_tzresult_lwt (
diff --git a/src/ligo/mini_c/compiler_type.ml b/src/ligo/mini_c/compiler_type.ml
index bddebbb2d..482102f55 100644
--- a/src/ligo/mini_c/compiler_type.ml
+++ b/src/ligo/mini_c/compiler_type.ml
@@ -68,12 +68,12 @@ module Ty = struct
         let%bind (Ex_ty capture) = environment_small c in
         let%bind (Ex_ty arg) = type_ arg in
         let%bind (Ex_ty ret) = type_ ret in
-        ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret)
+        ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret)
     | T_shallow_closure (c, arg, ret) ->
         let%bind (Ex_ty capture) = environment c in
         let%bind (Ex_ty arg) = type_ arg in
         let%bind (Ex_ty ret) = type_ ret in
-        ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret)
+        ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret)
     | T_map (k, v) ->
         let%bind (Ex_comparable_ty k') = comparable_type k in
         let%bind (Ex_ty v') = type_ v in
@@ -148,12 +148,12 @@ let rec type_ : type_value -> O.michelson result =
       let%bind capture = environment_small c in
       let%bind arg = type_ arg in
       let%bind ret = type_ ret in
-      ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret)
+      ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret)
   | T_shallow_closure (c, arg, ret) ->
       let%bind capture = environment c in
       let%bind arg = type_ arg in
       let%bind ret = type_ ret in
-      ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret)
+      ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret)
 
 and environment_element (name, tyv) =
   let%bind michelson_type = type_ tyv in