diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml
index a8e6a8057..f75e39e38 100644
--- a/src/ligo/ast_simplified.ml
+++ b/src/ligo/ast_simplified.ml
@@ -150,6 +150,10 @@ module PP = struct
   and access_path ppf (p:access_path) =
     fprintf ppf "%a" (list_sep ~pp_sep:(const ".") access) p
 
+  and type_annotation ppf (ta:type_expression option) = match ta with
+    | None -> fprintf ppf ""
+    | Some t -> type_expression ppf t
+
   and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotation with
     | None -> fprintf ppf "%a" expression ae.expression
     | Some t -> fprintf ppf "(%a) : %a" expression ae.expression type_expression t
@@ -461,7 +465,8 @@ module Simplify = struct
         let%bind lst = bind_list @@ List.map simpl_expression lst in
         ok @@ ae @@ Tuple lst
 
-  and simpl_local_declaration (t:Raw.local_decl) : instruction result =
+  and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
+    let return x = ok (Assignment x, x) in
     match t with
     | LocalVar x ->
         let x = x.value in
@@ -469,14 +474,14 @@ module Simplify = struct
         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}}
+        return {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}}
+        return {name;annotated_expression={expression with type_annotation}}
     | _ -> simple_fail "todo"
 
   and simpl_param (t:Raw.param_decl) : named_type_expression result =
@@ -514,7 +519,10 @@ module Simplify = struct
               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 local_declarations =
+                let%bind tmp = bind_list
+                  @@ List.map simpl_local_declaration local_decls in
+                ok (List.map fst tmp) in
               let%bind instructions = bind_list
                 @@ List.map simpl_instruction
                 @@ npseq_to_list block.value.instr in
@@ -536,11 +544,13 @@ module Simplify = struct
                     @@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
                       params
                   ) in
-                { type_name = "arguments" ; type_expression  } in
+                { type_name = "arguments" ; type_expression } 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 typed = bind_map_list simpl_local_declaration local_decls in
+                ok (List.map fst typed)
+              in
               let%bind output_type = simpl_type_expression ret_type in
               let%bind instructions = bind_list
                 @@ List.map simpl_instruction
@@ -552,7 +562,10 @@ module Simplify = struct
                   in
                   List.map aux params
                 in
-                let%bind r = simpl_expression return in
+                let%bind r =
+                  let%bind tmp = simpl_expression return in
+                  Rename.Value.rename_annotated_expression renamings tmp
+                in
                 let%bind b =
                   let tmp = local_declarations @ instructions in
                   Rename.Value.rename_block renamings tmp
@@ -561,7 +574,7 @@ module Simplify = struct
               let decl =
                 let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
                 let type_annotation = Some (Type_function (input_type, output_type)) in
-                Constant_declaration {name="arguments";annotated_expression = {expression;type_annotation}}
+                Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}}
               in
               ok decl
             )
diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml
index ab53237b5..128c59609 100644
--- a/src/ligo/ast_typed.ml
+++ b/src/ligo/ast_typed.ml
@@ -209,15 +209,19 @@ module Errors = struct
     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 different_size_type name a b =
+    let title = name ^ " 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
+  let different_size_constants = different_size_type "constants"
+
+  let different_size_tuples = different_size_type "tuples"
+
+  let different_size_sums = different_size_type "sums"
+
+  let different_size_records = different_size_type "records"
+
 end
 open Errors
 
@@ -240,31 +244,37 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
     )
   | Type_constant _, _ -> fail @@ different_kinds a b
-  | Type_sum a, Type_sum b -> (
-      let a' = list_of_smap a in
-      let b' = list_of_smap b in
+  | Type_sum sa, Type_sum sb -> (
+      let sa' = list_of_smap sa in
+      let sb' = list_of_smap sb in
       let aux ((ka, va), (kb, vb)) =
         let%bind _ =
           Assert.assert_true ~msg:"different keys in sum types"
           @@ (ka = kb) in
         assert_type_value_eq (va, vb)
       in
-      trace (simple_error "sum type")
-      @@ bind_list_iter aux (List.combine a' b')
+      let%bind _ =
+        trace_strong (different_size_sums a b)
+        @@ Assert.assert_list_same_size sa' sb' in
+      trace (simple_error "sum type") @@
+      bind_list_iter aux (List.combine sa' sb')
 
     )
   | Type_sum _, _ -> fail @@ different_kinds a b
-  | Type_record a, Type_record b -> (
-      let a' = list_of_smap a in
-      let b' = list_of_smap b in
+  | Type_record ra, Type_record rb -> (
+      let ra' = list_of_smap ra in
+      let rb' = list_of_smap rb in
       let aux ((ka, va), (kb, vb)) =
         let%bind _ =
           Assert.assert_true ~msg:"different keys in record types"
           @@ (ka = kb) in
         assert_type_value_eq (va, vb)
       in
+      let%bind _ =
+        trace_strong (different_size_records a b)
+        @@ Assert.assert_list_same_size ra' rb' in
       trace (simple_error "record type")
-      @@ bind_list_iter aux (List.combine a' b')
+      @@ bind_list_iter aux (List.combine ra' rb')
 
     )
   | Type_record _, _ -> fail @@ different_kinds a b
@@ -325,6 +335,9 @@ module Combinators = struct
     type_value (Type_record map) None
 
   let make_t_record m = t_record m None
+  let make_t_record_ez lst =
+    let m = SMap.of_list lst in
+    make_t_record m
 
   let t_sum m s : type_value = type_value (Type_sum m) s
   let make_t_sum m = t_sum m None
@@ -358,10 +371,12 @@ module Combinators = struct
     | Type_record m -> ok m
     | _ -> simple_fail "not a record"
 
-  let record (lst : (string * ae) list) : expression =
+  let record map : expression = Record map
+
+  let record_ez (lst : (string * ae) list) : expression =
     let aux prev (k, v) = SMap.add k v prev in
     let map = List.fold_left aux SMap.empty lst in
-    Record map
+    record map
 
   let int n : expression = Literal (Int n)
   let bool b : expression = Literal (Bool b)
@@ -370,6 +385,8 @@ module Combinators = struct
   let a_int n = annotated_expression (int n) make_t_int
   let a_bool b = annotated_expression (bool b) make_t_bool
   let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
+  let a_record r = annotated_expression (record r) (make_t_record (SMap.map (fun x -> x.type_annotation) r))
+  let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
 
   let get_a_int (t:annotated_expression) =
     match t.expression with
diff --git a/src/ligo/contracts/multiple-parameters.ligo b/src/ligo/contracts/multiple-parameters.ligo
index a0d1ef386..56aa45f38 100644
--- a/src/ligo/contracts/multiple-parameters.ligo
+++ b/src/ligo/contracts/multiple-parameters.ligo
@@ -1,2 +1,2 @@
-function bi(const a : int; const b : int) : int is
+function main(const a : int; const b : int) : int is
   begin skip end with (a + b)
diff --git a/src/ligo/ligo-helpers/trace.ml b/src/ligo/ligo-helpers/trace.ml
index b9e779700..8e314707d 100644
--- a/src/ligo/ligo-helpers/trace.ml
+++ b/src/ligo/ligo-helpers/trace.ml
@@ -66,6 +66,13 @@ let bind_smap (s:_ X_map.String.t) =
     ok @@ add k v' prev' in
   fold aux s (ok empty)
 
+let bind_fold_smap f init (smap : _ X_map.String.t) =
+  let aux k v prev =
+    prev >>? fun prev' ->
+    f prev' k v
+  in
+  X_map.String.fold aux smap init
+
 let bind_map_list f lst = bind_list (List.map f lst)
 
 let bind_fold_list f init lst =
diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml
index bc81c7c57..0debd3284 100644
--- a/src/ligo/ligo.ml
+++ b/src/ligo/ligo.ml
@@ -105,9 +105,9 @@ let type_file ?(debug_simplify = false) ?(debug_typed = false)
   let%bind typed =
     trace (simple_error "typing") @@
     type_ simpl in
-  (if debug_typed then
-     Format.(printf "Typed : %a\n%!" AST_Typed.PP.program typed)
-  ) ;
+  (if debug_typed then (
+      Format.(printf "Typed : %a\n%!" AST_Typed.PP.program typed)
+    )) ;
   ok typed
 
 let easy_run_typed
diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml
index ee86c46de..9830a8043 100644
--- a/src/ligo/mini_c.ml
+++ b/src/ligo/mini_c.ml
@@ -104,11 +104,6 @@ and block = block' * environment_wrap
 
 and program = toplevel_statement list
 
-let expression_to_value ((e, _, _):expression) : value result =
-  match e with
-  | Literal v -> ok v
-  | _ -> simple_fail "not a value"
-
 module PP = struct
   open Format
   open Ligo_helpers.PP
@@ -192,6 +187,13 @@ module PP = struct
     fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
 end
 
+let expression_to_value ((e', _, _) as e:expression) : value result =
+  match e' with
+  | Literal v -> ok v
+  | _ -> fail
+      @@ error "not a value"
+      @@ Format.asprintf "%a" PP.expression e
+
 module Free_variables = struct
   type free_variable = string
   type free_variables = free_variable list
@@ -627,6 +629,8 @@ module Translate_program = struct
     | "OR" -> ok @@ simple_binary @@ prim I_OR
     | "AND" -> ok @@ simple_binary @@ prim I_AND
     | "PAIR" -> ok @@ simple_binary @@ prim I_PAIR
+    | "CAR" -> ok @@ simple_unary @@ prim I_CAR
+    | "CDR" -> ok @@ simple_unary @@ prim I_CDR
     | "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
     | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
 
@@ -774,20 +778,21 @@ module Translate_program = struct
 
     let%bind () =
       let%bind (Ex_ty schema_ty) = Environment.to_ty env in
-      let%bind output_ty = Translate_type.type_ ty in
+      let%bind output_type = Translate_type.type_ ty in
       let%bind (Ex_ty output_ty) =
-        let error_message = Format.asprintf "%a" Michelson.pp output_ty in
+        let error_message = Format.asprintf "%a" Michelson.pp output_type in
         Trace.trace_tzresult_lwt (error "error parsing output ty" error_message) @@
-        Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_ty in
+        Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in
       let input_stack_ty = Stack.(Types.unit @: schema_ty @: nil) in
       let output_stack_ty = Stack.(Types.(pair output_ty unit) @: schema_ty @: nil) in
       let%bind error_message =
         let%bind schema_michelson = Environment.to_michelson_type env in
         ok @@ Format.asprintf
-          "expression : %a\ncode : %a\nschema type : %a"
+          "expression : %a\ncode : %a\nschema type : %a\noutput type : %a"
           PP.expression (expr', ty, env)
-          Tezos_utils.Micheline.Michelson.pp code
-          Tezos_utils.Micheline.Michelson.pp schema_michelson
+          Michelson.pp code
+          Michelson.pp schema_michelson
+          Michelson.pp output_type
       in
       let%bind _ =
         Trace.trace_tzresult_lwt (error "error parsing expression code" error_message) @@
@@ -1025,6 +1030,10 @@ module Combinators = struct
     | `Pair (a, b) -> ok (a, b)
     | _ -> simple_fail "not a pair"
 
+  let get_t_pair (t:type_value) = match t with
+    | `Pair (a, b) -> ok (a, b)
+    | _ -> simple_fail "not a type pair"
+
   let get_left (v:value) = match v with
     | `Left b -> ok b
     | _ -> simple_fail "not a left"
diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml
index f8859daf7..adb4e96aa 100644
--- a/src/ligo/test/integration_tests.ml
+++ b/src/ligo/test/integration_tests.ml
@@ -42,15 +42,18 @@ let complex_function () : unit result =
   ok ()
 
 let multiple_parameters () : unit result  =
-  let%bind program = type_file "./contracts/multiple-parameters.ligo" in
+  let%bind program = type_file ~debug_typed:true "./contracts/multiple-parameters.ligo" in
   let aux n =
     let open AST_Typed.Combinators in
-    let input = a_int n in
+    let input = a_record_ez [
+        ("a", a_int n) ;
+        ("b", a_int n) ;
+      ] in
     let%bind result = easy_run_main_typed program input in
     let%bind result' =
       trace (simple_error "bad result") @@
       get_a_int result in
-    Assert.assert_equal_int (3 * n + 2) result'
+    Assert.assert_equal_int (2 * n) result'
   in
   let%bind _ = bind_list
     @@ List.map aux
diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml
index 55f013c73..0306a47a5 100644
--- a/src/ligo/transpiler.ml
+++ b/src/ligo/transpiler.ml
@@ -167,32 +167,32 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
         ok (Predicate ("PAIR", [a; b]), `Pair(a_ty, b_ty), env)
       in
       Append_tree.fold_ne (translate_annotated_expression env) aux node
-  | Record_accessor (r, key) ->
-      let%bind (r'_expr, _, _) = translate_annotated_expression env r in
-      let%bind r_tv = get_t_record ae.type_annotation in
-      let node_tv = Append_tree.of_list @@ kv_list_of_map r_tv in
-      let%bind ae' =
-        let leaf (key', tv) : (expression' option * type_value) result =
-          let%bind tv = translate_type tv in
-          if key = key' then (
-            ok (Some (r'_expr), tv)
-          ) else (
-            ok (None, tv)
+  | Record_accessor (record, property) ->
+      let%bind translation = translate_annotated_expression env record in
+      let%bind record_type_map =
+        trace (simple_error (Format.asprintf "Accessing field of %a, that has type %a, which isn't a record" AST.PP.annotated_expression record AST.PP.type_value record.type_annotation)) @@
+        get_t_record record.type_annotation in
+      let node_tv = Append_tree.of_list @@ kv_list_of_map record_type_map in
+      let leaf (key, _) : expression result =
+        if property = key then (
+          ok translation
+        ) else (
+          simple_fail "bad leaf"
+        ) in
+      let node (a:expression result) b : expression result =
+        match%bind bind_lr (a, b) with
+        | `Left ((_, t, env) as ex) -> (
+            let%bind (a, _) = get_t_pair t in
+            ok (Predicate ("CAR", [ex]), a, env)
+          )
+        | `Right ((_, t, env) as ex) -> (
+            let%bind (_, b) = get_t_pair t in
+            ok (Predicate ("CDR", [ex]), b, env)
           ) in
-        let node a b : (expression' option * type_value) result =
-          let%bind a = a in
-          let%bind b = b in
-          match (a, b) with
-          | (None, a), (None, b) -> ok (None, `Pair (a, b))
-          | (Some _, _), (Some _, _) -> simple_fail "several identical keys in the same record (shouldn't happen here)"
-          | (Some v, a), (None, b) -> ok (Some (Predicate ("CAR", [v, a, env])), `Pair (a, b))
-          | (None, a), (Some v, b) -> ok (Some (Predicate ("CDR", [v, b, env])), `Pair (a, b))
-        in
-        let%bind (ae_opt, tv) = Append_tree.fold_ne leaf node node_tv in
-        let%bind ae = trace_option (simple_error "bad key in record (shouldn't happen here)")
-            ae_opt in
-        ok (ae, tv, env) in
-      ok ae'
+      let%bind expr =
+        trace_strong (simple_error "bad key in record (shouldn't happen here)") @@
+        Append_tree.fold_ne leaf node node_tv in
+      ok expr
   | Constant (name, lst) ->
       let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in
       ok (Predicate (name, lst'), tv, env)
diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml
index 7b79aed3e..d25537680 100644
--- a/src/ligo/typer.ml
+++ b/src/ligo/typer.ml
@@ -70,8 +70,18 @@ module Errors = struct
     let full = n in
     error title full
 
-  let constant_declaration_error (name:string) =
-    error "typing constant declaration" name
+  let program_error (p:I.program) =
+    let title = "typing program" in
+    let full = Format.asprintf "%a" I.PP.program p in
+    error title full
+
+  let constant_declaration_error (name:string) (ae:I.ae) =
+    let title = "typing constant declaration" in
+    let full =
+      Format.asprintf "%s = %a" name
+        I.PP.annotated_expression ae
+    in
+    error title full
 
 end
 open Errors
@@ -85,7 +95,7 @@ let rec type_program (p:I.program) : O.program result =
     | Some d' -> ok (e', d' :: acc)
   in
   let%bind (_, lst) =
-    trace (simple_error "typing program") @@
+    trace (program_error p) @@
     bind_fold_list aux (Environment.empty, []) p in
   ok @@ List.rev lst
 
@@ -96,7 +106,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
       ok (env', None)
   | Constant_declaration {name;annotated_expression} ->
       let%bind ae' =
-        trace (constant_declaration_error name) @@
+        trace (constant_declaration_error name annotated_expression) @@
         type_annotated_expression env annotated_expression in
       let env' = Environment.add env name ae'.type_annotation in
       ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
@@ -181,10 +191,9 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul
       let%bind t_tuple =
         trace_strong (simple_error "Matching tuple on not-a-tuple")
         @@ get_t_tuple t in
-      let%bind _ =
-        trace_strong (simple_error "Matching tuple of different size")
-        @@ Assert.assert_list_same_size t_tuple lst in
-      let lst' = List.combine lst t_tuple in
+      let%bind lst' =
+        generic_try (simple_error "Matching tuple of different size")
+        @@ (fun () -> List.combine lst t_tuple) in
       let aux prev (name, tv) = Environment.add prev name tv in
       let e' = List.fold_left aux e lst' in
       let%bind b' = type_block e' b in
@@ -293,12 +302,11 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
       ok O.{expression = O.Constructor(c, expr') ; type_annotation }
   (* Record *)
   | Record m ->
-      let aux k expr prev =
-        let%bind prev' = prev in
+      let aux prev k expr =
         let%bind expr' = type_annotated_expression e expr in
-        ok (SMap.add k expr' prev')
+        ok (SMap.add k expr' prev)
       in
-      let%bind m' = SMap.fold aux m (ok SMap.empty) in
+      let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
       let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
       ok O.{expression = O.Record m' ; type_annotation }
   | Lambda {