diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml
index 67429e040..511831b28 100644
--- a/src/bin/expect_tests/typer_error_tests.ml
+++ b/src/bin/expect_tests/typer_error_tests.ml
@@ -41,7 +41,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"}
+    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. different number of arguments to type constructors: Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the TC_tuple type constructor, but they have 3 and 2 arguments, respectively) {"a":"(TO_tuple[int , string , bool])","b":"(TO_tuple[int , string])","op":"TC_tuple","len_a":"3","len_b":"2"}
 
 
      If you're not sure how to fix this error, you can
diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml
index 4d99be97a..8b95d9a2d 100644
--- a/src/main/compile/of_mini_c.ml
+++ b/src/main/compile/of_mini_c.ml
@@ -9,15 +9,13 @@ let compile_contract : expression -> Compiler.compiled_expression result = fun e
   let%bind body = Compiler.Program.translate_function_body body [] input_ty in
   let expr = Self_michelson.optimize body in
   let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
-  let open! Compiler.Program in
-  ok { expr_ty ; expr }
+  ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
 
 let compile_expression : expression -> Compiler.compiled_expression result = fun e ->
   let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in
   let expr = Self_michelson.optimize expr in
   let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
-  let open! Compiler.Program in
-  ok { expr_ty ; expr }
+  ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
 
 let aggregate_and_compile = fun program form ->
   let%bind aggregated = aggregate_entry program form in
diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml
index 243ecd586..6d98bccc5 100644
--- a/src/main/compile/of_simplified.ml
+++ b/src/main/compile/of_simplified.ml
@@ -7,14 +7,15 @@ let compile (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solv
 
 let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression)
     : (Ast_typed.value * Typer.Solver.state) result =
-  Typer.type_expression env state ae
+  let () = Typer.Solver.discard_state state in
+  Typer.type_expression_subst env state ae
 
 let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result =
   let name = Var.of_name entry_point in
   let entry_point_var : Ast_simplified.expression =
     { expression = Ast_simplified.E_variable name ;
       location = Virtual "generated entry-point variable" } in
-  let applied : Ast_simplified.expression = 
+  let applied : Ast_simplified.expression =
     { expression = Ast_simplified.E_application (entry_point_var, param) ;
       location = Virtual "generated application" } in
   ok applied
diff --git a/src/main/compile/of_typed.ml b/src/main/compile/of_typed.ml
index a69f32c9d..c1b2930ef 100644
--- a/src/main/compile/of_typed.ml
+++ b/src/main/compile/of_typed.ml
@@ -14,7 +14,7 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
   match entry_point.type_annotation.type_value' with
   | T_arrow (args,_) -> (
       match args.type_value' with
-      | T_tuple [param_exp;storage_exp] -> (
+      | T_operator (TC_tuple [param_exp;storage_exp]) -> (
           match c with
           | Check_parameter -> assert_type_value_eq (param_exp,   param.type_annotation)
           | Check_storage   -> assert_type_value_eq (storage_exp, param.type_annotation)
@@ -24,4 +24,4 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
   | _ -> dummy_fail )
 
 let pretty_print ppf program =
-  Ast_typed.PP.program ppf program
\ No newline at end of file
+  Ast_typed.PP.program ppf program
diff --git a/src/passes/2-simplify/cameligo.ml b/src/passes/2-simplify/cameligo.ml
index a836ce2b0..dcbf94693 100644
--- a/src/passes/2-simplify/cameligo.ml
+++ b/src/passes/2-simplify/cameligo.ml
@@ -246,7 +246,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_map_list simpl_type_expression lst in
-      ok @@ make_t @@ T_tuple lst
+      ok @@ make_t @@ T_operator (TC_tuple lst)
 
 let rec simpl_expression :
   Raw.expr -> expr result = fun t ->
diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml
index fa98720c8..e8c72ce9a 100644
--- a/src/passes/2-simplify/pascaligo.ml
+++ b/src/passes/2-simplify/pascaligo.ml
@@ -267,7 +267,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_list @@ List.map simpl_type_expression lst in
-      ok @@ make_t @@ T_tuple lst
+      ok @@ make_t @@ T_operator (TC_tuple lst)
 
 let simpl_projection : Raw.projection Region.reg -> _ = fun p ->
   let (p' , loc) = r_split p in
@@ -663,7 +663,7 @@ and simpl_fun_decl :
        let arguments_name = Var.of_name "arguments" in
        let%bind params = bind_map_list simpl_param lst in
        let (binder , input_type) =
-         let type_expression = T_tuple (List.map snd params) in
+         let type_expression = t_tuple (List.map snd params) in
          (arguments_name , type_expression) in
        let%bind tpl_declarations =
          let aux = fun i x ->
@@ -682,8 +682,8 @@ and simpl_fun_decl :
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
        let expression =
-         e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
-       let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
+         e_lambda ~loc binder (Some input_type) (Some output_type) result in
+       let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
        ok ((Var.of_name fun_name.value, type_annotation), expression)
      )
   )
@@ -717,7 +717,7 @@ and simpl_fun_expression :
        let arguments_name = Var.of_name "arguments" in
        let%bind params = bind_map_list simpl_param lst in
        let (binder , input_type) =
-         let type_expression = T_tuple (List.map snd params) in
+         let type_expression = t_tuple (List.map snd params) in
          (arguments_name , type_expression) in
        let%bind tpl_declarations =
          let aux = fun i x ->
@@ -736,8 +736,8 @@ and simpl_fun_expression :
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
        let expression =
-         e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
-       let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
+         e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
+       let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
        ok (type_annotation, expression)
      )
   )
diff --git a/src/passes/4-typer-new/PP.ml b/src/passes/4-typer-new/PP.ml
new file mode 100644
index 000000000..a8829aef3
--- /dev/null
+++ b/src/passes/4-typer-new/PP.ml
@@ -0,0 +1,54 @@
+open Solver
+open Format
+
+let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
+  function
+  |SC_Constructor { tv; c_tag; tv_list=_ } ->
+    let ct = match c_tag with
+      | Solver.Core.C_arrow     -> "arrow"
+      | Solver.Core.C_option    -> "option"
+      | Solver.Core.C_tuple     -> "tuple"
+      | Solver.Core.C_record    -> failwith "record"
+      | Solver.Core.C_variant   -> failwith "variant"
+      | Solver.Core.C_map       -> "map"
+      | Solver.Core.C_big_map   -> "big_map"
+      | Solver.Core.C_list      -> "list"
+      | Solver.Core.C_set       -> "set"
+      | Solver.Core.C_unit      -> "unit"
+      | Solver.Core.C_bool      -> "bool"
+      | Solver.Core.C_string    -> "string"
+      | Solver.Core.C_nat       -> "nat"
+      | Solver.Core.C_mutez     -> "mutez"
+      | Solver.Core.C_timestamp -> "timestamp"
+      | Solver.Core.C_int       -> "int"
+      | Solver.Core.C_address   -> "address"
+      | Solver.Core.C_bytes     -> "bytes"
+      | Solver.Core.C_key_hash  -> "key_hash"
+      | Solver.Core.C_key       -> "key"
+      | Solver.Core.C_signature -> "signature"
+      | Solver.Core.C_operation -> "operation"
+      | Solver.Core.C_contract  -> "contract"
+      | Solver.Core.C_chain_id  -> "chain_id"
+    in
+    fprintf ppf "CTOR %a %s()" Var.pp tv ct
+  |SC_Alias       (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b
+  |SC_Poly        _ -> fprintf ppf "Poly"
+  |SC_Typeclass   _ -> fprintf ppf "TC"
+
+let all_constraints ppf ac =
+  fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
+
+let aliases ppf (al : unionfind) =
+  fprintf ppf "ALIASES %a" UF.print al
+
+let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs ->
+  let { all_constraints = a ; aliases = b ; _ } = structured_dbs in
+  fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b
+
+let already_selected : _ -> already_selected -> unit = fun ppf already_selected ->
+  let _ = already_selected in
+  fprintf ppf "ALREADY_SELECTED"
+
+let state : _ -> state -> unit = fun ppf state ->
+  let { structured_dbs=a ; already_selected=b } = state in
+  fprintf ppf "STATE %a %a" structured_dbs a already_selected b
diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml
index 2adac9659..4f9c96388 100644
--- a/src/passes/4-typer-new/solver.ml
+++ b/src/passes/4-typer-new/solver.ml
@@ -34,8 +34,6 @@ module Wrap = struct
 
   let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te ->
     match te.type_value' with
-    | T_tuple types ->
-      P_constant (C_tuple, List.map type_expression_to_type_value types)
     | T_sum kvmap ->
       P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
     | T_record kvmap ->
@@ -64,21 +62,20 @@ module Wrap = struct
       P_constant (csttag, [])
     | T_operator (type_operator) ->
       let (csttag, args) = Core.(match type_operator with
-          | TC_option o      -> (C_option, [o])
-          | TC_set s         -> (C_set, [s])
-          | TC_map (k,v)     -> (C_map, [k;v])
-          | TC_big_map (k,v) -> (C_big_map, [k;v])
-          | TC_list l        -> (C_list, [l])
-          | TC_contract c    -> (C_contract, [c])
+          | TC_option o            -> (C_option, [o])
+          | TC_set s               -> (C_set, [s])
+          | TC_map ( k , v )       -> (C_map, [k;v])
+          | TC_big_map ( k , v)    -> (C_big_map, [k;v])
+          | TC_list l              -> (C_list, [l])
+          | TC_contract c          -> (C_contract, [c])
+          | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
+          | TC_tuple lst           -> (C_tuple, lst)
       )
       in
       P_constant (csttag, List.map type_expression_to_type_value args)
-      
 
   let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
     match te.type_expression' with
-    | T_tuple types ->
-      P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
     | T_sum kvmap ->
       P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
     | T_record kvmap ->
@@ -96,12 +93,14 @@ module Wrap = struct
       P_constant (csttag,[])
     | T_operator (type_name) ->
       let (csttag, args) = Core.(match type_name with
-          | TC_option o       -> (C_option , [o])
-          | TC_list l         -> (C_list   , [l])
-          | TC_set  s         -> (C_set    , [s]) 
-          | TC_map  (k,v)     -> (C_map    , [k;v])
-          | TC_big_map  (k,v) -> (C_big_map, [k;v])
-          | TC_contract c     -> (C_contract, [c])
+          | TC_option o            -> (C_option , [o])
+          | TC_list l              -> (C_list   , [l])
+          | TC_set  s              -> (C_set    , [s])
+          | TC_map  ( k , v )      -> (C_map    , [k;v])
+          | TC_big_map  ( k , v )  -> (C_big_map, [k;v])
+          | TC_contract c          -> (C_contract, [c])
+          | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
+          | TC_tuple lst           -> (C_tuple, lst)
       )
       in
       P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
@@ -350,7 +349,7 @@ end
 module TypeVariable =
 struct
   type t = Core.type_variable
-  let compare a b= Var.compare a b
+  let compare a b = Var.compare a b
   let to_string = (fun s -> Format.asprintf "%a" Var.pp s)
 
 end
@@ -475,44 +474,69 @@ module UnionFindWrapper = struct
       in
       let dbs = { dbs with grouped_by_variable } in
       dbs
-  let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
+
+  let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs =
     fun variable_a variable_b dbs ->
+    (* get old representant for variable_a *)
     let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
     let dbs = { dbs with aliases } in
+    (* get old representant for variable_b *)
     let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
     let dbs = { dbs with aliases } in
-    let default d = function None -> d | Some y -> y in
-    let get_constraints ab =
-      TypeVariableMap.find_opt ab dbs.grouped_by_variable
-      |> default { constructor = [] ; poly = [] ; tc = [] } in
-    let constraints_a = get_constraints variable_repr_a in
-    let constraints_b = get_constraints variable_repr_b in
-    let all_constraints = {
-      constructor = constraints_a.constructor @ constraints_b.constructor ;
-      poly        = constraints_a.poly        @ constraints_b.poly        ;
-      tc          = constraints_a.tc          @ constraints_b.tc          ;
-    } in
-    let grouped_by_variable =
-      TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
-    let dbs = { dbs with grouped_by_variable} in
-    let grouped_by_variable =
-      TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
-    let dbs = { dbs with grouped_by_variable} in
-    dbs
+
+    (* alias variable_a and variable_b together *)
+    let aliases = UF.alias variable_a variable_b dbs.aliases in
+    let dbs = { dbs with aliases } in
+
+    (* Replace the two entries in grouped_by_variable by a single one *)
+    (
+      let get_constraints ab =
+        match TypeVariableMap.find_opt ab dbs.grouped_by_variable with
+        | Some x -> x
+        | None -> { constructor = [] ; poly = [] ; tc = [] } in
+      let constraints_a = get_constraints variable_repr_a in
+      let constraints_b = get_constraints variable_repr_b in
+      let all_constraints = {
+          constructor = constraints_a.constructor @ constraints_b.constructor ;
+          poly        = constraints_a.poly        @ constraints_b.poly        ;
+          tc          = constraints_a.tc          @ constraints_b.tc          ;
+        } in
+      let grouped_by_variable =
+        TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
+      let dbs = { dbs with grouped_by_variable} in
+      let grouped_by_variable =
+        TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
+      let dbs = { dbs with grouped_by_variable} in
+      dbs
+    )
 end
 
 (* sub-sub component: constraint normalizer: remove dupes and give structure
  * right now: union-find of unification vars
  * later: better database-like organisation of knowledge *)
 
-(* Each normalizer returns a  *)
-(* If implemented in a language with decent sets, should be 'b set not 'b list. *)
+(* Each normalizer returns an updated database (after storing the
+   incoming constraint) and a list of constraints, used when the
+   normalizer rewrites the constraints e.g. into simpler ones. *)
+(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *)
 type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
 
+(** Updates the dbs.all_constraints field when new constraints are
+   discovered.
+
+   This field contains a list of all the constraints, without any form of
+   grouping or sorting. *)
 let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
     ({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
 
+(** Updates the dbs.grouped_by_variable field when new constraints are
+   discovered.
+
+    This field contains a map from type variables to lists of
+   constraints that are related to that variable (in other words, the
+   key appears in the equation).
+ *)
 let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
   let store_constraint tvars constraints =
@@ -520,16 +544,18 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
       UnionFindWrapper.add_constraints_related_to tvar constraints dbs
     in List.fold_left aux dbs tvars
   in
-  let merge_constraints a b =
-    UnionFindWrapper.merge_variables a b dbs in
   let dbs = match new_constraint with
       SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = []  ; tc = []}
     | SC_Typeclass   ({tc = _ ; args}            as c) -> store_constraint args            {constructor = []  ; poly = []  ; tc = [c]}
     | SC_Poly        ({tv; forall = _}           as c) -> store_constraint [tv]            {constructor = []  ; poly = [c] ; tc = []}
-    | SC_Alias (a , b) -> merge_constraints a b
+    | SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs
   in (dbs , [new_constraint])
 
-(* Stores the first assinment ('a = ctor('b, …)) seen *)
+(** Stores the first assinment ('a = ctor('b, …)) that is encountered.
+
+    Subsequent ('a = ctor('b2, …)) with the same 'a are ignored.
+
+    TOOD: are we checking somewhere that 'b … = 'b2 … ? *)
 let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
     match new_constraint with
@@ -540,9 +566,14 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor
     | _ ->
       (dbs , [new_constraint])
 
+(** Evaluates a type-leval application. For now, only supports
+    immediate beta-reduction at the root of the type. *)
 let type_level_eval : type_value -> type_value * type_constraint list =
   fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
 
+(** Checks that a type-level application has been fully reduced. For
+    now, only some simple cases like applications of `forall`
+    <polymorphic types are allowed. *)
 let check_applied ((reduced, _new_constraints) as x) =
   let () = match reduced with
       P_apply _ -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
@@ -552,6 +583,14 @@ let check_applied ((reduced, _new_constraints) as x) =
 (* TODO: at some point there may be uses of named type aliases (type
    foo = int; let x : foo = 42). These should be inlined. *)
 
+(** This function converts constraints from type_constraint to
+    type_constraint_simpl. The former has more possible cases, and the
+    latter uses a more minimalistic constraint language.
+
+    It does not modify the dbs, and only rewrites the constraint
+
+    TODO: update the code to show that the dbs are always copied as-is
+ *)
 let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
   let insert_fresh a b =
diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml
index 05b11c897..ba9e10bd0 100644
--- a/src/passes/4-typer-new/typer.ml
+++ b/src/passes/4-typer-new/typer.ml
@@ -334,9 +334,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
     let%bind a' = evaluate_type e a in
     let%bind b' = evaluate_type e b in
     return (T_arrow (a', b'))
-  | T_tuple lst ->
-    let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-    return (T_tuple lst')
   | T_sum m ->
     let aux k v prev =
       let%bind prev' = prev in
@@ -382,6 +379,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ O.TC_contract c
+        | TC_arrow ( arg , ret ) ->
+           let%bind arg' = evaluate_type e arg in
+           let%bind ret' = evaluate_type e ret in
+           ok @@ O.TC_arrow ( arg' , ret' )
+        | TC_tuple lst ->
+           let%bind lst' = bind_map_list (evaluate_type e) lst in
+           ok @@ O.TC_tuple lst'
         in
       return (T_operator (opt))
 
@@ -469,10 +473,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
       return_wrapped (e_operation o) state @@ Wrap.literal (t_operation ())
     )
   | E_literal (Literal_unit) -> (
-      return_wrapped (e_unit) state @@ Wrap.literal (t_unit ())
+      return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
     )
   | E_skip -> (
-      failwith "TODO: missing implementation for E_skip"
+    (* E_skip just returns unit *)
+    return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
     )
   (* | E_literal (Literal_string s) -> (
    *     L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
@@ -516,7 +521,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
       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_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
 
@@ -932,9 +936,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
 (*
 Apply type_declaration on all the node of the AST_simplified from the root p
 *)
-let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result =
-  let env = Ast_typed.Environment.full_empty in
-  let state = Solver.initial_state in
+let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result =
   let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
     let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
     let ds' = match d'_opt with
@@ -949,51 +951,45 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
   let () = ignore (env' , state') in
   ok (env', state', declarations)
 
-(* module TSMap = TMap(Solver.TypeVariable) *)
-
-(* let c_tag_to_string : Solver.Core.constant_tag -> string = function
- *   | Solver.Core.C_arrow     -> "arrow"
- *   | Solver.Core.C_option    -> "option"
- *   | Solver.Core.C_tuple     -> "tuple"
- *   | Solver.Core.C_record    -> failwith "record"
- *   | Solver.Core.C_variant   -> failwith "variant"
- *   | Solver.Core.C_map       -> "map"
- *   | Solver.Core.C_big_map   -> "big"
- *   | Solver.Core.C_list      -> "list"
- *   | Solver.Core.C_set       -> "set"
- *   | Solver.Core.C_unit      -> "unit"
- *   | Solver.Core.C_bool      -> "bool"
- *   | Solver.Core.C_string    -> "string"
- *   | Solver.Core.C_nat       -> "nat"
- *   | Solver.Core.C_mutez     -> "mutez"
- *   | Solver.Core.C_timestamp -> "timestamp"
- *   | Solver.Core.C_int       -> "int"
- *   | Solver.Core.C_address   -> "address"
- *   | Solver.Core.C_bytes     -> "bytes"
- *   | Solver.Core.C_key_hash  -> "key_hash"
- *   | Solver.Core.C_key       -> "key"
- *   | Solver.Core.C_signature -> "signature"
- *   | Solver.Core.C_operation -> "operation"
- *   | Solver.Core.C_contract  -> "contract"
- *   | Solver.Core.C_chain_id  -> "chain_id" *)
-
-let type_program (p : I.program) : (O.program * Solver.state) result =
-  let%bind (env, state, program) = type_program_returns_state p in
+let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result =
+  let%bind (env, state, program) = type_xyz_returns_state env_state_node in
   let subst_all =
+    let aliases = state.structured_dbs.aliases in
     let assignments = state.structured_dbs.assignments in
-    let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) =
-      let%bind p = p in
-      let Solver.{ tv ; c_tag ; tv_list } = expr in
+    let substs : variable: I.type_variable -> _ = fun ~variable ->
+      to_option @@
+      let%bind root =
+        trace_option (simple_error (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@
+          (* TODO: after upgrading UnionFind, this will be an option, not an exception. *)
+          try Some (Solver.UF.repr variable aliases) with Not_found -> None in
+      let%bind assignment =
+        trace_option (simple_error (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
+          (Solver.TypeVariableMap.find_opt root assignments) in
+      let Solver.{ tv ; c_tag ; tv_list } = assignment in
       let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in
       let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in
-      Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in
-    (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *)
-    let p = Solver.TypeVariableMap.fold aux assignments (ok program) in
+      ok @@ expr
+    in
+    let p = apply_substs ~substs program in
     p in
   let%bind program = subst_all in
   let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (program, state)
 
+let type_program (p : I.program) : (O.program * Solver.state) result =
+  let empty_env = Ast_typed.Environment.full_empty in
+  let empty_state = Solver.initial_state in
+  type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
+
+let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.annotated_expression) Trace.result =
+  fun (env, state, e) ->
+  let%bind (e , state) = type_expression env state e in
+  ok (env, state, e)
+
+let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_value option) (e : I.expression) : (O.annotated_expression * Solver.state) result =
+  let () = ignore tv_opt in     (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
+  type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_annotated_expression type_expression_returns_state
+
  (*
 TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity
  *)
@@ -1021,9 +1017,6 @@ let type_program' : I.program -> O.program result = fun p ->
 let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
   (* TODO: or should we use t.simplified if present? *)
   let%bind t = match t.type_value' with
-  | O.T_tuple x ->
-    let%bind x' = bind_map_list untype_type_expression x in
-    ok @@ I.T_tuple x'
   | O.T_sum x ->
     let%bind x' = I.bind_map_cmap untype_type_expression x in
     ok @@ I.T_sum x'
@@ -1059,6 +1052,13 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
       | O.TC_contract c->
          let%bind c = untype_type_expression c in
          ok @@ I.TC_contract c
+      | O.TC_arrow ( arg , ret ) ->
+         let%bind arg' = untype_type_expression arg in
+         let%bind ret' = untype_type_expression ret in
+         ok @@ I.TC_arrow ( arg' , ret' )
+      | O.TC_tuple lst ->
+         let%bind lst' = bind_map_list untype_type_expression lst in
+         ok @@ I.TC_tuple lst'
       in
       ok @@ I.T_operator (type_name)
     in
diff --git a/src/passes/4-typer-new/typer.mli b/src/passes/4-typer-new/typer.mli
index 07c28338b..379b31b1e 100644
--- a/src/passes/4-typer-new/typer.mli
+++ b/src/passes/4-typer-new/typer.mli
@@ -44,6 +44,7 @@ val type_declaration : environment -> Solver.state -> I.declaration -> (environm
 (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
 val evaluate_type : environment -> I.type_expression -> O.type_value result
 val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val type_constant : I.constant -> O.type_value list -> O.type_value option -> (O.constant * O.type_value) result
 (*
 val untype_type_value : O.type_value -> (I.type_expression) result
diff --git a/src/passes/4-typer-old/typer.ml b/src/passes/4-typer-old/typer.ml
index 1e65fad3e..8c43ade15 100644
--- a/src/passes/4-typer-old/typer.ml
+++ b/src/passes/4-typer-old/typer.ml
@@ -327,9 +327,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
       let%bind a' = evaluate_type e a in
       let%bind b' = evaluate_type e b in
       return (T_arrow (a', b'))
-  | T_tuple lst ->
-      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      return (T_tuple lst')
   | T_sum m ->
       let aux k v prev =
         let%bind prev' = prev in
@@ -375,6 +372,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ I.TC_contract c
+        | TC_arrow ( arg , ret ) ->
+            let%bind arg' = evaluate_type e arg in
+            let%bind ret' = evaluate_type e ret in
+            ok @@ I.TC_arrow ( arg' , ret' )
+        | TC_tuple lst ->
+            let%bind lst' = bind_map_list (evaluate_type e) lst in
+            ok @@ I.TC_tuple lst'
         in
       return (T_operator (opt))
 
diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index c59346c8b..8ab5576a0 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -10,5 +10,5 @@ module Solver = Typer_new.Solver (* Both the old typer and the new typer use the
 type environment = Environment.t
 
 let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program
-let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression
+let type_expression_subst = if use_new_typer then Typer_new.type_expression_subst else Typer_old.type_expression (* the old typer does not have unification variables that would need substitution, so no need to "subst" anything. *)
 let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression
diff --git a/src/passes/4-typer/typer.mli b/src/passes/4-typer/typer.mli
index cd11ec423..b7c410383 100644
--- a/src/passes/4-typer/typer.mli
+++ b/src/passes/4-typer/typer.mli
@@ -12,5 +12,5 @@ module Solver = Typer_new.Solver
 type environment = Environment.t
 
 val type_program : I.program -> (O.program * Solver.state) result
-val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val untype_expression : O.annotated_expression -> I.expression result
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index 223264f7f..86c921c70 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -146,6 +146,11 @@ let rec transpile_type (t:AST.type_value) : type_value result =
   | T_operator (TC_option o) ->
       let%bind o' = transpile_type o in
       ok (T_option o')
+  | T_operator (TC_arrow (param , result)) -> (
+      let%bind param' = transpile_type param in
+      let%bind result' = transpile_type result in
+      ok (T_function (param', result'))
+    )
   (* TODO hmm *)
   | T_sum m ->
       let node = Append_tree.of_list @@ kv_list_of_cmap m in
@@ -173,7 +178,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
                         ok (Some ann, a))
                       aux node in
       ok @@ snd m'
-  | T_tuple lst ->
+  | T_operator (TC_tuple lst) ->
       let node = Append_tree.of_list lst in
       let aux a b : type_value result =
         let%bind a = a in
@@ -320,7 +325,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
   | E_tuple_accessor (tpl, ind) -> (
       let%bind ty' = transpile_type tpl.type_annotation in
       let%bind ty_lst =
-        trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
+        trace_strong (corner_case ~loc:__LOC__ "transpiler: E_tuple_accessor: not a tuple") @@
         get_t_tuple tpl.type_annotation in
       let%bind ty'_lst = bind_map_list transpile_type ty_lst in
       let%bind path =
@@ -505,7 +510,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
           match cur with
           | Access_tuple ind -> (
               let%bind ty_lst =
-                trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
+                trace_strong (corner_case ~loc:__LOC__ "transpiler: E_assign: Access_tuple: not a tuple") @@
                 AST.Combinators.get_t_tuple prev in
               let%bind ty'_lst = bind_map_list transpile_type ty_lst in
               let%bind path = tuple_access_to_lr ty' ty'_lst ind in
diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml
index a548003b0..cc572fa94 100644
--- a/src/passes/6-transpiler/untranspiler.ml
+++ b/src/passes/6-transpiler/untranspiler.ml
@@ -36,15 +36,6 @@ them. please report this to the developers." in
     ] in
     error ~data title content
 
-  let unknown_untranspile unknown_type value =
-    let title () = "untranspiling unknown value" in
-    let content () = Format.asprintf "can not untranspile %s" unknown_type in
-    let data = [
-      ("unknown_type" , fun () -> unknown_type) ;
-      ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
-    ] in
-    error ~data title content
-
 end
 
 open Errors
@@ -196,6 +187,22 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
       )
     | TC_contract _ ->
       fail @@ bad_untranspile "contract" v
+    | TC_arrow _ -> (
+        let%bind n =
+          trace_strong (wrong_mini_c_value "lambda as string" v) @@
+          get_string v in
+        return (E_literal (Literal_string n))
+      )
+    | TC_tuple lst ->
+      let%bind node = match Append_tree.of_list lst with
+        | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
+        | Full t -> ok t in
+      let%bind tpl =
+        trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
+        extract_tuple v node in
+      let%bind tpl' = bind_list
+        @@ List.map (fun (x, y) -> untranspile x y) tpl in
+      return (E_tuple tpl')
   )
   | T_sum m ->
       let lst = kv_list_of_cmap m in
@@ -208,16 +215,6 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         extract_constructor v node in
       let%bind sub = untranspile v tv in
       return (E_constructor (Constructor name, sub))
-  | T_tuple lst ->
-      let%bind node = match Append_tree.of_list lst with
-        | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
-        | Full t -> ok t in
-      let%bind tpl =
-        trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
-        extract_tuple v node in
-      let%bind tpl' = bind_list
-        @@ List.map (fun (x, y) -> untranspile x y) tpl in
-      return (E_tuple tpl')
   | T_record m ->
       let lst = kv_list_of_lmap m in
       let%bind node = match Append_tree.of_list lst with
diff --git a/src/stages/ast_simplified/PP.ml b/src/stages/ast_simplified/PP.ml
index b20ee456d..92138a014 100644
--- a/src/stages/ast_simplified/PP.ml
+++ b/src/stages/ast_simplified/PP.ml
@@ -18,7 +18,7 @@ and type_expression ppf (te: type_expression) : unit =
   te' ppf te.type_expression'
 
 let rec expression ppf (e:expression) = match e.expression with
-  | E_literal l -> literal ppf l
+  | E_literal l -> fprintf ppf "%a" literal l
   | E_variable n -> fprintf ppf "%a" name n
   | E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
   | E_constructor (c, ae) -> fprintf ppf "%a(%a)" constructor c expression ae
diff --git a/src/stages/ast_simplified/combinators.ml b/src/stages/ast_simplified/combinators.ml
index 611822768..2a3e0ab33 100644
--- a/src/stages/ast_simplified/combinators.ml
+++ b/src/stages/ast_simplified/combinators.ml
@@ -36,7 +36,7 @@ let t_key_hash     : type_expression = make_t @@ T_constant (TC_key_hash)
 let t_option  o    : type_expression = make_t @@ T_operator (TC_option o)
 let t_list  t      : type_expression = make_t @@ T_operator (TC_list t)
 let t_variable n   : type_expression = make_t @@ T_variable (Var.of_name n)
-let t_tuple lst    : type_expression = make_t @@ T_tuple lst
+let t_tuple lst    : type_expression = make_t @@ T_operator (TC_tuple lst)
 let t_pair (a , b) : type_expression = t_tuple [a ; b]
 let t_record_ez lst =
   let lst = List.map (fun (k, v) -> (Label k, v)) lst in
@@ -206,7 +206,7 @@ let get_e_list = fun t ->
 let get_e_tuple = fun t ->
   match t with
   | E_tuple lst -> ok lst
-  | _ -> simple_fail "not a tuple"
+  | _ -> simple_fail "ast_simplified: get_e_tuple: not a tuple"
 
 let extract_pair : expression -> (expression * expression) result = fun e ->
   match e.expression with
diff --git a/src/stages/ast_simplified/combinators.mli b/src/stages/ast_simplified/combinators.mli
index f6a6f7bce..d8349e0a2 100644
--- a/src/stages/ast_simplified/combinators.mli
+++ b/src/stages/ast_simplified/combinators.mli
@@ -27,8 +27,8 @@ val t_option    : type_expression -> type_expression
 *)
 val t_list      : type_expression -> type_expression
 val t_variable  : string -> type_expression
-(*
 val t_tuple     : type_expression list -> type_expression
+(*
 val t_record    : te_map -> type_expression
 *)
 val t_pair : ( type_expression * type_expression ) -> type_expression
diff --git a/src/stages/ast_simplified/misc.ml b/src/stages/ast_simplified/misc.ml
index b3301789d..bc214863a 100644
--- a/src/stages/ast_simplified/misc.ml
+++ b/src/stages/ast_simplified/misc.ml
@@ -1,6 +1,8 @@
 open Trace
 open Types
 
+include Stage_common.Misc
+
 module Errors = struct
   let different_literals_because_different_types name a b () =
     let title () = "literals have different types: " ^ name in
diff --git a/src/stages/ast_simplified/misc.mli b/src/stages/ast_simplified/misc.mli
index 9ef833e55..20813de49 100644
--- a/src/stages/ast_simplified/misc.mli
+++ b/src/stages/ast_simplified/misc.mli
@@ -1,5 +1,8 @@
 open Trace
 open Types
+
+include module type of Stage_common.Misc
+
 (*
 
 module Errors : sig
@@ -15,4 +18,4 @@ val assert_literal_eq : ( literal * literal ) -> unit result
 
 val assert_value_eq : ( expression * expression ) -> unit result
 
-val is_value_eq : ( expression * expression ) -> bool
\ No newline at end of file
+val is_value_eq : ( expression * expression ) -> bool
diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml
index 3a0e8c5a5..9d412cd53 100644
--- a/src/stages/ast_typed/PP.ml
+++ b/src/stages/ast_typed/PP.ml
@@ -15,13 +15,12 @@ and type_value ppf (tv:type_value) : unit =
 
 let rec annotated_expression ppf (ae:annotated_expression) : unit =
   match ae.type_annotation.simplified with
-  | Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
-  | _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
+  | _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
 
 and lambda ppf l =
   let ({ binder ; body } : lambda) = l in
-  fprintf ppf "lambda (%a) -> %a"
-    name binder 
+  fprintf ppf "(lambda (%a) -> %a)"
+    name binder
     annotated_expression body
 
 and option_inline ppf inline = 
@@ -33,9 +32,9 @@ and option_inline ppf inline =
 and expression ppf (e:expression) : unit =
   match e with
   | E_literal l -> Stage_common.PP.literal ppf l
-  | E_constant (b, lst) -> fprintf ppf "%a(%a)" constant b (list_sep_d annotated_expression) lst
-  | E_constructor (c, lst) -> fprintf ppf "%a(%a)" constructor c annotated_expression lst
-  | E_variable a -> fprintf ppf "%a" name a
+  | E_constant (b, lst) -> fprintf ppf "(e_constant %a(%a))" constant b (list_sep_d annotated_expression) lst
+  | E_constructor (c, lst) -> fprintf ppf "(e_constructor %a(%a))" constructor c annotated_expression lst
+  | E_variable a -> fprintf ppf "(e_var %a)" name a
   | E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
   | E_lambda l -> fprintf ppf "%a" lambda l
   | E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
@@ -50,7 +49,7 @@ and expression ppf (e:expression) : unit =
   | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
-  | E_sequence (a , b) -> fprintf ppf "%a ; %a" annotated_expression a annotated_expression b
+  | E_sequence (a , b) -> fprintf ppf "(e_seq %a ; %a)" annotated_expression a annotated_expression b
   | E_loop (expr , body) -> fprintf ppf "while %a { %a }" annotated_expression expr annotated_expression body
   | E_assign (name , path , expr) ->
     fprintf ppf "%a.%a := %a"
diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml
index 8ebe2b89d..17037787f 100644
--- a/src/stages/ast_typed/combinators.ml
+++ b/src/stages/ast_typed/combinators.ml
@@ -48,7 +48,7 @@ let t_mutez ?s ()      : type_value = make_t (T_constant TC_mutez) s
 let t_timestamp ?s ()  : type_value = make_t (T_constant TC_timestamp) s
 let t_unit ?s ()       : type_value = make_t (T_constant TC_unit) s
 let t_option o ?s ()   : type_value = make_t (T_operator (TC_option o)) s
-let t_tuple lst ?s ()  : type_value = make_t (T_tuple lst) s
+let t_tuple lst ?s ()  : type_value = make_t (T_operator (TC_tuple lst)) s
 let t_variable t ?s () : type_value = make_t (T_variable t) s
 let t_list t ?s ()     : type_value = make_t (T_operator (TC_list t)) s
 let t_set t ?s ()      : type_value = make_t (T_operator (TC_set t)) s
@@ -147,11 +147,11 @@ let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
   | _ -> fail @@ Errors.not_a_x_type "key_hash" t ()
 
 let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
-  | T_tuple lst -> ok lst
+  | T_operator (TC_tuple lst) -> ok lst
   | _ -> fail @@ Errors.not_a_x_type "tuple" t ()
 
 let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_value' with
-  | T_tuple lst ->
+  | T_operator (TC_tuple lst) ->
       let%bind () =
         trace_strong (Errors.not_a_x_type "pair (tuple with two elements)" t ()) @@
         Assert.assert_list_size lst 2 in
@@ -160,6 +160,7 @@ let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_
 
 let get_t_function (t:type_value) : (type_value * type_value) result = match t.type_value' with
   | T_arrow (a,r) -> ok (a,r)
+  | T_operator (TC_arrow (a , b)) -> ok (a , b)
   | _ -> fail @@ Errors.not_a_x_type "function" t ()
 
 let get_t_sum (t:type_value) : type_value constructor_map result = match t.type_value' with
@@ -253,11 +254,11 @@ let ez_e_record (lst : (label * ae) list) : expression =
   let map = List.fold_left aux LMap.empty lst in
   e_record map
 let e_some s : expression = E_constant (C_SOME, [s])
-let e_none   : expression = E_constant (C_NONE, [])
+let e_none () : expression = E_constant (C_NONE, [])
 
 let e_map lst : expression = E_map lst
 
-let e_unit : expression = E_literal (Literal_unit)
+let e_unit () : expression = E_literal (Literal_unit)
 let e_int n : expression = E_literal (Literal_int n)
 let e_nat n : expression = E_literal (Literal_nat n)
 let e_mutez n : expression = E_literal (Literal_mutez n)
@@ -279,7 +280,7 @@ let e_list lst : expression = E_list lst
 let e_let_in binder inline rhs result = E_let_in { binder ; rhs ; result; inline }
 let e_tuple lst : expression = E_tuple lst
 
-let e_a_unit = make_a_e e_unit (t_unit ())
+let e_a_unit = make_a_e (e_unit ()) (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
 let e_a_nat n = make_a_e (e_nat n) (t_nat ())
 let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ())
@@ -289,7 +290,7 @@ let e_a_address s = make_a_e (e_address s) (t_address ())
 let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
 let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
 let e_a_lambda l in_ty out_ty = make_a_e (e_lambda l) (t_function in_ty out_ty ())
-let e_a_none t = make_a_e e_none (t_option t ())
+let e_a_none t = make_a_e (e_none ()) (t_option t ())
 let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ())
 let e_a_record r = make_a_e (e_record r) (t_record (LMap.map get_type_annotation r) ())
 let e_a_application a b = make_a_e (e_application a b) (get_type_annotation b)
diff --git a/src/stages/ast_typed/combinators.mli b/src/stages/ast_typed/combinators.mli
index f9cd7d93d..4f794deb8 100644
--- a/src/stages/ast_typed/combinators.mli
+++ b/src/stages/ast_typed/combinators.mli
@@ -111,9 +111,9 @@ val ez_e_record : ( string * annotated_expression ) list -> expression
 
 *)
 val e_some : value -> expression
-val e_none : expression
+val e_none : unit -> expression
 val e_map : ( value * value ) list -> expression
-val e_unit : expression
+val e_unit : unit -> expression
 val e_int : int -> expression
 val e_nat : int -> expression
 val e_mutez : int -> expression
diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml
index 24aa06ff0..f56558b13 100644
--- a/src/stages/ast_typed/misc.ml
+++ b/src/stages/ast_typed/misc.ml
@@ -1,5 +1,6 @@
 open Trace
 open Types
+
 include Stage_common.Misc
 
 module Errors = struct
@@ -29,6 +30,21 @@ module Errors = struct
     ] in
     error ~data title message ()
 
+  let different_operator_number_of_arguments opa opb lena lenb () =
+    let title = (thunk "different number of arguments to type constructors") in
+    assert (String.equal (type_operator_name opa) (type_operator_name opb));
+    let message () = Format.asprintf
+                       "Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)"
+                       (type_operator_name opa) lena lenb in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opa) ;
+      ("b" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opb) ;
+      ("op" , fun () -> type_operator_name opa) ;
+      ("len_a" , fun () -> Format.asprintf "%d" lena) ;
+      ("len_b" , fun () -> Format.asprintf "%d" lenb) ;
+    ] in
+    error ~data title message ()
+
   let different_size_type name a b () =
     let title () = name ^ " have different sizes" in
     let message () = "Expected these two types to be the same, but they're different (both are " ^ name ^ ", but with a different number of arguments)" in
@@ -49,8 +65,6 @@ module Errors = struct
 
   let _different_size_constants = different_size_type "type constructors"
 
-  let different_size_tuples = different_size_type "tuples"
-
   let different_size_sums = different_size_type "sums"
 
   let different_size_records = different_size_type "records"
@@ -301,13 +315,6 @@ open Errors
 
        
 let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
-  | T_tuple ta, T_tuple tb -> (
-      let%bind _ =
-        trace_strong (fun () -> (different_size_tuples a b ()))
-        @@ Assert.assert_true List.(length ta = length tb) in
-      bind_list_iter assert_type_value_eq (List.combine ta tb)
-    )
-  | T_tuple _, _ -> fail @@ different_kinds a b
   | T_constant ca, T_constant cb -> (
       trace_strong (different_constants ca cb)
       @@ Assert.assert_true (ca = cb)
@@ -321,10 +328,16 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       | TC_set la, TC_set lb -> ok @@ ([la], [lb])
       | TC_map (ka,va), TC_map (kb,vb)
       | TC_big_map (ka,va), TC_big_map (kb,vb) -> ok @@ ([ka;va] ,[kb;vb]) 
-      | _,_ -> fail @@ different_operators opa opb
+      | TC_tuple lsta, TC_tuple lstb -> ok @@ (lsta , lstb) 
+      | TC_arrow (froma , toa) , TC_arrow (fromb , tob) -> ok @@ ([froma;toa] , [fromb;tob]) 
+      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _),
+        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _) -> fail @@ different_operators opa opb
       in
-    trace (different_types "arguments to type operators" a b)
-      @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
+      if List.length lsta <> List.length lstb then
+        fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
+      else
+        trace (different_types "arguments to type operators" a b)
+        @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
   )
   | T_operator _, _ -> fail @@ different_kinds a b
   | T_sum sa, T_sum sb -> (
diff --git a/src/stages/ast_typed/misc.mli b/src/stages/ast_typed/misc.mli
index 45efb025f..44e3ca324 100644
--- a/src/stages/ast_typed/misc.mli
+++ b/src/stages/ast_typed/misc.mli
@@ -1,6 +1,8 @@
 open Trace
 open Types
 
+include module type of Stage_common.Misc
+
 val assert_value_eq : ( value * value ) -> unit result
 
 val assert_type_value_eq : ( type_value * type_value ) -> unit result
@@ -43,7 +45,6 @@ module Errors : sig
   val different_size_type : name -> type_value -> type_value -> unit -> error
   val different_props_in_record : string -> string -> unit -> error
   val different_size_constants : type_value -> type_value -> unit -> error
-  val different_size_tuples : type_value -> type_value -> unit -> error
   val different_size_sums : type_value -> type_value -> unit -> error
   val different_size_records : type_value -> type_value -> unit -> error
   val different_types : name -> type_value -> type_value -> unit -> error
diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml
index 89be72a82..cf4957613 100644
--- a/src/stages/ast_typed/types.ml
+++ b/src/stages/ast_typed/types.ml
@@ -18,7 +18,7 @@ and environment_element_definition =
 and free_variables = expression_variable list
 
 and environment_element = {
-  type_value : type_value ;  
+  type_value : type_value ;
   source_environment : full_environment ;
   definition : environment_element_definition ;
 }
@@ -34,6 +34,12 @@ and annotated_expression = {
   location : Location.t ;
 }
 
+(* This seems to be used only for top-level declarations, and
+   represents the name of the top-level binding, and the expression
+   assigned to it. -- Suzanne.
+
+   TODO: if this is correct, then we should inline this in
+   "declaration" or at least move it close to it. *)
 and named_expression = {
   name: expression_variable ;
   annotated_expression: ae ;
@@ -41,6 +47,7 @@ and named_expression = {
 
 and ae = annotated_expression
 and type_value' = type_value type_expression'
+
 and type_value = {
   type_value' : type_value';
   simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *)
@@ -77,7 +84,7 @@ and 'a expression' =
   | E_application of (('a) * ('a))
   | E_lambda of lambda
   | E_let_in of let_in
-  (* Tuple *)
+  (* Tuple, TODO: remove tuples and use records with integer keys instead *)
   | E_tuple of ('a) list
   | E_tuple_accessor of (('a) * int) (* Access n'th tuple's element *)
   (* Sum *)
diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml
index 7d42e0c7e..deebe08ee 100644
--- a/src/stages/common/PP.ml
+++ b/src/stages/common/PP.ml
@@ -141,7 +141,6 @@ let lmap_sep_d x = lmap_sep x (const " , ")
 let rec type_expression' : type a . (formatter -> a -> unit) -> formatter -> a type_expression' -> unit =
   fun f ppf te ->
   match te with
-    | T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d f) lst
     | T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
     | T_record m -> fprintf ppf "record[%a]" (lmap_sep_d f ) m
     | T_arrow (a, b) -> fprintf ppf "%a -> %a" f a f b
@@ -178,6 +177,8 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope
     | TC_map    (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
     | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
     | TC_contract (c) -> Format.asprintf "Contract (%a)" f c
+    | TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b
+    | TC_tuple lst -> Format.asprintf "tuple[%a]" (list_sep_d f) lst
     in
   fprintf ppf "(TO_%s)" s
 
diff --git a/src/stages/common/misc.ml b/src/stages/common/misc.ml
index 7f38acf62..794a36e7c 100644
--- a/src/stages/common/misc.ml
+++ b/src/stages/common/misc.ml
@@ -7,7 +7,9 @@ let map_type_operator f = function
   | TC_list x -> TC_list (f x)
   | TC_set x -> TC_set (f x)
   | TC_map (x , y) -> TC_map (f x , f y)
-  | TC_big_map (x , y)-> TC_big_map (f x , f y)
+  | TC_big_map (x , y) -> TC_big_map (f x , f y)
+  | TC_arrow (x , y) -> TC_arrow (f x , f y)
+  | TC_tuple lst -> TC_tuple (List.map f lst)
 
 let bind_map_type_operator f = function
     TC_contract x -> let%bind x = f x in ok @@ TC_contract x
@@ -15,7 +17,9 @@ let bind_map_type_operator f = function
   | TC_list x -> let%bind x = f x in ok @@ TC_list x
   | TC_set x -> let%bind x = f x in ok @@ TC_set x
   | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y)
-  | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
+  | TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
+  | TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y)
+  | TC_tuple lst -> let%bind lst = bind_map_list f lst in ok @@ TC_tuple lst
 
 let type_operator_name = function
       TC_contract _ -> "TC_contract"
@@ -24,6 +28,8 @@ let type_operator_name = function
     | TC_set      _ -> "TC_set"
     | TC_map      _ -> "TC_map"
     | TC_big_map  _ -> "TC_big_map"
+    | TC_arrow    _ -> "TC_arrow"
+    | TC_tuple    _ -> "TC_tuple"
 
 let type_expression'_of_string = function
   | "TC_contract" , [x]     -> ok @@ T_operator(TC_contract x)
@@ -61,6 +67,8 @@ let string_of_type_operator = function
   | TC_set       x       -> "TC_set"      , [x]
   | TC_map       (x , y) -> "TC_map"      , [x ; y]
   | TC_big_map   (x , y) -> "TC_big_map"  , [x ; y]
+  | TC_arrow     (x , y) -> "TC_arrow"    , [x ; y]
+  | TC_tuple     lst     -> "TC_tuple"    , lst
 
 let string_of_type_constant = function
   | TC_unit      -> "TC_unit", []
@@ -81,5 +89,6 @@ let string_of_type_constant = function
 let string_of_type_expression' = function
   | T_operator o -> string_of_type_operator o
   | T_constant c -> string_of_type_constant c
-  | T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
+  | T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
      failwith "not a type operator or constant"
+
diff --git a/src/stages/common/misc.mli b/src/stages/common/misc.mli
new file mode 100644
index 000000000..78dfaf17e
--- /dev/null
+++ b/src/stages/common/misc.mli
@@ -0,0 +1,9 @@
+open Types
+
+val map_type_operator : ('a -> 'b) -> 'a type_operator -> 'b type_operator
+val bind_map_type_operator : ('a -> ('b * 'c list, 'd) Pervasives.result) -> 'a type_operator -> ('b type_operator * 'c list, 'd) Pervasives.result
+val type_operator_name : 'a type_operator -> string
+val type_expression'_of_string : string * 'a list -> ('a type_expression' * 'b list, 'c) Pervasives.result
+val string_of_type_operator : 'a type_operator -> string * 'a list
+val string_of_type_constant : type_constant -> string * 'a list
+val string_of_type_expression' : 'a type_expression' -> string * 'a list
diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml
index b25eb80a5..70c3bc80a 100644
--- a/src/stages/common/types.ml
+++ b/src/stages/common/types.ml
@@ -66,7 +66,6 @@ and literal =
 
 (* The ast is a tree of node, 'a is the type of the node (type_variable or {type_variable, previous_type}) *)
 type 'a type_expression' = 
-  | T_tuple of 'a list 
   | T_sum of 'a constructor_map
   | T_record of 'a label_map
   | T_arrow of 'a * 'a
@@ -96,6 +95,8 @@ and 'a type_operator =
   | TC_set of 'a
   | TC_map of 'a * 'a
   | TC_big_map of 'a * 'a
+  | TC_arrow of 'a * 'a
+  | TC_tuple of 'a list
 
 type type_base =
   | Base_unit 
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 3e05021d4..3321c670f 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -3,120 +3,122 @@ open Core
 let pair_map = fun f (x , y) -> (f x , f y)
 
 module Substitution = struct
-
   module Pattern = struct
 
     open Trace
     module T = Ast_typed
     (* module TSMap = Trace.TMap(String) *)
 
-    type 'a w = 'a -> 'a result
+    type substs = variable:type_variable -> T.type_value' option (* this string is a type_name or type_variable I think *)
+    let mk_substs ~v ~expr = (v , expr)
+
+    type 'a w = substs:substs -> 'a -> 'a result
 
     let rec rec_yes = true
-    and s_environment_element_definition ~v ~expr = function
+    and s_environment_element_definition ~substs = function
       | T.ED_binder -> ok @@ T.ED_binder
       | T.ED_declaration (val_, free_variables) ->
-        let%bind val_ = s_annotated_expression ~v ~expr  val_ in
-        let%bind free_variables = bind_map_list (s_variable ~v ~expr) free_variables in
+        let%bind val_ = s_annotated_expression ~substs  val_ in
+        let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
         ok @@ T.ED_declaration (val_, free_variables)
-    and s_environment ~v ~expr : T.environment w = fun env ->
+    and s_environment : T.environment w = fun ~substs env ->
       bind_map_list (fun (variable, T.{ type_value; source_environment; definition }) ->
-          let%bind variable = s_variable ~v ~expr variable in
-          let%bind type_value = s_type_value ~v ~expr type_value in
-          let%bind source_environment = s_full_environment ~v ~expr source_environment in
-          let%bind definition = s_environment_element_definition ~v ~expr definition in
+          let%bind variable = s_variable ~substs variable in
+          let%bind type_value = s_type_value ~substs type_value in
+          let%bind source_environment = s_full_environment ~substs source_environment in
+          let%bind definition = s_environment_element_definition ~substs definition in
           ok @@ (variable, T.{ type_value; source_environment; definition })) env
-    and s_type_environment ~v ~expr : T.type_environment w = fun tenv ->
+    and s_type_environment : T.type_environment w = fun ~substs tenv ->
       bind_map_list (fun (type_variable , type_value) ->
-        let%bind type_variable = s_type_variable ~v ~expr type_variable in
-        let%bind type_value = s_type_value ~v ~expr type_value in
+        let%bind type_variable = s_type_variable ~substs type_variable in
+        let%bind type_value = s_type_value ~substs type_value in
         ok @@ (type_variable , type_value)) tenv
-    and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) ->
-      let%bind environment = s_environment ~v ~expr environment in
-      let%bind type_environment = s_type_environment ~v ~expr type_environment in
+    and s_small_environment : T.small_environment w = fun ~substs (environment, type_environment) ->
+      let%bind environment = s_environment ~substs environment in
+      let%bind type_environment = s_type_environment ~substs type_environment in
       ok @@ (environment, type_environment)
-    and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) ->
-      let%bind a = s_small_environment ~v ~expr a in
-      let%bind b = bind_map_list (s_small_environment ~v ~expr) b in
+    and s_full_environment : T.full_environment w = fun ~substs (a , b) ->
+      let%bind a = s_small_environment ~substs a in
+      let%bind b = bind_map_list (s_small_environment ~substs) b in
       ok (a , b)
 
-    and s_variable ~v ~expr : T.expression_variable w = fun var ->
-      let () = ignore (v, expr) in
+    and s_variable : T.expression_variable w = fun ~substs var ->
+      let () = ignore @@ substs in
       ok var
 
-    and s_type_variable ~v ~expr : T.type_variable w = fun tvar ->
-      let _TODO = ignore (v, expr) in
+    and s_type_variable : T.type_variable w = fun ~substs tvar ->
+      let _TODO = ignore @@ substs in
       Printf.printf "TODO: subst: unimplemented case s_type_variable";
       ok @@ tvar
       (* if String.equal tvar v then
        *   expr
        * else
        *   ok tvar *)
-    and s_label ~v ~expr : T.label w = fun l ->
-      let () = ignore (v, expr) in
+    and s_label : T.label w = fun ~substs l ->
+      let () = ignore @@ substs in
       ok l
     
-    and s_build_in ~v ~expr : T.constant w = fun b ->
-      let () = ignore (v, expr) in
+    and s_build_in : T.constant w = fun ~substs b ->
+      let () = ignore @@ substs in
       ok b
 
-    and s_constructor ~v ~expr : T.constructor w = fun c ->
-      let () = ignore (v, expr) in
+    and s_constructor : T.constructor w = fun ~substs c ->
+      let () = ignore @@ substs in
       ok c
 
-    and s_type_name_constant ~v ~expr : T.type_constant w = fun type_name ->
+    and s_type_name_constant : T.type_constant w = fun ~substs type_name ->
       (* TODO: we don't need to subst anything, right? *)
-      let () = ignore (v , expr) in
+      let () = ignore @@ substs in
       ok @@ type_name
 
-    and s_type_value' ~v ~expr : T.type_value' w = function
-        | T.T_tuple type_value_list ->
-          let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
-          ok @@ T.T_tuple type_value_list
+    and s_type_value' : T.type_value' w = fun ~substs -> function
+        | T.T_operator (TC_tuple type_value_list) ->
+          let%bind type_value_list = bind_map_list (s_type_value ~substs) type_value_list in
+          ok @@ T.T_operator (TC_tuple type_value_list)
         | T.T_sum _ -> failwith "TODO: T_sum"
         | T.T_record _ -> failwith "TODO: T_record"
-        | T.T_constant (type_name) ->
-          let%bind type_name = s_type_name_constant ~v ~expr type_name in
+        | T.T_constant type_name ->
+          let%bind type_name = s_type_name_constant ~substs type_name in
           ok @@ T.T_constant (type_name)
         | T.T_variable variable ->
-           if Var.equal variable v
-           then ok @@ expr
-           else ok @@ T.T_variable variable
-        | T.T_operator (type_name_and_args) ->
-          let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *)
-          let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in
+           begin
+             match substs ~variable with
+             | Some expr -> s_type_value' ~substs expr (* TODO: is it the right thing to recursively examine this? We mustn't go into an infinite loop. *)
+             | None -> ok @@ T.T_variable variable
+           end
+        | T.T_operator type_name_and_args ->
+          let%bind type_name_and_args = T.Misc.bind_map_type_operator (s_type_value ~substs) type_name_and_args in
           ok @@ T.T_operator type_name_and_args
         | T.T_arrow _ ->
-          let _TODO = (v, expr) in
+          let _TODO = substs in
           failwith "TODO: T_function"
 
-    and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' ->
-      match type_expression' with
-        | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple"
-        | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
-        | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
-        | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
-        | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
-        | Ast_simplified.T_operator op ->
-           let%bind op =
-             Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *)
-               (s_type_expression ~v ~expr)
-               op in
-           ok @@ Ast_simplified.T_operator op
-        | Ast_simplified.T_constant constant ->
-           ok @@ Ast_simplified.T_constant constant
+    and s_type_expression' : _ Ast_simplified.type_expression' w = fun ~substs -> function
+      | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
+      | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
+      | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
+      | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
+      | Ast_simplified.T_operator op ->
+         let%bind op =
+           Ast_simplified.Misc.bind_map_type_operator
+             (s_type_expression ~substs)
+             op in
+         (* TODO: when we have generalized operators, we might need to subst the operator name itself? *)
+         ok @@ Ast_simplified.T_operator op
+      | Ast_simplified.T_constant constant ->
+         ok @@ Ast_simplified.T_constant constant
 
-    and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} ->
-      let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in
+    and s_type_expression : Ast_simplified.type_expression w = fun ~substs {type_expression'} ->
+      let%bind type_expression' = s_type_expression' ~substs type_expression' in
       ok @@ Ast_simplified.{type_expression'}
 
-    and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } ->
-      let%bind type_value' = s_type_value' ~v ~expr type_value' in
-      let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in
+    and s_type_value : T.type_value w = fun ~substs { type_value'; simplified } ->
+      let%bind type_value' = s_type_value' ~substs type_value' in
+      let%bind simplified = bind_map_option (s_type_expression ~substs) simplified in
       ok @@ T.{ type_value'; simplified }
-    and s_literal ~v ~expr : T.literal w = function
+    and s_literal : T.literal w = fun ~substs -> function
       | T.Literal_unit ->
-        let () = ignore (v, expr) in
+        let () = ignore @@ substs in
         ok @@ T.Literal_unit
       | (T.Literal_bool _ as x)
       | (T.Literal_int _ as x)
@@ -132,144 +134,145 @@ module Substitution = struct
       | (T.Literal_chain_id _ as x)
       | (T.Literal_operation _ as x) ->
         ok @@ x
-    and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->
-      let _TODO = v, expr in
+    and s_matching_expr : T.matching_expr w = fun ~substs _ ->
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_matching"
-    and s_named_type_value ~v ~expr : T.named_type_value w = fun _ ->
-      let _TODO = v, expr in
+    and s_named_type_value : T.named_type_value w = fun ~substs _ ->
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_named_type_value"
-    and s_access_path  ~v ~expr : T.access_path w = fun _ ->
-      let _TODO = v, expr in
+    and s_access_path  : T.access_path w = fun ~substs _ ->
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_access_path"
 
-    and s_expression ~v ~expr : T.expression w = function
+    and s_expression : T.expression w = fun ~(substs : substs) -> function
       | T.E_literal         x ->
-        let%bind x = s_literal ~v ~expr x in
+        let%bind x = s_literal ~substs x in
         ok @@ T.E_literal x
       | T.E_constant        (var, vals) ->
-        let%bind var = s_build_in ~v ~expr var in
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind var = s_build_in ~substs var in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_constant (var, vals)
       | T.E_variable        tv ->
-        let%bind tv = s_variable ~v ~expr tv in
+        let%bind tv = s_variable ~substs tv in
         ok @@ T.E_variable tv
       | T.E_application     (val1 , val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_application (val1 , val2)
       | T.E_lambda          { binder; body } ->
-        let%bind binder = s_variable ~v ~expr binder in
-        let%bind body = s_annotated_expression ~v ~expr body in
+        let%bind binder = s_variable ~substs binder in
+        let%bind body = s_annotated_expression ~substs body in
         ok @@ T.E_lambda { binder; body }
       | T.E_let_in          { binder; rhs; result; inline } ->
-        let%bind binder = s_variable ~v ~expr binder in
-        let%bind rhs = s_annotated_expression ~v ~expr rhs in
-        let%bind result = s_annotated_expression ~v ~expr result in
+        let%bind binder = s_variable ~substs binder in
+        let%bind rhs = s_annotated_expression ~substs rhs in
+        let%bind result = s_annotated_expression ~substs result in
         ok @@ T.E_let_in { binder; rhs; result; inline }
       | T.E_tuple           vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_tuple vals
       | T.E_tuple_accessor  (val_, i) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         let i = i in
         ok @@ T.E_tuple_accessor (val_, i)
       | T.E_constructor     (tvar, val_) ->
-        let%bind tvar = s_constructor ~v ~expr tvar in
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind tvar = s_constructor ~substs tvar in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         ok @@ T.E_constructor (tvar, val_)
       | T.E_record          aemap ->
         let _TODO = aemap in
         failwith "TODO: subst in record"
         (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
-         *     let key = s_type_variable ~v ~expr key in
-         *     let val_ = s_annotated_expression ~v ~expr val_ in
+         *     let key = s_type_variable ~substs key in
+         *     let val_ = s_annotated_expression ~substs val_ in
          *     ok @@ (key , val_)) aemap in
          * ok @@ T.E_record aemap *)
       | T.E_record_accessor (val_, l) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
-        let%bind l = s_label ~v ~expr l in
+        let%bind val_ = s_annotated_expression ~substs val_ in
+        let l = l in            (* Nothing to substitute, this is a label, not a type *)
         ok @@ T.E_record_accessor (val_, l)
-      | T.E_record_update (r, (l,e)) ->
-        let%bind r = s_annotated_expression ~v ~expr r in
-        let%bind e = s_annotated_expression ~v ~expr e in
-        ok @@ T.E_record_update (r,(l,e))
+      | T.E_record_update (r, (l, e)) ->
+        let%bind r = s_annotated_expression ~substs r in
+        let%bind e = s_annotated_expression ~substs e in
+        ok @@ T.E_record_update (r, (l, e))
       | T.E_map             val_val_list ->
         let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
-            let%bind val1 = s_annotated_expression ~v ~expr val1 in
-            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            let%bind val1 = s_annotated_expression ~substs val1 in
+            let%bind val2 = s_annotated_expression ~substs val2 in
             ok @@ (val1 , val2)
           ) val_val_list in
         ok @@ T.E_map val_val_list
       | T.E_big_map         val_val_list ->
         let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
-            let%bind val1 = s_annotated_expression ~v ~expr val1 in
-            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            let%bind val1 = s_annotated_expression ~substs val1 in
+            let%bind val2 = s_annotated_expression ~substs val2 in
             ok @@ (val1 , val2)
           ) val_val_list in
         ok @@ T.E_big_map val_val_list
       | T.E_list            vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_list vals
       | T.E_set             vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_set vals
       | T.E_look_up         (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_look_up (val1 , val2)
       | T.E_matching         (val_ , matching_expr) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
-        let%bind matching = s_matching_expr ~v ~expr matching_expr in
+        let%bind val_ = s_annotated_expression ~substs val_ in
+        let%bind matching = s_matching_expr ~substs matching_expr in
         ok @@ T.E_matching (val_ , matching)
       | T.E_sequence        (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_sequence (val1 , val2)
       | T.E_loop            (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_loop (val1 , val2)
       | T.E_assign          (named_tval, access_path, val_) ->
-        let%bind named_tval = s_named_type_value ~v ~expr named_tval in
-        let%bind access_path = s_access_path ~v ~expr access_path in
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind named_tval = s_named_type_value ~substs named_tval in
+        let%bind access_path = s_access_path ~substs access_path in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         ok @@ T.E_assign (named_tval, access_path, val_)
 
-    and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } ->
-      let%bind expression = s_expression ~v ~expr expression in
-      let%bind type_annotation = s_type_value ~v ~expr type_annotation in
-      let%bind environment = s_full_environment ~v ~expr environment in
+    and s_annotated_expression : T.annotated_expression w = fun ~substs { expression; type_annotation; environment; location } ->
+      let%bind expression = s_expression ~substs expression in
+      let%bind type_annotation = s_type_value ~substs type_annotation in
+      let%bind environment = s_full_environment ~substs environment in
       let location = location in
       ok T.{ expression; type_annotation; environment; location }
 
-    and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } ->
-      let%bind name = s_variable ~v ~expr name in
-      let%bind annotated_expression = s_annotated_expression ~v ~expr annotated_expression in
+    and s_named_expression : T.named_expression w = fun ~substs { name; annotated_expression } ->
+      let name = name in (* Nothing to substitute, this is a variable name *)
+      let%bind annotated_expression = s_annotated_expression ~substs annotated_expression in
       ok T.{ name; annotated_expression }
 
-    and s_declaration ~v ~expr : T.declaration w =
+    and s_declaration : T.declaration w = fun ~substs ->
       function
-        Ast_typed.Declaration_constant (e, i, (env1, env2)) ->
-        let%bind e = s_named_expression ~v ~expr e in
-        let%bind env1 = s_full_environment ~v ~expr env1 in
-        let%bind env2 = s_full_environment ~v ~expr env2 in
-        ok @@ Ast_typed.Declaration_constant (e, i, (env1, env2))
+        Ast_typed.Declaration_constant (e, inline, (env1, env2)) ->
+        let%bind e = s_named_expression ~substs e in
+        let%bind env1 = s_full_environment ~substs env1 in
+        let%bind env2 = s_full_environment ~substs env2 in
+        ok @@ Ast_typed.Declaration_constant (e, inline, (env1, env2))
 
-    and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d ->
-      Trace.bind_map_location (s_declaration ~v ~expr) d
+    and s_declaration_wrap : T.declaration Location.wrap w = fun ~substs d ->
+      Trace.bind_map_location (s_declaration ~substs) d
 
     (* Replace the type variable ~v with ~expr everywhere within the
        program ~p. TODO: issues with scoping/shadowing. *)
-    and program ~(p : Ast_typed.program) ~(v:type_variable) ~expr : Ast_typed.program Trace.result =
-      Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
+    and s_program : Ast_typed.program w = fun ~substs p ->
+      Trace.bind_map_list (s_declaration_wrap ~substs) p
 
     (*
        Computes `P[v := expr]`.
     *)
-    and type_value ~tv ~v ~expr =
-      let self tv = type_value ~tv ~v ~expr in
+    and type_value ~tv ~substs =
+      let self tv = type_value ~tv ~substs in
+      let (v, expr) = substs in
       match tv with
-      | P_variable v' when v' = v -> expr
+      | P_variable v' when Var.equal v' v -> expr
       | P_variable _ -> tv
       | P_constant (x , lst) -> (
           let lst' = List.map self lst in
@@ -280,7 +283,7 @@ module Substitution = struct
           P_apply ab'
         )
       | P_forall p -> (
-          let aux c = constraint_ ~c ~v ~expr in
+          let aux c = constraint_ ~c ~substs in
           let constraints = List.map aux p.constraints in
           if (p.binder = v) then (
             P_forall { p with constraints }
@@ -290,31 +293,33 @@ module Substitution = struct
           )
         )
 
-    and constraint_ ~c ~v ~expr =
+    and constraint_ ~c ~substs =
       match c with
       | C_equation ab -> (
-          let ab' = pair_map (fun tv -> type_value ~tv ~v ~expr) ab in
+          let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in
           C_equation ab'
         )
       | C_typeclass (tvs , tc) -> (
-          let tvs' = List.map (fun tv -> type_value ~tv ~v ~expr) tvs in
-          let tc' = typeclass ~tc ~v ~expr in
+          let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in
+          let tc' = typeclass ~tc ~substs in
           C_typeclass (tvs' , tc')
         )
       | C_access_label (tv , l , v') -> (
-          let tv' = type_value ~tv ~v ~expr in
+          let tv' = type_value ~tv ~substs in
           C_access_label (tv' , l , v')
         )
 
-    and typeclass ~tc ~v ~expr =
-      List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc
+    and typeclass ~tc ~substs =
+      List.map (List.map (fun tv -> type_value ~tv ~substs)) tc
+
+    let program = s_program
 
     (* Performs beta-reduction at the root of the type *)
     let eval_beta_root ~(tv : type_value) =
       match tv with
         P_apply (P_forall { binder; constraints; body }, arg) ->
-        let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in
-        (type_value ~tv:body ~v:binder ~expr:arg , constraints)
+        let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in
+        (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:arg) , constraints)
       | _ -> (tv , [])
   end
 
diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml
index b3a5c5b18..b34ef7554 100644
--- a/src/test/typer_tests.ml
+++ b/src/test/typer_tests.ml
@@ -12,7 +12,7 @@ let int () : unit result =
   let open Typer in
   let e = Environment.full_empty in
   let state = Typer.Solver.initial_state in
-  let%bind (post , new_state) = type_expression e state pre in
+  let%bind (post , new_state) = type_expression_subst e state pre in
   let () = Typer.Solver.discard_state new_state in
   let open! Typed in
   let open Combinators in
@@ -27,7 +27,7 @@ module TestExpressions = struct
     let pre = expr in
     let open Typer in
     let open! Typed in
-    let%bind (post , new_state) = type_expression env state pre in
+    let%bind (post , new_state) = type_expression_subst env state pre in
     let () = Typer.Solver.discard_state new_state in
     let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
     ok ()
@@ -37,7 +37,7 @@ module TestExpressions = struct
   module E = O
 
   let unit   () : unit result = test_expression I.(e_unit ())    O.(t_unit ())
-  let int    () : unit result = test_expression I.(e_int 32)  O.(t_int ())
+  let int    () : unit result = test_expression I.(e_int 32)     O.(t_int ())
   let bool   () : unit result = test_expression I.(e_bool true)  O.(t_bool ())
   let string () : unit result = test_expression I.(e_string "s") O.(t_string ())
   let bytes  () : unit result =
diff --git a/vendors/UnionFind/Partition0.ml b/vendors/UnionFind/Partition0.ml
index cd8b26ffc..33616080b 100644
--- a/vendors/UnionFind/Partition0.ml
+++ b/vendors/UnionFind/Partition0.ml
@@ -38,12 +38,10 @@ module Make (Item: Partition.Item) =
 
    (* Printing *)
 
-    let print (p: partition) =
-      let buffer = Buffer.create 80 in
+    let print ppf p =
       let print src dst =
-        let link =
-          Printf.sprintf "%s -> %s\n"
-                         (Item.to_string src) (Item.to_string dst)
-        in Buffer.add_string buffer link
-      in (ItemMap.iter print p; buffer)
+        Format.fprintf ppf "%s -> %s (%s)\n"
+          (Item.to_string src) (Item.to_string dst) (Item.to_string (repr src p))
+      in ItemMap.iter print p
+
   end