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..8bf2e30bf 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 *)
@@ -325,7 +325,7 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con
 let selector_break_ctor :  (type_constraint_simpl, output_break_ctor) selector =
   (* find two rules with the shape a = k(var …) and a = 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)
@@ -473,7 +473,7 @@ let propagator_break_ctor : output_break_ctor propagator =
   (* 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 +482,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 +507,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 +564,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 } =
@@ -574,7 +581,7 @@ let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector
   (* 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
@@ -594,17 +601,19 @@ 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 *)
 
diff --git a/src/passes/8-typer-new/wrap.ml b/src/passes/8-typer-new/wrap.ml
index d14397b51..17d9c103d 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 () =
@@ -342,19 +342,18 @@ let lambda
       (constraints * T.type_variable) =
   fun fresh arg body ->
   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_body = T.{ tsrc = "wrap: lambda: whole" ; t = P_variable (Core.fresh_type_variable ()) } 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
+    | Some arg -> [c_equation unification_arg (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
   let body'  = match body with
       None -> []
-    | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body) "wrap: lambda: body annot"]
+    | Some body -> [c_equation unification_body (type_expression_to_type_value body) "wrap: lambda: body 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 (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_body]))
                  "wrap: lambda: arrow (whole)"
      ] @ arg' @ body' , whole_expr
 
@@ -365,5 +364,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..bd693942c 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -223,24 +223,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 +270,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     []