diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml
index db1512f19..b76e55500 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,6 +34,9 @@ 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 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 67b8b16b8..02ee01b7e 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 with
+  let dbs = match new_constraint.c_simpl 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 with
+    match new_constraint.c_simpl 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
@@ -210,28 +210,28 @@ 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) in
-    let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b) 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
     (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) (List.combine fresh_vars 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 (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur) in
-  let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall }]) in
-  let gather_alias a b = (dbs , [SC_Alias { a ; b }]) 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
   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
-    let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced) in (* Note: this calls recursively but cant't fall in the same case. *)
+    let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced "normalizer: reduce_type_app") in (* Note: this calls recursively but cant't fall in the same case. *)
     (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) (List.combine fresh_vars 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 (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur) in
+    (dbs, [{c_simpl=SC_Typeclass { tc ; args = fresh_vars };reason_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
 
-  match new_constraint with
+  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
   (* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *)
@@ -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 with
+  match type_constraint_simpl.c_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) in
+  let eq1 = c_equation (P_variable a.tv) (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)) a.tv_list b.tv_list in
+    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 eqs = eq1 :: eqs3 in
     (eqs , []) (* no new assignments *)
 
@@ -531,7 +531,12 @@ and compare_type_expression = function
       | P_variable _ -> 1
       | P_constant _ -> 1
       | P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
-and compare_type_constraint = function
+and compare_type_constraint = fun { c = ca ; reason = ra } { c = cb ; reason = rb } ->
+  let c = compare_type_constraint_ ca cb in
+  if c < 0 then -1
+  else if c = 0 then String.compare ra rb
+  else 1
+and compare_type_constraint_ = function
   | C_equation { aval=a1; bval=a2 } -> (function
       | C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
       | C_typeclass _ -> -1
@@ -569,7 +574,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 with
+  match type_constraint_simpl.c_simpl with
     SC_Constructor c                ->
     (* vice versa *)
     let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in
@@ -599,7 +604,7 @@ let propagator_specialize1 : output_specialize1 propagator =
      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 (reduced, new_constraints) = check_applied @@ type_level_eval apply in
-  let eq1 = c_equation (P_variable b.tv) reduced in
+  let eq1 = c_equation (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 d5125e362..52d422c7f 100644
--- a/src/passes/8-typer-new/wrap.ml
+++ b/src/passes/8-typer-new/wrap.ml
@@ -117,12 +117,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_equation { aval = P_variable type_name ; bval = pattern }] , type_name
+  [{ c = C_equation { aval = 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_equation { aval = P_variable type_name ; bval = pattern }] , type_name
+  [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: literal" }] , type_name
 
 (*
   let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@@ -140,7 +140,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_equation { aval = P_variable type_name ; bval = pattern}] , type_name
+  [{ c = C_equation { aval = 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) *)
@@ -169,7 +169,7 @@ end
 let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) =
   let base' = type_expression_to_type_value base in
   let expr_type = Core.fresh_type_variable () in
-  [T.C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type }] , expr_type
+  [{ c = C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type } ; reason = "wrap: access_label" }] , expr_type
 
 open Ast_typed.Misc
 let constructor
@@ -180,25 +180,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 ;
-    c_equation t_arg c_arg ;
+    c_equation (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] , whole_expr
+  [c_equation (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 aux elt =
     let elt' = type_expression_to_type_value elt
-    in c_equation elttype elt' in
+    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]) ;
+      c_equation (P_variable whole_expr) (p_constant ctor [elttype]) "wrap: collection: whole" ;
   ] @ equations , whole_expr
 
 let list = collection T.C_list
@@ -210,15 +210,15 @@ let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_
   let v_type = 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' in
+    c_equation k_type k' "wrap: map: key" in
   let aux_v (_k , v) =
     let v' = type_expression_to_type_value v in
-    c_equation v_type v' in
+    c_equation v_type v' "wrap: map: value" in
   let equations_k = List.map aux_k kv_tys in
   let equations_v = List.map aux_v kv_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) ;
+      c_equation (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) =
@@ -227,17 +227,17 @@ let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.t
   let v_type = 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' in
+    c_equation k_type k' "wrap: big_map: key" in
   let aux_v (_k , v) =
     let v' = type_expression_to_type_value v in
-    c_equation v_type v' in
+    c_equation v_type v' "wrap: big_map: value" in
   let equations_k = List.map aux_k kv_tys in
   let equations_v = List.map aux_v kv_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
       (* 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]) ;
+      c_equation (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) =
@@ -246,7 +246,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]) ;
+      c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) "wrap: application: f" ;
   ] , whole_expr
 
 let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -256,8 +256,8 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va
   let whole_expr = Core.fresh_type_variable () in
   let v = Core.fresh_type_variable () in
   [
-      c_equation ds' (p_constant C_map [ind' ; P_variable v]) ;
-      c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) ;
+      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" ;
   ] , whole_expr
 
 let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -266,8 +266,8 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v
   let b' = type_expression_to_type_value b in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation a' (p_constant C_unit []) ;
-      c_equation b' (P_variable whole_expr) ;
+      c_equation a' (p_constant C_unit []) "wrap: sequence: first" ;
+      c_equation b' (P_variable whole_expr) "wrap: sequence: second (whole)" ;
   ] , whole_expr
 
 let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -276,9 +276,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)) ;
-      c_equation body'                   (p_constant C_unit []) ;
-      c_equation (P_variable whole_expr) (p_constant C_unit [])
+      c_equation expr'                   (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)" ;
   ] , whole_expr
 
 let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) =
@@ -287,10 +287,10 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression
   let result'     = type_expression_to_type_value result in
   let rhs_tv_opt' = match rhs_tv_opt with
       None -> []
-    | Some annot -> [c_equation rhs' (type_expression_to_type_value annot)] in
+    | 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) ;
+      c_equation result' (P_variable whole_expr) "wrap: let_in: result (whole)" ;
   ] @ rhs_tv_opt', whole_expr
 
 let recursive : T.type_expression -> (constraints * T.type_variable) =
@@ -298,7 +298,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) ;
+      c_equation fun_type (P_variable whole_expr) "wrap: recursive: fun_type (whole)" ;
   ], whole_expr
 
 let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -307,8 +307,8 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var
   let e' = type_expression_to_type_value e in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation v'  e' ;
-      c_equation (P_variable whole_expr) (p_constant C_unit []) ;
+      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)" ;
   ] , whole_expr
 
 let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -317,15 +317,15 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type
   let annot' = type_expression_to_type_value annot in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation e' annot' ;
-      c_equation e' (P_variable whole_expr) ;
+      c_equation e' annot' "wrap: annotation: expr type must eq annot" ;
+      c_equation e' (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) type_expressions
+  let cs = List.map (fun e -> c_equation (P_variable whole_expr) e "wrap: matching: case (whole)") type_expressions
   in cs, whole_expr
 
 let fresh_binder () =
@@ -342,15 +342,16 @@ let lambda
   let unification_body = 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)] in
+    | Some arg -> [c_equation (P_variable 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)]
+    | Some body -> [c_equation (P_variable 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) ;
+      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]))
+                 "wrap: lambda: arrow (whole)"
      ] @ arg' @ body' , whole_expr
 
 (* This is pretty much a wrapper for an n-ary function. *)
@@ -360,5 +361,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]))
+      c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) "wrap: constant: as declared for built-in"
   ] , whole_expr
diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml
index daa4efd6b..c071aa9b8 100644
--- a/src/stages/4-ast_typed/misc.ml
+++ b/src/stages/4-ast_typed/misc.ml
@@ -536,4 +536,4 @@ let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) =
       p_ctor_args : p_ctor_args ;
     }
 
-let c_equation aval bval = C_equation { aval ; bval }
+let c_equation aval bval reason = { c = C_equation { aval ; bval }; reason }
diff --git a/src/stages/4-ast_typed/misc.mli b/src/stages/4-ast_typed/misc.mli
index fae2a1a36..76727dbdc 100644
--- a/src/stages/4-ast_typed/misc.mli
+++ b/src/stages/4-ast_typed/misc.mli
@@ -73,4 +73,4 @@ val get_entry : program -> string -> expression result
 val program_environment : program -> full_environment
 
 val p_constant : constant_tag -> p_ctor_args -> type_value
-val c_equation : type_value -> type_value -> type_constraint
+val c_equation : type_value -> type_value -> string -> type_constraint
diff --git a/src/stages/4-ast_typed/types.ml b/src/stages/4-ast_typed/types.ml
index 450559d1b..b080b7c79 100644
--- a/src/stages/4-ast_typed/types.ml
+++ b/src/stages/4-ast_typed/types.ml
@@ -509,8 +509,11 @@ and c_access_label = {
     c_access_label_tvar : type_variable ;
   }
 
-(*What i was saying just before *)
-and type_constraint =
+and type_constraint = {
+  reason : string ;
+  c : type_constraint_ ;
+}
+and type_constraint_ =
   (* | C_assignment of (type_variable * type_pattern) *)
   | C_equation of c_equation (* TVA = TVB *)
   | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
@@ -569,7 +572,11 @@ and c_poly_simpl = {
   tv     : type_variable ;
   forall : p_forall      ;
 }
-and type_constraint_simpl =
+and type_constraint_simpl = {
+    reason_simpl : string ;
+    c_simpl : 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 *)
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 17c1d3eff..cbb90084d 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -245,7 +245,10 @@ module Substitution = struct
           )
         )
 
-    and constraint_ ~c ~substs =
+    and constraint_ ~c:{c;reason} ~substs =
+      {c = constraint__ ~c ~substs;reason}
+
+    and constraint__ ~c ~substs =
       match c with
       | C_equation { aval; bval } -> (
         let aux tv = type_value ~tv ~substs in
diff --git a/src/stages/typesystem/shorthands.ml b/src/stages/typesystem/shorthands.ml
index c01775120..2e431b93c 100644
--- a/src/stages/typesystem/shorthands.ml
+++ b/src/stages/typesystem/shorthands.ml
@@ -3,7 +3,7 @@ open Core
 open Ast_typed.Misc
 
 let tc type_vars allowed_list : type_constraint =
-  C_typeclass {tc_args = type_vars ; typeclass = allowed_list}
+  { c = C_typeclass {tc_args = type_vars ; typeclass = allowed_list} ; reason = "shorthands: typeclass" }
 
 let forall binder f =
   let () = ignore binder in