diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index d743aa11f..f6f51b482 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -939,15 +939,19 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
   let () = ignore (env' , state') in
   ok (env', state', declarations)
 
+module TSMap = TMap(Solver.TypeVariable)
+
 let type_program (p : I.program) : (O.program * Solver.state) result =
   let%bind (env, state, program) = type_program_returns_state p in
   let subst_all =
     let assignments = state.structured_dbs.assignments in
-    let aux (v : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program) =
+    let aux (v : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program result) =
+      let%bind p = p in
       Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in
-    let p = SMap.fold aux assignments program in
+    (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *)
+    let p = Solver.TypeVariableMap.fold aux assignments (ok program) in
     p in
-  let program = subst_all in
+  let%bind program = subst_all in
   let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (program, state)
 
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 096a5cea8..88b06e3fd 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -6,12 +6,17 @@ module Substitution = struct
 
   module Pattern = struct
 
-    let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap =
-      let _TODO = (d, v, expr) in
-      failwith "TODO: subst declaration"
+    open Trace
 
-    and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program =
-      List.map (fun d -> declaration ~d ~v ~expr) p
+    let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap result =
+      Trace.bind_map_location (function
+            Ast_typed.Declaration_constant (e, (env1, env2)) ->
+            let _ = v, expr, failwith "TODO: subst" in
+            ok @@ Ast_typed.Declaration_constant (e, (env1, env2))
+        ) d
+
+    and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program Trace.result =
+      Trace.bind_map_list (fun d -> declaration ~d ~v ~expr) p
 
     (*
        Computes `P[v := expr]`.
diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml
index 7a0326eec..e8f3b43eb 100644
--- a/vendors/ligo-utils/simple-utils/trace.ml
+++ b/vendors/ligo-utils/simple-utils/trace.ml
@@ -592,6 +592,16 @@ let bind_fold_list f init lst =
   in
   List.fold_left aux (ok init) lst
 
+module TMap(X : Map.OrderedType) = struct
+  module MX = Map.Make(X)
+  let bind_fold_Map f init map =
+    let aux k v x  =
+      x >>? fun x ->
+      f ~x ~k ~v
+    in
+    MX.fold aux map (ok init)
+end
+
 let bind_fold_pair f init (a,b) = 
   let aux x y =
     x >>? fun x ->