diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml
index eaaef767b..b940422e0 100644
--- a/src/passes/4-typer/solver.ml
+++ b/src/passes/4-typer/solver.ml
@@ -7,6 +7,21 @@ module Wrap = struct
   module T = Ast_typed
   module O = Core
 
+  module Errors = struct
+
+    let unknown_type_constructor (ctor : string) (te : T.type_value) () =
+      let title = (thunk "unknown type constructor") in
+      (* TODO: sanitize the "ctor" argument before displaying it. *)
+      let message () = ctor in
+      let data = [
+        ("ctor" , fun () -> ctor) ;
+        ("expression" , fun () -> Format.asprintf "%a"  T.PP.type_value te) ;
+        (* ("location" , fun () -> Format.asprintf "%a" Location.pp te.location) *) (* TODO *)
+      ] in
+      error ~data title message ()
+  end
+
+
   type constraints = O.type_constraint list
 
   (* let add_type state t = *)
@@ -30,16 +45,33 @@ module Wrap = struct
     | T_variable type_name -> P_variable type_name
     | T_constant (type_name , args) ->
       let csttag = Core.(match type_name with
-          | "arrow"  -> C_arrow
-          | "option" -> C_option
-          | "tuple"  -> C_tuple
-          | "map"    -> C_map
-          | "list"   -> C_list
-          | "set"    -> C_set
-          | "unit"   -> C_unit
-          | "bool"   -> C_bool
-          | "string" -> C_string
-          | _        -> failwith "unknown type constructor")
+          | "arrow"     -> C_arrow
+          | "option"    -> C_option
+          | "tuple"     -> C_tuple
+          (* record *)
+          (* variant *)
+          | "map"       -> C_map
+          | "big_map"   -> C_map
+          | "list"      -> C_list
+          | "set"       -> C_set
+          | "unit"      -> C_unit
+          | "bool"      -> C_bool
+          | "string"    -> C_string
+          | "nat"       -> C_nat
+          | "mutez"     -> C_tez  (* TODO: rename tez to mutez*)
+          | "timestamp" -> C_timestamp
+          | "int"       -> C_int
+          | "address"   -> C_address
+          | "bytes"     -> C_bytes
+          | "key_hash"  -> C_key_hash
+          | "key"       -> C_key
+          | "signature" -> C_signature
+          | "operation" -> C_operation
+          | "contract"  -> C_contract
+          | unknown  ->
+            (* TODO: return a Trace.result *)
+            let _ = fail (fun () -> Errors.unknown_type_constructor unknown te ()) in
+            failwith ("unknown type constructor " ^ unknown))
       in
       P_constant (csttag, List.map type_expression_to_type_value args)
 
@@ -336,10 +368,6 @@ module UF = Union_find.Partition0.Make(TV)
 
 type unionfind = UF.t
 
-let empty = UF.empty                           (* DEMO *)
-let representative_toto = UF.repr "toto" empty (* DEMO *)
-let merge x y = UF.equiv x y                   (* DEMO *)
-
 (* end unionfind *)
 
 (* representant for an equivalence class of type variables *)
@@ -521,7 +549,8 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor
     | _ ->
       (dbs , [new_constraint])
 
-let type_level_eval : type_value -> type_value * type_constraint list = failwith "implemented in other branch"
+let type_level_eval : type_value -> type_value * type_constraint list =
+  fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
 
 let check_applied ((reduced, _new_constraints) as x) =
   let () = match reduced with
@@ -972,10 +1001,10 @@ let select_and_propagate_all' : _ -> type_constraint_simpl selector_input -> str
 
 (* Takes a list of constraints, applies all selector+propagator pairs
    to each in turn. *)
-let rec select_and_propagate_all : _ -> type_constraint selector_input list -> structured_dbs -> structured_dbs =
+let rec select_and_propagate_all : _ -> type_constraint selector_input list -> structured_dbs -> _ * structured_dbs =
   fun already_selected new_constraints dbs ->
     match new_constraints with
-    | [] -> dbs
+    | [] -> (already_selected, dbs)
     | new_constraint :: tl ->
       let { state = dbs ; list = modified_constraints } = normalizers new_constraint dbs in
       let (already_selected , new_constraints' , dbs) =
@@ -998,21 +1027,40 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s
 
 (* Below is a draft *)
 
+(* type state = {
+ *   (\* when α-renaming x to y, we put them in the same union-find class *\)
+ *   unification_vars : unionfind ;
+ *
+ *   (\* assigns a value to the representant in the unionfind *\)
+ *   assignments : type_value TypeVariableMap.t ;
+ *
+ *   (\* constraints related to a type variable *\)
+ *   constraints : constraints TypeVariableMap.t ;
+ * } *)
+
 type state = {
-  (* when α-renaming x to y, we put them in the same union-find class *)
-  unification_vars : unionfind ;
-
-  (* assigns a value to the representant in the unionfind *)
-  assignments : type_value TypeVariableMap.t ;
-
-  (* constraints related to a type variable *)
-  constraints : constraints TypeVariableMap.t ;
+  structured_dbs   : structured_dbs   ;
+  already_selected : already_selected ;
 }
 
-let initial_state : state = {
-  unification_vars = UF.empty ;
-  constraints = TypeVariableMap.empty ;
-  assignments = TypeVariableMap.empty ;
+let initial_state : state = (* {
+ *   unification_vars = UF.empty ;
+ *   constraints = TypeVariableMap.empty ;
+ *   assignments = TypeVariableMap.empty ;
+ * } *)
+{
+  structured_dbs =
+  {
+    all_constraints = [] ; (* type_constraint_simpl list *)
+    aliases = UF.empty ; (* unionfind *)
+    assignments = TypeVariableMap.empty; (* c_constructor_simpl TypeVariableMap.t *)
+    grouped_by_variable = TypeVariableMap.empty; (* constraints TypeVariableMap.t *)
+    cycle_detection_toposort = (); (* unit *)
+  } ;
+  already_selected = {
+    break_ctor = M_break_ctor.AlreadySelected.empty ;
+    specialize1 = M_specialize1.AlreadySelected.empty ;
+  }
 }
 
 (* This function is called when a program is fully compiled, and the
@@ -1045,7 +1093,8 @@ let discard_state (_ : state) = ()
 let aggregate_constraints : state -> type_constraint list -> state result = fun state newc ->
   (* TODO: Iterate over constraints *)
   let _todo = ignore (state, newc) in
-  failwith "TODO"
+  let (a, b) = select_and_propagate_all state.already_selected newc state.structured_dbs in
+  ok { already_selected = a ; structured_dbs = b }
 (*let { constraints ; eqv } = state in
   ok { constraints = constraints @ newc ; eqv }*)
 
diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index 906766540..d743aa11f 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -920,7 +920,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
 (* TODO: we ended up with two versions of type_program… ??? *)
 
 (*
-Apply type_declaration on all the node of the AST_simplified from the root p 
+Apply type_declaration on all the node of the AST_simplified from the root p
 *)
 let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result =
   let env = Ast_typed.Environment.full_empty in
@@ -941,7 +941,14 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
 
 let type_program (p : I.program) : (O.program * Solver.state) result =
   let%bind (env, state, program) = type_program_returns_state p in
-  let program = let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in program 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) =
+      Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in
+    let p = SMap.fold aux assignments program in
+    p in
+  let program = subst_all in
+  let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (program, state)
 
  (*
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index 9d53b6ea3..66e841689 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -102,6 +102,13 @@ them. please report this to the developers." in
       ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
     ] in
     error ~data title content
+
+  let not_found content =
+    let title () = "Not_found" in
+    let content () = content in
+    let data = [
+    ] in
+    error ~data title content
 end
 open Errors
 
@@ -539,7 +546,10 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
               let%bind ty'_map = bind_map_smap transpile_type ty_map in
               let%bind path = record_access_to_lr ty' ty'_map prop in
               let path' = List.map snd path in
-            ok (Map.String.find prop ty_map, acc @ path')
+            let%bind prop_in_ty_map = trace_option
+                (Errors.not_found "acessing prop in ty_map [TODO: better error message]")
+                (Map.String.find_opt prop ty_map) in
+            ok (prop_in_ty_map, acc @ path')
           )
           | Access_map _k -> fail (corner_case ~loc:__LOC__ "no patch for map yet")
       in
diff --git a/src/stages/ast_typed/environment.ml b/src/stages/ast_typed/environment.ml
index 673f8645f..6281f0094 100644
--- a/src/stages/ast_typed/environment.ml
+++ b/src/stages/ast_typed/environment.ml
@@ -43,7 +43,10 @@ let get_constructor : string -> t -> (type_value * type_value) option = fun k x
   let aux = fun x ->
     let aux = fun (_type_name , x) ->
       match x.type_value' with
-      | T_sum m when Map.String.mem k m -> Some (Map.String.find k m , x)
+      | T_sum m ->
+        (match Map.String.find_opt k m with
+           Some km -> Some (km , x)
+         | None -> None)
       | _ -> None
     in
     List.find_map aux (Small.get_type_environment x) in
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 96baf197b..096a5cea8 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -6,10 +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"
+
+    and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program =
+      List.map (fun d -> declaration ~d ~v ~expr) p
+
     (*
        Computes `P[v := expr]`.
     *)
-    let rec type_value ~tv ~v ~expr =
+    and type_value ~tv ~v ~expr =
       let self tv = type_value ~tv ~v ~expr in
       match tv with
       | P_variable v' when v' = v -> expr
@@ -52,6 +59,13 @@ module Substitution = struct
     and typeclass ~tc ~v ~expr =
       List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc
 
+    (* Performs beta-reduction at the root of the type *)
+    let eval_beta_root ~(tv : type_value) =
+      match tv with
+        P_apply (P_forall { binder; constraints; body }, arg) ->
+        let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in
+        (type_value ~tv:body ~v:binder ~expr:arg , constraints)
+      | _ -> (tv , [])
   end
 
 end
diff --git a/src/test/test.ml b/src/test/test.ml
index a3709700e..aebade390 100644
--- a/src/test/test.ml
+++ b/src/test/test.ml
@@ -2,9 +2,8 @@
 
 open Test_helpers
 
-
 let () =
-  (* Printexc.record_backtrace true ; *)
+  Printexc.record_backtrace true ;
   run_test @@ test_suite "LIGO" [
     Integration_tests.main ;
     Compiler_tests.main ;
diff --git a/src/union_find/dune b/src/union_find/dune
index a4c27e725..fad355c7a 100644
--- a/src/union_find/dune
+++ b/src/union_find/dune
@@ -12,5 +12,5 @@
 
 (test
  (modules PartitionMain)
- (libraries UnionFind)
+ (libraries union_find)
  (name PartitionMain))