diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
index 3ba22074a..c9c0a2b3a 100644
--- a/cli/subcommands/src/cargo_hax.rs
+++ b/cli/subcommands/src/cargo_hax.rs
@@ -298,7 +298,7 @@ fn run_engine(
     let mut output = Output {
         diagnostics: vec![],
         files: vec![],
-        debug_json: None,
+        debug_json: vec![],
     };
     {
         let mut rctx = hax_types::diagnostics::report::ReportCtx::default();
@@ -396,9 +396,7 @@ fn run_engine(
                         HaxMessage::ProducedFile { path, wrote }.report(message_format, None)
                     }
                 }
-                FromEngine::DebugString(debug) => {
-                    output.debug_json = Some(debug);
-                }
+                FromEngine::DebugString(debug) => output.debug_json.push(debug),
                 FromEngine::PrettyPrintDiagnostic(diag) => {
                     send!(&ToEngine::PrettyPrintedDiagnostic(format!("{}", diag)));
                 }
@@ -447,8 +445,9 @@ fn run_engine(
     if backend.dry_run {
         serde_json::to_writer(std::io::BufWriter::new(std::io::stdout()), &output).unwrap()
     }
-    if let Some(debug_json) = &output.debug_json {
+    if !output.debug_json.is_empty() {
         use DebugEngineMode;
+        let debug_json = &format!("[{}]", output.debug_json.join(","));
         match &backend.debug_engine {
             Some(DebugEngineMode::Interactive) => {
                 eprintln!("----------------------------------------------");
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index 9a8cd7359..f1533a20a 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -157,7 +157,7 @@ let run (options : Types.engine_options) : Types.output =
   {
     diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics;
     files = Option.value ~default:[] files;
-    debug_json = None;
+    debug_json = [];
   }
 
 (** Shallow parses a `id_table::Node<T>` (or a raw `T`) JSON *)
@@ -224,6 +224,10 @@ let parse_options () =
   Profiling.enabled := options.backend.profile;
   options
 
+let send_debug_strings =
+  Phase_utils.DebugBindPhase.export
+  >> List.iter ~f:(fun json -> DebugString json |> Hax_io.write)
+
 (** Entrypoint of the engine. Assumes `Hax_io.init` was called. *)
 let engine () =
   let options = Profiling.profile (Other "parse_options") 1 parse_options in
@@ -241,16 +245,12 @@ let engine () =
   in
   match result with
   | Ok results ->
-      let debug_json = Phase_utils.DebugBindPhase.export () in
-      let results = { results with debug_json } in
-      Logs.info (fun m -> m "Outputting JSON");
-
       List.iter
         ~f:(fun diag -> Diagnostic diag |> Hax_io.write)
         results.diagnostics;
       List.iter ~f:(fun file -> File file |> Hax_io.write) results.files;
 
-      Option.iter ~f:(fun json -> DebugString json |> Hax_io.write) debug_json;
+      send_debug_strings ();
       Hax_io.close ();
 
       Logs.info (fun m -> m "Exiting Hax engine (success)")
@@ -258,9 +258,36 @@ let engine () =
       Logs.info (fun m -> m "Exiting Hax engine (with an unexpected failure)");
       Printexc.raise_with_backtrace exn bt
 
+module ExportFullAst = Export_ast.Make (Features.Full)
 module ExportRustAst = Export_ast.Make (Features.Rust)
 module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage)
 
+let driver_for_rust_engine_inner (query : Rust_engine_types.query) :
+    Rust_engine_types.response =
+  Profiling.enabled := query.profiling;
+  if query.debug_bind_phase then Phase_utils.DebugBindPhase.enable ();
+  match query.kind with
+  | Types.ImportThir { input; translation_options } ->
+      let imported_items =
+        import_thir_items translation_options.include_namespaces input
+      in
+      let rust_ast_items =
+        List.concat_map ~f:ExportRustAst.ditem imported_items
+      in
+      Rust_engine_types.ImportThir { output = rust_ast_items }
+  | Types.ApplyPhases { input; phases } ->
+      let items = List.concat_map ~f:Import_ast.ditem input in
+      let module Phase =
+        (val List.map
+               ~f:(fun name ->
+                 Untyped_phases.phase_of_name name |> Option.value_exn)
+               phases
+             |> Untyped_phases.bind_list)
+      in
+      let items = Phase.ditems items in
+      let output = List.concat_map ~f:ExportFullAst.ditem items in
+      Rust_engine_types.ApplyPhases { output }
+
 (** Entry point for interacting with the Rust hax engine *)
 let driver_for_rust_engine () : unit =
   let query : Rust_engine_types.query =
@@ -269,23 +296,7 @@ let driver_for_rust_engine () : unit =
   in
   Concrete_ident.ImplInfoStore.init
     (Concrete_ident_generated.impl_infos @ query.impl_infos);
-  match query.kind with
-  | Types.ImportThir { input; apply_phases; translation_options } ->
-      (* Note: `apply_phases` comes from the type `QueryKind` in
-       `ocaml_engine.rs`. This is a temporary flag that applies some phases while
-       importing THIR. In the future (when #1550 is merged), we will be able to
-       import THIR and then apply phases. *)
-      let imported_items =
-        import_thir_items translation_options.include_namespaces input
-      in
-      let rust_ast_items =
-        if apply_phases then
-          let imported_items = Lean_backend.apply_phases imported_items in
-          List.concat_map
-            ~f:(fun item -> ExportLeanAst.ditem item)
-            imported_items
-        else List.concat_map ~f:ExportRustAst.ditem imported_items
-      in
-      let response = Rust_engine_types.ImportThir { output = rust_ast_items } in
-      Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response);
-      Hax_io.write_json ([%yojson_of: Types.from_engine] Exit)
+  let response = driver_for_rust_engine_inner query in
+  send_debug_strings ();
+  Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response);
+  Hax_io.write_json ([%yojson_of: Types.from_engine] Exit)
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 96fb0c6a4..4c24eef1e 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -909,6 +909,67 @@ module Make (F : Features.T) = struct
   let string_lit span (s : string) : expr =
     { span; typ = TStr; e = Literal (String s) }
 
+  module HaxFailure = struct
+    module Build = struct
+      let pat span (typ : ty) (msg : string) : pat =
+        let (module M) = M.make span in
+        let constructor =
+          Global_ident.of_name ~value:true Rust_primitives__hax__Failure__Ctor
+        in
+        let pat = M.pat_PConstant ~typ ~lit:(String msg) in
+        let fields = [ { field = constructor; pat } ] in
+        M.pat_PConstruct ~typ ~is_record:false ~is_struct:true ~constructor
+          ~fields
+
+      let expr span (typ : ty) (error : string) (ast : string) =
+        let args = List.map ~f:(string_lit span) [ error; ast ] in
+        call Rust_primitives__hax__failure args span typ
+
+      let ty (payload : string) =
+        let ident =
+          `Concrete
+            (Concrete_ident.of_name ~value:false Rust_primitives__hax__Failure)
+        in
+        let (module M) = M.make (Span.dummy ()) in
+        let payload = M.expr_Literal ~typ:TBool (String payload) in
+        TApp { ident; args = [ GConst payload ] }
+    end
+
+    open struct
+      let destruct_str_lit e =
+        let* l = D.expr_Literal e in
+        match l with String s -> Some s | _ -> None
+    end
+
+    module Destruct = struct
+      let pat (p : pat) : string option =
+        let* p = D.pat_PConstruct p in
+        let*? () =
+          Global_ident.eq_name Rust_primitives__hax__Failure__Ctor p.constructor
+        in
+        let* { pat; _ } = D.list_1 p.fields in
+        let* s = D.pat_PConstant pat in
+        match s.lit with String s -> Some s | _ -> None
+
+      let expr (e : expr) : (string * string) option =
+        let* app = D.expr_App e in
+        let* id = D.expr_GlobalVar app.f in
+        let*? _ = Global_ident.eq_name Rust_primitives__hax__failure id in
+        let* x, y = D.list_2 app.args in
+
+        let* x = destruct_str_lit x in
+        let* y = destruct_str_lit y in
+        Some (x, y)
+
+      let ty (t : ty) : string option =
+        match t with
+        | TApp { ident; args = [ GConst payload ] }
+          when Global_ident.eq_name Rust_primitives__hax__Failure ident ->
+            destruct_str_lit payload
+        | _ -> None
+    end
+  end
+
   let hax_failure_expr' span (typ : ty) (context, kind) (ast : string) =
     let ast =
       (* Remove consecutive withe spaces *)
@@ -921,19 +982,11 @@ module Make (F : Features.T) = struct
       else ast
     in
     let error = Diagnostics.pretty_print_context_kind context kind in
-    let args = List.map ~f:(string_lit span) [ error; ast ] in
-    call Rust_primitives__hax__failure args span typ
+    HaxFailure.Build.expr span typ error ast
 
   let hax_failure_expr span (typ : ty) (context, kind) (expr0 : Ast.Full.expr) =
     hax_failure_expr' span typ (context, kind) (Print_rust.pexpr_str expr0)
 
-  let hax_failure_typ =
-    let ident =
-      `Concrete
-        (Concrete_ident.of_name ~value:false Rust_primitives__hax__failure)
-    in
-    TApp { ident; args = [] }
-
   module LiftToFullAst = struct
     let expr : AST.expr -> Ast.Full.expr = Stdlib.Obj.magic
     let ty : AST.ty -> Ast.Full.ty = Stdlib.Obj.magic
diff --git a/engine/lib/concrete_ident/explicit_def_id.ml b/engine/lib/concrete_ident/explicit_def_id.ml
index fd4ffa3be..4a4acc084 100644
--- a/engine/lib/concrete_ident/explicit_def_id.ml
+++ b/engine/lib/concrete_ident/explicit_def_id.ml
@@ -149,7 +149,7 @@ module FromRustAST = struct
       ({ krate; path; parent; kind; _ } : A.def_id) : B.def_id_contents =
     let f (o : A.def_id) : B.def_id =
       let contents : B.node_for__def_id_contents =
-        { value = def_id_contents_to_rust_ast o; id = Int64.of_int (-1) }
+        { value = def_id_contents_to_rust_ast o; id = Int64.zero }
       in
       { contents }
     in
@@ -159,7 +159,7 @@ module FromRustAST = struct
       path;
       parent;
       kind;
-      index = (Int64.of_int (-1), Int64.of_int (-1), None);
+      index = (Int64.zero, Int64.zero, None);
       is_local = false;
     }
 
@@ -167,5 +167,7 @@ module FromRustAST = struct
     { is_constructor; def_id = def_id_contents_to_rust_ast def_id }
 end
 
+let def_id_to_rust_ast = ToRustAST.def_id_contents_to_rust_ast
+let def_id_from_rust_ast = FromRustAST.def_id_contents_to_rust_ast
 let to_rust_ast = ToRustAST.to_rust_ast
 let from_rust_ast = FromRustAST.to_rust_ast
diff --git a/engine/lib/concrete_ident/explicit_def_id.mli b/engine/lib/concrete_ident/explicit_def_id.mli
index 051daea3a..8b458718f 100644
--- a/engine/lib/concrete_ident/explicit_def_id.mli
+++ b/engine/lib/concrete_ident/explicit_def_id.mli
@@ -84,5 +84,7 @@ module ImplInfoStore : sig
       [None] even though the supplied identifier points to an [Impl] block. *)
 end
 
+val def_id_to_rust_ast : Types.def_id_contents -> Types.def_id_inner
+val def_id_from_rust_ast : Types.def_id_inner -> Types.def_id_contents
 val to_rust_ast : t -> Rust_engine_types.explicit_def_id
 val from_rust_ast : Rust_engine_types.explicit_def_id -> t
diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml
index 4e555ead4..d37424a8e 100644
--- a/engine/lib/diagnostics.ml
+++ b/engine/lib/diagnostics.ml
@@ -10,6 +10,7 @@ module Phase = struct
   module Rejection = struct
     type t =
       | NotInBackendLang of Backend.t
+      | CoercionForUntypedPhase of string
       | ArbitraryLhs
       | Continue
       | Break
diff --git a/engine/lib/export_ast.ml b/engine/lib/export_ast.ml
index d02ee49da..9cbde557f 100644
--- a/engine/lib/export_ast.ml
+++ b/engine/lib/export_ast.ml
@@ -6,50 +6,71 @@ type missing_type = unit
 
 module B = Rust_engine_types
 
+let to_error_node (span : Ast.span) (payload : string) : Types.error_node =
+  try [%of_yojson: Types.error_node] (Yojson.Safe.from_string payload)
+  with _ ->
+    let diagnostic : Types.diagnostic =
+      let node : Types.fragment = Unknown "OCamlEngineError" in
+      let info : B.diagnostic_info =
+        {
+          context = Import;
+          kind = OcamlEngineErrorPayload payload;
+          span = Span.to_rust_ast_span span;
+        }
+      in
+      { node; info }
+    in
+
+    { fragment = Unknown "OCamlEngineError"; diagnostics = [ diagnostic ] }
+
 module Make (FA : Features.T) = struct
   open Ast
   module A = Ast.Make (FA)
+  module U = Ast_utils.Make (FA)
 
   let dsafety_kind (safety : A.safety_kind) : B.safety_kind =
     match safety with Safe -> B.Safe | Unsafe _ -> B.Unsafe
 
-  let rec dty (ty : A.ty) : B.ty =
-    match ty with
-    | TBool -> Newtypety (Primitive Bool)
-    | TChar -> Newtypety (Primitive Char)
-    | TInt k -> Newtypety (Primitive (Int (dint_kind k)))
-    | TFloat k -> Newtypety (Primitive (Float (dfloat_kind k)))
-    | TStr -> Newtypety (Primitive Str)
-    | TApp { ident; args } ->
-        Newtypety
-          (B.App
-             {
-               head = dglobal_ident ident;
-               args = List.map ~f:dgeneric_value args;
-             })
-    | TArray { typ; length } ->
-        Newtypety (Array { ty = dty typ; length = dexpr length })
-    | TSlice { witness = _; ty } -> Newtypety (Slice (dty ty))
-    | TRef { witness = _; typ; mut; region = _ } ->
-        Newtypety
-          (Ref
-             {
-               inner = dty typ;
-               mutable' = (match mut with Mutable _ -> true | _ -> false);
-               region = B.EmptyStructregion2;
-             })
-    | TParam local_ident -> Newtypety (Param (dlocal_ident local_ident))
-    | TArrow (inputs, output) ->
-        Newtypety
-          (Arrow { inputs = List.map ~f:dty inputs; output = dty output })
-    | TAssociatedType { impl; item } ->
-        Newtypety
-          (AssociatedType
-             { impl_ = dimpl_expr impl; item = dconcrete_ident item })
-    | TOpaque ident -> Newtypety (Opaque (dconcrete_ident ident))
-    | TRawPointer { witness = _ } -> Newtypety RawPointer
-    | TDyn { witness = _; goals } ->
-        Newtypety (Dyn (List.map ~f:ddyn_trait_goal goals))
+  let rec dty_no_error (span : Ast.span) (ty : A.ty) : B.ty =
+    Newtypety
+      (match ty with
+      | TBool -> Primitive Bool
+      | TChar -> Primitive Char
+      | TInt k -> Primitive (Int (dint_kind k))
+      | TFloat k -> Primitive (Float (dfloat_kind k))
+      | TStr -> Primitive Str
+      | TApp { ident; args } ->
+          B.App
+            {
+              head = dglobal_ident ident;
+              args = List.map ~f:(dgeneric_value span) args;
+            }
+      | TArray { typ; length } ->
+          Array { ty = dty span typ; length = dexpr length }
+      | TSlice { witness = _; ty } -> Slice (dty span ty)
+      | TRef { witness = _; typ; mut; region = _ } ->
+          Ref
+            {
+              inner = dty span typ;
+              mutable' = (match mut with Mutable _ -> true | _ -> false);
+              region = B.EmptyStructregion2;
+            }
+      | TParam local_ident -> Param (dlocal_ident local_ident)
+      | TArrow (inputs, output) ->
+          Arrow
+            { inputs = List.map ~f:(dty span) inputs; output = dty span output }
+      | TAssociatedType { impl; item } ->
+          AssociatedType
+            { impl_ = dimpl_expr span impl; item = dconcrete_ident item }
+      | TOpaque ident -> Opaque (dconcrete_ident ident)
+      | TRawPointer { witness = _ } -> RawPointer
+      | TDyn { witness = _; goals } ->
+          Dyn (List.map ~f:(ddyn_trait_goal span) goals))
+
+  and dty (span : Ast.span) (ty : A.ty) : B.ty =
+    match U.HaxFailure.Destruct.ty ty with
+    | Some s -> Newtypety (Error (to_error_node span s))
+    | None -> dty_no_error span ty
 
   and dint_kind (ik : int_kind) : B.int_kind =
     let size : B.int_size =
@@ -96,56 +117,60 @@ module Make (FA : Features.T) = struct
   and dconcrete_ident (gi : concrete_ident) : B.global_id =
     dglobal_ident (`Concrete gi)
 
-  and ddyn_trait_goal (r : A.dyn_trait_goal) : B.dyn_trait_goal =
+  and ddyn_trait_goal span (r : A.dyn_trait_goal) : B.dyn_trait_goal =
     {
-      non_self_args = List.map ~f:dgeneric_value r.non_self_args;
+      non_self_args = List.map ~f:(dgeneric_value span) r.non_self_args;
       trait_ = dconcrete_ident r.trait;
     }
 
-  and dtrait_goal (r : A.trait_goal) : B.trait_goal =
+  and dtrait_goal span (r : A.trait_goal) : B.trait_goal =
     {
-      args = List.map ~f:dgeneric_value r.args;
+      args = List.map ~f:(dgeneric_value span) r.args;
       trait_ = dconcrete_ident r.trait;
     }
 
-  and dimpl_ident (r : A.impl_ident) : B.impl_ident =
-    { goal = dtrait_goal r.goal; name = Newtypesymbol r.name }
+  and dimpl_ident span (r : A.impl_ident) : B.impl_ident =
+    { goal = dtrait_goal span r.goal; name = Newtypesymbol r.name }
 
-  and dprojection_predicate (r : A.projection_predicate) :
+  and dprojection_predicate span (r : A.projection_predicate) :
       B.projection_predicate =
     {
       assoc_item = dconcrete_ident r.assoc_item;
-      impl_ = dimpl_expr r.impl;
-      ty = dty r.typ;
+      impl_ = dimpl_expr span r.impl;
+      ty = dty span r.typ;
     }
 
-  and dimpl_expr (i : A.impl_expr) : B.impl_expr =
-    { goal = dtrait_goal i.goal; kind = dimpl_expr_kind i.kind }
+  and dimpl_expr span (i : A.impl_expr) : B.impl_expr =
+    { goal = dtrait_goal span i.goal; kind = dimpl_expr_kind span i.kind }
 
-  and dimpl_expr_kind (i : A.impl_expr_kind) : B.impl_expr_kind =
+  and dimpl_expr_kind span (i : A.impl_expr_kind) : B.impl_expr_kind =
     match i with
     | A.Self -> B.Self_
-    | A.Concrete tr -> B.Concrete (dtrait_goal tr)
+    | A.Concrete tr -> B.Concrete (dtrait_goal span tr)
     | A.LocalBound { id } -> B.LocalBound { id = B.Newtypesymbol id }
     | A.Parent { impl; ident } ->
-        B.Parent { impl_ = dimpl_expr impl; ident = dimpl_ident ident }
+        B.Parent
+          { impl_ = dimpl_expr span impl; ident = dimpl_ident span ident }
     | A.Projection { impl; item; ident } ->
         B.Projection
           {
-            impl_ = dimpl_expr impl;
+            impl_ = dimpl_expr span impl;
             item = dconcrete_ident item;
-            ident = dimpl_ident ident;
+            ident = dimpl_ident span ident;
           }
     | A.ImplApp { impl; args } ->
         B.ImplApp
-          { impl_ = dimpl_expr impl; args = List.map ~f:dimpl_expr args }
+          {
+            impl_ = dimpl_expr span impl;
+            args = List.map ~f:(dimpl_expr span) args;
+          }
     | A.Dyn -> B.Dyn
-    | A.Builtin tr -> B.Builtin (dtrait_goal tr)
+    | A.Builtin tr -> B.Builtin (dtrait_goal span tr)
 
-  and dgeneric_value (generic_value : A.generic_value) : B.generic_value =
+  and dgeneric_value span (generic_value : A.generic_value) : B.generic_value =
     match generic_value with
     | GLifetime _ -> B.Lifetime
-    | GType t -> B.Ty (dty t)
+    | GType t -> B.Ty (dty span t)
     | GConst e -> B.Expr (dexpr e)
 
   and dborrow_kind (borrow_kind : A.borrow_kind) : B.borrow_kind =
@@ -168,14 +193,19 @@ module Make (FA : Features.T) = struct
     { kind; span = dspan a.span }
 
   and dpat (p : A.pat) : B.pat =
-    { kind = dpat' p.p; meta = dmetadata p.span; ty = dty p.typ }
+    let kind : B.pat_kind =
+      match U.HaxFailure.Destruct.pat p with
+      | Some s -> Error (to_error_node p.span s)
+      | _ -> dpat' p.span p.p
+    in
+    { kind; meta = dmetadata p.span; ty = dty p.span p.typ }
 
-  and dpat' (pat : A.pat') : B.pat_kind =
+  and dpat' span (pat : A.pat') : B.pat_kind =
     match pat with
     | PWild -> Wild
     | PAscription { typ; typ_span; pat } ->
         Ascription
-          { pat = dpat pat; ty = { span = dspan typ_span; ty = dty typ } }
+          { pat = dpat pat; ty = { span = dspan typ_span; ty = dty span typ } }
     | PConstruct { constructor; is_record; is_struct; fields } ->
         Construct
           {
@@ -201,7 +231,7 @@ module Make (FA : Features.T) = struct
             sub_pat = Option.map ~f:(fun (p, _) -> dpat p) subpat;
           }
 
-  and dspan : span -> B.span = Span.to_span2
+  and dspan : span -> B.span = Span.to_rust_ast_span
 
   and dbinding_mode (binding_mode : A.binding_mode) : B.binding_mode =
     match binding_mode with
@@ -209,9 +239,14 @@ module Make (FA : Features.T) = struct
     | ByRef (kind, _witness) -> B.ByRef (dborrow_kind kind)
 
   and dexpr (e : A.expr) : B.expr =
-    { kind = dexpr' e.e; ty = dty e.typ; meta = dmetadata e.span }
+    let kind : B.expr_kind =
+      match U.HaxFailure.Destruct.expr e with
+      | Some (s, _) -> Error (to_error_node e.span s)
+      | None -> dexpr' e.span e.e
+    in
+    { kind; ty = dty e.span e.typ; meta = dmetadata e.span }
 
-  and dexpr' (expr : A.expr') : B.expr_kind =
+  and dexpr' span (expr : A.expr') : B.expr_kind =
     match expr with
     | If { cond; then_; else_ } ->
         If
@@ -225,12 +260,12 @@ module Make (FA : Features.T) = struct
           {
             head = dexpr f;
             args = List.map ~f:dexpr args;
-            generic_args = List.map ~f:dgeneric_value generic_args;
-            bounds_impls = List.map ~f:dimpl_expr bounds_impls;
+            generic_args = List.map ~f:(dgeneric_value span) generic_args;
+            bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls;
             trait_ =
               Option.map
                 ~f:(fun (impl, args) ->
-                  (dimpl_expr impl, List.map ~f:dgeneric_value args))
+                  (dimpl_expr span impl, List.map ~f:(dgeneric_value span) args))
                 trait;
           }
     | Literal lit -> Literal (dliteral lit)
@@ -253,30 +288,35 @@ module Make (FA : Features.T) = struct
         Block { body = dexpr e; safety_mode = dsafety_kind safety_mode }
     | LocalVar id -> LocalId (dlocal_ident id)
     | GlobalVar id -> GlobalId (dglobal_ident id)
-    | Ascription { e; typ } -> Ascription { e = dexpr e; ty = dty typ }
+    | Ascription { e; typ } -> Ascription { e = dexpr e; ty = dty span typ }
     | MacroInvokation _ -> deprecated_node "MacroInvokation"
     | Assign { lhs; e; witness = _ } ->
-        Assign { lhs = dlhs lhs; value = dexpr e }
+        Assign { lhs = dlhs span lhs; value = dexpr e }
     | Loop { body; kind; state; control_flow; label; witness = _ } ->
         Loop
           {
             body = dexpr body;
-            kind = dloop_kind kind;
+            kind = dloop_kind span kind;
             state = Option.map ~f:dloop_state state;
             control_flow =
               Option.map ~f:(fun (k, _) -> dcontrol_flow_kind k) control_flow;
             label = Option.map ~f:(fun s -> B.Newtypesymbol s) label;
           }
-    | Break { e; acc = _; label; witness = _ } ->
+    | Break { e; acc; label; witness = _ } ->
         Break
           {
             value = dexpr e;
             label = Option.map ~f:(fun s -> B.Newtypesymbol s) label;
+            state = Option.map ~f:(fst >> dexpr) acc;
           }
     | Return { e; witness = _ } -> Return { value = dexpr e }
     | QuestionMark _ -> deprecated_node "QuestionMark"
-    | Continue { acc = _; label; witness = _ } ->
-        Continue { label = Option.map ~f:(fun s -> B.Newtypesymbol s) label }
+    | Continue { acc; label; witness = _ } ->
+        Continue
+          {
+            label = Option.map ~f:(fun s -> B.Newtypesymbol s) label;
+            state = Option.map ~f:(fst >> dexpr) acc;
+          }
     | Borrow { kind; e; witness = _ } ->
         Borrow
           {
@@ -297,7 +337,7 @@ module Make (FA : Features.T) = struct
             captures = List.map ~f:dexpr captures;
           }
     | EffectAction _ -> deprecated_node "EffectAction"
-    | Quote q -> Quote { contents = dquote q }
+    | Quote q -> Quote { contents = dquote span q }
 
   and dcontrol_flow_kind (cfk : A.cf_kind) : B.control_flow_kind =
     match cfk with BreakOnly -> B.BreakOnly | BreakOrReturn -> B.BreakOrReturn
@@ -313,12 +353,12 @@ module Make (FA : Features.T) = struct
           { value = Newtypesymbol value; negative; kind = dfloat_kind kind }
     | Bool b -> B.Bool b
 
-  and dquote ({ contents; _ } : A.quote) : B.quote =
+  and dquote span ({ contents; _ } : A.quote) : B.quote =
     let f = function
       | A.Verbatim code -> B.Verbatim code
       | A.Expr e -> B.Expr (dexpr e)
       | A.Pattern p -> B.Pattern (dpat p)
-      | A.Typ t -> B.Ty (dty t)
+      | A.Typ t -> B.Ty (dty span t)
     in
     Newtypequote (List.map ~f contents)
 
@@ -345,7 +385,7 @@ module Make (FA : Features.T) = struct
         | `Replace -> B.Replace);
     }
 
-  and dloop_kind (k : A.loop_kind) : B.loop_kind =
+  and dloop_kind span (k : A.loop_kind) : B.loop_kind =
     match k with
     | A.UnconditionalLoop -> B.UnconditionalLoop
     | A.WhileLoop { condition; witness = _ } ->
@@ -358,7 +398,7 @@ module Make (FA : Features.T) = struct
             start = dexpr start;
             end' = dexpr end_;
             var = dlocal_ident var;
-            var_ty = dty var_typ;
+            var_ty = dty span var_typ;
           }
 
   and dloop_state (s : A.loop_state) : B.loop_state =
@@ -380,16 +420,17 @@ module Make (FA : Features.T) = struct
     | IfLet { lhs; rhs; witness = _ } ->
         B.IfLet { lhs = dpat lhs; rhs = dexpr rhs }
 
-  and dlhs (lhs : A.lhs) : B.lhs =
+  and dlhs span (lhs : A.lhs) : B.lhs =
     match lhs with
     | A.LhsLocalVar { var; typ } ->
-        B.LocalVar { var = dlocal_ident var; ty = dty typ }
+        B.LocalVar { var = dlocal_ident var; ty = dty span typ }
     | A.LhsArbitraryExpr { e; witness = _ } -> B.ArbitraryExpr (dexpr e)
     | A.LhsFieldAccessor { e; field; typ; witness = _ } ->
         B.FieldAccessor
-          { e = dlhs e; field = dglobal_ident field; ty = dty typ }
+          { e = dlhs span e; field = dglobal_ident field; ty = dty span typ }
     | A.LhsArrayAccessor { e; index; typ; witness = _ } ->
-        B.ArrayAccessor { e = dlhs e; index = dexpr index; ty = dty typ }
+        B.ArrayAccessor
+          { e = dlhs span e; index = dexpr index; ty = dty span typ }
 
   let dgeneric_param ({ ident; span; attrs; kind } : A.generic_param) :
       B.generic_param =
@@ -397,111 +438,113 @@ module Make (FA : Features.T) = struct
       match kind with
       | GPLifetime { witness = _ } -> Lifetime
       | GPType -> Type
-      | GPConst { typ } -> Const { ty = dty typ }
+      | GPConst { typ } -> Const { ty = dty span typ }
     in
     { ident = dlocal_ident ident; meta = dmetadata ~attrs span; kind }
 
-  let dgeneric_constraint (generic_constraint : A.generic_constraint) :
+  let dgeneric_constraint span (generic_constraint : A.generic_constraint) :
       B.generic_constraint =
     match generic_constraint with
     | GCLifetime (lf, _witness) -> Lifetime lf
-    | GCType impl_ident -> Type (dimpl_ident impl_ident)
-    | GCProjection projection -> Projection (dprojection_predicate projection)
+    | GCType impl_ident -> Type (dimpl_ident span impl_ident)
+    | GCProjection projection ->
+        Projection (dprojection_predicate span projection)
 
-  let dgenerics (g : A.generics) : B.generics =
+  let dgenerics span (g : A.generics) : B.generics =
     {
-      constraints = List.map ~f:dgeneric_constraint g.constraints;
+      constraints = List.map ~f:(dgeneric_constraint span) g.constraints;
       params = List.map ~f:dgeneric_param g.params;
     }
 
-  let dparam (p : A.param) : B.param =
+  let dparam span (p : A.param) : B.param =
     {
       attributes = List.map ~f:dattr p.attrs;
       pat = dpat p.pat;
-      ty = dty p.typ;
+      ty = dty span p.typ;
       ty_span = Option.map ~f:dspan p.typ_span;
     }
 
-  let dvariant (v : A.variant) : B.variant =
+  let dvariant span (v : A.variant) : B.variant =
     let dattrs = List.map ~f:dattr in
     {
       arguments =
         List.map
-          ~f:(fun (id, t, a) -> (dconcrete_ident id, dty t, dattrs a))
+          ~f:(fun (id, t, a) -> (dconcrete_ident id, dty span t, dattrs a))
           v.arguments;
       attributes = dattrs v.attrs;
       is_record = v.is_record;
       name = dconcrete_ident v.name;
     }
 
-  let dtrait_item' (ti : A.trait_item') : B.trait_item_kind =
+  let dtrait_item' span (ti : A.trait_item') : B.trait_item_kind =
     match ti with
-    | TIType idents -> Type (List.map ~f:dimpl_ident idents)
-    | TIFn t -> Fn (dty t)
+    | TIType idents -> Type (List.map ~f:(dimpl_ident span) idents)
+    | TIFn t -> Fn (dty span t)
     | TIDefault { params; body; witness = _ } ->
-        Default { params = List.map ~f:dparam params; body = dexpr body }
+        Default { params = List.map ~f:(dparam span) params; body = dexpr body }
 
   let dtrait_item (ti : A.trait_item) : B.trait_item =
     {
-      generics = dgenerics ti.ti_generics;
+      generics = dgenerics ti.ti_span ti.ti_generics;
       ident = dconcrete_ident ti.ti_ident;
-      kind = dtrait_item' ti.ti_v;
+      kind = dtrait_item' ti.ti_span ti.ti_v;
       meta = dmetadata ~attrs:ti.ti_attrs ti.ti_span;
     }
 
-  let dimpl_item' (ii : A.impl_item') : B.impl_item_kind =
+  let dimpl_item' span (ii : A.impl_item') : B.impl_item_kind =
     match ii with
     | IIType { typ; parent_bounds } ->
         Type
           {
-            ty = dty typ;
+            ty = dty span typ;
             parent_bounds =
-              List.map ~f:(dimpl_expr *** dimpl_ident) parent_bounds;
+              List.map ~f:(dimpl_expr span *** dimpl_ident span) parent_bounds;
           }
     | IIFn { body; params } ->
-        Fn { body = dexpr body; params = List.map ~f:dparam params }
+        Fn { body = dexpr body; params = List.map ~f:(dparam span) params }
 
   let dimpl_item (ii : A.impl_item) : B.impl_item =
     {
-      generics = dgenerics ii.ii_generics;
+      generics = dgenerics ii.ii_span ii.ii_generics;
       ident = dconcrete_ident ii.ii_ident;
-      kind = dimpl_item' ii.ii_v;
+      kind = dimpl_item' ii.ii_span ii.ii_v;
       meta = dmetadata ~attrs:ii.ii_attrs ii.ii_span;
     }
 
-  let ditem' (item : A.item') (span : Types.span2) : B.item_kind =
+  let ditem' (span : Ast.span) (item : A.item') : B.item_kind =
     match item with
     | A.Fn { name; generics; body; params; safety } ->
         B.Fn
           {
             name = dconcrete_ident name;
-            generics = dgenerics generics;
+            generics = dgenerics span generics;
             body = dexpr body;
-            params = List.map ~f:dparam params;
+            params = List.map ~f:(dparam span) params;
             safety = dsafety_kind safety;
           }
     | A.Type { name; generics; variants; is_struct } ->
         B.Type
           {
             name = dconcrete_ident name;
-            generics = dgenerics generics;
-            variants = List.map ~f:dvariant variants;
+            generics = dgenerics span generics;
+            variants = List.map ~f:(dvariant span) variants;
             is_struct;
           }
     | A.TyAlias { name; generics; ty } ->
         B.TyAlias
           {
             name = dconcrete_ident name;
-            generics = dgenerics generics;
-            ty = dty ty;
+            generics = dgenerics span generics;
+            ty = dty span ty;
           }
     | A.IMacroInvokation _ -> deprecated_node "IMacroInvokation"
-    | A.Trait { name; generics; items; safety = _ } ->
+    | A.Trait { name; generics; items; safety } ->
         B.Trait
           {
             name = dconcrete_ident name;
-            generics = dgenerics generics;
+            generics = dgenerics span generics;
             items = List.map ~f:dtrait_item items;
+            safety = dsafety_kind safety;
           }
     | A.Impl
         {
@@ -514,15 +557,16 @@ module Make (FA : Features.T) = struct
         } ->
         B.Impl
           {
-            generics = dgenerics generics;
-            self_ty = dty self_ty;
+            generics = dgenerics span generics;
+            self_ty = dty span self_ty;
             of_trait =
               ( dconcrete_ident trait_id,
-                List.map ~f:dgeneric_value trait_generics );
+                List.map ~f:(dgeneric_value span) trait_generics );
             items = List.map ~f:dimpl_item items;
             parent_bounds =
               List.map
-                ~f:(fun (impl, ident) -> (dimpl_expr impl, dimpl_ident ident))
+                ~f:(fun (impl, ident) ->
+                  (dimpl_expr span impl, dimpl_ident span ident))
                 parent_bounds;
             safety = dsafety_kind safety;
           }
@@ -530,20 +574,16 @@ module Make (FA : Features.T) = struct
         B.Alias { name = dconcrete_ident name; item = dconcrete_ident item }
     | A.Use { path; is_external; rename } -> B.Use { path; is_external; rename }
     | A.Quote { quote; origin } ->
-        B.Quote { quote = dquote quote; origin = ditem_quote_origin origin }
-    | A.HaxError details ->
-        let fragment : Types.fragment = Unknown "HaxError" in
-        let info : B.diagnostic_info =
-          { context = Import; kind = AssertionFailure { details }; span }
-        in
-        Error { fragment; diagnostics = [ { node = fragment; info } ] }
+        B.Quote
+          { quote = dquote span quote; origin = ditem_quote_origin origin }
     | A.NotImplementedYet -> B.NotImplementedYet
+    | A.HaxError s -> Error (to_error_node span s)
 
   let ditem (i : A.item) : B.item list =
     [
       {
         ident = dconcrete_ident i.ident;
-        kind = ditem' i.v (dspan i.span);
+        kind = ditem' i.span i.v;
         meta = dmetadata ~attrs:i.attrs i.span;
       };
     ]
diff --git a/engine/lib/import_ast.ml b/engine/lib/import_ast.ml
new file mode 100644
index 000000000..90f8dd967
--- /dev/null
+++ b/engine/lib/import_ast.ml
@@ -0,0 +1,624 @@
+open! Prelude
+
+let refute_resugared s =
+  failwith
+    ("Got a resugared node at " ^ s
+   ^ ". The AST is never supposed to be sent to the OCaml engine with \
+      resugared nodes.")
+
+let broken_invariant s = failwith s
+
+type missing_type = unit
+
+module A = Rust_engine_types
+module F = Features.Full
+
+module B = struct
+  include Ast
+  include Ast.Make (F)
+end
+
+module U = Ast_utils.Make (F)
+module Build = Ast_builder.Make (F)
+
+let from_error_node (error_node : Types.error_node) : string =
+  match (error_node.fragment, error_node.diagnostics) with
+  | ( Unknown "OCamlEngineError",
+      [
+        {
+          node = Unknown "OCamlEngineError";
+          info = { kind = OcamlEngineErrorPayload payload; _ };
+          _;
+        };
+      ] ) ->
+      payload
+  | _ -> [%yojson_of: Types.error_node] error_node |> Yojson.Safe.to_string
+
+let dsafety_kind (safety : A.safety_kind) : B.safety_kind =
+  match safety with Safe -> B.Safe | Unsafe -> B.Unsafe F.unsafe
+
+let rec dty (Newtypety ty : A.ty) : B.ty =
+  match ty with
+  | Primitive Bool -> TBool
+  | Primitive Char -> TChar
+  | Primitive (Int k) -> TInt (dint_kind k)
+  | Primitive (Float k) -> TFloat (dfloat_kind k)
+  | Primitive Str -> TStr
+  | App { head; args } ->
+      TApp
+        { ident = dglobal_ident head; args = List.map ~f:dgeneric_value args }
+  | Array { ty; length } -> TArray { typ = dty ty; length = dexpr length }
+  | Slice ty -> TSlice { ty = dty ty; witness = F.slice }
+  | Ref { inner; mutable'; region = _ } ->
+      TRef
+        {
+          witness = F.reference;
+          typ = dty inner;
+          mut = (if mutable' then Mutable F.mutable_reference else Immutable);
+          region = "unknown";
+        }
+  | Param local_ident -> TParam (dlocal_ident local_ident)
+  | Arrow { inputs; output } -> TArrow (List.map ~f:dty inputs, dty output)
+  | AssociatedType { impl_; item } ->
+      TAssociatedType { impl = dimpl_expr impl_; item = dconcrete_ident item }
+  | Opaque ident -> TOpaque (dconcrete_ident ident)
+  | RawPointer -> TRawPointer { witness = F.raw_pointer }
+  | Dyn goals ->
+      TDyn { witness = F.dyn; goals = List.map ~f:ddyn_trait_goal goals }
+  | Resugared _ -> refute_resugared "ty"
+  | Error s -> U.HaxFailure.Build.ty (from_error_node s)
+
+and dint_kind (ik : A.int_kind) : B.int_kind =
+  let size : B.size =
+    match ik.size with
+    | S8 -> S8
+    | S16 -> S16
+    | S32 -> S32
+    | S64 -> S64
+    | S128 -> S128
+    | SSize -> SSize
+  in
+  {
+    size;
+    signedness =
+      (match ik.signedness with Signed -> Signed | Unsigned -> Unsigned);
+  }
+
+and dfloat_kind (fk : A.float_kind) : B.float_kind =
+  match fk with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128
+
+and dglobal_ident (Newtypeglobal_id gi : A.global_id) : B.global_ident =
+  match gi with
+  | Types.Concrete c -> (
+      let ci = Concrete_ident.from_rust_ast c in
+      match c.def_id.def_id.kind with
+      | Field -> `Projector (`Concrete ci)
+      | _ ->
+          let is name = Concrete_ident.eq_name name ci in
+          if is Rust_primitives__hax__deref_op then `Primitive Deref
+          else if is Rust_primitives__hax__cast_op then `Primitive Cast
+          else if is Rust_primitives__hax__logical_op_and then
+            `Primitive (LogicalOp And)
+          else if is Rust_primitives__hax__logical_op_or then
+            `Primitive (LogicalOp Or)
+          else `Concrete ci)
+  | Types.Tuple t -> (
+      match t with
+      | Types.Type { length } -> `TupleType (Int.of_string length)
+      | Types.Constructor { length } -> `TupleCons (Int.of_string length)
+      | Types.Field { length; field } ->
+          `TupleField (Int.of_string field, Int.of_string length))
+
+and dlocal_ident (Newtypelocal_id (Newtypesymbol li) : A.local_id) :
+    B.local_ident =
+  { id = (Expr, 0); name = li }
+
+and dconcrete_ident (gi : A.global_id) : B.concrete_ident =
+  match dglobal_ident gi with
+  | `Concrete id -> id
+  (* For variant fields *)
+  | `Projector (`Concrete id) -> id
+  | _ ->
+      broken_invariant
+        ("dconcrete_ident: got something else than a [`Concrete _]: "
+        ^ [%show: A.global_id] gi)
+
+and ddyn_trait_goal (r : A.dyn_trait_goal) : B.dyn_trait_goal =
+  {
+    non_self_args = List.map ~f:dgeneric_value r.non_self_args;
+    trait = dconcrete_ident r.trait_;
+  }
+
+and dtrait_goal (r : A.trait_goal) : B.trait_goal =
+  { args = List.map ~f:dgeneric_value r.args; trait = dconcrete_ident r.trait_ }
+
+and dimpl_ident (r : A.impl_ident) : B.impl_ident =
+  {
+    goal = dtrait_goal r.goal;
+    name = (match r.name with Newtypesymbol name -> name);
+  }
+
+and dprojection_predicate (r : A.projection_predicate) : B.projection_predicate
+    =
+  {
+    assoc_item = dconcrete_ident r.assoc_item;
+    impl = dimpl_expr r.impl_;
+    typ = dty r.ty;
+  }
+
+and dimpl_expr (i : A.impl_expr) : B.impl_expr =
+  { goal = dtrait_goal i.goal; kind = dimpl_expr_kind i.kind }
+
+and dimpl_expr_kind (i : A.impl_expr_kind) : B.impl_expr_kind =
+  match i with
+  | A.Self_ -> B.Self
+  | A.Concrete tr -> B.Concrete (dtrait_goal tr)
+  | A.LocalBound { id = A.Newtypesymbol id } -> B.LocalBound { id }
+  | A.Parent { impl_; ident } ->
+      B.Parent { impl = dimpl_expr impl_; ident = dimpl_ident ident }
+  | A.Projection { impl_; item; ident } ->
+      B.Projection
+        {
+          impl = dimpl_expr impl_;
+          item = dconcrete_ident item;
+          ident = dimpl_ident ident;
+        }
+  | A.ImplApp { impl_; args } ->
+      B.ImplApp { impl = dimpl_expr impl_; args = List.map ~f:dimpl_expr args }
+  | A.Dyn -> B.Dyn
+  | A.Builtin tr -> B.Builtin (dtrait_goal tr)
+
+and dgeneric_value (generic_value : A.generic_value) : B.generic_value =
+  match generic_value with
+  | Lifetime -> B.GLifetime { lt = ""; witness = F.lifetime }
+  | Ty t -> B.GType (dty t)
+  | Expr e -> B.GConst (dexpr e)
+
+and dborrow_kind (borrow_kind : A.borrow_kind) : B.borrow_kind =
+  match borrow_kind with
+  | Shared -> B.Shared
+  | Unique -> B.Unique
+  | Mut -> B.Mut F.mutable_reference
+
+and dattributes (m : A.attribute2 list) : B.attrs = List.map ~f:dattr m
+and dspan = Span.from_rust_ast_span
+
+and dattr (a : A.attribute) : B.attr =
+  let kind : B.attr_kind =
+    match a.kind with
+    | Tool { path; tokens } -> B.Tool { path; tokens }
+    | DocComment { kind; body } ->
+        let kind = match kind with Line -> B.DCKLine | Block -> DCKBlock in
+        B.DocComment { kind; body }
+  in
+  { kind; span = dspan a.span }
+
+and dpat (p : A.pat) : B.pat =
+  let typ = dty p.ty in
+  let span = dspan p.meta.span in
+  { p = dpat' span typ p.kind; span; typ }
+
+and dpat' span parent_ty (pat : A.pat_kind) : B.pat' =
+  match pat with
+  | Wild -> PWild
+  | Ascription { pat; ty = { ty; span } } ->
+      PAscription { pat = dpat pat; typ_span = dspan span; typ = dty ty }
+  | Construct { constructor; is_record; is_struct; fields } ->
+      PConstruct
+        {
+          constructor = dglobal_ident constructor;
+          is_record;
+          is_struct;
+          fields =
+            List.map
+              ~f:(fun (field, pat) ->
+                B.{ field = dglobal_ident field; pat = dpat pat })
+              fields;
+        }
+  | Or { sub_pats } -> POr { subpats = List.map ~f:dpat sub_pats }
+  | Array { args } -> PArray { args = List.map ~f:dpat args }
+  | Deref { sub_pat } -> PDeref { subpat = dpat sub_pat; witness = F.reference }
+  | Constant { lit } -> PConstant { lit = dliteral lit }
+  | Binding { mutable'; mode; var; sub_pat } ->
+      let mut = if mutable' then B.Mutable F.mutable_variable else Immutable in
+      PBinding
+        {
+          mut;
+          mode = dbinding_mode mode;
+          var = dlocal_ident var;
+          subpat = Option.map ~f:(fun p -> (dpat p, F.as_pattern)) sub_pat;
+          typ = parent_ty;
+        }
+  | Resugared _ -> refute_resugared "ty"
+  | Error diag ->
+      let s = from_error_node diag in
+      (U.HaxFailure.Build.pat span parent_ty s).p
+
+and dbinding_mode (binding_mode : A.binding_mode) : B.binding_mode =
+  match binding_mode with
+  | ByValue -> B.ByValue
+  | ByRef kind -> B.ByRef (dborrow_kind kind, F.reference)
+
+and dexpr (e : A.expr) : B.expr =
+  let typ = dty e.ty in
+  let span = dspan e.meta.span in
+  { e = dexpr' span typ e.kind; typ; span }
+
+and dexpr' span typ (expr : A.expr_kind) : B.expr' =
+  match expr with
+  | If { condition; then'; else_ } ->
+      If
+        {
+          cond = dexpr condition;
+          then_ = dexpr then';
+          else_ = Option.map ~f:dexpr else_;
+        }
+  | App { head; args; generic_args; bounds_impls; trait_ } ->
+      App
+        {
+          f = dexpr head;
+          args = List.map ~f:dexpr args;
+          generic_args = List.map ~f:dgeneric_value generic_args;
+          bounds_impls = List.map ~f:dimpl_expr bounds_impls;
+          trait =
+            Option.map
+              ~f:(fun (impl, args) ->
+                (dimpl_expr impl, List.map ~f:dgeneric_value args))
+              trait_;
+        }
+  | Literal lit -> Literal (dliteral lit)
+  | Array exprs -> Array (List.map ~f:dexpr exprs)
+  | Construct { constructor; is_record; is_struct; fields; base } ->
+      Construct
+        {
+          constructor = dglobal_ident constructor;
+          fields =
+            List.map ~f:(fun (id, e) -> (dglobal_ident id, dexpr e)) fields;
+          base = Option.map ~f:(fun e -> (dexpr e, F.construct_base)) base;
+          is_record;
+          is_struct;
+        }
+  | Match { scrutinee; arms } ->
+      Match { scrutinee = dexpr scrutinee; arms = List.map ~f:darm arms }
+  | Let { lhs; rhs; body } ->
+      Let { lhs = dpat lhs; rhs = dexpr rhs; body = dexpr body; monadic = None }
+  | Block { body; safety_mode } ->
+      Block
+        {
+          e = dexpr body;
+          safety_mode = dsafety_kind safety_mode;
+          witness = F.block;
+        }
+  | LocalId id -> LocalVar (dlocal_ident id)
+  | GlobalId id -> GlobalVar (dglobal_ident id)
+  | Ascription { e; ty } -> Ascription { e = dexpr e; typ = dty ty }
+  | Assign { lhs; value } ->
+      Assign { lhs = dlhs lhs; e = dexpr value; witness = F.mutable_variable }
+  | Loop { body; kind; state; control_flow; label } ->
+      Loop
+        {
+          body = dexpr body;
+          kind = dloop_kind kind;
+          state = Option.map ~f:dloop_state state;
+          control_flow =
+            Option.map
+              ~f:(fun k -> (dcontrol_flow_kind k, F.fold_like_loop))
+              control_flow;
+          label = Option.map ~f:(fun (A.Newtypesymbol s) -> s) label;
+          witness = F.loop;
+        }
+  | Break { value; label; state } ->
+      Break
+        {
+          e = dexpr value;
+          label = Option.map ~f:(fun (A.Newtypesymbol s) -> s) label;
+          acc = Option.map ~f:(fun e -> (dexpr e, F.state_passing_loop)) state;
+          witness = (F.break, F.loop);
+        }
+  | Return { value } -> Return { e = dexpr value; witness = F.early_exit }
+  | Continue { label; state } ->
+      Continue
+        {
+          label = Option.map ~f:(fun (Newtypesymbol s) -> s) label;
+          acc = Option.map ~f:(fun e -> (dexpr e, F.state_passing_loop)) state;
+          witness = (F.continue, F.loop);
+        }
+  | Borrow { mutable'; inner } ->
+      Borrow
+        {
+          e = dexpr inner;
+          kind = (if mutable' then Mut F.mutable_reference else B.Shared);
+          witness = F.reference;
+        }
+  | AddressOf { mutable'; inner } ->
+      AddressOf
+        {
+          e = dexpr inner;
+          mut = (if mutable' then Mutable F.mutable_pointer else Immutable);
+          witness = F.raw_pointer;
+        }
+  | Closure { params; body; captures } ->
+      Closure
+        {
+          params = List.map ~f:dpat params;
+          body = dexpr body;
+          captures = List.map ~f:dexpr captures;
+        }
+  | Quote { contents } -> Quote (dquote contents)
+  | Resugared _ -> refute_resugared "expr"
+  | Error diag -> (U.HaxFailure.Build.expr span typ (from_error_node diag) "").e
+
+and dcontrol_flow_kind (cfk : A.control_flow_kind) : B.cf_kind =
+  match cfk with BreakOnly -> B.BreakOnly | BreakOrReturn -> B.BreakOrReturn
+
+and dliteral (l : A.literal) : B.literal =
+  match l with
+  | String (Newtypesymbol s) -> B.String s
+  | Char c -> B.Char c
+  | Int { value = Newtypesymbol value; negative; kind } ->
+      B.Int { value; negative; kind = dint_kind kind }
+  | Float { value = Newtypesymbol value; negative; kind } ->
+      B.Float { value; negative; kind = dfloat_kind kind }
+  | Bool b -> B.Bool b
+
+and dquote (Newtypequote contents : A.quote) : B.quote =
+  let f = function
+    | A.Verbatim code -> B.Verbatim code
+    | A.Expr e -> B.Expr (dexpr e)
+    | A.Pattern p -> B.Pattern (dpat p)
+    | A.Ty t -> B.Typ (dty t)
+  in
+  { contents = List.map ~f contents; witness = F.quote }
+
+and ditem_quote_origin (iqo : A.item_quote_origin) : B.item_quote_origin =
+  {
+    item_ident = dconcrete_ident iqo.item_ident;
+    item_kind =
+      (match iqo.item_kind with
+      | A.Fn -> `Fn
+      | A.TyAlias -> `TyAlias
+      | A.Type -> `Type
+      | A.MacroInvocation -> `IMacroInvokation
+      | A.Trait -> `Trait
+      | A.Impl -> `Impl
+      | A.Alias -> `Alias
+      | A.Use -> `Use
+      | A.Quote -> `Quote
+      | A.HaxError -> `HaxError
+      | A.NotImplementedYet -> `NotImplementedYet);
+    position =
+      (match iqo.position with
+      | A.Before -> `Before
+      | A.After -> `After
+      | A.Replace -> `Replace);
+  }
+
+and dloop_kind (k : A.loop_kind) : B.loop_kind =
+  match k with
+  | A.UnconditionalLoop -> B.UnconditionalLoop
+  | A.WhileLoop { condition } ->
+      B.WhileLoop { condition = dexpr condition; witness = F.while_loop }
+  | A.ForLoop { iterator; pat } ->
+      B.ForLoop { it = dexpr iterator; pat = dpat pat; witness = F.for_loop }
+  | A.ForIndexLoop { start; end'; var; var_ty } ->
+      B.ForIndexLoop
+        {
+          start = dexpr start;
+          end_ = dexpr end';
+          var = dlocal_ident var;
+          var_typ = dty var_ty;
+          witness = F.for_index_loop;
+        }
+
+and dloop_state (s : A.loop_state) : B.loop_state =
+  {
+    bpat = dpat s.body_pat;
+    init = dexpr s.init;
+    witness = F.state_passing_loop;
+  }
+
+and darm (a : A.arm) : B.arm =
+  {
+    arm =
+      {
+        body = dexpr a.body;
+        guard = Option.map ~f:dguard a.guard;
+        arm_pat = dpat a.pat;
+      };
+    span = dspan a.meta.span;
+  }
+
+and dguard (a : A.guard) : B.guard =
+  { guard = dguard' a.kind; span = dspan a.meta.span }
+
+and dguard' (guard : A.guard_kind) : B.guard' =
+  match guard with
+  | IfLet { lhs; rhs } ->
+      B.IfLet { lhs = dpat lhs; rhs = dexpr rhs; witness = F.match_guard }
+
+and dlhs (lhs : A.lhs) : B.lhs =
+  match lhs with
+  | A.LocalVar { var; ty } ->
+      B.LhsLocalVar { var = dlocal_ident var; typ = dty ty }
+  | A.ArbitraryExpr e ->
+      B.LhsArbitraryExpr { e = dexpr e; witness = F.arbitrary_lhs }
+  | A.FieldAccessor { e; field; ty } ->
+      B.LhsFieldAccessor
+        {
+          e = dlhs e;
+          field = dglobal_ident field;
+          typ = dty ty;
+          witness = F.nontrivial_lhs;
+        }
+  | A.ArrayAccessor { e; index; ty } ->
+      B.LhsArrayAccessor
+        {
+          e = dlhs e;
+          index = dexpr index;
+          typ = dty ty;
+          witness = F.nontrivial_lhs;
+        }
+
+let dgeneric_param ({ ident; meta; kind } : A.generic_param) : B.generic_param =
+  let kind : B.generic_param_kind =
+    match kind with
+    | Lifetime -> GPLifetime { witness = F.lifetime }
+    | Type -> GPType
+    | Const { ty } -> GPConst { typ = dty ty }
+  in
+  {
+    ident = dlocal_ident ident;
+    span = dspan meta.span;
+    attrs = dattributes meta.attributes;
+    kind;
+  }
+
+let dgeneric_constraint (generic_constraint : A.generic_constraint) :
+    B.generic_constraint =
+  match generic_constraint with
+  | Lifetime lf -> GCLifetime (lf, F.lifetime)
+  | Type impl_ident -> GCType (dimpl_ident impl_ident)
+  | Projection projection -> GCProjection (dprojection_predicate projection)
+
+let dgenerics (g : A.generics) : B.generics =
+  {
+    constraints = List.map ~f:dgeneric_constraint g.constraints;
+    params = List.map ~f:dgeneric_param g.params;
+  }
+
+let dparam (p : A.param) : B.param =
+  {
+    attrs = dattributes p.attributes;
+    pat = dpat p.pat;
+    typ = dty p.ty;
+    typ_span = Option.map ~f:dspan p.ty_span;
+  }
+
+let dvariant (v : A.variant) : B.variant =
+  {
+    arguments =
+      List.map
+        ~f:(fun (id, t, a) -> (dconcrete_ident id, dty t, dattributes a))
+        v.arguments;
+    attrs = dattributes v.attributes;
+    is_record = v.is_record;
+    name = dconcrete_ident v.name;
+  }
+
+let dtrait_item' (ti : A.trait_item_kind) : B.trait_item' =
+  match ti with
+  | Type idents -> TIType (List.map ~f:dimpl_ident idents)
+  | Fn t -> TIFn (dty t)
+  | Default { params; body } ->
+      TIDefault
+        {
+          params = List.map ~f:dparam params;
+          body = dexpr body;
+          witness = F.trait_item_default;
+        }
+  | Resugared _ -> refute_resugared "trait_item"
+
+let dtrait_item (ti : A.trait_item) : B.trait_item =
+  {
+    ti_generics = dgenerics ti.generics;
+    ti_ident = dconcrete_ident ti.ident;
+    ti_v = dtrait_item' ti.kind;
+    ti_span = dspan ti.meta.span;
+    ti_attrs = dattributes ti.meta.attributes;
+  }
+
+let dimpl_item' (ii : A.impl_item_kind) : B.impl_item' =
+  match ii with
+  | Type { ty; parent_bounds } ->
+      IIType
+        {
+          typ = dty ty;
+          parent_bounds = List.map ~f:(dimpl_expr *** dimpl_ident) parent_bounds;
+        }
+  | Fn { body; params } ->
+      IIFn { body = dexpr body; params = List.map ~f:dparam params }
+  | Resugared _ -> refute_resugared "impl_item"
+
+let dimpl_item (ii : A.impl_item) : B.impl_item =
+  {
+    ii_generics = dgenerics ii.generics;
+    ii_ident = dconcrete_ident ii.ident;
+    ii_v = dimpl_item' ii.kind;
+    ii_span = dspan ii.meta.span;
+    ii_attrs = dattributes ii.meta.attributes;
+  }
+
+let ditem' (item : A.item_kind) : B.item' =
+  match item with
+  | A.Fn { name; generics; body; params; safety } ->
+      B.Fn
+        {
+          name = dconcrete_ident name;
+          generics = dgenerics generics;
+          body = dexpr body;
+          params = List.map ~f:dparam params;
+          safety = dsafety_kind safety;
+        }
+  | A.Type { name; generics; variants; is_struct } ->
+      B.Type
+        {
+          name = dconcrete_ident name;
+          generics = dgenerics generics;
+          variants = List.map ~f:dvariant variants;
+          is_struct;
+        }
+  | A.TyAlias { name; generics; ty } ->
+      B.TyAlias
+        {
+          name = dconcrete_ident name;
+          generics = dgenerics generics;
+          ty = dty ty;
+        }
+  | A.Trait { name; generics; items; safety } ->
+      B.Trait
+        {
+          name = dconcrete_ident name;
+          generics = dgenerics generics;
+          items = List.map ~f:dtrait_item items;
+          safety = dsafety_kind safety;
+        }
+  | A.Impl
+      {
+        generics;
+        self_ty;
+        of_trait = trait_id, trait_generics;
+        items;
+        parent_bounds;
+        safety;
+      } ->
+      B.Impl
+        {
+          generics = dgenerics generics;
+          self_ty = dty self_ty;
+          of_trait =
+            (dconcrete_ident trait_id, List.map ~f:dgeneric_value trait_generics);
+          items = List.map ~f:dimpl_item items;
+          parent_bounds =
+            List.map
+              ~f:(fun (impl, ident) -> (dimpl_expr impl, dimpl_ident ident))
+              parent_bounds;
+          safety = dsafety_kind safety;
+        }
+  | A.Alias { name; item } ->
+      B.Alias { name = dconcrete_ident name; item = dconcrete_ident item }
+  | A.Use { path; is_external; rename } -> B.Use { path; is_external; rename }
+  | A.Quote { quote; origin } ->
+      B.Quote { quote = dquote quote; origin = ditem_quote_origin origin }
+  | A.Error diag -> HaxError (from_error_node diag)
+  | A.NotImplementedYet -> B.NotImplementedYet
+  | Resugared _ -> refute_resugared "item_kind"
+
+let ditem (i : A.item) : B.item list =
+  [
+    {
+      ident = dconcrete_ident i.ident;
+      v = ditem' i.kind;
+      span = dspan i.meta.span;
+      attrs = dattributes i.meta.attributes;
+    };
+  ]
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 5601b3727..0cb342a79 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -406,7 +406,7 @@ end) : EXPR = struct
     with Diagnostics.SpanFreeError.Exn (Data (ctx, kind)) ->
       let typ : ty =
         try c_ty e.span e.ty
-        with Diagnostics.SpanFreeError.Exn _ -> U.hax_failure_typ
+        with Diagnostics.SpanFreeError.Exn _ -> U.HaxFailure.Build.ty ""
       in
       let span = Span.of_thir e.span in
       U.hax_failure_expr' span typ (ctx, kind) ""
diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml
index 32ed2ec83..f90d75e41 100644
--- a/engine/lib/phase_utils.ml
+++ b/engine/lib/phase_utils.ml
@@ -181,7 +181,7 @@ end
 
 module DebugBindPhase : sig
   val add : DebugPhaseInfo.t -> int -> (unit -> Ast.Full.item list) -> unit
-  val export : unit -> string option
+  val export : unit -> string list
   val enable : unit -> unit
 end = struct
   let enabled = ref false
@@ -205,40 +205,38 @@ end = struct
 
   let export' () =
     Logs.info (fun m -> m "Exporting debug informations");
-    let json =
-      Hashtbl.to_alist cache
-      |> List.sort ~compare:(fun (_, (a, _)) (_, (b, _)) -> Int.compare a b)
-      |> List.map ~f:(fun (k, (nth, l)) ->
-             let regenerate_span_ids =
-               (object
-                  inherit [_] Visitors.map
-                  method! visit_span = Fn.const Span.refresh_id
-               end)
-                 #visit_item
-                 ()
-             in
-             (* we regenerate spans IDs, so that we have more precise regions *)
-             let l = List.map ~f:regenerate_span_ids !l in
-             let rustish = Print_rust.pitems l in
-             let json =
-               `Assoc
-                 [
-                   ("name", `String ([%show: DebugPhaseInfo.t] k));
-                   ("nth", `Int nth);
-                   ("items", [%yojson_of: Ast.Full.item list] l);
-                   ( "rustish",
-                     [%yojson_of: Print_rust.AnnotatedString.Output.t] rustish
-                   );
-                 ]
-             in
-             json)
-    in
-    `List json |> Yojson.Safe.pretty_to_string
+
+    Hashtbl.to_alist cache
+    |> List.sort ~compare:(fun (_, (a, _)) (_, (b, _)) -> Int.compare a b)
+    |> List.map ~f:(fun (k, (nth, l)) ->
+           let regenerate_span_ids =
+             (object
+                inherit [_] Visitors.map
+                method! visit_span = Fn.const Span.refresh_id
+             end)
+               #visit_item
+               ()
+           in
+           (* we regenerate spans IDs, so that we have more precise regions *)
+           let l = List.map ~f:regenerate_span_ids !l in
+           let rustish = Print_rust.pitems l in
+           let json =
+             `Assoc
+               [
+                 ("name", `String ([%show: DebugPhaseInfo.t] k));
+                 ("nth", `Int nth);
+                 ("items", [%yojson_of: Ast.Full.item list] l);
+                 ( "rustish",
+                   [%yojson_of: Print_rust.AnnotatedString.Output.t] rustish );
+               ]
+           in
+           json)
+    |> List.map ~f:Yojson.Safe.to_string
 
   let export () =
     if !enabled (* recall: ! is deref, not `not`, great op. choice..... *) then
-      Some (export' ())
-    else None
+      export' ()
+    else []
 end
 
 module type S = sig
diff --git a/engine/lib/span.ml b/engine/lib/span.ml
index 749d546d2..0cf1a6387 100644
--- a/engine/lib/span.ml
+++ b/engine/lib/span.ml
@@ -156,12 +156,16 @@ let owner_hint span =
          Option.value_exn
            (List.nth !owner_id_list (!owner_id_list_len - id - 1)))
 
-let to_span2 span : Types.span2 =
+let to_rust_ast_span span : Rust_engine_types.span =
   {
     data = List.map ~f:Imported.span_to_thir span.data;
     id = Int.to_string span.id;
-    owner_hint =
-      Option.map
-        ~f:(fun (OwnerId n) -> Types.Newtypeowner_id (Int.to_string n))
-        span.owner_hint;
+    owner_hint = owner_hint span;
+  }
+
+let from_rust_ast_span (span : Rust_engine_types.span) : t =
+  {
+    data = List.map ~f:Imported.span_of_thir span.data;
+    id = Int.of_string span.id;
+    owner_hint = Option.map ~f:fresh_owner_id span.owner_hint;
   }
diff --git a/engine/lib/span.mli b/engine/lib/span.mli
index 1884fffce..fd2ab7142 100644
--- a/engine/lib/span.mli
+++ b/engine/lib/span.mli
@@ -37,5 +37,7 @@ val owner_hint : t -> Types.def_id option
 (** Looks up the owner hint for a span. This should be used for user reports
     only. *)
 
-val to_span2 : t -> Types.span2
-(** Converts this span to a span2 for export to the Rust engine. *)
+val to_rust_ast_span : t -> Rust_engine_types.span
+(** Converts this span to a Rust engine span. *)
+
+val from_rust_ast_span : Rust_engine_types.span -> t
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index 2c81a7a8f..34adee32e 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -167,7 +167,7 @@ struct
       let typ : B.ty =
         try dty e.span e.typ
         with Diagnostics.SpanFreeError.Exn (Data (_context, _kind)) ->
-          UB.hax_failure_typ
+          UB.HaxFailure.Build.ty ""
       in
       UB.hax_failure_expr e.span typ (context, kind) (UA.LiftToFullAst.expr e)
 
diff --git a/engine/lib/untyped_phases/gen.js b/engine/lib/untyped_phases/gen.js
new file mode 100755
index 000000000..292d80002
--- /dev/null
+++ b/engine/lib/untyped_phases/gen.js
@@ -0,0 +1,149 @@
+#!/usr/bin/env node
+const { readdirSync, readFileSync } = require('fs');
+
+let f = s => ((s.split("include module type")[0] || "").match(/(with|and) type[^)]*/g) || []).join("").split('and type').map(x => x.replace(/(with|and) type/g, '').trim()).filter(x => x).map(x => x.split('=')[1].trim().split('.').slice(1));
+
+let phases = readdirSync("../phases").filter(x => x.endsWith(".mli")).map(filename => ({
+  filename,
+  contents: f(readFileSync("../phases/" + filename).toString()),
+}));
+
+let rejections = readFileSync("../phases/phase_reject.ml")
+  .toString()
+  .split('\n')
+  .map(s => s.match(/^module ([a-z][a-z_]+)/i)?.[1])
+  .filter(s => s);
+
+console.log(`
+open Prelude
+    
+module type PHASE_FULL =
+  Phase_utils.PHASE
+    with module FA = Features.Full
+     and module FB = Features.Full
+     and module A = Ast.Full
+     and module B = Ast.Full
+
+module BindPhaseFull (A : PHASE_FULL) (B : PHASE_FULL) : PHASE_FULL = struct
+  include Phase_utils.BindPhase (A) (B)
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+end
+
+module IdentityFull : PHASE_FULL = struct
+  include Phase_utils.Identity (Features.Full)
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+end
+
+let bind (module A : PHASE_FULL) (module B : PHASE_FULL) : (module PHASE_FULL) =
+  (module BindPhaseFull (A) (B))
+
+let bind_list : (module PHASE_FULL) list -> (module PHASE_FULL) =
+  List.reduce ~f:bind
+  >> Option.value ~default:(module IdentityFull : PHASE_FULL)
+
+`);
+
+
+for (let phase of phases) {
+  let name_lc = phase.filename.replace(/^phase_/, "").replace(/[.]mli$/, "");
+  let name = name_lc.replace(/^(.)/, l => l.toUpperCase());
+  phase.name_lc = name_lc;
+  phase.name = name;
+  phase.module_expression = `Phases.${name}`;
+}
+
+
+for (let rejection of rejections) {
+  let name = 'Reject_' + rejection.replace(/^(.)/, l => l.toLowerCase()).replace(/[A-Z]/g, c => `_${c}`).toLowerCase();
+  phases.push({
+    name_lc: name.toLowerCase(),
+    name,
+    module_expression: 'Phase_reject.' + rejection,
+    contents: [],
+  });
+}
+
+phases.push({
+  name_lc: "hoist_side_effects",
+  name: 'Hoist_side_effects',
+  module_expression: 'Side_effect_utils.Hoist',
+  contents: [
+    ['Off', 'monadic_binding'],
+    ['Off', 'for_index_loop'],
+  ],
+});
+
+
+for (let phase of phases) {
+  let { name, module_expression } = phase;
+
+  console.log(`
+module ${name} : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    ${phase.contents.map(([status, f]) => `include ${status}.${f.replace(/^(.)/, l => l.toUpperCase())}`).join('\n')}
+  end
+
+  module Phase = ${module_expression} (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        ${phase.contents.map(([status, f]) =>
+    `let ${f} = ` + (status == 'On' ? 'fun _ _ -> Features.On.' + f : 'reject')
+  ).join('\n')}
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+`);
+}
+
+
+for (let phase of phases) {
+  console.log(`let ${phase.name_lc} : (module PHASE_FULL) = (module ${phase.name})`)
+}
+console.log(`let phases_list : (module PHASE_FULL) list = [${phases.map(p => p.name_lc).join(';')}]`)
+
+
+console.log(`
+let phase_of_name: string -> (module PHASE_FULL) option = 
+    function
+    ${phases.map(p => `| "${p.name_lc}" -> Some ${p.name_lc}`).join('')}
+    | _ -> None
+
+let phases: string list = [${phases.map(p => `"${p.name_lc}"`).join(';')}]
+
+(*
+${phases.map(p => `${p.name_lc}`).join(', ')}
+*)
+`);
+
+
+
+
diff --git a/engine/lib/untyped_phases/untyped_phases.ml b/engine/lib/untyped_phases/untyped_phases.ml
new file mode 100644
index 000000000..15edb3555
--- /dev/null
+++ b/engine/lib/untyped_phases/untyped_phases.ml
@@ -0,0 +1,1571 @@
+open Prelude
+
+module type PHASE_FULL =
+  Phase_utils.PHASE
+    with module FA = Features.Full
+     and module FB = Features.Full
+     and module A = Ast.Full
+     and module B = Ast.Full
+
+module BindPhaseFull (A : PHASE_FULL) (B : PHASE_FULL) : PHASE_FULL = struct
+  include Phase_utils.BindPhase (A) (B)
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+end
+
+module IdentityFull : PHASE_FULL = struct
+  include Phase_utils.Identity (Features.Full)
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+end
+
+let bind (module A : PHASE_FULL) (module B : PHASE_FULL) : (module PHASE_FULL) =
+  (module BindPhaseFull (A) (B))
+
+let bind_list : (module PHASE_FULL) list -> (module PHASE_FULL) =
+  List.reduce ~f:bind
+  >> Option.value ~default:(module IdentityFull : PHASE_FULL)
+
+module And_mut_defsite : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include On.Mutable_variable
+    include On.Mutable_reference
+    include On.Nontrivial_lhs
+    include On.Arbitrary_lhs
+    include On.Reference
+  end
+
+  module Phase = Phases.And_mut_defsite (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let mutable_variable = fun _ _ -> Features.On.mutable_variable
+        let mutable_reference = fun _ _ -> Features.On.mutable_reference
+        let nontrivial_lhs = fun _ _ -> Features.On.nontrivial_lhs
+        let arbitrary_lhs = fun _ _ -> Features.On.arbitrary_lhs
+        let reference = fun _ _ -> Features.On.reference
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Bundle_cycles : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Bundle_cycles (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Cf_into_monads : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Monadic_action
+    include Off.Monadic_binding
+  end
+
+  module Phase = Phases.Cf_into_monads (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let monadic_action = reject
+        let monadic_binding = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Direct_and_mut : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Raw_pointer
+    include Off.Mutable_pointer
+  end
+
+  module Phase = Phases.Direct_and_mut (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let raw_pointer = reject
+        let mutable_pointer = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Drop_blocks : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Drop_blocks (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Drop_match_guards : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Drop_match_guards (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Drop_references : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Raw_pointer
+    include Off.Mutable_reference
+  end
+
+  module Phase = Phases.Drop_references (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let raw_pointer = reject
+        let mutable_reference = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Drop_return_break_continue : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Drop_return_break_continue (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Drop_sized_trait : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Drop_sized_trait (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Functionalize_loops : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Continue
+    include Off.Early_exit
+    include Off.Break
+  end
+
+  module Phase = Phases.Functionalize_loops (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let continue = reject
+        let early_exit = reject
+        let break = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Hoist_disjunctive_patterns : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Hoist_disjunctive_patterns (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Local_mutation : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Mutable_reference
+    include Off.Mutable_pointer
+    include Off.Raw_pointer
+    include Off.Arbitrary_lhs
+    include Off.Nontrivial_lhs
+    include Off.Monadic_action
+    include Off.Monadic_binding
+    include Off.For_index_loop
+  end
+
+  module Phase = Phases.Local_mutation (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let mutable_reference = reject
+        let mutable_pointer = reject
+        let raw_pointer = reject
+        let arbitrary_lhs = reject
+        let nontrivial_lhs = reject
+        let monadic_action = reject
+        let monadic_binding = reject
+        let for_index_loop = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Newtype_as_refinement : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Newtype_as_refinement (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reconstruct_asserts : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reconstruct_asserts (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reconstruct_for_index_loops : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reconstruct_for_index_loops (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reconstruct_for_loops : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reconstruct_for_loops (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reconstruct_question_marks : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reconstruct_question_marks (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reconstruct_while_loops : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reconstruct_while_loops (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reorder_fields : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Reorder_fields (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Rewrite_control_flow : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Rewrite_control_flow (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Rewrite_local_self : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Rewrite_local_self (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Simplify_hoisting : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Simplify_hoisting (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Simplify_match_return : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Simplify_match_return (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Simplify_question_marks : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Simplify_question_marks (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Sort_items : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Sort_items (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Specialize : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Specialize (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Traits_specs : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Traits_specs (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Transform_hax_lib_inline : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Transform_hax_lib_inline (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Trivialize_assign_lhs : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phases.Trivialize_assign_lhs (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_arbitrary_lhs : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Arbitrary_lhs (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_continue : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Continue (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_question_mark : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Question_mark (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_raw_or_mut_pointer : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.RawOrMutPointer (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_early_exit : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.EarlyExit (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_as_pattern : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.As_pattern (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_dyn : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Dyn (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_trait_item_default : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Trait_item_default (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Reject_unsafe : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+  end
+
+  module Phase = Phase_reject.Unsafe (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+module Hoist_side_effects : PHASE_FULL = struct
+  module FA = Features.Full
+  module FB = Features.Full
+  module A = Ast.Full
+  module B = Ast.Full
+
+  module ExpectedFA = struct
+    open Features
+    include On
+    include Off.Monadic_binding
+    include Off.For_index_loop
+  end
+
+  module Phase = Side_effect_utils.Hoist (ExpectedFA)
+
+  module Coerce =
+    Feature_gate.Make (Features.Full) (ExpectedFA)
+      (struct
+        module A = Features.Full
+        module B = ExpectedFA
+        include Feature_gate.DefaultSubtype
+
+        let monadic_binding = reject
+        let for_index_loop = reject
+
+        let metadata =
+          Phase_reject.make_metadata
+            (CoercionForUntypedPhase
+               ([%show: Diagnostics.Phase.t] Phase.metadata.current_phase))
+      end)
+
+  let metadata = Phase.metadata
+  let to_full_ast : Phase.B.item list -> Ast.Full.item list = Stdlib.Obj.magic
+
+  let ditems =
+    List.map ~f:Coerce.ditem >> List.concat >> Phase.ditems >> to_full_ast
+end
+
+let and_mut_defsite : (module PHASE_FULL) = (module And_mut_defsite)
+let bundle_cycles : (module PHASE_FULL) = (module Bundle_cycles)
+let cf_into_monads : (module PHASE_FULL) = (module Cf_into_monads)
+let direct_and_mut : (module PHASE_FULL) = (module Direct_and_mut)
+let drop_blocks : (module PHASE_FULL) = (module Drop_blocks)
+let drop_match_guards : (module PHASE_FULL) = (module Drop_match_guards)
+let drop_references : (module PHASE_FULL) = (module Drop_references)
+
+let drop_return_break_continue : (module PHASE_FULL) =
+  (module Drop_return_break_continue)
+
+let drop_sized_trait : (module PHASE_FULL) = (module Drop_sized_trait)
+let functionalize_loops : (module PHASE_FULL) = (module Functionalize_loops)
+
+let hoist_disjunctive_patterns : (module PHASE_FULL) =
+  (module Hoist_disjunctive_patterns)
+
+let local_mutation : (module PHASE_FULL) = (module Local_mutation)
+let newtype_as_refinement : (module PHASE_FULL) = (module Newtype_as_refinement)
+let reconstruct_asserts : (module PHASE_FULL) = (module Reconstruct_asserts)
+
+let reconstruct_for_index_loops : (module PHASE_FULL) =
+  (module Reconstruct_for_index_loops)
+
+let reconstruct_for_loops : (module PHASE_FULL) = (module Reconstruct_for_loops)
+
+let reconstruct_question_marks : (module PHASE_FULL) =
+  (module Reconstruct_question_marks)
+
+let reconstruct_while_loops : (module PHASE_FULL) =
+  (module Reconstruct_while_loops)
+
+let reorder_fields : (module PHASE_FULL) = (module Reorder_fields)
+let rewrite_control_flow : (module PHASE_FULL) = (module Rewrite_control_flow)
+let rewrite_local_self : (module PHASE_FULL) = (module Rewrite_local_self)
+let simplify_hoisting : (module PHASE_FULL) = (module Simplify_hoisting)
+let simplify_match_return : (module PHASE_FULL) = (module Simplify_match_return)
+
+let simplify_question_marks : (module PHASE_FULL) =
+  (module Simplify_question_marks)
+
+let sort_items : (module PHASE_FULL) = (module Sort_items)
+let specialize : (module PHASE_FULL) = (module Specialize)
+let traits_specs : (module PHASE_FULL) = (module Traits_specs)
+
+let transform_hax_lib_inline : (module PHASE_FULL) =
+  (module Transform_hax_lib_inline)
+
+let trivialize_assign_lhs : (module PHASE_FULL) = (module Trivialize_assign_lhs)
+let reject_arbitrary_lhs : (module PHASE_FULL) = (module Reject_arbitrary_lhs)
+let reject_continue : (module PHASE_FULL) = (module Reject_continue)
+let reject_question_mark : (module PHASE_FULL) = (module Reject_question_mark)
+
+let reject_raw_or_mut_pointer : (module PHASE_FULL) =
+  (module Reject_raw_or_mut_pointer)
+
+let reject_early_exit : (module PHASE_FULL) = (module Reject_early_exit)
+let reject_as_pattern : (module PHASE_FULL) = (module Reject_as_pattern)
+let reject_dyn : (module PHASE_FULL) = (module Reject_dyn)
+
+let reject_trait_item_default : (module PHASE_FULL) =
+  (module Reject_trait_item_default)
+
+let reject_unsafe : (module PHASE_FULL) = (module Reject_unsafe)
+let hoist_side_effects : (module PHASE_FULL) = (module Hoist_side_effects)
+
+let phases_list : (module PHASE_FULL) list =
+  [
+    and_mut_defsite;
+    bundle_cycles;
+    cf_into_monads;
+    direct_and_mut;
+    drop_blocks;
+    drop_match_guards;
+    drop_references;
+    drop_return_break_continue;
+    drop_sized_trait;
+    functionalize_loops;
+    hoist_disjunctive_patterns;
+    local_mutation;
+    newtype_as_refinement;
+    reconstruct_asserts;
+    reconstruct_for_index_loops;
+    reconstruct_for_loops;
+    reconstruct_question_marks;
+    reconstruct_while_loops;
+    reorder_fields;
+    rewrite_control_flow;
+    rewrite_local_self;
+    simplify_hoisting;
+    simplify_match_return;
+    simplify_question_marks;
+    sort_items;
+    specialize;
+    traits_specs;
+    transform_hax_lib_inline;
+    trivialize_assign_lhs;
+    reject_arbitrary_lhs;
+    reject_continue;
+    reject_question_mark;
+    reject_raw_or_mut_pointer;
+    reject_early_exit;
+    reject_as_pattern;
+    reject_dyn;
+    reject_trait_item_default;
+    reject_unsafe;
+    hoist_side_effects;
+  ]
+
+let phase_of_name : string -> (module PHASE_FULL) option = function
+  | "and_mut_defsite" -> Some and_mut_defsite
+  | "bundle_cycles" -> Some bundle_cycles
+  | "cf_into_monads" -> Some cf_into_monads
+  | "direct_and_mut" -> Some direct_and_mut
+  | "drop_blocks" -> Some drop_blocks
+  | "drop_match_guards" -> Some drop_match_guards
+  | "drop_references" -> Some drop_references
+  | "drop_return_break_continue" -> Some drop_return_break_continue
+  | "drop_sized_trait" -> Some drop_sized_trait
+  | "functionalize_loops" -> Some functionalize_loops
+  | "hoist_disjunctive_patterns" -> Some hoist_disjunctive_patterns
+  | "local_mutation" -> Some local_mutation
+  | "newtype_as_refinement" -> Some newtype_as_refinement
+  | "reconstruct_asserts" -> Some reconstruct_asserts
+  | "reconstruct_for_index_loops" -> Some reconstruct_for_index_loops
+  | "reconstruct_for_loops" -> Some reconstruct_for_loops
+  | "reconstruct_question_marks" -> Some reconstruct_question_marks
+  | "reconstruct_while_loops" -> Some reconstruct_while_loops
+  | "reorder_fields" -> Some reorder_fields
+  | "rewrite_control_flow" -> Some rewrite_control_flow
+  | "rewrite_local_self" -> Some rewrite_local_self
+  | "simplify_hoisting" -> Some simplify_hoisting
+  | "simplify_match_return" -> Some simplify_match_return
+  | "simplify_question_marks" -> Some simplify_question_marks
+  | "sort_items" -> Some sort_items
+  | "specialize" -> Some specialize
+  | "traits_specs" -> Some traits_specs
+  | "transform_hax_lib_inline" -> Some transform_hax_lib_inline
+  | "trivialize_assign_lhs" -> Some trivialize_assign_lhs
+  | "reject_arbitrary_lhs" -> Some reject_arbitrary_lhs
+  | "reject_continue" -> Some reject_continue
+  | "reject_question_mark" -> Some reject_question_mark
+  | "reject_raw_or_mut_pointer" -> Some reject_raw_or_mut_pointer
+  | "reject_early_exit" -> Some reject_early_exit
+  | "reject_as_pattern" -> Some reject_as_pattern
+  | "reject_dyn" -> Some reject_dyn
+  | "reject_trait_item_default" -> Some reject_trait_item_default
+  | "reject_unsafe" -> Some reject_unsafe
+  | "hoist_side_effects" -> Some hoist_side_effects
+  | _ -> None
+
+let phases : string list =
+  [
+    "and_mut_defsite";
+    "bundle_cycles";
+    "cf_into_monads";
+    "direct_and_mut";
+    "drop_blocks";
+    "drop_match_guards";
+    "drop_references";
+    "drop_return_break_continue";
+    "drop_sized_trait";
+    "functionalize_loops";
+    "hoist_disjunctive_patterns";
+    "local_mutation";
+    "newtype_as_refinement";
+    "reconstruct_asserts";
+    "reconstruct_for_index_loops";
+    "reconstruct_for_loops";
+    "reconstruct_question_marks";
+    "reconstruct_while_loops";
+    "reorder_fields";
+    "rewrite_control_flow";
+    "rewrite_local_self";
+    "simplify_hoisting";
+    "simplify_match_return";
+    "simplify_question_marks";
+    "sort_items";
+    "specialize";
+    "traits_specs";
+    "transform_hax_lib_inline";
+    "trivialize_assign_lhs";
+    "reject_arbitrary_lhs";
+    "reject_continue";
+    "reject_question_mark";
+    "reject_raw_or_mut_pointer";
+    "reject_early_exit";
+    "reject_as_pattern";
+    "reject_dyn";
+    "reject_trait_item_default";
+    "reject_unsafe";
+    "hoist_side_effects";
+  ]
+
+(*
+and_mut_defsite, bundle_cycles, cf_into_monads, direct_and_mut, drop_blocks, drop_match_guards, drop_references, drop_return_break_continue, drop_sized_trait, functionalize_loops, hoist_disjunctive_patterns, local_mutation, newtype_as_refinement, reconstruct_asserts, reconstruct_for_index_loops, reconstruct_for_loops, reconstruct_question_marks, reconstruct_while_loops, reorder_fields, rewrite_control_flow, rewrite_local_self, simplify_hoisting, simplify_match_return, simplify_question_marks, sort_items, specialize, traits_specs, transform_hax_lib_inline, trivialize_assign_lhs, reject_arbitrary_lhs, reject_continue, reject_question_mark, reject_raw_or_mut_pointer, reject_early_exit, reject_as_pattern, reject_dyn, reject_trait_item_default, reject_unsafe, hoist_side_effects
+*)
diff --git a/hax-types/src/diagnostics/mod.rs b/hax-types/src/diagnostics/mod.rs
index 0e3fb8c82..7acc33066 100644
--- a/hax-types/src/diagnostics/mod.rs
+++ b/hax-types/src/diagnostics/mod.rs
@@ -105,7 +105,8 @@ impl Kind {
             Kind::ExpectedMutRef => Some(420),
             Kind::NonTrivialAndMutFnInput => Some(1405),
             Kind::AttributeRejected { .. } => None,
-            Kind::FStarParseError { .. } => todo!(),
+            Kind::FStarParseError { .. } => None,
+            Kind::OcamlEngineErrorPayload { .. } => None,
         }
     }
 }
@@ -180,6 +181,9 @@ pub enum Kind {
         fstar_snippet: String,
         details: String,
     } = 13,
+
+    /// Internal encoding
+    OcamlEngineErrorPayload(String) = 9999,
 }
 
 impl Kind {
diff --git a/hax-types/src/engine_api.rs b/hax-types/src/engine_api.rs
index b9fc41429..d529c93a1 100644
--- a/hax-types/src/engine_api.rs
+++ b/hax-types/src/engine_api.rs
@@ -56,7 +56,7 @@ pub struct File {
 pub struct Output {
     pub diagnostics: Vec<crate::diagnostics::Diagnostics>,
     pub files: Vec<File>,
-    pub debug_json: Option<String>,
+    pub debug_json: Vec<String>,
 }
 
 #[derive_group(Serializers)]
diff --git a/rust-engine/src/ast.rs b/rust-engine/src/ast.rs
index 40c9dc358..27874a755 100644
--- a/rust-engine/src/ast.rs
+++ b/rust-engine/src/ast.rs
@@ -915,12 +915,6 @@ pub enum ExprKind {
         inner: Expr,
     },
 
-    /// A dereference
-    ///
-    /// # Example:
-    /// `*x`
-    Deref(Expr),
-
     /// A `let` expression used in expressions.
     ///
     /// # Example:
@@ -997,6 +991,9 @@ pub enum ExprKind {
         value: Expr,
         /// What loop shall we break? By default, the parent enclosing loop.
         label: Option<Symbol>,
+        /// When a loop has a state (see [`ExprKind::Loop::state`]), this field
+        /// `state` is `Some(_)`. This carries the updated state for the loop.
+        state: Option<Expr>,
     },
 
     /// Return from a function.
@@ -1015,6 +1012,9 @@ pub enum ExprKind {
     Continue {
         /// The loop we continue.
         label: Option<Symbol>,
+        /// When a loop has a state (see [`ExprKind::Loop::state`]), this field
+        /// `state` is `Some(_)`. This carries the updated state for the loop.
+        state: Option<Expr>,
     },
 
     /// Closure (anonymous function)
@@ -1345,6 +1345,9 @@ pub enum ItemKind {
         /// # Example:
         /// `type Assoc;`, `fn m ...;`
         items: Vec<TraitItem>,
+
+        /// Safe or unsafe
+        safety: SafetyKind,
     },
 
     /// A trait implementation.
diff --git a/rust-engine/src/ast/span.rs b/rust-engine/src/ast/span.rs
index 68886fe49..0bc49d2cb 100644
--- a/rust-engine/src/ast/span.rs
+++ b/rust-engine/src/ast/span.rs
@@ -9,10 +9,6 @@ fn fresh_id() -> usize {
     CURRENT_ID.fetch_add(1, Ordering::Relaxed)
 }
 
-/// Identifier used to track the origin Rust item of a span
-#[derive_group_for_ast]
-pub struct OwnerId(usize);
-
 /// Position of a Rust source
 #[derive_group_for_ast]
 pub struct Span {
@@ -27,7 +23,7 @@ pub struct Span {
     /// A reference to the item in which this span lives. This information is
     /// used for debugging and profiling purposes, e.g. for `cargo hax into
     /// --stats backend`.
-    owner_hint: Option<OwnerId>,
+    owner_hint: Option<hax_frontend_exporter::DefId>,
 }
 
 impl Span {
diff --git a/rust-engine/src/backends.rs b/rust-engine/src/backends.rs
index c9cf53ddb..88faed948 100644
--- a/rust-engine/src/backends.rs
+++ b/rust-engine/src/backends.rs
@@ -21,6 +21,7 @@ use std::collections::HashMap;
 
 use crate::{
     ast::{Item, Metadata, Module, span::Span},
+    phase::legacy::group_consecutive_ocaml_phases,
     printer::{Print, Printer},
 };
 use camino::Utf8PathBuf;
@@ -89,7 +90,7 @@ pub trait Backend {
 /// modules via [`Backend::items_to_module`], and then uses the backend's printer
 /// to generate source files with paths determined by [`Backend::module_path`].
 pub fn apply_backend<B: Backend + 'static>(backend: B, mut items: Vec<Item>) -> Vec<File> {
-    for phase in backend.phases() {
+    for phase in group_consecutive_ocaml_phases(backend.phases()) {
         phase.apply(&mut items);
     }
 
diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs
index 018097e57..97ca53d09 100644
--- a/rust-engine/src/backends/lean.rs
+++ b/rust-engine/src/backends/lean.rs
@@ -139,7 +139,43 @@ impl Backend for LeanBackend {
     }
 
     fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
-        vec![Box::new(RejectNotDoLeanDSL), Box::new(ExplicitMonadic)]
+        use crate::phase::legacy::*;
+        vec![
+            reject_raw_or_mut_pointer(),
+            rewrite_local_self(),
+            transform_hax_lib_inline(),
+            specialize(),
+            drop_sized_trait(),
+            simplify_question_marks(),
+            and_mut_defsite(),
+            reconstruct_asserts(),
+            reconstruct_for_loops(),
+            reconstruct_while_loops(),
+            direct_and_mut(),
+            reject_arbitrary_lhs(),
+            drop_blocks(),
+            drop_match_guards(),
+            drop_references(),
+            trivialize_assign_lhs(),
+            hoist_side_effects(),
+            hoist_disjunctive_patterns(),
+            simplify_match_return(),
+            local_mutation(),
+            rewrite_control_flow(),
+            drop_return_break_continue(),
+            functionalize_loops(),
+            reject_question_mark(),
+            reject_as_pattern(),
+            traits_specs(),
+            simplify_hoisting(),
+            newtype_as_refinement(),
+            reject_trait_item_default(),
+            bundle_cycles(),
+            reorder_fields(),
+            sort_items(),
+            Box::new(RejectNotDoLeanDSL),
+            Box::new(ExplicitMonadic),
+        ]
     }
 }
 
@@ -598,7 +634,7 @@ set_option linter.unusedVariables false
                 ]
                 .group(),
 
-                ExprKind::Borrow { .. } | ExprKind::Deref(_) => {
+                ExprKind::Borrow { .. } => {
                     unreachable_by_invariant!(Drop_references)
                 }
                 ExprKind::AddressOf { .. } => unreachable_by_invariant!(Reject_raw_or_mut_pointer),
@@ -932,6 +968,7 @@ set_option linter.unusedVariables false
                     name,
                     generics,
                     items,
+                    safety: _,
                 } => {
                     // Type parameters are also parameters of the class, but constraints are fields of the class
                     docs![
diff --git a/rust-engine/src/hax_io.rs b/rust-engine/src/hax_io.rs
index 78bcb179a..ea0f1fa9c 100644
--- a/rust-engine/src/hax_io.rs
+++ b/rust-engine/src/hax_io.rs
@@ -1,16 +1,18 @@
 //! This module helps communicating with `cargo-hax`.
 
-use crate::ocaml_engine::ExtendedToEngine;
 use hax_types::engine_api::protocol::FromEngine;
-use serde::Deserialize;
+use serde::de::DeserializeOwned;
 use std::io::{BufRead, BufReader, Stdin, stdin, stdout};
 use std::sync::{LazyLock, Mutex};
 
+use hax_frontend_exporter::id_table::WithTable;
+use hax_types::engine_api::{EngineOptions, protocol::ToEngine};
+
 static STDIN: LazyLock<Mutex<BufReader<Stdin>>> =
     LazyLock::new(|| Mutex::new(BufReader::new(stdin())));
 
-/// Reads a `ExtendedToEngine` message
-pub fn read() -> ExtendedToEngine {
+/// Reads a message of any type from stdin
+fn read<T: DeserializeOwned>() -> T {
     let mut stdin = STDIN.lock().unwrap();
     let mut slice = Vec::new();
     stdin
@@ -18,8 +20,22 @@ pub fn read() -> ExtendedToEngine {
         .expect("No message left! Did the engine crash?");
     let mut de = serde_json::Deserializer::from_slice(&slice);
     de.disable_recursion_limit();
-    ExtendedToEngine::deserialize(serde_stacker::Deserializer::new(&mut de))
-        .expect("Could not parse as a `ExtendedToEngine` message!")
+    T::deserialize(serde_stacker::Deserializer::new(&mut de)).unwrap_or_else(|err| {
+        panic!(
+            "Could not parse as a `{}` message! Error: {err}",
+            std::any::type_name::<T>()
+        )
+    })
+}
+
+/// Reads a `ToEngine` message from the engine
+pub fn read_to_engine_message() -> ToEngine {
+    read()
+}
+
+/// Reads the engine input JSON payload.
+pub fn read_engine_input_message() -> WithTable<EngineOptions> {
+    read()
 }
 
 /// Writes a `ExtendedFromEngine` message
diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs
index a022f4ca0..023a85be3 100644
--- a/rust-engine/src/main.rs
+++ b/rust-engine/src/main.rs
@@ -1,26 +1,25 @@
 use hax_rust_engine::{
     backends,
-    ocaml_engine::{ExtendedToEngine, Response},
+    ocaml_engine::{self, Response},
 };
 use hax_types::{cli_options::Backend, engine_api::File};
 
 fn main() {
-    let ExtendedToEngine::Query(input) = hax_rust_engine::hax_io::read() else {
-        panic!()
-    };
-    let (value, table) = input.destruct();
+    let (value, table) = hax_rust_engine::hax_io::read_engine_input_message().destruct();
 
-    let query = hax_rust_engine::ocaml_engine::Query {
+    ocaml_engine::initialize(ocaml_engine::Meta {
         hax_version: value.hax_version,
         impl_infos: value.impl_infos,
-        kind: hax_rust_engine::ocaml_engine::QueryKind::ImportThir {
-            input: value.input,
-            apply_phases: !matches!(&value.backend.backend, Backend::GenerateRustEngineNames),
-            translation_options: value.backend.translation_options,
-        },
+        debug_bind_phase: value.backend.debug_engine.is_some(),
+        profiling: value.backend.profile,
+    });
+
+    let query = hax_rust_engine::ocaml_engine::QueryKind::ImportThir {
+        input: value.input,
+        translation_options: value.backend.translation_options,
     };
 
-    let Some(Response::ImportThir { output: items }) = query.execute(table) else {
+    let Some(Response::ImportThir { output: items }) = query.execute(Some(table)) else {
         panic!()
     };
 
diff --git a/rust-engine/src/ocaml_engine.rs b/rust-engine/src/ocaml_engine.rs
index 35bd00c1a..98cc4c755 100644
--- a/rust-engine/src/ocaml_engine.rs
+++ b/rust-engine/src/ocaml_engine.rs
@@ -2,21 +2,27 @@
 //! interface, the rust engine can communicate with the OCaml engine, and reuse
 //! some of its components.
 
-use std::io::BufRead;
+use std::{io::BufRead, sync::OnceLock};
 
 use hax_frontend_exporter::{
     ThirBody,
     id_table::{Table, WithTable},
 };
-use hax_types::engine_api::{
-    EngineOptions,
-    protocol::{FromEngine, ToEngine},
-};
+use hax_types::engine_api::protocol::{FromEngine, ToEngine};
 use serde::Deserialize;
 
 /// A query for the OCaml engine
 #[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
 pub struct Query {
+    #[serde(flatten)]
+    meta: Meta,
+    /// The kind of query we want to send to the engine
+    kind: QueryKind,
+}
+
+/// The metadata required to perform a query.
+#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
+pub struct Meta {
     /// The version of hax currently used
     pub hax_version: String,
     /// Dictionary from `DefId`s to `impl_infos`
@@ -24,8 +30,19 @@ pub struct Query {
         hax_frontend_exporter::DefId,
         hax_frontend_exporter::ImplInfos,
     )>,
-    /// The kind of query we want to send to the engine
-    pub kind: QueryKind,
+    /// Enable debugging of phases in the OCaml engine
+    pub debug_bind_phase: bool,
+    /// Enable profiling in the OCaml engine
+    pub profiling: bool,
+}
+
+static STATE: OnceLock<Meta> = OnceLock::new();
+
+/// Initialize query metadata.
+pub fn initialize(meta: Meta) {
+    STATE
+        .set(meta)
+        .expect("`ocaml_engine::initialize` was called more than once")
 }
 
 /// The payload of the query. [`Response`] below mirrors this enum to represent
@@ -36,13 +53,18 @@ pub enum QueryKind {
     ImportThir {
         /// The input THIR items
         input: Vec<hax_frontend_exporter::Item<ThirBody>>,
-        /// Temporary option to enable a set of default phases
-        apply_phases: bool,
         /// Translation options which contains include clauses (items filtering)
         translation_options: hax_types::cli_options::TranslationOptions,
     },
-}
 
+    /// Ask the OCaml engine to run given phases on given items
+    ApplyPhases {
+        /// The phases to run. See `untyped_phases.ml`.
+        phases: Vec<String>,
+        /// The items on which the phases will be applied.
+        input: Vec<crate::ast::Item>,
+    },
+}
 /// A Response after a [`Query`]
 #[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
 pub enum Response {
@@ -51,16 +73,11 @@ pub enum Response {
         /// The output Rust AST items
         output: Vec<crate::ast::Item>,
     },
-}
-
-/// Extends the common `ToEngine` messages with one extra case: `Query`.
-#[derive(::serde::Deserialize, ::serde::Serialize)]
-#[serde(untagged)]
-pub enum ExtendedToEngine {
-    /// A standard `ToEngine` message
-    ToEngine(ToEngine),
-    /// A `Query`
-    Query(Box<WithTable<EngineOptions>>),
+    /// Return items after phase application
+    ApplyPhases {
+        /// The output Rust AST items after phases
+        output: Vec<crate::ast::Item>,
+    },
 }
 
 /// Extends the common `FromEngine` messages with one extra case: `Response`.
@@ -73,9 +90,16 @@ pub enum ExtendedFromEngine {
     Response(Response),
 }
 
-impl Query {
+impl QueryKind {
     /// Execute the query synchronously.
-    pub fn execute(&self, table: Table) -> Option<Response> {
+    pub fn execute(self, table: Option<Table>) -> Option<Response> {
+        let query = Query {
+            meta: STATE
+                .get()
+                .expect("`ocaml_engine::initialize` should be called first")
+                .clone(),
+            kind: self,
+        };
         use std::io::Write;
         use std::process::Command;
 
@@ -102,9 +126,13 @@ impl Query {
                 .expect("Could not write on stdin"),
         );
 
-        WithTable::run(table, self, |with_table| {
-            send!(stdin, with_table);
-        });
+        if let Some(table) = table {
+            WithTable::run(table, query, |with_table| {
+                send!(stdin, with_table);
+            });
+        } else {
+            send!(stdin, &(vec![] as Vec<()>, query));
+        }
 
         let mut response = None;
         let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
@@ -132,11 +160,7 @@ impl Query {
                 ExtendedFromEngine::FromEngine(from_engine) => {
                     crate::hax_io::write(&from_engine);
                     if from_engine.requires_response() {
-                        let ExtendedToEngine::ToEngine(response) = crate::hax_io::read() else {
-                            panic!(
-                                "The frontend sent an incorrect message: expected `ExtendedToEngine::ToEngine` since we sent a `ExtendedFromEngine::FromEngine`."
-                            )
-                        };
+                        let response: ToEngine = crate::hax_io::read_to_engine_message();
                         send!(stdin, &response);
                     }
                 }
diff --git a/rust-engine/src/phase.rs b/rust-engine/src/phase.rs
index a8eb383c8..63e1a7ff0 100644
--- a/rust-engine/src/phase.rs
+++ b/rust-engine/src/phase.rs
@@ -7,7 +7,7 @@ macro_rules! unreachable_by_invariant {
     ($phase:ident) => {
         unreachable!(
             "The phase {} should make this unreachable",
-            stringify!($ident)
+            stringify!($phase)
         )
     };
 }
@@ -18,7 +18,16 @@ pub trait Phase {
     /// Apply the phase on items.
     /// A phase may transform an item into zero, one or more items.
     fn apply(&self, items: &mut Vec<Item>);
+
+    /// This is a compatibility layer for the OCaml engine.
+    /// This will be dropped when the OCaml engine is dropped.
+    /// Returns `Some` when the phase is actually an OCaml phase.
+    /// This is useful for `group_consecutive_ocaml_phases`.
+    fn legacy_ocaml_phase(&self) -> Option<&str> {
+        None
+    }
 }
 
 pub mod explicit_monadic;
+pub mod legacy;
 pub mod reject_not_do_lean_dsl;
diff --git a/rust-engine/src/phase/explicit_monadic.rs b/rust-engine/src/phase/explicit_monadic.rs
index e621e8d80..f80df7acd 100644
--- a/rust-engine/src/phase/explicit_monadic.rs
+++ b/rust-engine/src/phase/explicit_monadic.rs
@@ -183,8 +183,7 @@ impl ExplicitMonadicVisitor {
             }
             ExprKind::Assign { value: inner, .. }
             | ExprKind::Borrow { inner, .. }
-            | ExprKind::AddressOf { inner, .. }
-            | ExprKind::Deref(inner) => {
+            | ExprKind::AddressOf { inner, .. } => {
                 self.visit_expr_coerce(MonadicStatus::Value, inner);
                 Some(MonadicStatus::Value)
             }
diff --git a/rust-engine/src/phase/legacy.rs b/rust-engine/src/phase/legacy.rs
new file mode 100644
index 000000000..72c38f6ec
--- /dev/null
+++ b/rust-engine/src/phase/legacy.rs
@@ -0,0 +1,111 @@
+//! This module exposes the legacy phases written in OCaml in the OCaml engine.
+
+use crate::{ast::Item, phase::Phase};
+
+struct LegacyOCamlPhases {
+    phases: Vec<String>,
+}
+
+impl Phase for LegacyOCamlPhases {
+    fn apply(&self, items: &mut Vec<Item>) {
+        eprintln!("Applying phases: {:#?}", &self.phases);
+        use crate::ocaml_engine::Response;
+        let query = crate::ocaml_engine::QueryKind::ApplyPhases {
+            input: std::mem::take(items),
+            phases: self.phases.clone(),
+        };
+        let Some(Response::ApplyPhases { output }) = query.execute(None) else {
+            panic!()
+        };
+        *items = output;
+    }
+
+    fn legacy_ocaml_phase(&self) -> Option<&str> {
+        match self.phases.as_slice() {
+            [phase] => Some(phase.as_str()),
+            _ => None,
+        }
+    }
+}
+
+/// Group consecutive ocaml phases as one monolithic phase, so that we avoid extra roundtrips to the OCaml engine.
+pub fn group_consecutive_ocaml_phases(phases: Vec<Box<dyn Phase>>) -> Vec<Box<dyn Phase>> {
+    let mut output: Vec<Box<dyn Phase>> = vec![];
+    let mut ocaml_phases = vec![];
+    let mut phases = phases.into_iter();
+
+    loop {
+        let phase = phases.next();
+        if let Some(ocaml_phase) = phase.as_ref().and_then(|phase| phase.legacy_ocaml_phase()) {
+            ocaml_phases.push(ocaml_phase.to_string())
+        } else {
+            if !ocaml_phases.is_empty() {
+                output.push(Box::new(LegacyOCamlPhases {
+                    phases: std::mem::take(&mut ocaml_phases),
+                }));
+            }
+            if let Some(phase) = phase {
+                output.push(phase);
+            } else {
+                break;
+            }
+        }
+    }
+
+    output
+}
+
+macro_rules! make_ocaml_legacy_phase {
+    ($($name:ident),*) => {
+        $(
+            #[doc = concat!("The phase ", stringify!($name), " from the OCaml engine.")]
+            pub fn $name() -> Box<dyn Phase> {
+                Box::new(LegacyOCamlPhases {
+                    phases: vec![stringify!($name).to_string()],
+                })
+            }
+        )*
+    };
+}
+
+make_ocaml_legacy_phase!(
+    and_mut_defsite,
+    bundle_cycles,
+    cf_into_monads,
+    direct_and_mut,
+    drop_blocks,
+    drop_match_guards,
+    drop_references,
+    drop_return_break_continue,
+    drop_sized_trait,
+    functionalize_loops,
+    hoist_disjunctive_patterns,
+    local_mutation,
+    newtype_as_refinement,
+    reconstruct_asserts,
+    reconstruct_for_index_loops,
+    reconstruct_for_loops,
+    reconstruct_question_marks,
+    reconstruct_while_loops,
+    reorder_fields,
+    rewrite_control_flow,
+    rewrite_local_self,
+    simplify_hoisting,
+    simplify_match_return,
+    simplify_question_marks,
+    sort_items,
+    specialize,
+    traits_specs,
+    transform_hax_lib_inline,
+    trivialize_assign_lhs,
+    reject_arbitrary_lhs,
+    reject_continue,
+    reject_question_mark,
+    reject_raw_or_mut_pointer,
+    reject_early_exit,
+    reject_as_pattern,
+    reject_dyn,
+    reject_trait_item_default,
+    reject_unsafe,
+    hoist_side_effects
+);