diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml
index 04ebf8236..33fe71c80 100644
--- a/src/passes/8-typer-new/solver.ml
+++ b/src/passes/8-typer-new/solver.ml
@@ -622,18 +622,13 @@ let propagator_specialize1 : output_specialize1 propagator =
   (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
+     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
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index bd693942c..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
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