diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml
index 138671f6e..ff72e1bc5 100644
--- a/src/passes/4-typer/solver.ml
+++ b/src/passes/4-typer/solver.ml
@@ -112,8 +112,8 @@ module Wrap = struct
     [C_equation (P_variable (type_name) , pattern)] , type_name
    *)
 
-  let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys ->
-    let patterns = List.map type_expression_to_type_value_copypasted tys in
+  let tuple : T.type_value list -> (constraints * O.type_variable) = fun tys ->
+    let patterns = List.map type_expression_to_type_value tys in
     let pattern = O.(P_constant (C_tuple , patterns)) in
     let type_name = Core.fresh_type_variable () in
     [C_equation (P_variable (type_name) , pattern)] , type_name
@@ -143,7 +143,7 @@ module Wrap = struct
   end
 
   (* TODO: I think we should take an I.expression for the base+label *)
-  let access_label ~base ~label : (constraints * O.type_variable) =
+  let access_label ~(base : T.type_value) ~(label : O.label) : (constraints * O.type_variable) =
     let base' = type_expression_to_type_value base in
     let expr_type = Core.fresh_type_variable () in
     [O.C_access_label (base' , label , expr_type)] , expr_type
@@ -151,14 +151,14 @@ module Wrap = struct
   let access_int ~base ~index = access_label ~base ~label:(L_int index)
   let access_string ~base ~property = access_label ~base ~label:(L_string property)
 
-  let access_map : base:I.type_expression -> key:I.type_expression -> (constraints * O.type_variable) =
+  let access_map : base:T.type_value -> key:T.type_value -> (constraints * O.type_variable) =
     let mk_map_type key_type element_type =
       O.P_constant O.(C_map , [P_variable element_type; P_variable key_type]) in
     fun ~base ~key ->
       let key_type = Core.fresh_type_variable () in
       let element_type = Core.fresh_type_variable () in
-      let base' = type_expression_to_type_value_copypasted base in
-      let key' = type_expression_to_type_value_copypasted key in
+      let base' = type_expression_to_type_value base in
+      let key' = type_expression_to_type_value key in
       let base_expected = mk_map_type key_type element_type in
       let expr_type = Core.fresh_type_variable () in
       O.[C_equation (base' , base_expected);
@@ -166,27 +166,27 @@ module Wrap = struct
          C_equation (P_variable expr_type , P_variable element_type)] , expr_type
 
   let constructor
-    : I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable)
+    : T.type_value -> T.type_value -> T.type_value -> (constraints * O.type_variable)
     = fun t_arg c_arg sum ->
-      let t_arg = type_expression_to_type_value_copypasted t_arg in
-      let c_arg = type_expression_to_type_value_copypasted c_arg in
-      let sum = type_expression_to_type_value_copypasted sum in
+      let t_arg = type_expression_to_type_value t_arg in
+      let c_arg = type_expression_to_type_value c_arg in
+      let sum = type_expression_to_type_value sum in
       let whole_expr = Core.fresh_type_variable () in
       [
         C_equation (P_variable (whole_expr) , sum) ;
         C_equation (t_arg , c_arg)
       ] , whole_expr
 
-  let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields ->
-    let record_type = type_expression_to_type_value_copypasted (I.t_record fields) in
+  let record : T.type_value I.type_name_map -> (constraints * O.type_variable) = fun fields ->
+    let record_type = type_expression_to_type_value (T.t_record fields ()) in
     let whole_expr = Core.fresh_type_variable () in
     [C_equation (P_variable whole_expr , record_type)] , whole_expr
 
-  let collection : O.constant_tag -> I.type_expression list -> (constraints * O.type_variable) =
+  let collection : O.constant_tag -> T.type_value list -> (constraints * O.type_variable) =
     fun ctor element_tys ->
       let elttype = O.P_variable (Core.fresh_type_variable ()) in
       let aux elt =
-        let elt' = type_expression_to_type_value_copypasted elt
+        let elt' = type_expression_to_type_value elt
         in O.C_equation (elttype , elt') in
       let equations = List.map aux element_tys in
       let whole_expr = Core.fresh_type_variable () in
@@ -197,15 +197,15 @@ module Wrap = struct
   let list = collection O.C_list
   let set  = collection O.C_set
 
-  let map : (I.type_expression * I.type_expression) list -> (constraints * O.type_variable) =
+  let map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
     fun kv_tys ->
       let k_type = O.P_variable (Core.fresh_type_variable ()) in
       let v_type = O.P_variable (Core.fresh_type_variable ()) in
       let aux_k (k , _v) =
-        let k' = type_expression_to_type_value_copypasted k in
+        let k' = type_expression_to_type_value k in
         O.C_equation (k_type , k') in
       let aux_v (_k , v) =
-        let v' = type_expression_to_type_value_copypasted v in
+        let v' = type_expression_to_type_value v in
         O.C_equation (v_type , v') in
       let equations_k = List.map aux_k kv_tys in
       let equations_v = List.map aux_v kv_tys in
@@ -214,19 +214,38 @@ module Wrap = struct
         C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
       ] @ equations_k @ equations_v , whole_expr
 
-  let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
+  let big_map : (T.type_value * T.type_value) list -> (constraints * O.type_variable) =
+    fun kv_tys ->
+      let k_type = O.P_variable (Core.fresh_type_variable ()) in
+      let v_type = O.P_variable (Core.fresh_type_variable ()) in
+      let aux_k (k , _v) =
+        let k' = type_expression_to_type_value k in
+        O.C_equation (k_type , k') in
+      let aux_v (_k , v) =
+        let v' = type_expression_to_type_value v in
+        O.C_equation (v_type , v') in
+      let equations_k = List.map aux_k kv_tys in
+      let equations_v = List.map aux_v kv_tys in
+      let whole_expr = Core.fresh_type_variable () in
+      O.[
+        (* TODO: this doesn't tag big_maps uniquely (i.e. if two
+           big_map have the same type, they can be swapped. *)
+        C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type]))
+      ] @ equations_k @ equations_v , whole_expr
+
+  let application : T.type_value -> T.type_value -> (constraints * O.type_variable) =
     fun f arg ->
       let whole_expr = Core.fresh_type_variable () in
-      let f'   = type_expression_to_type_value_copypasted f in
-      let arg' = type_expression_to_type_value_copypasted arg in
+      let f'   = type_expression_to_type_value f in
+      let arg' = type_expression_to_type_value arg in
       O.[
         C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
       ] , whole_expr
 
-  let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
+  let look_up : T.type_value -> T.type_value -> (constraints * O.type_variable) =
     fun ds ind ->
-      let ds'  = type_expression_to_type_value_copypasted ds in
-      let ind' = type_expression_to_type_value_copypasted ind in
+      let ds'  = type_expression_to_type_value ds in
+      let ind' = type_expression_to_type_value ind in
       let whole_expr = Core.fresh_type_variable () in
       let v = Core.fresh_type_variable () in
       O.[
@@ -234,20 +253,20 @@ module Wrap = struct
         C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
       ] , whole_expr
 
-  let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
+  let sequence : T.type_value -> T.type_value -> (constraints * O.type_variable) =
     fun a b ->
-      let a' = type_expression_to_type_value_copypasted a in
-      let b' = type_expression_to_type_value_copypasted b in
+      let a' = type_expression_to_type_value a in
+      let b' = type_expression_to_type_value b in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (a' , P_constant (C_unit , [])) ;
         C_equation (b' , P_variable whole_expr)
       ] , whole_expr
 
-  let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
+  let loop : T.type_value -> T.type_value -> (constraints * O.type_variable) =
     fun expr body ->
-      let expr' = type_expression_to_type_value_copypasted expr in
-      let body' = type_expression_to_type_value_copypasted body in
+      let expr' = type_expression_to_type_value expr in
+      let body' = type_expression_to_type_value body in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (expr'                 , P_constant (C_bool , [])) ;
@@ -255,13 +274,13 @@ module Wrap = struct
         C_equation (P_variable whole_expr , P_constant (C_unit , []))
       ] , whole_expr
 
-  let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) =
+  let let_in : T.type_value -> T.type_value option -> T.type_value -> (constraints * O.type_variable) =
     fun rhs rhs_tv_opt result ->
-      let rhs'        = type_expression_to_type_value_copypasted rhs in
-      let result'     = type_expression_to_type_value_copypasted result in
+      let rhs'        = type_expression_to_type_value rhs in
+      let result'     = type_expression_to_type_value result in
       let rhs_tv_opt' = match rhs_tv_opt with
           None -> []
-        | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value_copypasted annot)] in
+        | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (result' , P_variable whole_expr)
diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index 70ad57305..eba974e5f 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -474,39 +474,35 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
    *     | _ -> return (E_literal (Literal_string s)) (t_string ())
    *   ) *)
   (* Tuple *)
-  | E_tuple lst ->
-    let aux state hd = type_expression e state hd >>? swap in
-    let%bind (state', lst') = bind_fold_map_list aux state lst in
-    let tv_lst = List.map get_type_annotation lst' in
-    return (E_tuple lst') (t_tuple tv_lst ())
-  | E_accessor (ae', path) ->
-    let%bind e' = type_expression e ae' in
-    let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
-      match a with
-      | Access_tuple index -> (
-          let%bind tpl_tv = get_t_tuple prev.type_annotation in
-          let%bind tv =
-            generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
-            @@ (fun () -> List.nth tpl_tv index) in
-          return (E_tuple_accessor (prev , index)) tv
-        )
-      | Access_record property -> (
-          let%bind r_tv = get_t_record prev.type_annotation in
-          let%bind tv =
-            generic_try (bad_record_access property ae' prev.type_annotation ae.location)
-            @@ (fun () -> SMap.find property r_tv) in
-          return (E_record_accessor (prev , property)) tv
-        )
-      | Access_map ae' -> (
-          let%bind ae'' = type_expression e ae' in
-          let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in
-          let%bind () =
-            Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in
-          return (E_look_up (prev , ae'')) v
-        )
-    in
-    trace (simple_info "accessing") @@
-    bind_fold_list aux e' path
+  | E_tuple lst  -> (
+      let aux state hd = type_expression e state hd >>? swap in
+      let%bind (state', lst') = bind_fold_map_list aux state lst in
+      let tv_lst = List.map get_type_annotation lst' in
+      return_wrapped (e_tuple lst') state' @@ Wrap.tuple tv_lst
+    )
+  | E_accessor (base , [Access_tuple index]) -> (
+      let%bind (base' , state') = type_expression e state base in
+      let wrapped = Wrap.access_int ~base:base'.type_annotation ~index in
+      return_wrapped (E_tuple_accessor (base' , index)) state' wrapped
+    )
+  | E_accessor (base , [Access_record property]) -> (
+      let%bind (base' , state') = type_expression e state base in
+      let wrapped = Wrap.access_string ~base:base'.type_annotation ~property in
+      return_wrapped (E_record_accessor (base' , property)) state' wrapped
+    )
+  | E_accessor (base , [Access_map key_ae]) -> (
+      let%bind (base' , state') = type_expression e state base in
+      let%bind (key_ae' , state'') = type_expression e state' key_ae in
+      let xyz = get_type_annotation key_ae' in
+      let wrapped = Wrap.access_map ~base:base'.type_annotation ~key:xyz in
+      return_wrapped (E_look_up (base' , key_ae')) state'' wrapped
+    )
+
+  | E_accessor (_base , []) | E_accessor (_base , _ :: _ :: _) -> (
+      failwith
+        "The simplifier should produce E_accessor with only a single path element, not a list of path elements."
+    )
+
   (* Sum *)
   | E_constructor (c, expr) ->
     let%bind (c_tv, sum_tv) =
@@ -520,9 +516,10 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
       trace_option error @@
       Environment.get_constructor c e in
     let%bind (expr' , state') = type_expression e state expr in
-    let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in
+    let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
     let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in
     return_wrapped (E_constructor (c , expr')) state' wrapped
+
   (* Record *)
   | E_record m ->
     let aux (acc, state) k expr =
@@ -533,6 +530,8 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
     let wrapped = Wrap.record (SMap.map get_type_annotation m') in
     return_wrapped (E_record m') state' wrapped
   (* Data-structure *)
+
+(*
   | E_list lst ->
     let%bind lst' = bind_map_list (type_expression e) lst in
     let%bind tv =
@@ -605,112 +604,152 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
       ok (t_map key_type value_type ())
     in
     return (E_map lst') tv
-  | E_big_map lst ->
-    let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
-    let%bind tv =
-      let aux opt c =
-        match opt with
-        | None -> ok (Some c)
-        | Some c' ->
-          let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
-          ok (Some c') in
-      let%bind key_type =
-        let%bind sub =
-          bind_fold_list aux None
-          @@ List.map get_type_annotation
-          @@ List.map fst lst' in
-        let%bind annot = bind_map_option get_t_big_map_key tv_opt in
-        trace (simple_info "empty map expression without a type annotation") @@
-        O.merge_annotation annot sub (needs_annotation ae "this map literal")
-      in
-      let%bind value_type =
-        let%bind sub =
-          bind_fold_list aux None
-          @@ List.map get_type_annotation
-          @@ List.map snd lst' in
-        let%bind annot = bind_map_option get_t_big_map_value tv_opt in
-        trace (simple_info "empty map expression without a type annotation") @@
-        O.merge_annotation annot sub (needs_annotation ae "this map literal")
-      in
-      ok (t_big_map key_type value_type ())
-    in
-    return (E_big_map lst') tv
-  | E_lambda {
-      binder ;
-      input_type ;
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type =
-        let%bind input_type =
-          (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
-          let default_action e () = fail @@ (needs_annotation e "the returned value") in
-          match input_type with
-          | Some ty -> ok ty
-          | None -> (
-              match result.expression with
-              | I.E_let_in li -> (
-                  match li.rhs.expression with
-                  | I.E_variable name when name = (fst binder) -> (
-                      match snd li.binder with
-                      | Some ty -> ok ty
-                      | None -> default_action li.rhs ()
-                    )
-                  | _ -> default_action li.rhs ()
-                )
-              | _ -> default_action result ()
-            )
-        in
-        evaluate_type e input_type in
-      let%bind output_type =
-        bind_map_option (evaluate_type e) output_type
-      in
-      let e' = Environment.add_ez_binder (fst binder) input_type e in
-      let%bind body = type_expression ?tv_opt:output_type e' result in
-      let output_type = body.type_annotation in
-      return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
-    )
-  | E_constant (name, lst) ->
-    let%bind lst' = bind_list @@ List.map (type_expression e) lst in
-    let tv_lst = List.map get_type_annotation lst' in
-    let%bind (name', tv) =
-      type_constant name tv_lst tv_opt ae.location in
-    return (E_constant (name' , lst')) tv
+*)
+
+  | E_list lst ->
+    let%bind (state', lst') =
+      bind_fold_map_list (fun state' elt -> type_expression e state' elt >>? swap) state lst in
+    let wrapped = Wrap.list (List.map (fun x -> O.(x.type_annotation)) lst') in
+    return_wrapped (E_list lst') state' wrapped
+  | E_set set ->
+    let aux = fun state' elt -> type_expression e state' elt >>? swap in
+    let%bind (state', set') =
+      bind_fold_map_list aux state set in
+    let wrapped = Wrap.set (List.map (fun x -> O.(x.type_annotation)) set') in
+    return_wrapped (E_set set') state' wrapped
+  | E_map map ->
+    let aux' state' elt = type_expression e state' elt >>? swap in
+    let aux = fun state' elt -> bind_fold_map_pair aux' state' elt in
+    let%bind (state', map') =
+      bind_fold_map_list aux state map in
+    let aux (x, y) = O.(x.type_annotation , y.type_annotation) in
+    let wrapped = Wrap.map (List.map aux map') in
+    return_wrapped (E_map map') state' wrapped
+
+  (* | E_big_map lst ->
+   *   let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
+   *   let%bind tv =
+   *     let aux opt c =
+   *       match opt with
+   *       | None -> ok (Some c)
+   *       | Some c' ->
+   *         let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+   *         ok (Some c') in
+   *     let%bind key_type =
+   *       let%bind sub =
+   *         bind_fold_list aux None
+   *         @@ List.map get_type_annotation
+   *         @@ List.map fst lst' in
+   *       let%bind annot = bind_map_option get_t_big_map_key tv_opt in
+   *       trace (simple_info "empty map expression without a type annotation") @@
+   *       O.merge_annotation annot sub (needs_annotation ae "this map literal")
+   *     in
+   *     let%bind value_type =
+   *       let%bind sub =
+   *         bind_fold_list aux None
+   *         @@ List.map get_type_annotation
+   *         @@ List.map snd lst' in
+   *       let%bind annot = bind_map_option get_t_big_map_value tv_opt in
+   *       trace (simple_info "empty map expression without a type annotation") @@
+   *       O.merge_annotation annot sub (needs_annotation ae "this map literal")
+   *     in
+   *     ok (t_big_map key_type value_type ())
+   *   in
+   *   return (E_big_map lst') tv *)
+  | E_big_map big_map ->
+    let aux' state' elt = type_expression e state' elt >>? swap in
+    let aux = fun state' elt -> bind_fold_map_pair aux' state' elt in
+    let%bind (state', big_map') =
+      bind_fold_map_list aux state big_map in
+    let aux (x, y) = O.(x.type_annotation , y.type_annotation) in
+    let wrapped = Wrap.big_map (List.map aux big_map') in
+    return_wrapped (E_big_map big_map') state' wrapped
+
+  (* | E_lambda {
+   *     binder ;
+   *     input_type ;
+   *     output_type ;
+   *     result ;
+   *   } -> (
+   *     let%bind input_type =
+   *       let%bind input_type =
+   *         (\* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *\)
+   *         let default_action e () = fail @@ (needs_annotation e "the returned value") in
+   *         match input_type with
+   *         | Some ty -> ok ty
+   *         | None -> (
+   *             match result.expression with
+   *             | I.E_let_in li -> (
+   *                 match li.rhs.expression with
+   *                 | I.E_variable name when name = (fst binder) -> (
+   *                     match snd li.binder with
+   *                     | Some ty -> ok ty
+   *                     | None -> default_action li.rhs ()
+   *                   )
+   *                 | _ -> default_action li.rhs ()
+   *               )
+   *             | _ -> default_action result ()
+   *           )
+   *       in
+   *       evaluate_type e input_type in
+   *     let%bind output_type =
+   *       bind_map_option (evaluate_type e) output_type
+   *     in
+   *     let e' = Environment.add_ez_binder (fst binder) input_type e in
+   *     let%bind body = type_expression ?tv_opt:output_type e' result in
+   *     let output_type = body.type_annotation in
+   *     return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
+   *   ) *)
+
+  (* | E_constant (name, lst) ->
+   *   let%bind lst' = bind_list @@ List.map (type_expression e) lst in
+   *   let tv_lst = List.map get_type_annotation lst' in
+   *   let%bind (name', tv) =
+   *     type_constant name tv_lst tv_opt ae.location in
+   *   return (E_constant (name' , lst')) tv *)
   | E_application (f, arg) ->
     let%bind (f' , state') = type_expression e state f in
     let%bind (arg , state'') = type_expression e state' arg in
     let wrapped = Wrap.application f'.type_annotation arg.type_annotation in
     return_wrapped (E_application (f' , arg)) state'' wrapped
+
+  (* | E_look_up dsi ->
+   *   let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
+   *   let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
+   *   let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
+   *   return (E_look_up (ds , ind)) (t_option dst ()) *)
+
   | E_look_up dsi ->
-    let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
-    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
-    let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
-    return (E_look_up (ds , ind)) (t_option dst ())
+    let aux' state' elt = type_expression e state' elt >>? swap in
+    let%bind (state'' , (ds , ind)) = bind_fold_map_pair aux' state dsi in
+    let wrapped = Wrap.look_up ds.type_annotation ind.type_annotation in
+    return_wrapped (E_look_up (ds , ind)) state'' wrapped
+
   (* Advanced *)
-  | E_matching (ex, m) -> (
-      let%bind ex' = type_expression e ex in
-      let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
-      let tvs =
-        let aux (cur:O.value O.matching) =
-          match cur with
-          | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
-          | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
-          | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
-          | Match_tuple (_ , match_tuple) -> [ match_tuple ]
-          | Match_variant (lst , _) -> List.map snd lst in
-        List.map get_type_annotation @@ aux m' in
-      let aux prec cur =
-        let%bind () =
-          match prec with
-          | None -> ok ()
-          | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
-        ok (Some cur) in
-      let%bind tv_opt = bind_fold_list aux None tvs in
-      let%bind tv =
-        trace_option (match_empty_variant m ae.location) @@
-        tv_opt in
-      return (O.E_matching (ex', m')) tv
-    )
+  (* | E_matching (ex, m) -> (
+   *     let%bind ex' = type_expression e ex in
+   *     let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
+   *     let tvs =
+   *       let aux (cur:O.value O.matching) =
+   *         match cur with
+   *         | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
+   *         | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
+   *         | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
+   *         | Match_tuple (_ , match_tuple) -> [ match_tuple ]
+   *         | Match_variant (lst , _) -> List.map snd lst in
+   *       List.map get_type_annotation @@ aux m' in
+   *     let aux prec cur =
+   *       let%bind () =
+   *         match prec with
+   *         | None -> ok ()
+   *         | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
+   *       ok (Some cur) in
+   *     let%bind tv_opt = bind_fold_list aux None tvs in
+   *     let%bind tv =
+   *       trace_option (match_empty_variant m ae.location) @@
+   *       tv_opt in
+   *     return (O.E_matching (ex', m')) tv
+   *   ) *)
   | E_sequence (a , b) ->
     let%bind (a' , state') = type_expression e state a in
     let%bind (b' , state'') = type_expression e state' b in
diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml
index a4909851c..af742b334 100644
--- a/src/stages/ast_typed/combinators.ml
+++ b/src/stages/ast_typed/combinators.ml
@@ -246,6 +246,7 @@ let e_application a b : expression = E_application (a , b)
 let e_variable v : expression = E_variable v
 let e_list lst : expression = E_list lst
 let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
+let e_tuple lst : expression = E_tuple lst
 
 let e_a_unit = make_a_e e_unit (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml
index 7380139d1..8aef87157 100644
--- a/src/stages/typesystem/core.ml
+++ b/src/stages/typesystem/core.ml
@@ -17,6 +17,7 @@
     | C_record    (* ( label , * ) … -> * *)
     | C_variant   (* ( label , * ) … -> * *)
     | C_map       (* * -> * -> * *)
+    | C_big_map       (* * -> * -> * *)
     | C_list      (* * -> * *)
     | C_set       (* * -> * *)
     | C_unit      (* * *)
diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml
index 75cc3bf85..7e5083695 100644
--- a/vendors/ligo-utils/simple-utils/trace.ml
+++ b/vendors/ligo-utils/simple-utils/trace.ml
@@ -665,7 +665,10 @@ let bind_and (a, b) =
 let bind_pair = bind_and
 let bind_map_pair f (a, b) =
   bind_pair (f a, f b)
-
+let bind_fold_map_pair f acc (a, b) =
+  f acc a >>? fun (acc' , a') ->
+  f acc' b >>? fun (acc'' , b') ->
+  ok (acc'' , (a' , b'))
 
 
 (**