diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml
index b76e55500..c5199f60d 100644
--- a/src/passes/8-typer-new/PP.ml
+++ b/src/passes/8-typer-new/PP.ml
@@ -2,7 +2,7 @@ open Ast_typed
 open Format
 module UF = UnionFind.Poly2
 
-let type_constraint_ : _ -> type_constraint_simpl_ -> unit = fun ppf ->
+let type_constraint_ : _ -> type_constraint_simpl -> unit = fun ppf ->
   function
   |SC_Constructor { tv; c_tag; tv_list=_ } ->
     let ct = match c_tag with
@@ -34,8 +34,8 @@ let type_constraint_ : _ -> type_constraint_simpl_ -> unit = fun ppf ->
   |SC_Poly        _ -> fprintf ppf "Poly"
   |SC_Typeclass   _ -> fprintf ppf "TC"
 
-let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf { reason_simpl ; c_simpl } ->
-  fprintf ppf "%a (reason: %s)" type_constraint_ c_simpl reason_simpl
+let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf c ->
+  fprintf ppf "%a (reason: %s)" type_constraint_ c (reason_simpl c)
 
 let all_constraints ppf ac =
   fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml
index 02ee01b7e..33fe71c80 100644
--- a/src/passes/8-typer-new/solver.ml
+++ b/src/passes/8-typer-new/solver.ml
@@ -159,7 +159,7 @@ 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 dbs = match new_constraint.c_simpl with
+  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 = []}
@@ -173,7 +173,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
     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.c_simpl with
+    match new_constraint with
     | SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) ->
       let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in
       let dbs = {dbs with assignments} in
@@ -191,7 +191,7 @@ let type_level_eval : type_value -> type_value * type_constraint list =
     <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." *)
+      { tsrc = _ ; t = P_apply _ } -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
     | _ -> ()
   in x
 
@@ -210,16 +210,16 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
   fun dbs new_constraint ->
   let insert_fresh a b =
     let fresh = Core.fresh_type_variable () in
-    let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a "normalizer: simpl") in
-    let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b "normalizer: simpl") in
+    let (dbs , cs1) = normalizer_simpl dbs (c_equation { tsrc = "solver: normalizer: simpl 1" ; t = P_variable fresh } a "normalizer: simpl 1") in
+    let (dbs , cs2) = normalizer_simpl dbs (c_equation { tsrc = "solver: normalizer: simpl 2" ; t = P_variable fresh } b "normalizer: simpl 2") in
     (dbs , cs1 @ cs2) in
   let split_constant a c_tag args =
     let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
-    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_constant") (List.combine fresh_vars args) in
+    let fresh_eqns = List.map (fun (v,t) -> c_equation { tsrc = "solver: normalizer: split_constant" ; t = P_variable v } t "normalizer: split_constant") (List.combine fresh_vars args) in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs , [{c_simpl=SC_Constructor {tv=a;c_tag;tv_list=fresh_vars};reason_simpl="normalizer: split constant"}] @ List.flatten recur) in
-  let gather_forall a forall = (dbs , [{c_simpl=SC_Poly { tv=a; forall };reason_simpl="normalizer: gather_forall"}]) in
-  let gather_alias a b = (dbs , [{c_simpl=SC_Alias { a ; b };reason_simpl="normalizer: gather_alias"}]) in
+    (dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars;reason_constr_simpl=Format.asprintf "normalizer: split constant %a = %a (%a)" Var.pp a Ast_typed.PP_generic.constant_tag c_tag (PP_helpers.list_sep Ast_typed.PP_generic.type_value (fun ppf () -> Format.fprintf ppf ", ")) args}] @ List.flatten recur) in
+  let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall ; reason_poly_simpl="normalizer: gather_forall"}]) in
+  let gather_alias a b = (dbs , [SC_Alias { a ; b ; reason_alias_simpl="normalizer: gather_alias"}]) in
   let reduce_type_app a b =
     let (reduced, new_constraints) = check_applied @@ type_level_eval b in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in
@@ -227,27 +227,27 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
     (dbs , resimpl @ List.flatten recur) in
   let split_typeclass args tc =
     let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
-    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_typeclass") (List.combine fresh_vars args) in
+    let fresh_eqns = List.map (fun (v,t) -> c_equation { tsrc = "solver: normalizer: split typeclass" ; t = P_variable v} t "normalizer: split_typeclass") (List.combine fresh_vars args) in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs, [{c_simpl=SC_Typeclass { tc ; args = fresh_vars };reason_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
+    (dbs, [SC_Typeclass { tc ; args = fresh_vars ; reason_typeclass_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
 
   match new_constraint.c with
   (* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *)
-  | C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)}     -> insert_fresh a b
+  | C_equation {aval=({ tsrc = _ ; t = P_forall _ } as a); bval=({ tsrc = _ ; t = P_forall _ } as b)}     -> insert_fresh a b
   (* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *)
-  | C_equation {aval=(P_forall _ as a); bval=(P_constant _ as b)}   -> insert_fresh a b
+  | C_equation {aval=({ tsrc = _ ; t = P_forall _ } as a); bval=({ tsrc = _ ; t = P_constant _ } as b)}   -> insert_fresh a b
   (* break down (c(args) = c'(args')) into ('a = c(args) and 'a = c'(args')) *)
-  | C_equation {aval=(P_constant _ as a); bval=(P_constant _ as b)} -> insert_fresh a b
+  | C_equation {aval=({ tsrc = _ ; t = P_constant _ } as a); bval=({ tsrc = _ ; t = P_constant _ } as b)} -> insert_fresh a b
   (* break down (c(args) = forall 'b, body) into ('a = c(args) and 'a = forall 'b, body) *)
-  | C_equation {aval=(P_constant _ as a); bval=(P_forall _ as b)}   -> insert_fresh a b
-  | C_equation {aval=(P_forall forall); bval=(P_variable b)}        -> gather_forall b forall
-  | C_equation {aval=P_variable a; bval=P_forall forall}            -> gather_forall a forall
-  | C_equation {aval=P_variable a; bval=P_variable b}               -> gather_alias a b
-  | C_equation {aval=P_variable a; bval=P_constant { p_ctor_tag; p_ctor_args }} -> split_constant a p_ctor_tag p_ctor_args
-  | C_equation {aval=P_constant {p_ctor_tag; p_ctor_args}; bval=P_variable b}   -> split_constant b p_ctor_tag p_ctor_args
+  | C_equation {aval=({ tsrc = _ ; t = P_constant _ } as a); bval=({ tsrc = _ ; t = P_forall _ } as b)}   -> insert_fresh a b
+  | C_equation {aval={ tsrc = _ ; t = P_forall forall }; bval={ tsrc = _ ; t = P_variable b }}        -> gather_forall b forall
+  | C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_forall forall }}            -> gather_forall a forall
+  | C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_variable b }}               -> gather_alias a b
+  | C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_constant { p_ctor_tag; p_ctor_args } }} -> split_constant a p_ctor_tag p_ctor_args
+  | C_equation {aval={ tsrc = _ ; t = P_constant {p_ctor_tag; p_ctor_args} }; bval={ tsrc = _ ; t = P_variable b }}   -> split_constant b p_ctor_tag p_ctor_args
   (*  Reduce the type-level application, and simplify the resulting constraint + the extra constraints (typeclasses) that appeared at the forall binding site *)
-  | C_equation {aval=(_ as a); bval=(P_apply _ as b)}               -> reduce_type_app a b
-  | C_equation {aval=(P_apply _ as a); bval=(_ as b)}               -> reduce_type_app b a
+  | C_equation {aval=(_ as a); bval=({ tsrc = _ ; t = P_apply _ } as b)}               -> reduce_type_app a b
+  | C_equation {aval=({ tsrc = _ ; t = P_apply _ } as a); bval=(_ as b)}               -> reduce_type_app b a
   (* break down (TC(args)) into (TC('a, …) and ('a = arg) …) *)
   | C_typeclass { tc_args; typeclass }                              -> split_typeclass tc_args typeclass
   | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO" (* tv, label, result *)
@@ -323,9 +323,9 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con
  * For now: break pair(a, b) = pair(c, d) into a = c, b = d *)
 
 let selector_break_ctor :  (type_constraint_simpl, output_break_ctor) selector =
-  (* find two rules with the shape a = k(var …) and a = k'(var' …) *)
+  (* find two rules with the shape x = k(var …) and x = k'(var' …) *)
   fun type_constraint_simpl dbs ->
-  match type_constraint_simpl.c_simpl with
+  match type_constraint_simpl with
     SC_Constructor c ->
     (* finding other constraints related to the same type variable and
        with the same sort of constraint (constructor vs. constructor)
@@ -470,10 +470,14 @@ let propagator_break_ctor : output_break_ctor propagator =
   let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
   let a = selected.a_k_var in
   let b = selected.a_k'_var' in
+
+  (* The selector is expected to provice two constraints with the shape x = k(var …) and x = k'(var' …) *)
+  assert (Var.equal (a : c_constructor_simpl).tv (b : c_constructor_simpl).tv);
+
   (* produce constraints: *)
 
   (* a.tv = b.tv *)
-  let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) "propagator: break_ctor" in
+  let eq1 = c_equation { tsrc = "solver: propagator: break_ctor a" ; t = P_variable a.tv} { tsrc = "solver: propagator: break_ctor b" ; t = P_variable b.tv} "propagator: break_ctor" in
   (* a.c_tag = b.c_tag *)
   if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then
     failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag))
@@ -482,7 +486,7 @@ let propagator_break_ctor : output_break_ctor propagator =
   if List.length a.tv_list <> List.length b.tv_list then
     failwith "type error: incompatible types, not same length"
   else
-    let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb) "propagator: break_ctor") a.tv_list b.tv_list in
+    let eqs3 = List.map2 (fun aa bb -> c_equation { tsrc = "solver: propagator: break_ctor aa" ; t = P_variable aa} { tsrc = "solver: propagator: break_ctor bb" ; t = P_variable bb} "propagator: break_ctor") a.tv_list b.tv_list in
     let eqs = eq1 :: eqs3 in
     (eqs , []) (* no new assignments *)
 
@@ -507,7 +511,12 @@ let compare_label (a:label) (b:label) =
   let Label b = b in
   String.compare a b
 let rec compare_typeclass a b = compare_list (compare_list compare_type_expression) a b
-and compare_type_expression = function
+and compare_type_expression { tsrc = _ ; t = ta } { tsrc = _ ; t = tb } =
+  (* Note: this comparison ignores the tsrc, the idea is that types
+     will often be compared to see if they are the same, regardless of
+     where the type comes from .*)
+  compare_type_expression_ ta tb
+and compare_type_expression_ = function
   | P_forall { binder=a1; constraints=a2; body=a3 } -> (function
       | P_forall { binder=b1; constraints=b2; body=b3 } ->
         compare_type_variable a1 b1 <? fun () ->
@@ -559,7 +568,9 @@ let compare_p_forall
 let compare_c_poly_simpl { tv = a1; forall = a2 } { tv = b1; forall = b2 } =
   compare_type_variable a1 b1 <? fun () ->
     compare_p_forall a2 b2
-let compare_c_constructor_simpl { tv=a1; c_tag=a2; tv_list=a3 } { tv=b1; c_tag=b2; tv_list=b3 } =
+let compare_c_constructor_simpl { reason_constr_simpl = _ ; tv=a1; c_tag=a2; tv_list=a3 } { reason_constr_simpl = _ ; tv=b1; c_tag=b2; tv_list=b3 } =
+  (* We do not compare the reasons, as they are only for debugging and
+     not part of the type *)
   compare_type_variable a1 b1 <? fun () -> compare_simple_c_constant a2 b2  <? fun () -> compare_list compare_type_variable a3 b3
 
 let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var = b2 } =
@@ -570,21 +581,21 @@ let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_va
   compare_c_constructor_simpl a1 b1 <? fun () -> compare_c_constructor_simpl a2 b2
 
 let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector =
-  (* find two rules with the shape (a = forall b, d) and a = k'(var' …) or vice versa *)
+  (* find two rules with the shape (x = forall b, d) and x = k'(var' …) or vice versa *)
   (* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *)
   (* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *)
   fun type_constraint_simpl dbs ->
-  match type_constraint_simpl.c_simpl with
+  match type_constraint_simpl with
     SC_Constructor c                ->
     (* vice versa *)
     let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in
-    let other_cs = List.filter (fun (x : c_poly_simpl) -> c.tv = x.tv) other_cs in (* TODO: does equality work in OCaml? *)
+    let other_cs = List.filter (fun (x : c_poly_simpl) -> Var.equal c.tv x.tv) other_cs in
     let cs_pairs = List.map (fun x -> { poly = x ; a_k_var = c }) other_cs in
     WasSelected cs_pairs
   | SC_Alias       _                -> WasNotSelected (* TODO: ??? *)
   | SC_Poly        p                ->
     let other_cs = (UnionFindWrapper.get_constraints_related_to p.tv dbs).constructor in
-    let other_cs = List.filter (fun (x : c_constructor_simpl) -> x.tv = p.tv) other_cs in (* TODO: does equality work in OCaml? *)
+    let other_cs = List.filter (fun (x : c_constructor_simpl) -> Var.equal x.tv p.tv) other_cs in
     let cs_pairs = List.map (fun x -> { poly = p ; a_k_var = x }) other_cs in
     WasSelected cs_pairs
   | SC_Typeclass   _                -> WasNotSelected
@@ -594,37 +605,37 @@ let propagator_specialize1 : output_specialize1 propagator =
   let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
   let a = selected.poly in
   let b = selected.a_k_var in
-  let () = if (a.tv <> b.tv) then failwith "internal error" else () in
+
+  (* The selector is expected to provice two constraints with the shape (x = forall y, z) and x = k'(var' …) *)
+  assert (Var.equal (a : c_poly_simpl).tv (b : c_constructor_simpl).tv);
 
   (* produce constraints: *)
 
-  (* create a fresh existential variable to instantiate the polymorphic type b *)
+  (* create a fresh existential variable to instantiate the polymorphic type y *)
   let fresh_existential = Core.fresh_type_variable () in
   (* Produce the constraint (b.tv = a.body[a.binder |-> fresh_existential])
      The substitution is obtained by immediately applying the forall. *)
-  let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in
+  let apply = { tsrc = "solver: propagator: specialize1 apply" ; t = P_apply {tf = { tsrc = "solver: propagator: specialize1 tf" ; t = P_forall a.forall }; targ = { tsrc = "solver: propagator: specialize1 targ" ; t = P_variable fresh_existential }} } in
   let (reduced, new_constraints) = check_applied @@ type_level_eval apply in
-  let eq1 = c_equation (P_variable b.tv) reduced "propagator: specialize1" in
+  let eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in
   let eqs = eq1 :: new_constraints in
   (eqs, []) (* no new assignments *)
 
-  let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
-    let mem elt set = match RedBlackTrees.PolySet.find_opt elt set with None -> false | Some _ -> true in
-    fun selector propagator ->
-    fun already_selected old_type_constraint dbs ->
-      (* TODO: thread some state to know which selector outputs were already seen *)
-      match selector old_type_constraint dbs with
-        WasSelected selected_outputs ->
-        (* TODO: fold instead. *)
-        let (already_selected , selected_outputs) = List.fold_left (fun (already_selected, selected_outputs) elt -> if mem elt already_selected then (RedBlackTrees.PolySet.add elt already_selected , elt :: selected_outputs)
-  else (already_selected , selected_outputs)) (already_selected , selected_outputs) selected_outputs in
-        (* Call the propagation rule *)
-        let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in
-        let (new_constraints , new_assignments) = List.split new_contraints_and_assignments in
-        (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
-        (already_selected , List.flatten new_constraints , List.flatten new_assignments)
-      | WasNotSelected ->
-        (already_selected, [] , [])
+let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
+  fun selector propagator ->
+  fun already_selected old_type_constraint dbs ->
+  (* TODO: thread some state to know which selector outputs were already seen *)
+  match selector old_type_constraint dbs with
+    WasSelected selected_outputs ->
+     let open RedBlackTrees.PolySet in
+     let { set = already_selected ; duplicates = _ ; added = selected_outputs } = add_list selected_outputs already_selected in
+     (* Call the propagation rule *)
+     let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in
+     let (new_constraints , new_assignments) = List.split new_contraints_and_assignments in
+     (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
+     (already_selected , List.flatten new_constraints , List.flatten new_assignments)
+  | WasNotSelected ->
+     (already_selected, [] , [])
 
 let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
 let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1
diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml
index 13a7def62..89f1183aa 100644
--- a/src/passes/8-typer-new/typer.ml
+++ b/src/passes/8-typer-new/typer.ml
@@ -420,8 +420,7 @@ and type_lambda e state {
       let e' = Environment.add_ez_binder (binder) fresh e in
 
       let%bind (result , state') = type_expression e' state result in
-      let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
-      let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
+      let wrapped = Solver.Wrap.lambda fresh input_type' output_type' result.type_expression in
       ok (({binder;result}:O.lambda),state',wrapped)
 
 and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
diff --git a/src/passes/8-typer-new/wrap.ml b/src/passes/8-typer-new/wrap.ml
index d14397b51..5c0302887 100644
--- a/src/passes/8-typer-new/wrap.ml
+++ b/src/passes/8-typer-new/wrap.ml
@@ -44,7 +44,7 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
   | T_arrow {type1;type2} ->
      p_constant C_arrow (List.map type_expression_to_type_value [ type1 ; type2 ])
 
-  | T_variable (type_name) -> P_variable type_name
+  | T_variable (type_name) -> { tsrc = "wrap: from source code maybe?" ; t = P_variable type_name }
   | T_constant (type_name) ->
      let csttag = T.(match type_name with
                         | TC_unit      -> C_unit
@@ -89,7 +89,7 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
      p_constant C_record (List.map type_expression_to_type_value_copypasted tlist)
   | T_arrow {type1;type2} ->
      p_constant C_arrow (List.map type_expression_to_type_value_copypasted [ type1 ; type2 ])
-  | T_variable type_name -> P_variable (type_name) (* eird stuff*)
+  | T_variable type_name -> { tsrc = "wrap: from source code maybe?" ; t = P_variable type_name }
   | T_constant (type_name) ->
      let csttag = T.(match type_name with
                         | TC_unit   -> C_unit
@@ -121,12 +121,12 @@ let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
 let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr ->
   let pattern = type_expression_to_type_value expr in
   let type_name = Core.fresh_type_variable () in
-  [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: variable" }] , type_name
+  [{ c = C_equation { aval = { tsrc = "wrap: variable: whole" ; t = P_variable type_name } ; bval = pattern } ; reason = "wrap: variable" }] , type_name
 
 let literal : T.type_expression -> (constraints * T.type_variable) = fun t ->
   let pattern = type_expression_to_type_value t in
   let type_name = Core.fresh_type_variable () in
-  [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: literal" }] , type_name
+  [{ c = C_equation { aval = { tsrc = "wrap: literal: whole" ; t = P_variable type_name } ; bval = pattern } ; reason = "wrap: literal" }] , type_name
 
 (*
   let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@@ -144,7 +144,7 @@ let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys
   let patterns = List.map type_expression_to_type_value tys in
   let pattern = p_constant C_record patterns in
   let type_name = Core.fresh_type_variable () in
-  [{ c = C_equation { aval = P_variable type_name ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
+  [{ c = C_equation { aval = { tsrc = "wrap: tuple: whole" ; t = P_variable type_name } ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
 
 (* let t_tuple         = ('label:int, 'v) … -> record ('label : 'v) … *)
 (* let t_constructor   = ('label:string, 'v) -> variant ('label : 'v) *)
@@ -184,25 +184,25 @@ let constructor
   let sum = type_expression_to_type_value sum in
   let whole_expr = Core.fresh_type_variable () in
   [
-    c_equation (P_variable whole_expr) sum "wrap: constructor: whole" ;
+    c_equation { tsrc = "wrap: constructor: whole" ; t = P_variable whole_expr } sum "wrap: constructor: whole" ;
     c_equation t_arg c_arg "wrap: construcotr: arg" ;
   ] , whole_expr
 
 let record : T.field_content T.label_map -> (constraints * T.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 "wrap: record: whole"] , whole_expr
+  [c_equation { tsrc = "wrap: record: whole" ; t = P_variable whole_expr } record_type "wrap: record: whole"] , whole_expr
 
 let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
   fun ctor element_tys ->
-  let elttype = T.P_variable (Core.fresh_type_variable ()) in
+  let elttype = T.{ tsrc = "wrap: collection: p_variable" ; t = P_variable (Core.fresh_type_variable ()) } in
   let aux elt =
     let elt' = type_expression_to_type_value elt
     in c_equation elttype elt' "wrap: collection: elt" in
   let equations = List.map aux element_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation (P_variable whole_expr) (p_constant ctor [elttype]) "wrap: collection: whole" ;
+      c_equation { tsrc = "wrap: collection: whole" ; t = P_variable whole_expr} (p_constant ctor [elttype]) "wrap: collection: whole" ;
   ] @ equations , whole_expr
 
 let list = collection T.C_list
@@ -210,8 +210,8 @@ let set  = collection T.C_set
 
 let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
   fun kv_tys ->
-  let k_type = T.P_variable (Core.fresh_type_variable ()) in
-  let v_type = T.P_variable (Core.fresh_type_variable ()) in
+  let k_type = T.{ tsrc = "wrap: map: k" ; t = P_variable (Core.fresh_type_variable ()) } in
+  let v_type = T.{ tsrc = "wrap: map: v" ; t = P_variable (Core.fresh_type_variable ()) } in
   let aux_k (k , _v) =
     let k' = type_expression_to_type_value k in
     c_equation k_type k' "wrap: map: key" in
@@ -222,13 +222,13 @@ let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_
   let equations_v = List.map aux_v kv_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
+      c_equation ({ tsrc = "wrap: map: whole" ; t = P_variable whole_expr }) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
   ] @ equations_k @ equations_v , whole_expr
 
 let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
   fun kv_tys ->
-  let k_type = T.P_variable (Core.fresh_type_variable ()) in
-  let v_type = T.P_variable (Core.fresh_type_variable ()) in
+  let k_type = T.{ tsrc = "wrap: big_map: k" ; t = P_variable (Core.fresh_type_variable ()) } in
+  let v_type = T.{ tsrc = "wrap: big_map: v" ; t = P_variable (Core.fresh_type_variable ()) } in
   let aux_k (k , _v) =
     let k' = type_expression_to_type_value k in
     c_equation k_type k' "wrap: big_map: key" in
@@ -241,7 +241,7 @@ let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.t
   [
       (* 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) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
+      c_equation ({ tsrc = "wrap: big_map: whole" ; t = P_variable whole_expr}) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
   ] @ equations_k @ equations_v , whole_expr
 
 let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -250,7 +250,7 @@ let application : T.type_expression -> T.type_expression -> (constraints * T.typ
   let f'   = type_expression_to_type_value f in
   let arg' = type_expression_to_type_value arg in
   [
-      c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) "wrap: application: f" ;
+      c_equation f' (p_constant C_arrow [arg' ; { tsrc = "wrap: application: whole" ; t = P_variable whole_expr }]) "wrap: application: f" ;
   ] , whole_expr
 
 let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -258,10 +258,10 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va
   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
+  let v = T.{ tsrc = "wrap: look_up: ds" ; t = P_variable (Core.fresh_type_variable ()) } in
   [
-      c_equation ds' (p_constant C_map [ind' ; P_variable v]) "wrap: look_up: map" ;
-      c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) "wrap: look_up: whole" ;
+      c_equation ds' (p_constant C_map [ind' ; v]) "wrap: look_up: map" ;
+      c_equation ({ tsrc = "wrap: look_up: whole" ; t = P_variable whole_expr }) (p_constant C_option [v]) "wrap: look_up: whole" ;
   ] , whole_expr
 
 let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -271,7 +271,7 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v
   let whole_expr = Core.fresh_type_variable () in
   [
       c_equation a' (p_constant C_unit []) "wrap: sequence: first" ;
-      c_equation b' (P_variable whole_expr) "wrap: sequence: second (whole)" ;
+      c_equation b' ({ tsrc = "wrap: sequence: whole" ; t = P_variable whole_expr}) "wrap: sequence: second (whole)" ;
   ] , whole_expr
 
 let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -280,9 +280,9 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
   let body' = type_expression_to_type_value body in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation expr'                   (P_variable Stage_common.Constant.t_bool) "wrap: loop: expr" ;
+      c_equation expr'                   ({ tsrc = "built-in type" ; t = P_variable Stage_common.Constant.t_bool }) "wrap: loop: expr" ;
       c_equation body'                   (p_constant C_unit []) "wrap: loop: body" ;
-      c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: loop: whole (unit)" ;
+      c_equation (p_constant C_unit [])  ({ tsrc = "wrap: loop: whole" ; t = P_variable whole_expr}) "wrap: loop: whole (unit)" ;
   ] , whole_expr
 
 let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) =
@@ -294,7 +294,7 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression
     | Some annot -> [c_equation rhs' (type_expression_to_type_value annot) "wrap: let_in: rhs"] in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation result' (P_variable whole_expr) "wrap: let_in: result (whole)" ;
+      c_equation result' { tsrc = "wrap: let_in: whole" ; t = P_variable whole_expr } "wrap: let_in: result (whole)" ;
   ] @ rhs_tv_opt', whole_expr
 
 let recursive : T.type_expression -> (constraints * T.type_variable) =
@@ -302,7 +302,7 @@ let recursive : T.type_expression -> (constraints * T.type_variable) =
   let fun_type = type_expression_to_type_value fun_type in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation fun_type (P_variable whole_expr) "wrap: recursive: fun_type (whole)" ;
+      c_equation fun_type ({ tsrc = "wrap: recursive: whole" ; t = P_variable whole_expr }) "wrap: recursive: fun_type (whole)" ;
   ], whole_expr
 
 let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -312,7 +312,7 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var
   let whole_expr = Core.fresh_type_variable () in
   [
       c_equation v'  e' "wrap: assign: var type must eq rhs type" ;
-      c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: assign: unit (whole)" ;
+      c_equation { tsrc = "wrap: assign: whole" ; t = P_variable whole_expr } (p_constant C_unit []) "wrap: assign: unit (whole)" ;
   ] , whole_expr
 
 let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -322,14 +322,14 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type
   let whole_expr = Core.fresh_type_variable () in
   [
       c_equation e' annot' "wrap: annotation: expr type must eq annot" ;
-      c_equation e' (P_variable whole_expr) "wrap: annotation: whole" ;
+      c_equation e' { tsrc = "wrap: annotation: whole" ; t = P_variable whole_expr } "wrap: annotation: whole" ;
   ] , whole_expr
 
 let matching : T.type_expression list -> (constraints * T.type_variable) =
   fun es ->
   let whole_expr = Core.fresh_type_variable () in
   let type_expressions = (List.map type_expression_to_type_value es) in
-  let cs = List.map (fun e -> c_equation (P_variable whole_expr) e "wrap: matching: case (whole)") type_expressions
+  let cs = List.map (fun e -> c_equation { tsrc = "wrap: matching: case" ; t = P_variable whole_expr } e "wrap: matching: case (whole)") type_expressions
   in cs, whole_expr
 
 let fresh_binder () =
@@ -339,24 +339,26 @@ let lambda
     : T.type_expression ->
       T.type_expression option ->
       T.type_expression option ->
+      T.type_expression ->
       (constraints * T.type_variable) =
-  fun fresh arg body ->
+  fun fresh arg output result ->
   let whole_expr = Core.fresh_type_variable () in
-  let unification_arg = Core.fresh_type_variable () in
-  let unification_body = Core.fresh_type_variable () in
+  let unification_arg = T.{ tsrc = "wrap: lambda: arg" ; t = P_variable (Core.fresh_type_variable ()) } in
+  let unification_output = T.{ tsrc = "wrap: lambda: whole" ; t = P_variable (Core.fresh_type_variable ()) } in
+  let result' = type_expression_to_type_value result in
   let arg'  = match arg with
       None -> []
-    | Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
-  let body'  = match body with
+    | Some arg -> [c_equation unification_arg (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
+  let output'  = match output with
       None -> []
-    | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body) "wrap: lambda: body annot"]
+    | Some output -> [c_equation unification_output (type_expression_to_type_value output) "wrap: lambda: output annot"]
   in [
-      c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) "wrap: lambda: arg" ;
-      c_equation (P_variable whole_expr)
-                 (p_constant C_arrow ([P_variable unification_arg ;
-                                       P_variable unification_body]))
+      c_equation unification_output result' "wrap: lambda: result" ;
+      c_equation (type_expression_to_type_value fresh) unification_arg "wrap: lambda: arg" ;
+      c_equation ({ tsrc = "wrap: lambda: whole" ; t = P_variable whole_expr })
+                 (p_constant C_arrow ([unification_arg ; unification_output]))
                  "wrap: lambda: arrow (whole)"
-     ] @ arg' @ body' , whole_expr
+     ] @ arg' @ output' , whole_expr
 
 (* This is pretty much a wrapper for an n-ary function. *)
 let constant : O.type_value -> T.type_expression list -> (constraints * T.type_variable) =
@@ -365,5 +367,5 @@ let constant : O.type_value -> T.type_expression list -> (constraints * T.type_v
   let args'      = List.map type_expression_to_type_value args in
   let args_tuple = p_constant C_record args' in
   [
-      c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) "wrap: constant: as declared for built-in"
+      c_equation f (p_constant C_arrow ([args_tuple ; { tsrc = "wrap: lambda: whole" ; t = P_variable whole_expr }])) "wrap: constant: as declared for built-in"
   ] , whole_expr
diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml
index ce870c27c..dc63d5573 100644
--- a/src/passes/operators/operators.ml
+++ b/src/passes/operators/operators.ml
@@ -434,17 +434,17 @@ module Typer = struct
   module Operators_types = struct
     open Typesystem.Shorthands
 
-    let tc_subarg   a b c = tc [a;b;c] [ (*TODO…*) ]
-    let tc_sizearg  a     = tc [a]     [ [int] ]
-    let tc_packable a     = tc [a]     [ [int] ; [string] ; [bool] (*TODO…*) ]
-    let tc_timargs  a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
-    let tc_edivargs a b c = tc [a;b;c] [ (*TODO…*) ]
-    let tc_divargs  a b c = tc [a;b;c] [ (*TODO…*) ]
-    let tc_modargs  a b c = tc [a;b;c] [ (*TODO…*) ]
-    let tc_addargs  a b c = tc [a;b;c] [ (*TODO…*) ]
-    let tc_comparable a   = tc [a]     [ [nat] ; [int] ; [mutez] ; [timestamp] ]
-    let tc_concatable a   = tc [a]     [ [string] ; [bytes] ]
-    let tc_storable a     = tc [a]     [ [string] ; [bytes] ; (*Humm .. TODO ?*) ]
+    let tc_subarg   a b c = tc "arguments for (-)"        [a;b;c] [ (*TODO…*) ]
+    let tc_sizearg  a     = tc "arguments for size"       [a]     [ [int] ]
+    let tc_packable a     = tc "packable"                 [a]     [ [int] ; [string] ; [bool] (*TODO…*) ]
+    let tc_timargs  a b c = tc "arguments for ( * )"      [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
+    let tc_edivargs a b c = tc "arguments for ediv"       [a;b;c] [ (*TODO…*) ]
+    let tc_divargs  a b c = tc "arguments for div"        [a;b;c] [ (*TODO…*) ]
+    let tc_modargs  a b c = tc "arguments for mod"        [a;b;c] [ (*TODO…*) ]
+    let tc_addargs  a b c = tc "arguments for (+)"        [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
+    let tc_comparable a   = tc "comparable"               [a]     [ [nat] ; [int] ; [mutez] ; [timestamp] ]
+    let tc_concatable a   = tc "concatenable"             [a]     [ [string] ; [bytes] ]
+    let tc_storable a     = tc "storable"                 [a]     [ [string] ; [bytes] ; (*Humm .. TODO ?*) ]
 
     let t_none         = forall "a" @@ fun a -> option a
 
diff --git a/src/stages/4-ast_typed/ast.ml b/src/stages/4-ast_typed/ast.ml
index 8a846aa61..99b532754 100644
--- a/src/stages/4-ast_typed/ast.ml
+++ b/src/stages/4-ast_typed/ast.ml
@@ -463,11 +463,15 @@ type constant_tag =
   | C_chain_id  (* * *)
 
 (* TODO: rename to type_expression or something similar (it includes variables, and unevaluated functions + applications *)
-type type_value =
+type type_value_ =
   | P_forall       of p_forall
   | P_variable     of type_variable
   | P_constant     of p_constant
   | P_apply        of p_apply
+and type_value = {
+  tsrc : string;
+  t : type_value_ ;
+}
 
 and p_apply = {
     tf : type_value ;
@@ -556,6 +560,7 @@ and constraints = {
 }
 and type_variable_list = type_variable list
 and c_constructor_simpl = {
+  reason_constr_simpl : string ;
   tv : type_variable;
   c_tag : constant_tag;
   tv_list : type_variable_list;
@@ -569,24 +574,23 @@ and c_equation_e = {
     bex : type_expression ;
   }
 and c_typeclass_simpl = {
+  reason_typeclass_simpl : string ;
   tc   : typeclass          ;
   args : type_variable_list ;
 }
 and c_poly_simpl = {
+  reason_poly_simpl : string ;
   tv     : type_variable ;
   forall : p_forall      ;
 }
-and type_constraint_simpl = {
-    reason_simpl : string ;
-    c_simpl : type_constraint_simpl_ ;
-  }
-and type_constraint_simpl_ =
+and type_constraint_simpl =
   | SC_Constructor of c_constructor_simpl             (* α = ctor(β, …) *)
   | SC_Alias       of c_alias                         (* α = β *)
   | SC_Poly        of c_poly_simpl                    (* α = forall β, δ where δ can be a more complex type *)
   | SC_Typeclass   of c_typeclass_simpl               (* TC(α, …) *)
 
 and c_alias = {
+    reason_alias_simpl : string ;
     a : type_variable ;
     b : type_variable ;
   }
diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml
index 7528dab2e..537a734f3 100644
--- a/src/stages/4-ast_typed/misc.ml
+++ b/src/stages/4-ast_typed/misc.ml
@@ -527,10 +527,19 @@ let equal_variables a b : bool =
   | E_variable a, E_variable b -> Var.equal a b
   |  _, _ -> false
 
-let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) =
-  P_constant {
+let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) = {
+  tsrc = "misc.ml/p_constant" ;
+  t = P_constant {
       p_ctor_tag : constant_tag ;
       p_ctor_args : p_ctor_args ;
     }
+}
 
 let c_equation aval bval reason = { c = C_equation { aval ; bval }; reason }
+
+let reason_simpl : type_constraint_simpl -> string = function
+  | SC_Constructor { reason_constr_simpl=reason; _ }
+  | SC_Alias { reason_alias_simpl=reason; _ }
+  | SC_Poly { reason_poly_simpl=reason; _ }
+  | SC_Typeclass { reason_typeclass_simpl=reason; _ }
+  -> reason
diff --git a/src/stages/4-ast_typed/misc.mli b/src/stages/4-ast_typed/misc.mli
index 561458303..71bb8a291 100644
--- a/src/stages/4-ast_typed/misc.mli
+++ b/src/stages/4-ast_typed/misc.mli
@@ -73,3 +73,5 @@ val get_entry : program -> string -> expression result
 
 val p_constant : constant_tag -> p_ctor_args -> type_value
 val c_equation : type_value -> type_value -> string -> type_constraint
+
+val reason_simpl : type_constraint_simpl -> string
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 336f8cdf2..c42040854 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -29,7 +29,6 @@ module Substitution = struct
           ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env
     and s_type_environment : T.type_environment w = fun ~substs tenv ->
       bind_map_list (fun T.{type_variable ; type_} ->
-        let%bind type_variable = s_type_variable ~substs type_variable in
         let%bind type_ = s_type_expression ~substs type_ in
         ok @@ T.{type_variable ; type_}) tenv
     and s_environment : T.environment w = fun ~substs T.{expression_environment ; type_environment} ->
@@ -45,14 +44,6 @@ module Substitution = struct
       let () = ignore @@ substs in
       ok var
 
-    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 : T.label w = fun ~substs l ->
       let () = ignore @@ substs in
       ok l
@@ -71,7 +62,12 @@ module Substitution = struct
       ok @@ type_name
 
     and s_type_content : T.type_content w = fun ~substs -> function
-        | T.T_sum _ -> failwith "TODO: T_sum"
+        | T.T_sum s ->
+           let aux T.{ ctor_type; michelson_annotation ; ctor_decl_pos } =
+             let%bind ctor_type = s_type_expression ~substs ctor_type in
+             ok @@ T.{ ctor_type; michelson_annotation; ctor_decl_pos } in
+           let%bind s = Ast_typed.Helpers.bind_map_cmap aux s in
+           ok @@ T.T_sum s
         | T.T_record _ -> failwith "TODO: T_record"
         | T.T_constant type_name ->
           let%bind type_name = s_type_name_constant ~substs type_name in
@@ -223,24 +219,24 @@ module Substitution = struct
     and type_value ~tv ~substs =
       let self tv = type_value ~tv ~substs in
       let (v, expr) = substs in
-      match (tv : type_value) with
+      match (tv : type_value).t with
       | P_variable v' when Var.equal v' v -> expr
       | P_variable _ -> tv
       | P_constant {p_ctor_tag=x ; p_ctor_args=lst} -> (
           let lst' = List.map self lst in
-          P_constant {p_ctor_tag=x ; p_ctor_args=lst'}
+          { tsrc = "?TODO1?" ; t = P_constant {p_ctor_tag=x ; p_ctor_args=lst'} }
         )
       | P_apply { tf; targ } -> (
-          P_apply { tf = self tf ; targ = self targ }
+          { tsrc = "?TODO2?" ; t = P_apply { tf = self tf ; targ = self targ } }
         )
       | P_forall p -> (
           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 }
+            { tsrc = "?TODO3?" ; t = P_forall { p with constraints } }
           ) else (
             let body = self p.body in
-            P_forall { p with constraints ; body }
+            { tsrc = "?TODO4?" ; t = P_forall { p with constraints ; body } }
           )
         )
 
@@ -270,9 +266,10 @@ module Substitution = struct
 
     (* Performs beta-reduction at the root of the type *)
     let eval_beta_root ~(tv : type_value) =
-      match tv with
-        P_apply {tf = P_forall { binder; constraints; body }; targ} ->
+      match tv.t with
+        P_apply {tf = { tsrc = _ ; t = P_forall { binder; constraints; body } }; targ} ->
         let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:targ)) constraints in
+        (* TODO: indicate in the result's tsrc that it was obtained via beta-reduction of the original type *)
         (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:targ) , constraints)
       | _ -> (tv , [])
   end
diff --git a/src/stages/typesystem/shorthands.ml b/src/stages/typesystem/shorthands.ml
index 2e431b93c..dc82b2d09 100644
--- a/src/stages/typesystem/shorthands.ml
+++ b/src/stages/typesystem/shorthands.ml
@@ -2,19 +2,24 @@ open Ast_typed.Types
 open Core
 open Ast_typed.Misc
 
-let tc type_vars allowed_list : type_constraint =
-  { c = C_typeclass {tc_args = type_vars ; typeclass = allowed_list} ; reason = "shorthands: typeclass" }
+let tc description type_vars allowed_list : type_constraint = {
+    c = C_typeclass {tc_args = type_vars ;typeclass = allowed_list} ;
+    reason = "typeclass for operator: " ^ description
+  }
 
 let forall binder f =
   let () = ignore binder in
   let freshvar = fresh_type_variable () in
-  P_forall { binder = freshvar ; constraints = [] ; body = f (P_variable freshvar) }
+  let body = f { tsrc = "shorthands.ml/forall" ; t = P_variable freshvar } in
+  { tsrc = "shorthands.ml/forall" ;
+    t = P_forall { binder = freshvar ; constraints = [] ; body } }
 
 let forall_tc binder f =
   let () = ignore binder in
   let freshvar = fresh_type_variable () in
-  let (tc, ty) = f (P_variable freshvar) in
-  P_forall { binder = freshvar ; constraints = tc ; body = ty }
+  let (tc, ty) = f { tsrc = "shorthands.ml/forall_tc" ; t = P_variable freshvar } in
+  { tsrc = "shorthands.ml/forall_tc" ;
+    t = P_forall { binder = freshvar ; constraints = tc ; body = ty } }
 
 (* chained forall *)
 let forall2 a b f =
@@ -55,7 +60,7 @@ let map  k v      = p_constant C_map       [k; v]
 let unit          = p_constant C_unit      []
 let list   t      = p_constant C_list      [t]
 let set    t      = p_constant C_set       [t]
-let bool          = P_variable Stage_common.Constant.t_bool
+let bool          = { tsrc = "built-in type" ; t = P_variable Stage_common.Constant.t_bool }
 let string        = p_constant C_string    []
 let nat           = p_constant C_nat       []
 let mutez         = p_constant C_mutez     []
diff --git a/src/test/coase_tests.ml b/src/test/coase_tests.ml
index f5d7819fd..c1cc1d680 100644
--- a/src/test/coase_tests.ml
+++ b/src/test/coase_tests.ml
@@ -13,15 +13,15 @@ let get_program =
     | Some s -> ok s
     | None -> (
         let%bind (program , state) = type_file "./contracts/coase.ligo" in
-        let () = Typer.Solver.discard_state state in
-        s := Some program ;
-        ok program
+        s := Some (program , state) ;
+        ok (program , state)
       )
 
 let compile_main () = 
-  let%bind typed_prg      = get_program () in
-  let%bind mini_c_prg     = Ligo.Compile.Of_typed.compile typed_prg in
-  let%bind michelson_prg  = Ligo.Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg "main" in
+  let%bind (typed_prg, state) = get_program () in
+  let () = Typer.Solver.discard_state state in
+  let%bind mini_c_prg         = Ligo.Compile.Of_typed.compile typed_prg in
+  let%bind michelson_prg      = Ligo.Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg "main" in
   let%bind (_contract: Tezos_utils.Michelson.michelson) =
     (* fails if the given entry point is not a valid contract *)
     Ligo.Compile.Of_michelson.build_contract michelson_prg in
diff --git a/src/test/hash_lock_tests.ml b/src/test/hash_lock_tests.ml
index 3f9e79c79..b7bbe7bf1 100644
--- a/src/test/hash_lock_tests.ml
+++ b/src/test/hash_lock_tests.ml
@@ -50,7 +50,7 @@ let empty_message = e_lambda (Var.of_name "arguments")
 
 
 let commit () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
   let%bind lock_time = mk_time "2000-01-02T00:10:11Z" in
   let test_hash_raw = sha_256_hash (Bytes.of_string "hello world") in
@@ -79,12 +79,12 @@ let commit () =
       ~sender:first_contract
       ()
   in
-  expect_eq ~options program "commit"
+  expect_eq ~options (program, state) "commit"
     (e_pair salted_hash init_storage) (e_pair empty_op_list post_storage)
 
 (* Test that the contract fails if we haven't committed before revealing the answer *)
 let reveal_no_commit () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
                             ("message", empty_message)]
@@ -95,13 +95,13 @@ let reveal_no_commit () =
                                                               ("salted_hash", (t_bytes ()))])
   in
   let init_storage = storage test_hash true pre_commits in
-  expect_string_failwith program "reveal"
+  expect_string_failwith (program, state) "reveal"
     (e_pair reveal init_storage)
     "You have not made a commitment to hash against yet."
 
 (* Test that the contract fails if our commit isn't 24 hours old yet *)
 let reveal_young_commit () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
                             ("message", empty_message)]
@@ -128,13 +128,13 @@ let reveal_young_commit () =
       ~sender:first_contract
       ()
   in
-  expect_string_failwith ~options program "reveal"
+  expect_string_failwith ~options (program, state) "reveal"
     (e_pair reveal init_storage)
     "It has not been 24 hours since your commit yet."
 
 (* Test that the contract fails if our reveal doesn't meet our commitment *)
 let reveal_breaks_commit () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
                             ("message", empty_message)]
@@ -160,13 +160,13 @@ let reveal_breaks_commit () =
       ~sender:first_contract
       ()
   in
-  expect_string_failwith ~options program "reveal"
+  expect_string_failwith ~options (program, state) "reveal"
     (e_pair reveal init_storage)
     "This reveal does not match your commitment."
 
 (* Test that the contract fails if we reveal the wrong bytes for the stored hash *)
 let reveal_wrong_commit () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello");
                             ("message", empty_message)]
@@ -192,13 +192,13 @@ let reveal_wrong_commit () =
       ~sender:first_contract
       ()
   in
-  expect_string_failwith ~options program "reveal"
+  expect_string_failwith ~options (program, state) "reveal"
     (e_pair reveal init_storage)
     "Your commitment did not match the storage hash."
 
 (* Test that the contract fails if we try to reuse it after unused flag changed *)
 let reveal_no_reuse () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello");
                             ("message", empty_message)]
@@ -224,13 +224,13 @@ let reveal_no_reuse () =
       ~sender:first_contract
       ()
   in
-  expect_string_failwith ~options program "reveal"
+  expect_string_failwith ~options (program, state) "reveal"
     (e_pair reveal init_storage)
     "This contract has already been used."
 
 (* Test that the contract executes successfully with valid commit-reveal *)
 let reveal () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let empty_message = empty_message in
   let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
                             ("message", empty_message)]
@@ -257,7 +257,7 @@ let reveal () =
       ~sender:first_contract
       ()
   in
-  expect_eq ~options program "reveal"
+  expect_eq ~options (program, state) "reveal"
     (e_pair reveal init_storage) (e_pair empty_op_list post_storage)
 
 let main = test_suite "Hashlock" [
diff --git a/src/test/id_tests.ml b/src/test/id_tests.ml
index f5839dd5b..a1fca2a62 100644
--- a/src/test/id_tests.ml
+++ b/src/test/id_tests.ml
@@ -33,7 +33,7 @@ let (first_owner , first_contract) =
   Protocol.Alpha_context.Contract.to_b58check kt , kt
 
 let buy_id () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -60,13 +60,13 @@ let buy_id () =
                               e_int 2;
                               e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
-  let%bind () = expect_eq ~options program "buy" 
+  let%bind () = expect_eq ~options (program, state) "buy" 
       (e_pair param storage) 
       (e_pair (e_list []) new_storage)
   in ok ()
 
 let buy_id_sender_addr () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -93,14 +93,14 @@ let buy_id_sender_addr () =
                               e_int 2;
                               e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
-  let%bind () = expect_eq ~options program "buy" 
+  let%bind () = expect_eq ~options (program, state) "buy" 
       (e_pair param storage) 
       (e_pair (e_list []) new_storage)
   in ok ()
 
 (* Test that contract fails if we attempt to buy an ID for the wrong amount *)
 let buy_id_wrong_amount () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -117,13 +117,13 @@ let buy_id_wrong_amount () =
       ~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
   in
   let param = e_pair owner_website (e_some (e_address new_addr)) in
-  let%bind () = expect_string_failwith ~options program "buy" 
+  let%bind () = expect_string_failwith ~options (program, state) "buy" 
       (e_pair param storage) 
       "Incorrect amount paid."
   in ok ()
 
 let update_details_owner () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -158,13 +158,13 @@ let update_details_owner () =
   let param = e_tuple [e_int 1 ; 
                        e_some details ;
                        e_some (e_address new_addr)] in
-  let%bind () = expect_eq ~options program "update_details"
+  let%bind () = expect_eq ~options (program, state) "update_details"
       (e_pair param storage)
       (e_pair (e_list []) new_storage)
   in ok ()
 
 let update_details_controller () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -199,14 +199,14 @@ let update_details_controller () =
   let param = e_tuple [e_int 1 ; 
                        e_some details ;
                        e_some (e_address owner_addr)] in
-  let%bind () = expect_eq ~options program "update_details"
+  let%bind () = expect_eq ~options (program, state) "update_details"
       (e_pair param storage)
       (e_pair (e_list []) new_storage)
   in ok ()
 
 (* Test that contract fails when we attempt to update details of nonexistent ID *)
 let update_details_nonexistent () = 
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -233,14 +233,14 @@ let update_details_nonexistent () =
   let param = e_tuple [e_int 2 ; 
                        e_some details ;
                        e_some (e_address owner_addr)] in
-  let%bind () = expect_string_failwith ~options program "update_details"
+  let%bind () = expect_string_failwith ~options (program, state) "update_details"
       (e_pair param storage)
       "This ID does not exist."
   in ok ()
 
 (* Test that contract fails when we attempt to update details from wrong addr *)
 let update_details_wrong_addr () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -266,14 +266,14 @@ let update_details_wrong_addr () =
   let param = e_tuple [e_int 0 ; 
                        e_some details ;
                        e_some (e_address owner_addr)] in
-  let%bind () = expect_string_failwith ~options program "update_details"
+  let%bind () = expect_string_failwith ~options (program, state) "update_details"
       (e_pair param storage)
       "You are not the owner or controller of this ID."
   in ok ()
 
 (* Test that giving none on both profile and controller address is a no-op *)
 let update_details_unchanged () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -299,13 +299,13 @@ let update_details_unchanged () =
   let param = e_tuple [e_int 1 ; 
                        e_typed_none (t_bytes ()) ;
                        e_typed_none (t_address ())] in
-  let%bind () = expect_eq ~options program "update_details"
+  let%bind () = expect_eq ~options (program, state) "update_details"
       (e_pair param storage)
       (e_pair (e_list []) storage)
   in ok ()
 
 let update_owner () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -337,14 +337,14 @@ let update_owner () =
                              e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
   let param = e_pair (e_int 1) (e_address owner_addr) in
-  let%bind () = expect_eq ~options program "update_owner"
+  let%bind () = expect_eq ~options (program, state) "update_owner"
       (e_pair param storage)
       (e_pair (e_list []) new_storage)
   in ok ()
 
 (* Test that contract fails when we attempt to update owner of nonexistent ID *)
 let update_owner_nonexistent () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -368,14 +368,14 @@ let update_owner_nonexistent () =
                          e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
   let param = e_pair (e_int 2) (e_address new_addr) in
-  let%bind () = expect_string_failwith ~options program "update_owner"
+  let%bind () = expect_string_failwith ~options (program, state) "update_owner"
       (e_pair param storage)
       "This ID does not exist."
   in ok ()
 
 (* Test that contract fails when we attempt to update owner from non-owner addr *)
 let update_owner_wrong_addr () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -399,13 +399,13 @@ let update_owner_wrong_addr () =
                          e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
   let param = e_pair (e_int 0) (e_address new_addr) in
-  let%bind () = expect_string_failwith ~options program "update_owner"
+  let%bind () = expect_string_failwith ~options (program, state) "update_owner"
       (e_pair param storage)
       "You are not the owner of this ID."
   in ok ()
 
 let skip () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -432,14 +432,14 @@ let skip () =
                              e_int 3;
                              e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
-  let%bind () = expect_eq ~options program "skip"
+  let%bind () = expect_eq ~options (program, state) "skip"
       (e_pair (e_unit ()) storage)
       (e_pair (e_list []) new_storage)
   in ok ()
 
 (* Test that contract fails if we try to skip without paying the right amount *)
 let skip_wrong_amount () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let owner_addr = addr 5 in
   let owner_website = e_bytes_string "ligolang.org" in
   let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@@ -461,7 +461,7 @@ let skip_wrong_amount () =
                          e_int 2;
                          e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
   in
-  let%bind () = expect_string_failwith ~options program "skip"
+  let%bind () = expect_string_failwith ~options (program, state) "skip"
       (e_pair (e_unit ()) storage)
       "Incorrect amount paid."
   in ok ()
diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml
index bbe645b47..ab9242837 100644
--- a/src/test/integration_tests.ml
+++ b/src/test/integration_tests.ml
@@ -4,17 +4,11 @@ open Test_helpers
 open Ast_imperative.Combinators
 
 let retype_file f =
-  let%bind typed,state = Ligo.Compile.Utils.type_file f "reasonligo" Env in
-  let () = Typer.Solver.discard_state state in
-  ok typed
+  Ligo.Compile.Utils.type_file f "reasonligo" Env
 let mtype_file f =
-  let%bind typed,state = Ligo.Compile.Utils.type_file f "cameligo" Env in
-  let () = Typer.Solver.discard_state state in
-  ok typed
+  Ligo.Compile.Utils.type_file f "cameligo" Env
 let type_file f =
-  let%bind typed,state = Ligo.Compile.Utils.type_file f "pascaligo" Env in
-  let () = Typer.Solver.discard_state state in
-  ok typed
+  Ligo.Compile.Utils.type_file f "pascaligo" Env
 
 let type_alias () : unit result =
   let%bind program = type_file "./contracts/type-alias.ligo" in
diff --git a/src/test/multisig_tests.ml b/src/test/multisig_tests.ml
index b618dadd9..df3a42887 100644
--- a/src/test/multisig_tests.ml
+++ b/src/test/multisig_tests.ml
@@ -76,39 +76,39 @@ let params counter msg keys is_validl f s =
 
 (* Provide one valid signature when the threshold is two of two keys *)
 let not_enough_1_of_2 f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let exp_failwith = "Not enough signatures passed the check" in
   let keys = gen_keys () in
   let%bind test_params = params 0 empty_message [keys] [true] f s in
   let%bind () = expect_string_failwith
-    program "main" (e_pair test_params (init_storage 2 0 [keys;gen_keys()])) exp_failwith in
+    (program, state) "main" (e_pair test_params (init_storage 2 0 [keys;gen_keys()])) exp_failwith in
   ok ()
 
 let unmatching_counter f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let exp_failwith = "Counters does not match" in
   let keys = gen_keys () in
   let%bind test_params = params 1 empty_message [keys] [true] f s in
   let%bind () = expect_string_failwith
-    program "main" (e_pair test_params (init_storage 1 0 [keys])) exp_failwith in
+    (program, state) "main" (e_pair test_params (init_storage 1 0 [keys])) exp_failwith in
   ok ()
 
 (* Provide one invalid signature (correct key but incorrect signature)
    when the threshold is one of one key *)
 let invalid_1_of_1 f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let exp_failwith = "Invalid signature" in
   let keys = [gen_keys ()] in
   let%bind test_params = params 0 empty_message keys [false] f s in
   let%bind () = expect_string_failwith
-    program "main" (e_pair test_params (init_storage 1 0 keys)) exp_failwith in
+    (program, state) "main" (e_pair test_params (init_storage 1 0 keys)) exp_failwith in
   ok ()
 
 (* Provide one valid signature when the threshold is one of one key *)
 let valid_1_of_1 f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let keys = gen_keys () in
-  let%bind () = expect_eq_n_trace_aux [0;1;2] program "main"
+  let%bind () = expect_eq_n_trace_aux [0;1;2] (program, state) "main"
       (fun n ->
         let%bind params = params n empty_message [keys] [true] f s in
         ok @@ e_pair params (init_storage 1 n [keys])
@@ -120,10 +120,10 @@ let valid_1_of_1 f s () =
 
 (* Provive two valid signatures when the threshold is two of three keys *)
 let valid_2_of_3 f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let param_keys = [gen_keys (); gen_keys ()] in
   let st_keys = param_keys @ [gen_keys ()] in
-  let%bind () = expect_eq_n_trace_aux [0;1;2] program "main"
+  let%bind () = expect_eq_n_trace_aux [0;1;2] (program, state) "main"
       (fun n ->
         let%bind params = params n empty_message param_keys [true;true] f s in
         ok @@ e_pair params (init_storage 2 n st_keys)
@@ -135,7 +135,7 @@ let valid_2_of_3 f s () =
 
 (* Provide one invalid signature and two valid signatures when the threshold is two of three keys *)
 let invalid_3_of_3 f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let valid_keys = [gen_keys() ; gen_keys()] in
   let invalid_key = gen_keys () in
   let param_keys = valid_keys @ [invalid_key] in
@@ -143,18 +143,18 @@ let invalid_3_of_3 f s () =
   let%bind test_params = params 0 empty_message param_keys [false;true;true] f s in
   let exp_failwith = "Invalid signature" in
   let%bind () = expect_string_failwith
-    program "main" (e_pair test_params (init_storage 2 0 st_keys)) exp_failwith in
+    (program, state) "main" (e_pair test_params (init_storage 2 0 st_keys)) exp_failwith in
   ok ()
 
 (* Provide two valid signatures when the threshold is three of three keys *)
 let not_enough_2_of_3 f s () =
-  let%bind program,_ = get_program f s() in
+  let%bind (program , state) = get_program f s() in
   let valid_keys = [gen_keys() ; gen_keys()] in
   let st_keys = gen_keys () :: valid_keys  in
   let%bind test_params = params 0 empty_message (valid_keys) [true;true] f s in
   let exp_failwith = "Not enough signatures passed the check" in
   let%bind () = expect_string_failwith
-    program "main" (e_pair test_params (init_storage 3 0 st_keys)) exp_failwith in
+    (program, state) "main" (e_pair test_params (init_storage 3 0 st_keys)) exp_failwith in
   ok ()
 
 let main = test_suite "Multisig" [
diff --git a/src/test/multisig_v2_tests.ml b/src/test/multisig_v2_tests.ml
index bf163195c..6c230881e 100644
--- a/src/test/multisig_v2_tests.ml
+++ b/src/test/multisig_v2_tests.ml
@@ -65,7 +65,7 @@ let storage {state_hash ; threshold ; max_proposal ; max_msg_size ; id_counter_l
 
 (* sender not stored in the authorized set *)
 let wrong_addr () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage {
     threshold = 1 ; max_proposal = 1 ; max_msg_size = 1 ; state_hash = Bytes.empty ;
     id_counter_list = [1,0 ; 2,0] ;
@@ -75,13 +75,13 @@ let wrong_addr () =
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
   let%bind () =
     let exp_failwith = "Unauthorized address" in
-    expect_string_failwith ~options program "main"
+    expect_string_failwith ~options (program, state) "main"
     (e_pair (send_param empty_message) init_storage) exp_failwith in
   ok ()
 
 (* send a message which exceed the size limit *)
 let message_size_exceeded () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage {
     threshold = 1 ; max_proposal = 1 ; max_msg_size = 1 ; state_hash = Bytes.empty ;
     id_counter_list = [1,0] ;
@@ -91,13 +91,13 @@ let message_size_exceeded () =
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
   let%bind () =
     let exp_failwith = "Message size exceed maximum limit" in
-    expect_string_failwith ~options program "main"
+    expect_string_failwith ~options (program, state) "main"
     (e_pair (send_param empty_message)  init_storage) exp_failwith in
   ok ()
 
 (* sender has already has reached maximum number of proposal *)
 let maximum_number_of_proposal () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload1 = pack_payload program (send_param empty_message) in
   let bytes1 = e_bytes_raw packed_payload1 in
   let init_storage = storage {
@@ -109,13 +109,13 @@ let maximum_number_of_proposal () =
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
   let%bind () =
     let exp_failwith = "Maximum number of proposal reached" in
-    expect_string_failwith ~options program "main"
+    expect_string_failwith ~options (program, state) "main"
       (e_pair (send_param empty_message2) init_storage) exp_failwith in
   ok ()
 
 (* sender message is already stored in the message store *)
 let send_already_accounted () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let init_storage = storage {
@@ -126,12 +126,12 @@ let send_already_accounted () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair (send_param empty_message) init_storage) (e_pair empty_op_list init_storage)
 
 (* sender message isn't stored in the message store *)
 let send_never_accounted () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let init_storage' = {
@@ -147,12 +147,12 @@ let send_never_accounted () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair (send_param empty_message) init_storage) (e_pair empty_op_list final_storage)
 
 (* sender withdraw message is already binded to one address in the message store *)
 let withdraw_already_accounted_one () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let param = withdraw_param in
@@ -168,12 +168,12 @@ let withdraw_already_accounted_one () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list final_storage)
 
 (* sender withdraw message is already binded to two addresses in the message store *)
 let withdraw_already_accounted_two () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let param = withdraw_param in
@@ -189,12 +189,12 @@ let withdraw_already_accounted_two () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list final_storage)
 
 (* triggers the threshold and check that all the participants get their counters decremented *)
 let counters_reset () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let param = send_param empty_message in
@@ -212,12 +212,12 @@ let counters_reset () =
   let options =
     let sender = contract 3 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list final_storage)
 
 (* sender withdraw message was never accounted *)
 let withdraw_never_accounted () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let param = withdraw_param in
   let init_storage = storage {
     threshold = 2 ; max_proposal = 1 ;  max_msg_size = 1 ; state_hash = Bytes.empty ;
@@ -227,12 +227,12 @@ let withdraw_never_accounted () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list init_storage)
 
 (* successful storing in the message store *)
 let succeeded_storing () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind packed_payload = pack_payload program empty_message in
   let bytes = e_bytes_raw packed_payload in
   let init_storage th = {
@@ -243,7 +243,7 @@ let succeeded_storing () =
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  let%bind () = expect_eq_n_trace_aux ~options [1;2] program "main"
+  let%bind () = expect_eq_n_trace_aux ~options [1;2] (program, state) "main"
       (fun th ->
         let init_storage = storage (init_storage th) in
         ok @@ e_pair (send_param empty_message) init_storage
diff --git a/src/test/pledge_tests.ml b/src/test/pledge_tests.ml
index a10b17295..6f6b371ea 100644
--- a/src/test/pledge_tests.ml
+++ b/src/test/pledge_tests.ml
@@ -45,36 +45,36 @@ let empty_message = e_lambda (Var.of_name "arguments")
 
 
 let pledge () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let storage = e_address oracle_addr in
   let parameter = e_unit () in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options
                   ~sender:oracle_contract
                   ~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
   in
-  expect_eq ~options program "donate"
+  expect_eq ~options (program, state) "donate"
     (e_pair parameter storage)
     (e_pair (e_list []) storage)
 
 let distribute () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let storage = e_address oracle_addr in
   let parameter =  empty_message in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options
                   ~sender:oracle_contract ()
   in
-  expect_eq ~options program "distribute"
+  expect_eq ~options (program, state) "distribute"
     (e_pair parameter storage)
     (e_pair (e_list []) storage)
 
 let distribute_unauthorized () =
-  let%bind program, _ = get_program () in
+  let%bind (program , state) = get_program () in
   let storage = e_address oracle_addr in
   let parameter =  empty_message in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options
                   ~sender:stranger_contract ()
   in
-  expect_string_failwith ~options program "distribute"
+  expect_string_failwith ~options (program, state) "distribute"
     (e_pair parameter storage)
     "You're not the oracle for this distribution."
 
diff --git a/src/test/replaceable_id_tests.ml b/src/test/replaceable_id_tests.ml
index 6de612bab..771b439a7 100644
--- a/src/test/replaceable_id_tests.ml
+++ b/src/test/replaceable_id_tests.ml
@@ -39,45 +39,45 @@ let entry_pass_message = e_constructor "Pass_message"
   @@ empty_message
 
 let change_addr_success () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage 1 in
   let param = entry_change_addr 2 in
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list (storage 2))
 
 let change_addr_fail () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage 1 in
   let param = entry_change_addr 2 in
   let options =
     let sender = contract 3 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
   let exp_failwith = "Unauthorized sender" in
-  expect_string_failwith ~options program "main"
+  expect_string_failwith ~options (program, state) "main"
     (e_pair param init_storage) exp_failwith
 
 let pass_message_success () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage 1 in
   let param = entry_pass_message in
   let options =
     let sender = contract 1 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair param init_storage) (e_pair empty_op_list init_storage)
 
 let pass_message_fail () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let init_storage = storage 1 in
   let param = entry_pass_message in
   let options =
     let sender = contract 2 in
     Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
   let exp_failwith = "Unauthorized sender" in
-  expect_string_failwith ~options program "main"
+  expect_string_failwith ~options (program, state) "main"
     (e_pair param init_storage) exp_failwith
 
 let main = test_suite "Replaceable ID" [
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index adeb5649a..cc1e25afb 100644
--- a/src/test/test_helpers.ml
+++ b/src/test/test_helpers.ml
@@ -86,11 +86,10 @@ let sha_256_hash pl =
 open Ast_imperative.Combinators
 
 let typed_program_with_imperative_input_to_michelson
-    (program: Ast_typed.program) (entry_point: string)
+    ((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string)
     (input: Ast_imperative.expression) : Compiler.compiled_expression result =
   Printexc.record_backtrace true;
   let env = Ast_typed.program_environment Environment.default program in
-  let state = Typer.Solver.initial_state in
   let%bind sugar            = Compile.Of_imperative.compile_expression input in
   let%bind core             = Compile.Of_sugar.compile_expression sugar in
   let%bind app              = Compile.Of_core.apply entry_point core in
@@ -100,9 +99,9 @@ let typed_program_with_imperative_input_to_michelson
   Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied
 
 let run_typed_program_with_imperative_input ?options
-    (program: Ast_typed.program) (entry_point: string)
+    ((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string)
     (input: Ast_imperative.expression) : Ast_core.expression result =
-  let%bind michelson_program = typed_program_with_imperative_input_to_michelson program entry_point input in
+  let%bind michelson_program = typed_program_with_imperative_input_to_michelson (program , state) entry_point input in
   let%bind michelson_output  = Ligo.Run.Of_michelson.run_no_failwith ?options michelson_program.expr michelson_program.expr_ty in
   Uncompile.uncompile_typed_program_entry_function_result program entry_point michelson_output
  
@@ -160,7 +159,7 @@ let expect_eq_core ?options program entry_point input expected =
     Ast_core.Misc.assert_value_eq (expected,result) in
   expect ?options program entry_point input expecter
 
-let expect_evaluate program entry_point expecter =
+let expect_evaluate (program, _state) entry_point expecter =
   let error =
     let title () = "expect evaluate" in
     let content () = Format.asprintf "Entry_point: %s" entry_point in
@@ -173,11 +172,11 @@ let expect_evaluate program entry_point expecter =
   let%bind res_simpl       = Uncompile.uncompile_typed_program_entry_expression_result program entry_point res_michelson in
   expecter res_simpl
 
-let expect_eq_evaluate program entry_point expected =
+let expect_eq_evaluate ((program , state) : Ast_typed.program * Ast_typed.typer_state) entry_point expected =
   let%bind expected  = expression_to_core expected in
   let expecter = fun result ->
     Ast_core.Misc.assert_value_eq (expected , result) in
-  expect_evaluate program entry_point expecter
+  expect_evaluate (program, state) entry_point expecter
 
 let expect_n_aux ?options lst program entry_point make_input make_expecter =
   let aux n =
diff --git a/src/test/time_lock_repeat_tests.ml b/src/test/time_lock_repeat_tests.ml
index adfe66169..efadf31a2 100644
--- a/src/test/time_lock_repeat_tests.ml
+++ b/src/test/time_lock_repeat_tests.ml
@@ -43,21 +43,21 @@ let storage st interval execute =
                ("execute", execute)]
 
 let early_call () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
   let%bind lock_time = mk_time "2000-01-01T10:10:10Z" in
   let init_storage = storage lock_time 86400 empty_message in
   let options =
     Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
   let exp_failwith = "You have to wait before you can execute this contract again." in
-  expect_string_failwith ~options program "main"
+  expect_string_failwith ~options (program, state) "main"
     (e_pair (e_unit ())  init_storage) exp_failwith
 
 let fake_uncompiled_empty_message = e_string "[lambda of type: (lambda unit (list operation)) ]"
 
 (* Test that when we use the contract the next use time advances by correct interval *)
 let interval_advance () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind predecessor_timestamp = mk_time "2000-01-01T10:10:10Z" in
   let%bind lock_time = mk_time "2000-01-01T00:10:10Z" in
   let init_storage = storage lock_time 86400 empty_message in
@@ -66,7 +66,7 @@ let interval_advance () =
   let new_storage_fake = storage new_timestamp 86400 fake_uncompiled_empty_message in
   let options =
     Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
   (e_pair (e_unit ()) init_storage) (e_pair empty_op_list new_storage_fake)
 
 let main = test_suite "Time Lock Repeating" [
diff --git a/src/test/time_lock_tests.ml b/src/test/time_lock_tests.ml
index f345401c9..ee99d1542 100644
--- a/src/test/time_lock_tests.ml
+++ b/src/test/time_lock_tests.ml
@@ -41,24 +41,24 @@ let to_sec t = Tezos_utils.Time.Protocol.to_seconds t
 let storage st = e_timestamp (Int64.to_int @@ to_sec st)
 
 let early_call () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
   let%bind lock_time = mk_time "2000-01-01T10:10:10Z" in
   let init_storage = storage lock_time in
   let options =
     Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
   let exp_failwith = "Contract is still time locked" in
-  expect_string_failwith ~options program "main"
+  expect_string_failwith ~options (program, state) "main"
     (e_pair (call empty_message)  init_storage) exp_failwith
 
 let call_on_time () =
-  let%bind program,_ = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind predecessor_timestamp = mk_time "2000-01-01T10:10:10Z" in
   let%bind lock_time = mk_time "2000-01-01T00:10:10Z" in
   let init_storage = storage lock_time in
   let options =
     Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
-  expect_eq ~options program "main"
+  expect_eq ~options (program, state) "main"
     (e_pair (call empty_message) init_storage) (e_pair empty_op_list init_storage)
 
 let main = test_suite "Time lock" [
diff --git a/src/test/tzip12_tests.ml b/src/test/tzip12_tests.ml
index db5996c9e..af81b9672 100644
--- a/src/test/tzip12_tests.ml
+++ b/src/test/tzip12_tests.ml
@@ -49,7 +49,7 @@ let sender = e_address @@ sender
 let external_contract = e_annotation (e_constant C_IMPLICIT_ACCOUNT [e_key_hash external_contract]) (t_contract (t_nat ()))
 
 let transfer f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair sender from_, e_nat 100)]);
@@ -64,10 +64,10 @@ let transfer f s () =
   let input = e_pair parameter storage in
   let expected = e_pair (e_typed_list [] (t_operation ())) new_storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_eq program ~options "transfer" input expected
+  expect_eq (program, state) ~options "transfer" input expected
 
 let transfer_not_e_allowance f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair sender from_, e_nat 0)]);
@@ -76,11 +76,11 @@ let transfer_not_e_allowance f s () =
   let parameter = e_record_ez [("address_from", from_);("address_to",to_); ("value",e_nat 10)] in
   let input = e_pair parameter storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_string_failwith ~options program "transfer" input
+  expect_string_failwith ~options (program, state) "transfer" input
   "Not Enough Allowance"
 
 let transfer_not_e_balance f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 0); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair sender from_, e_nat 100)]);
@@ -89,11 +89,11 @@ let transfer_not_e_balance f s () =
   let parameter = e_record_ez [("address_from", from_);("address_to",to_); ("value",e_nat 10)] in
   let input = e_pair parameter storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_string_failwith ~options program "transfer" input
+  expect_string_failwith ~options (program, state) "transfer" input
   "Not Enough Balance"
 
 let approve f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair from_ sender, e_nat 0)]);
@@ -108,10 +108,10 @@ let approve f s () =
   let input = e_pair parameter storage in
   let expected = e_pair (e_typed_list [] (t_operation ())) new_storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_eq program ~options "approve" input expected
+  expect_eq (program, state) ~options "approve" input expected
 
 let approve_unsafe f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@@ -120,11 +120,11 @@ let approve_unsafe f s () =
   let parameter = e_record_ez [("spender", from_);("value",e_nat 100)] in
   let input = e_pair parameter storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_string_failwith ~options program "approve" input
+  expect_string_failwith ~options (program, state) "approve" input
   "Unsafe Allowance Change"
 
 let get_allowance f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@@ -134,10 +134,10 @@ let get_allowance f s () =
   let input = e_pair parameter storage in
   let expected = e_pair (e_typed_list [] (t_operation ())) storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_eq program ~options "getAllowance" input expected
+  expect_eq (program, state) ~options "getAllowance" input expected
 
 let get_balance f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@@ -147,10 +147,10 @@ let get_balance f s () =
   let input = e_pair parameter storage in
   let expected = e_pair (e_typed_list [] (t_operation ())) storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_eq program ~options "getBalance" input expected
+  expect_eq (program, state) ~options "getBalance" input expected
 
 let get_total_supply f s () =
-  let%bind program,_ = get_program f s () in
+  let%bind (program , state) = get_program f s () in
   let storage = e_record_ez [
     ("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
     ("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@@ -160,7 +160,7 @@ let get_total_supply f s () =
   let input = e_pair parameter storage in
   let expected = e_pair (e_typed_list [] (t_operation ())) storage in
   let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
-  expect_eq program ~options "getTotalSupply" input expected
+  expect_eq (program, state) ~options "getTotalSupply" input expected
 
 let main = test_suite "tzip-12" [
   test "transfer"                          (transfer                 file_FA12 "pascaligo");
diff --git a/src/test/vote_tests.ml b/src/test/vote_tests.ml
index 24cce7663..89f829a86 100644
--- a/src/test/vote_tests.ml
+++ b/src/test/vote_tests.ml
@@ -2,8 +2,7 @@ open Trace
 open Test_helpers
 
 let type_file f =
-  let%bind typed,state = Ligo.Compile.Utils.type_file f "cameligo" (Contract "main") in
-  ok @@ (typed,state)
+  Ligo.Compile.Utils.type_file f "cameligo" (Contract "main")
 
 let get_program =
   let s = ref None in
@@ -36,10 +35,10 @@ let reset title start_time finish_time =
 let yea = e_constructor "Vote" (e_constructor "Yea" (e_unit ()))
 
 let init_vote () =
-  let%bind (program , _) = get_program () in
+  let%bind (program , state) = get_program () in
   let%bind result =
     Test_helpers.run_typed_program_with_imperative_input
-      program "main" (e_pair yea (init_storage "basic")) in
+      (program, state) "main" (e_pair yea (init_storage "basic")) in
   let%bind (_, storage) = Ast_core.extract_pair result in
   let%bind storage' = Ast_core.extract_record storage in
 (*  let votes = List.assoc (Label "voters") storage' in
diff --git a/vendors/Red-Black_Trees/PolySet.ml b/vendors/Red-Black_Trees/PolySet.ml
index ab26380f2..1dc3c12b0 100644
--- a/vendors/Red-Black_Trees/PolySet.ml
+++ b/vendors/Red-Black_Trees/PolySet.ml
@@ -23,6 +23,17 @@ let find elt set =
 
 let find_opt elt set = RB.find_opt ~cmp:set.cmp elt set.tree
 
+let mem elt set = match RB.find_opt ~cmp:set.cmp elt set.tree with None -> false | Some _ -> true
+
+type 'a added = {set : 'a set; duplicates : 'a list; added : 'a list}
+
+let add_list elts set =
+  let aux = fun {set ; duplicates ; added} elt ->
+    if mem elt set
+    then {set; duplicates = elt :: duplicates ; added}
+    else {set = add elt set; duplicates; added = elt :: added} in
+  List.fold_left aux {set; duplicates=[]; added = []} elts
+
 let elements set = RB.elements set.tree
 
 let iter f set = RB.iter f set.tree
diff --git a/vendors/Red-Black_Trees/PolySet.mli b/vendors/Red-Black_Trees/PolySet.mli
index c8eb4b6d4..589a1374b 100644
--- a/vendors/Red-Black_Trees/PolySet.mli
+++ b/vendors/Red-Black_Trees/PolySet.mli
@@ -46,10 +46,28 @@ val find : 'elt -> 'elt t -> 'elt
 
 val find_opt : 'elt -> 'elt t -> 'elt option
 
+(* The value of the call [mem elt set] is [true] if there exists an
+   element [y] of set [set] such that [cmp y elt = true], where [cmp]
+   is the comparison function of [set] (see [create]). If [elt] is not
+   in [set], then [false] is returned instead. *)
+
+val mem : 'elt -> 'elt t -> bool
+
 (* The value of the call [element set] is the list of elements of the
    set [set] in increasing order (with respect to the total comparison
    function used to create the set). *)
 
+(* The value of the call [add_list element_list set] is a record of
+   type ['a added]. The elements from the [element_list] are added to
+   the [set] starting from the head of the list. The elements which
+   are already part of the [set] at the point at which they are added
+   are gathered in the [duplicates] list (and the [set] is not updated
+   for these elements, i.e. it keeps the pre-existing version of the
+   element). The elements which are not already members of the set are
+   added to the [set], and gathered in the [added] list. *)
+type 'a added = {set : 'a set; duplicates : 'a list; added : 'a list}
+val add_list : 'a list -> 'a set -> 'a added
+
 val elements : 'elt t -> 'elt list
 
 (* The side-effect of evaluating the call [iter f set] is the