diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
index 91d3ad30..e312aef4 100644
--- a/charon-ml/src/CharonVersion.ml
+++ b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.60"
+let supported_charon_version = "0.1.61"
diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml
index 010ce869..a1803c0e 100644
--- a/charon-ml/src/generated/Generated_GAst.ml
+++ b/charon-ml/src/generated/Generated_GAst.ml
@@ -113,14 +113,6 @@ and call = { func : fn_operand; args : operand list; dest : place }
  *)
 and assertion = { cond : operand; expected : bool }
 
-(** The id of a translated item. *)
-and any_decl_id =
-  | IdType of type_decl_id
-  | IdFun of fun_decl_id
-  | IdGlobal of global_decl_id
-  | IdTraitDecl of trait_decl_id
-  | IdTraitImpl of trait_impl_id
-
 and closure_kind = Fn | FnMut | FnOnce
 
 (** Additional information for closures.
diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml
index a28270ad..6222a456 100644
--- a/charon-ml/src/generated/Generated_GAstOfJson.ml
+++ b/charon-ml/src/generated/Generated_GAstOfJson.ml
@@ -1057,6 +1057,20 @@ and trait_type_constraint_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ trait_ref; type_name; ty } : trait_type_constraint)
     | _ -> Error "")
 
+and generics_source_of_json (ctx : of_json_ctx) (js : json) :
+    (generics_source, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("Item", item) ] ->
+        let* item = any_decl_id_of_json ctx item in
+        Ok (Item item)
+    | `Assoc [ ("Method", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = trait_decl_id_of_json ctx x_0 in
+        let* x_1 = trait_item_name_of_json ctx x_1 in
+        Ok (Method (x_0, x_1))
+    | `String "Builtin" -> Ok Builtin
+    | _ -> Error "")
+
 and generic_args_of_json (ctx : of_json_ctx) (js : json) :
     (generic_args, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1067,6 +1081,7 @@ and generic_args_of_json (ctx : of_json_ctx) (js : json) :
           ("types", types);
           ("const_generics", const_generics);
           ("trait_refs", trait_refs);
+          ("target", _);
         ] ->
         let* regions =
           vector_of_json region_id_of_json region_of_json ctx regions
diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml
index d0c6a6ea..261470f0 100644
--- a/charon-ml/src/generated/Generated_Types.ml
+++ b/charon-ml/src/generated/Generated_Types.ml
@@ -298,8 +298,16 @@ class virtual ['self] mapreduce_const_generic_base =
       fun _ x -> (x, self#zero)
   end
 
+(** The id of a translated item. *)
+type any_decl_id =
+  | IdType of type_decl_id
+  | IdFun of fun_decl_id
+  | IdGlobal of global_decl_id
+  | IdTraitDecl of trait_decl_id
+  | IdTraitImpl of trait_impl_id
+
 (** Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value *)
-type const_generic =
+and const_generic =
   | CgGlobal of global_decl_id  (** A global constant *)
   | CgVar of const_generic_var_id de_bruijn_var  (** A const generic variable *)
   | CgValue of literal  (** A concrete value *)
@@ -549,6 +557,13 @@ and trait_impl_ref = {
   impl_generics : generic_args;
 }
 
+(** Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. *)
+and generics_source =
+  | Item of any_decl_id  (** A top-level item. *)
+  | Method of trait_decl_id * trait_item_name  (** A trait method. *)
+  | Builtin  (** A builtin item like `Box`. *)
+
+(** A set of generic arguments. *)
 and generic_args = {
   regions : region list;
   types : ty list;
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 4535df23..c7fb22fc 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -213,7 +213,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.60"
+version = "0.1.61"
 dependencies = [
  "annotate-snippets",
  "anstream",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index 8579aee2..5d060a00 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.60"
+version = "0.1.61"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"
diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs
index e6bcca84..5f985792 100644
--- a/charon/src/ast/krate.rs
+++ b/charon/src/ast/krate.rs
@@ -218,15 +218,21 @@ impl<'ctx> AnyTransItem<'ctx> {
         }
     }
 
+    /// See [`GenericParams::identity_args`].
+    pub fn identity_args(&self) -> GenericArgs {
+        self.generic_params()
+            .identity_args(GenericsSource::Item(self.id()))
+    }
+
     /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
     /// `AnyTransItem` isn't contained in any of our types.
     pub fn drive<V: VisitAst>(&self, visitor: &mut V) -> ControlFlow<V::Break> {
-        match self {
-            AnyTransItem::Type(d) => d.drive(visitor),
-            AnyTransItem::Fun(d) => d.drive(visitor),
-            AnyTransItem::Global(d) => d.drive(visitor),
-            AnyTransItem::TraitDecl(d) => d.drive(visitor),
-            AnyTransItem::TraitImpl(d) => d.drive(visitor),
+        match *self {
+            AnyTransItem::Type(d) => visitor.visit(d),
+            AnyTransItem::Fun(d) => visitor.visit(d),
+            AnyTransItem::Global(d) => visitor.visit(d),
+            AnyTransItem::TraitDecl(d) => visitor.visit(d),
+            AnyTransItem::TraitImpl(d) => visitor.visit(d),
         }
     }
 }
@@ -257,11 +263,11 @@ impl<'ctx> AnyTransItemMut<'ctx> {
     /// `AnyTransItemMut` isn't contained in any of our types.
     pub fn drive_mut<V: VisitAstMut>(&mut self, visitor: &mut V) -> ControlFlow<V::Break> {
         match self {
-            AnyTransItemMut::Type(d) => d.drive_mut(visitor),
-            AnyTransItemMut::Fun(d) => d.drive_mut(visitor),
-            AnyTransItemMut::Global(d) => d.drive_mut(visitor),
-            AnyTransItemMut::TraitDecl(d) => d.drive_mut(visitor),
-            AnyTransItemMut::TraitImpl(d) => d.drive_mut(visitor),
+            AnyTransItemMut::Type(d) => visitor.visit(*d),
+            AnyTransItemMut::Fun(d) => visitor.visit(*d),
+            AnyTransItemMut::Global(d) => visitor.visit(*d),
+            AnyTransItemMut::TraitDecl(d) => visitor.visit(*d),
+            AnyTransItemMut::TraitImpl(d) => visitor.visit(*d),
         }
     }
 }
diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs
index 7f29b2e3..e6b4b67d 100644
--- a/charon/src/ast/types.rs
+++ b/charon/src/ast/types.rs
@@ -195,13 +195,29 @@ pub struct TraitTypeConstraint {
     pub ty: Ty,
 }
 
-#[derive(Default, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+/// Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one.
+#[derive(Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+pub enum GenericsSource {
+    /// A top-level item.
+    Item(AnyTransId),
+    /// A trait method.
+    Method(TraitDeclId, TraitItemName),
+    /// A builtin item like `Box`.
+    Builtin,
+}
+
+/// A set of generic arguments.
+#[derive(Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct GenericArgs {
     pub regions: Vector<RegionId, Region>,
     pub types: Vector<TypeVarId, Ty>,
     pub const_generics: Vector<ConstGenericVarId, ConstGeneric>,
     // TODO: rename to match [GenericParams]?
     pub trait_refs: Vector<TraitClauseId, TraitRef>,
+    #[charon::opaque]
+    #[drive(skip)]
+    /// Each `GenericArgs` is meant for a corresponding `GenericParams`; this records which one.
+    pub target: GenericsSource,
 }
 
 /// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs
index 7b7aac53..e6e16bee 100644
--- a/charon/src/ast/types_utils.rs
+++ b/charon/src/ast/types_utils.rs
@@ -5,6 +5,7 @@ use derive_generic_visitor::*;
 use std::collections::HashSet;
 use std::convert::Infallible;
 use std::iter::Iterator;
+use std::mem;
 use std::ops::Index;
 
 impl GenericParams {
@@ -71,12 +72,12 @@ impl GenericParams {
     /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds
     /// each required parameter with itself. E.g. given parameters for `<T, U> where U:
     /// PartialEq<T>`, the arguments would be `<T, U>[@TraitClause0]`.
-    pub fn identity_args(&self) -> GenericArgs {
-        self.identity_args_at_depth(DeBruijnId::zero())
+    pub fn identity_args(&self, target: GenericsSource) -> GenericArgs {
+        self.identity_args_at_depth(target, DeBruijnId::zero())
     }
 
     /// Like `identity_args` but uses variables bound at the given depth.
-    pub fn identity_args_at_depth(&self, depth: DeBruijnId) -> GenericArgs {
+    pub fn identity_args_at_depth(&self, target: GenericsSource, depth: DeBruijnId) -> GenericArgs {
         GenericArgs {
             regions: self
                 .regions
@@ -91,25 +92,7 @@ impl GenericParams {
                 kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, id)),
                 trait_decl_ref: clause.trait_.clone(),
             }),
-        }
-    }
-
-    /// Like `identity_args`, but uses free variables instead of bound ones.
-    pub fn free_identity_args(&self) -> GenericArgs {
-        GenericArgs {
-            regions: self
-                .regions
-                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::free(id))),
-            types: self
-                .types
-                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()),
-            const_generics: self
-                .const_generics
-                .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::free(id))),
-            trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef {
-                kind: TraitRefKind::Clause(DeBruijnVar::free(id)),
-                trait_decl_ref: clause.trait_.clone(),
-            }),
+            target,
         }
     }
 }
@@ -142,6 +125,7 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs,
+            target: _,
         } = self;
         regions.len() + types.len() + const_generics.len() + trait_refs.len()
     }
@@ -150,14 +134,20 @@ impl GenericArgs {
         self.len() == 0
     }
 
-    pub fn empty() -> Self {
-        GenericArgs::default()
+    pub fn empty(target: GenericsSource) -> Self {
+        GenericArgs {
+            regions: Default::default(),
+            types: Default::default(),
+            const_generics: Default::default(),
+            trait_refs: Default::default(),
+            target,
+        }
     }
 
-    pub fn new_from_types(types: Vector<TypeVarId, Ty>) -> Self {
+    pub fn new_for_builtin(types: Vector<TypeVarId, Ty>) -> Self {
         GenericArgs {
             types,
-            ..Self::default()
+            ..Self::empty(GenericsSource::Builtin)
         }
     }
 
@@ -166,15 +156,23 @@ impl GenericArgs {
         types: Vector<TypeVarId, Ty>,
         const_generics: Vector<ConstGenericVarId, ConstGeneric>,
         trait_refs: Vector<TraitClauseId, TraitRef>,
+        target: GenericsSource,
     ) -> Self {
         Self {
             regions,
             types,
             const_generics,
             trait_refs,
+            target,
         }
     }
 
+    /// Changes the target.
+    pub fn with_target(mut self, target: GenericsSource) -> Self {
+        self.target = target;
+        self
+    }
+
     /// Check whether this matches the given `GenericParams`.
     /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
     pub fn matches(&self, params: &GenericParams) -> bool {
@@ -189,43 +187,38 @@ impl GenericArgs {
     /// because the first type argument is the type for which the trait is
     /// implemented.
     pub fn pop_first_type_arg(&self) -> (Ty, Self) {
-        let GenericArgs {
-            regions,
-            types,
-            const_generics,
-            trait_refs,
-        } = self;
-        let mut it = types.iter();
-        let ty = it.next().unwrap().clone();
-        let types = it.cloned().collect();
-        (
-            ty,
-            GenericArgs {
-                regions: regions.clone(),
-                types,
-                const_generics: const_generics.clone(),
-                trait_refs: trait_refs.clone(),
-            },
-        )
+        let mut generics = self.clone();
+        let mut it = mem::take(&mut generics.types).into_iter();
+        let ty = it.next().unwrap();
+        generics.types = it.collect();
+        (ty, generics)
     }
 
     /// Concatenate this set of arguments with another one. Use with care, you must manage the
     /// order of arguments correctly.
-    pub fn concat(mut self, other: &Self) -> Self {
+    pub fn concat(mut self, target: GenericsSource, other: &Self) -> Self {
         let Self {
             regions,
             types,
             const_generics,
             trait_refs,
+            target: _,
         } = other;
         self.regions.extend_from_slice(regions);
         self.types.extend_from_slice(types);
         self.const_generics.extend_from_slice(const_generics);
         self.trait_refs.extend_from_slice(trait_refs);
+        self.target = target;
         self
     }
 }
 
+impl GenericsSource {
+    pub fn item<I: Into<AnyTransId>>(id: I) -> Self {
+        Self::Item(id.into())
+    }
+}
+
 impl IntegerTy {
     pub fn is_signed(&self) -> bool {
         matches!(
@@ -278,7 +271,7 @@ impl Ty {
 
     /// Return the unit type
     pub fn mk_unit() -> Ty {
-        TyKind::Adt(TypeId::Tuple, GenericArgs::empty()).into_ty()
+        TyKind::Adt(TypeId::Tuple, GenericArgs::empty(GenericsSource::Builtin)).into_ty()
     }
 
     /// Return true if this is a scalar type
@@ -381,6 +374,35 @@ impl std::ops::Deref for Ty {
 /// For deref patterns.
 unsafe impl std::ops::DerefPure for Ty {}
 
+impl TypeId {
+    pub fn generics_target(&self) -> GenericsSource {
+        match *self {
+            TypeId::Adt(decl_id) => GenericsSource::item(decl_id),
+            TypeId::Tuple | TypeId::Builtin(..) => GenericsSource::Builtin,
+        }
+    }
+}
+
+impl FunId {
+    pub fn generics_target(&self) -> GenericsSource {
+        match *self {
+            FunId::Regular(fun_id) => GenericsSource::item(fun_id),
+            FunId::Builtin(..) => GenericsSource::Builtin,
+        }
+    }
+}
+
+impl FunIdOrTraitMethodRef {
+    pub fn generics_target(&self) -> GenericsSource {
+        match self {
+            FunIdOrTraitMethodRef::Fun(fun_id) => fun_id.generics_target(),
+            FunIdOrTraitMethodRef::Trait(trait_ref, name, _) => {
+                GenericsSource::Method(trait_ref.trait_decl_ref.skip_binder.trait_id, name.clone())
+            }
+        }
+    }
+}
+
 impl Field {
     /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
     pub fn renamed_name(&self) -> Option<&str> {
diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs
index e9be37b8..7930530e 100644
--- a/charon/src/ast/visitor.rs
+++ b/charon/src/ast/visitor.rs
@@ -75,6 +75,10 @@ use index_vec::Idx;
     )
 )]
 pub trait AstVisitable: Any {
+    /// The name of the type, used for debug logging.
+    fn name(&self) -> &'static str {
+        std::any::type_name::<Self>()
+    }
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
         self.drive(&mut DynVisitor::new_shared::<T>(f));
diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs
index 46bf9c6c..a8822d9e 100644
--- a/charon/src/bin/charon-driver/driver.rs
+++ b/charon/src/bin/charon-driver/driver.rs
@@ -1,9 +1,9 @@
 use crate::translate::translate_crate_to_ullbc;
 use charon_lib::export;
 use charon_lib::options;
-use charon_lib::reorder_decls::compute_reordered_decls;
-use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES};
-use charon_lib::ullbc_to_llbc;
+use charon_lib::transform::{
+    FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, ULLBC_PASSES,
+};
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface::Compiler, Queries};
 use rustc_middle::ty::TyCtxt;
@@ -231,6 +231,10 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
     // serializing the result.
 
     // Run the micro-passes that clean up bodies.
+    for pass in INITIAL_CLEANUP_PASSES.iter() {
+        trace!("# Starting pass {}", pass.name());
+        pass.run(&mut ctx)
+    }
     for pass in ULLBC_PASSES.iter() {
         trace!("# Starting pass {}", pass.name());
         pass.run(&mut ctx)
@@ -252,28 +256,12 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
     // - or they want the structured LLBC, in which case we reconstruct the
     //   control-flow and apply micro-passes
     if !options.ullbc {
-        // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing
-        // the control flow.
-        ullbc_to_llbc::translate_functions(&mut ctx);
-
-        if options.print_built_llbc {
-            info!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",);
-        }
-
         // Run the micro-passes that clean up bodies.
         for pass in LLBC_PASSES.iter() {
             trace!("# Starting pass {}", pass.name());
             pass.run(&mut ctx)
         }
 
-        // # Reorder the graph of dependencies and compute the strictly
-        // connex components to:
-        // - compute the order in which to extract the definitions
-        // - find the recursive definitions
-        // - group the mutually recursive definitions
-        let reordered_decls = compute_reordered_decls(&ctx);
-        ctx.translated.ordered_decls = Some(reordered_decls);
-
         if options.print_llbc {
             println!("# Final LLBC before serialization:\n\n{ctx}\n");
         } else {
@@ -281,7 +269,11 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
         }
     }
 
-    trace!("Done");
+    // Final passes before serialization.
+    for pass in FINAL_CLEANUP_PASSES.iter() {
+        trace!("# Starting pass {}", pass.name());
+        pass.run(&mut ctx)
+    }
 
     // Update the error count
     internal.error_count = ctx.errors.error_count;
diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
index 2c394e5c..c4602c2b 100644
--- a/charon/src/bin/charon-driver/translate/translate_constants.rs
+++ b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -112,9 +112,14 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     generics,
                     trait_refs
                 );
-                let generics = self.translate_generic_args(span, generics, trait_refs, None)?;
-
                 let global_id = self.register_global_decl_id(span, id);
+                let generics = self.translate_generic_args(
+                    span,
+                    generics,
+                    trait_refs,
+                    None,
+                    GenericsSource::item(global_id),
+                )?;
                 RawConstantExpr::Global(GlobalDeclRef {
                     id: global_id,
                     generics,
diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
index 8bf96436..910e2579 100644
--- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
@@ -301,6 +301,7 @@ pub fn translate<'tcx, 'ctx>(
         no_code_duplication: options.no_code_duplication,
         hide_marker_traits: options.hide_marker_traits,
         no_merge_goto_chains: options.no_merge_goto_chains,
+        print_built_llbc: options.print_built_llbc,
         item_opacities: ctx.options.item_opacities,
     };
 
diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
index 31bd020c..febc01d4 100644
--- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -127,13 +127,15 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 overrides_default,
                 ..
             } => {
+                let impl_id = self.register_trait_impl_id(span, impl_id);
                 let impl_ref = TraitImplRef {
-                    impl_id: self.register_trait_impl_id(span, impl_id),
+                    impl_id,
                     generics: self.translate_generic_args(
                         span,
                         impl_generics,
                         impl_required_impl_exprs,
                         None,
+                        GenericsSource::item(impl_id),
                     )?,
                 };
                 let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
@@ -648,7 +650,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         ))
                     }
                     hax::AggregateKind::Tuple => Ok(Rvalue::Aggregate(
-                        AggregateKind::Adt(TypeId::Tuple, None, None, GenericArgs::empty()),
+                        AggregateKind::Adt(
+                            TypeId::Tuple,
+                            None,
+                            None,
+                            GenericArgs::empty(GenericsSource::Builtin),
+                        ),
                         operands_t,
                     )),
                     hax::AggregateKind::Adt(
@@ -666,13 +673,18 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         // types we need.
                         let _ = user_annotation;
 
-                        // Translate the substitution
-                        let generics =
-                            self.translate_generic_args(span, substs, trait_refs, None)?;
-
                         let type_id = self.translate_type_id(span, adt_id)?;
                         // Sanity check
-                        matches!(&type_id, TypeId::Adt(_));
+                        assert!(matches!(&type_id, TypeId::Adt(_)));
+
+                        // Translate the substitution
+                        let generics = self.translate_generic_args(
+                            span,
+                            substs,
+                            trait_refs,
+                            None,
+                            type_id.generics_target(),
+                        )?;
 
                         use hax::AdtKind;
                         let variant_id = match kind {
@@ -694,6 +706,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                             closure_args.tupled_sig
                         );
 
+                        let fun_id = self.register_fun_decl_id(span, def_id);
+
                         // Retrieve the late-bound variables.
                         let binder = closure_args.tupled_sig.as_ref().rebind(());
                         // Translate the substitution
@@ -702,10 +716,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                             &closure_args.parent_args,
                             &closure_args.parent_trait_refs,
                             Some(binder),
+                            GenericsSource::item(fun_id),
                         )?;
 
-                        let def_id = self.register_fun_decl_id(span, def_id);
-                        let akind = AggregateKind::Closure(def_id, generics);
+                        let akind = AggregateKind::Closure(fun_id, generics);
 
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
@@ -782,14 +796,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             _ => None,
         };
 
-        // Translate the type parameters
-        let generics = self.translate_generic_args(span, substs, trait_refs, binder)?;
-
-        // Translate the arguments
-        let args = args
-            .map(|args| self.translate_arguments(span, args))
-            .transpose()?;
-
         // Trait information
         trace!(
             "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}",
@@ -804,7 +810,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
         // Check if the function is considered primitive: primitive
         // functions benefit from special treatment.
-        let func = if let Some(builtin_fun) = builtin_fun {
+        let fun_id = if let Some(builtin_fun) = builtin_fun {
             // Primitive function.
             //
             // Note that there are subtleties with regards to the way types parameters
@@ -859,8 +865,26 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 }
             }
         };
+
+        // Translate the type parameters
+        let generics = self.translate_generic_args(
+            span,
+            substs,
+            trait_refs,
+            binder,
+            fun_id.generics_target(),
+        )?;
+
+        // Translate the arguments
+        let args = args
+            .map(|args| self.translate_arguments(span, args))
+            .transpose()?;
+
         let sfid = SubstFunId {
-            func: FnPtr { func, generics },
+            func: FnPtr {
+                func: fun_id,
+                generics,
+            },
             args,
         };
         Ok(SubstFunIdOrPanic::Fun(sfid))
@@ -1321,7 +1345,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                             TypeId::Adt(adt_decl_id),
                             variant,
                             None,
-                            sig.generics.identity_args(),
+                            sig.generics
+                                .identity_args(GenericsSource::item(adt_decl_id)),
                         ),
                         args,
                     ),
@@ -1486,7 +1511,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 let state_ty = {
                     // Group the state types into a tuple
                     let state_ty =
-                        TyKind::Adt(TypeId::Tuple, GenericArgs::new_from_types(state.clone()))
+                        TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(state.clone()))
                             .into_ty();
                     // Depending on the kind of the closure, add a reference
                     match &kind {
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 771faa95..874e7168 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -37,15 +37,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         Ok(())
     }
 
-    pub(crate) fn translate_trait_decl_ref(
+    pub(crate) fn translate_poly_trait_ref(
         &mut self,
         span: Span,
         bound_trait_ref: &hax::Binder<hax::TraitRef>,
     ) -> Result<PolyTraitDeclRef, Error> {
         self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
-            let trait_id = ctx.register_trait_decl_id(span, &trait_ref.def_id);
-            let generics = ctx.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
-            Ok(TraitDeclRef { trait_id, generics })
+            ctx.translate_trait_ref(span, trait_ref)
         })
     }
 
@@ -66,7 +64,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<TraitDeclRef, Error> {
         let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
         // For now a trait has no required bounds, so we pass an empty list.
-        let generics = self.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
+        let generics = self.translate_generic_args(
+            span,
+            &trait_ref.generic_args,
+            &[],
+            None,
+            GenericsSource::item(trait_id),
+        )?;
         Ok(TraitDeclRef { trait_id, generics })
     }
 
@@ -188,7 +192,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         span: Span,
         impl_expr: &hax::ImplExpr,
     ) -> Result<TraitRef, Error> {
-        let trait_decl_ref = self.translate_trait_decl_ref(span, &impl_expr.r#trait)?;
+        let trait_decl_ref = self.translate_poly_trait_ref(span, &impl_expr.r#trait)?;
 
         match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
             Ok(res) => Ok(res),
@@ -223,7 +227,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 generics,
             } => {
                 let impl_id = self.register_trait_impl_id(span, impl_def_id);
-                let generics = self.translate_generic_args(span, generics, nested, None)?;
+                let generics = self.translate_generic_args(
+                    span,
+                    generics,
+                    nested,
+                    None,
+                    GenericsSource::item(impl_id),
+                )?;
                 TraitRef {
                     kind: TraitRefKind::TraitImpl(impl_id, generics),
                     trait_decl_ref,
diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 22ebd791..e919ff32 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -95,12 +95,13 @@ impl BodyTransCtx<'_, '_> {
                         let fun_generics = bt_ctx
                             .outermost_binder()
                             .params
-                            .identity_args_at_depth(DeBruijnId::one())
+                            .identity_args_at_depth(GenericsSource::item(def_id), DeBruijnId::one())
                             .concat(
-                                &bt_ctx
-                                    .innermost_binder()
-                                    .params
-                                    .identity_args_at_depth(DeBruijnId::zero()),
+                                GenericsSource::item(fun_id),
+                                &bt_ctx.innermost_binder().params.identity_args_at_depth(
+                                    GenericsSource::Method(def_id.into(), item_name.clone()),
+                                    DeBruijnId::zero(),
+                                ),
                             );
                         Ok(FunDeclRef {
                             id: fun_id,
@@ -120,9 +121,11 @@ impl BodyTransCtx<'_, '_> {
                     if hax_item.has_value {
                         // The parameters of the constant are the same as those of the item that
                         // declares them.
+                        let id = self.register_global_decl_id(item_span, item_def_id);
+                        let generics_target = GenericsSource::item(id);
                         let gref = GlobalDeclRef {
-                            id: self.register_global_decl_id(item_span, item_def_id),
-                            generics: self.the_only_binder().params.identity_args(),
+                            id,
+                            generics: self.the_only_binder().params.identity_args(generics_target),
                         };
                         const_defaults.insert(item_name.clone(), gref);
                     };
@@ -211,8 +214,13 @@ impl BodyTransCtx<'_, '_> {
         let trait_id = self.register_trait_decl_id(span, implemented_trait_id);
         let implemented_trait = {
             let implemented_trait = &trait_pred.trait_ref;
-            let generics =
-                self.translate_generic_args(span, &implemented_trait.generic_args, &[], None)?;
+            let generics = self.translate_generic_args(
+                span,
+                &implemented_trait.generic_args,
+                &[],
+                None,
+                GenericsSource::item(trait_id),
+            )?;
             TraitDeclRef { trait_id, generics }
         };
 
@@ -256,12 +264,22 @@ impl BodyTransCtx<'_, '_> {
                                     let fun_generics = bt_ctx
                                         .outermost_binder()
                                         .params
-                                        .identity_args_at_depth(DeBruijnId::one())
+                                        .identity_args_at_depth(
+                                            GenericsSource::item(def_id),
+                                            DeBruijnId::one(),
+                                        )
                                         .concat(
+                                            GenericsSource::item(fun_id),
                                             &bt_ctx
                                                 .innermost_binder()
                                                 .params
-                                                .identity_args_at_depth(DeBruijnId::zero()),
+                                                .identity_args_at_depth(
+                                                    GenericsSource::Method(
+                                                        trait_id.into(),
+                                                        name.clone(),
+                                                    ),
+                                                    DeBruijnId::zero(),
+                                                ),
                                         );
                                     Ok(FunDeclRef {
                                         id: fun_id,
@@ -282,11 +300,17 @@ impl BodyTransCtx<'_, '_> {
                 }
                 hax::FullDefKind::AssocConst { .. } => {
                     let id = self.register_global_decl_id(item_span, item_def_id);
+                    let generics_target = GenericsSource::item(id);
                     // The parameters of the constant are the same as those of the item that
                     // declares them.
                     let generics = match &impl_item.value {
-                        Provided { .. } => self.the_only_binder().params.identity_args(),
-                        _ => implemented_trait.generics.clone(),
+                        Provided { .. } => {
+                            self.the_only_binder().params.identity_args(generics_target)
+                        }
+                        _ => implemented_trait
+                            .generics
+                            .clone()
+                            .with_target(generics_target),
                     };
                     let gref = GlobalDeclRef { id, generics };
                     consts.push((name, gref));
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 04c57fb1..34541ebb 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -144,12 +144,18 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             } => {
                 trace!("Adt: {:?}", def_id);
 
-                // Translate the type parameters instantiation
-                let mut generics = self.translate_generic_args(span, substs, trait_refs, None)?;
-
                 // Retrieve the type identifier
                 let type_id = self.translate_type_id(span, def_id)?;
 
+                // Translate the type parameters instantiation
+                let mut generics = self.translate_generic_args(
+                    span,
+                    substs,
+                    trait_refs,
+                    None,
+                    type_id.generics_target(),
+                )?;
+
                 // Filter the type arguments.
                 // TODO: do this in a micro-pass
                 if let TypeId::Builtin(builtin_ty) = type_id {
@@ -171,7 +177,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 trace!("Str");
 
                 let id = TypeId::Builtin(BuiltinTy::Str);
-                TyKind::Adt(id, GenericArgs::empty())
+                TyKind::Adt(id, GenericArgs::empty(GenericsSource::Builtin))
             }
             hax::TyKind::Array(ty, const_param) => {
                 trace!("Array");
@@ -180,14 +186,23 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 let tys = vec![self.translate_ty(span, ty)?].into();
                 let cgs = vec![c].into();
                 let id = TypeId::Builtin(BuiltinTy::Array);
-                TyKind::Adt(id, GenericArgs::new(Vector::new(), tys, cgs, Vector::new()))
+                TyKind::Adt(
+                    id,
+                    GenericArgs::new(
+                        Vector::new(),
+                        tys,
+                        cgs,
+                        Vector::new(),
+                        GenericsSource::Builtin,
+                    ),
+                )
             }
             hax::TyKind::Slice(ty) => {
                 trace!("Slice");
 
                 let tys = vec![self.translate_ty(span, ty)?].into();
                 let id = TypeId::Builtin(BuiltinTy::Slice);
-                TyKind::Adt(id, GenericArgs::new_from_types(tys))
+                TyKind::Adt(id, GenericArgs::new_for_builtin(tys))
             }
             hax::TyKind::Ref(region, ty, mutability) => {
                 trace!("Ref");
@@ -220,7 +235,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     params.push(param_ty);
                 }
 
-                TyKind::Adt(TypeId::Tuple, GenericArgs::new_from_types(params))
+                TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(params))
             }
 
             hax::TyKind::Param(param) => {
@@ -240,8 +255,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
             hax::TyKind::Foreign(def_id) => {
                 trace!("Foreign");
-                let def_id = self.translate_type_id(span, def_id)?;
-                TyKind::Adt(def_id, GenericArgs::empty())
+                let adt_id = self.translate_type_id(span, def_id)?;
+                TyKind::Adt(adt_id, GenericArgs::empty(adt_id.generics_target()))
             }
             hax::TyKind::Infer(_) => {
                 trace!("Infer");
@@ -310,6 +325,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         substs: &[hax::GenericArg],
         trait_refs: &[hax::ImplExpr],
         late_bound: Option<hax::Binder<()>>,
+        target: GenericsSource,
     ) -> Result<GenericArgs, Error> {
         use hax::GenericArg::*;
         trace!("{:?}", substs);
@@ -353,6 +369,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             types,
             const_generics,
             trait_refs,
+            target,
         })
     }
 
diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs
index b60bd70f..8941ac33 100644
--- a/charon/src/bin/generate-ml/main.rs
+++ b/charon/src/bin/generate-ml/main.rs
@@ -1118,7 +1118,6 @@ fn generate_ml(
                     extra_types: &[],
                 })), &[
                     "Var",
-                    "AnyTransId",
                     "FnOperand",
                     "Call",
                     "Assert",
@@ -1253,6 +1252,7 @@ fn generate_ml(
                         "type_var_id",
                     ],
                 })), &[
+                    "AnyTransId",
                     "ConstGeneric",
                 ]),
                 // Can't merge into above because aeneas uses the above alongside their own partial
@@ -1276,6 +1276,7 @@ fn generate_ml(
                     "TraitImplRef",
                     "FunDeclRef",
                     "GlobalDeclRef",
+                    "GenericsSource",
                     "GenericArgs",
                 ]),
                 // TODO: can't merge into above because of field name clashes (`types`, `regions` etc).
diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs
index a53b486c..d521c9e8 100644
--- a/charon/src/name_matcher/mod.rs
+++ b/charon/src/name_matcher/mod.rs
@@ -49,14 +49,20 @@ impl Pattern {
     }
 
     pub fn matches(&self, ctx: &TranslatedCrate, name: &Name) -> bool {
-        self.matches_with_generics(ctx, name, &GenericArgs::empty())
+        self.matches_with_generics(ctx, name, None)
+    }
+
+    pub fn matches_item(&self, ctx: &TranslatedCrate, item: AnyTransItem<'_>) -> bool {
+        let generics = item.identity_args();
+        let name = &item.item_meta().name;
+        self.matches_with_generics(ctx, name, Some(&generics))
     }
 
     pub fn matches_with_generics(
         &self,
         ctx: &TranslatedCrate,
         name: &Name,
-        args: &GenericArgs,
+        args: Option<&GenericArgs>,
     ) -> bool {
         let zipped = self.elems.iter().zip_longest(&name.name).collect_vec();
         let zipped_len = zipped.len();
@@ -64,7 +70,7 @@ impl Pattern {
             let is_last = i + 1 == zipped_len;
             match x {
                 EitherOrBoth::Both(pat, elem) => {
-                    let args = if is_last { args } else { &GenericArgs::empty() };
+                    let args = if is_last { args } else { None };
                     if !pat.matches_with_generics(ctx, elem, args) {
                         return false;
                     }
@@ -89,11 +95,11 @@ impl Pattern {
                 let Some(type_name) = ctx.item_name(*type_id) else {
                     return false;
                 };
-                self.matches_with_generics(ctx, type_name, args)
+                self.matches_with_generics(ctx, type_name, Some(args))
             }
             TyKind::Adt(TypeId::Builtin(builtin_ty), args) => {
                 let name = builtin_ty.get_name();
-                self.matches_with_generics(ctx, &name, args)
+                self.matches_with_generics(ctx, &name, Some(args))
             }
             TyKind::Adt(TypeId::Tuple, _)
             | TyKind::TypeVar(..)
@@ -153,7 +159,7 @@ impl PatElem {
         &self,
         ctx: &TranslatedCrate,
         elem: &PathElem,
-        args: &GenericArgs,
+        args: Option<&GenericArgs>,
     ) -> bool {
         match (self, elem) {
             (PatElem::Glob, _) => true,
@@ -168,7 +174,7 @@ impl PatElem {
                 // `crate` is a special keyword that referes to the current crate.
                 let same_ident =
                     pat_ident == ident || (pat_ident == "crate" && ident == &ctx.real_crate_name);
-                same_ident && (generics.is_empty() || PatTy::matches_generics(ctx, generics, args))
+                same_ident && PatTy::matches_generics(ctx, generics, args)
             }
             (PatElem::Impl(_pat), PathElem::Impl(ImplElem::Ty(..), _)) => {
                 // TODO
@@ -181,7 +187,7 @@ impl PatElem {
                 let Some(trait_name) = ctx.item_name(timpl.impl_trait.trait_id) else {
                     return false;
                 };
-                pat.matches_with_generics(ctx, trait_name, &timpl.impl_trait.generics)
+                pat.matches_with_generics(ctx, trait_name, Some(&timpl.impl_trait.generics))
             }
             _ => false,
         }
@@ -189,7 +195,19 @@ impl PatElem {
 }
 
 impl PatTy {
-    pub fn matches_generics(ctx: &TranslatedCrate, pats: &[Self], generics: &GenericArgs) -> bool {
+    pub fn matches_generics(
+        ctx: &TranslatedCrate,
+        pats: &[Self],
+        generics: Option<&GenericArgs>,
+    ) -> bool {
+        let Some(generics) = generics else {
+            // If we'r ematching on a plain name without generics info, we ignore pattern generics.
+            return true;
+        };
+        if pats.is_empty() {
+            // If no generics are provided, this counts as a match.
+            return true;
+        }
         // We don't include regions in patterns.
         if pats.len() != generics.types.len() + generics.const_generics.len() {
             return false;
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index 962317ab..fe4b0543 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -304,6 +304,7 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs: _,
+            target: _,
         } = self;
         for x in regions {
             params.push(x.fmt_with_ctx(ctx));
@@ -327,6 +328,7 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs,
+            target: _,
         } = self;
         for x in regions {
             params.push(x.fmt_with_ctx(ctx));
diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs
index 964c9208..13e0763a 100644
--- a/charon/src/transform/check_generics.rs
+++ b/charon/src/transform/check_generics.rs
@@ -1,5 +1,6 @@
 //! Check that all supplied generic types match the corresponding generic parameters.
 use derive_generic_visitor::*;
+use itertools::Itertools;
 use std::fmt::Display;
 
 use crate::{errors::ErrorCtx, llbc_ast::*, register_error_or_panic};
@@ -9,142 +10,76 @@ use super::{ctx::TransformPass, TransformCtx};
 #[derive(Visitor)]
 struct CheckGenericsVisitor<'a> {
     translated: &'a TranslatedCrate,
+    phase: &'static str,
     error_ctx: &'a mut ErrorCtx,
-    // Count how many `GenericArgs` we handled. This is to make sure we don't miss one.
-    discharged_args: u32,
     // Tracks an enclosing span to make errors useful.
-    item_span: Span,
+    span: Span,
+    /// Remember the names of the types visited up to here.
+    visit_stack: Vec<&'static str>,
 }
 
 impl CheckGenericsVisitor<'_> {
     fn error(&mut self, message: impl Display) {
-        let span = self.item_span;
-        let message = message.to_string();
-        register_error_or_panic!(self.error_ctx, self.translated, span, message);
-    }
-
-    /// Count that we just discharged one instance of `GenericArgs`.
-    fn discharged_one_generics(&mut self) {
-        self.discharged_args += 1;
-    }
-
-    fn generics_should_match(&mut self, args: &GenericArgs, params: &GenericParams) {
-        self.discharged_one_generics();
-        if !args.matches(params) {
-            self.error(format!(
-                "Mismatched generics:\nexpected: {params:?}\n     got: {args:?}"
-            ))
-        }
-    }
-    fn generics_should_match_item(&mut self, args: &GenericArgs, item_id: impl Into<AnyTransId>) {
-        if let Some(item) = self.translated.get_item(item_id.into()) {
-            let params = item.generic_params();
-            self.generics_should_match(args, params);
-        } else {
-            self.discharged_one_generics();
-        }
-    }
-    fn check_typeid_generics(&mut self, args: &GenericArgs, ty_kind: &TypeId) {
-        match ty_kind {
-            TypeId::Adt(id) => self.generics_should_match_item(args, *id),
-            TypeId::Tuple => {
-                self.discharged_one_generics();
-                if !(args.regions.is_empty()
-                    && args.const_generics.is_empty()
-                    && args.trait_refs.is_empty())
-                {
-                    self.error("Mismatched generics: generics for a tuple should be only types")
-                }
-            }
-            TypeId::Builtin(..) => {
-                // TODO: check generics for built-in types
-                self.discharged_one_generics()
-            }
-        }
+        let message = format!(
+            "Found inconsistent generics {}:\n{message}\nVisitor stack:\n  {}",
+            self.phase,
+            self.visit_stack.iter().rev().join("\n  ")
+        );
+        register_error_or_panic!(self.error_ctx, self.translated, self.span, message);
     }
 }
 
-// Visitor functions
 impl VisitAst for CheckGenericsVisitor<'_> {
-    fn enter_aggregate_kind(&mut self, agg: &AggregateKind) {
+    fn visit<'a, T: AstVisitable>(&'a mut self, x: &T) -> ControlFlow<Self::Break> {
+        self.visit_stack.push(x.name());
+        x.drive(self)?; // default behavior
+        self.visit_stack.pop();
+        Continue(())
+    }
+
+    fn visit_aggregate_kind(&mut self, agg: &AggregateKind) -> ControlFlow<Self::Break> {
         match agg {
-            AggregateKind::Adt(kind, _, _, args) => {
-                self.check_typeid_generics(args, kind);
-            }
-            AggregateKind::Closure(_id, _args) => {
+            AggregateKind::Adt(..) => self.visit_inner(agg)?,
+            AggregateKind::Closure(_id, args) => {
                 // TODO(#194): handle closure generics properly
-                // self.generics_should_match_item(args, *id);
-                self.discharged_one_generics()
-            }
-            AggregateKind::Array(..) => {}
-        }
-    }
-    fn enter_fn_ptr(&mut self, fn_ptr: &FnPtr) {
-        match &fn_ptr.func {
-            FunIdOrTraitMethodRef::Fun(FunId::Regular(id)) => {
-                let args = &fn_ptr.generics;
-                self.generics_should_match_item(args, *id);
-            }
-            FunIdOrTraitMethodRef::Trait(tref, method, _) => {
-                let trait_id = tref.trait_decl_ref.skip_binder.trait_id;
-                if let Some(trait_decl) = self.translated.trait_decls.get(trait_id) {
-                    if let Some((_, bound_fn)) = trait_decl
-                        .required_methods
-                        .iter()
-                        .chain(trait_decl.provided_methods.iter())
-                        .find(|(n, _)| n == method)
-                    {
-                        // Function generics should match expected method generics.
-                        self.generics_should_match(&fn_ptr.generics, &bound_fn.params);
-                    } else {
-                        self.discharged_one_generics()
-                    }
-                } else {
-                    self.discharged_one_generics()
-                }
+                // This does not visit the args themselves, only their contents, because we mess up
+                // closure generics for now.
+                self.visit_inner(args)?
             }
-            FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {
-                // TODO: check generics for built-in types
-                self.discharged_one_generics()
-            }
-        }
-    }
-    fn enter_fun_decl_ref(&mut self, fun_ref: &FunDeclRef) {
-        self.generics_should_match_item(&fun_ref.generics, fun_ref.id);
-    }
-    fn enter_global_decl_ref(&mut self, global_ref: &GlobalDeclRef) {
-        self.generics_should_match_item(&global_ref.generics, global_ref.id);
-    }
-    fn enter_trait_decl_ref(&mut self, tref: &TraitDeclRef) {
-        self.generics_should_match_item(&tref.generics, tref.trait_id);
-    }
-    fn enter_trait_impl_ref(&mut self, impl_ref: &TraitImplRef) {
-        self.generics_should_match_item(&impl_ref.generics, impl_ref.impl_id);
-    }
-    fn enter_trait_ref(&mut self, tref: &TraitRef) {
-        match &tref.kind {
-            TraitRefKind::TraitImpl(id, args) => self.generics_should_match_item(args, *id),
-            TraitRefKind::BuiltinOrAuto(..)
-            | TraitRefKind::Dyn(..)
-            | TraitRefKind::Clause(..)
-            | TraitRefKind::ParentClause(..)
-            | TraitRefKind::ItemClause(..)
-            | TraitRefKind::SelfId
-            | TraitRefKind::Unknown(_) => {}
-        }
-    }
-    fn enter_ty(&mut self, ty: &Ty) {
-        if let TyKind::Adt(kind, args) = ty.kind() {
-            self.check_typeid_generics(args, kind);
+            AggregateKind::Array(..) => self.visit_inner(agg)?,
         }
+        Continue(())
     }
 
     fn enter_generic_args(&mut self, args: &GenericArgs) {
-        if self.discharged_args == 0 {
-            // Ensure we counted all `GenericArgs`
-            panic!("Unexpected `GenericArgs` in the AST! {args:?}")
+        let params = match &args.target {
+            GenericsSource::Item(item_id) => {
+                let Some(item) = self.translated.get_item(*item_id) else {
+                    return;
+                };
+                item.generic_params()
+            }
+            GenericsSource::Method(trait_id, method_name) => {
+                let Some(trait_decl) = self.translated.trait_decls.get(*trait_id) else {
+                    return;
+                };
+                let Some((_, bound_fn)) = trait_decl
+                    .required_methods
+                    .iter()
+                    .chain(trait_decl.provided_methods.iter())
+                    .find(|(n, _)| n == method_name)
+                else {
+                    return;
+                };
+                &bound_fn.params
+            }
+            GenericsSource::Builtin => return,
+        };
+        if !args.matches(params) {
+            self.error(format!(
+                "Mismatched generics:\nexpected: {params:?}\n     got: {args:?}"
+            ))
         }
-        self.discharged_args -= 1;
     }
 
     // Special case that is not represented as a `GenericArgs`.
@@ -176,29 +111,28 @@ impl VisitAst for CheckGenericsVisitor<'_> {
     }
 
     fn visit_llbc_statement(&mut self, st: &Statement) -> ControlFlow<Self::Break> {
-        let old_span = self.item_span;
-        self.item_span = st.span;
+        // Track span for more precise error messages.
+        let old_span = self.span;
+        self.span = st.span;
         self.visit_inner(st)?;
-        self.item_span = old_span;
+        self.span = old_span;
         Continue(())
     }
 }
 
-pub struct Check;
+// The argument is a name to disambiguate the two times we run this check.
+pub struct Check(pub &'static str);
 impl TransformPass for Check {
     fn transform_ctx(&self, ctx: &mut TransformCtx) {
         for item in ctx.translated.all_items() {
             let mut visitor = CheckGenericsVisitor {
                 translated: &ctx.translated,
                 error_ctx: &mut ctx.errors,
-                discharged_args: 0,
-                item_span: item.item_meta().span,
+                phase: self.0,
+                span: item.item_meta().span,
+                visit_stack: Default::default(),
             };
             item.drive(&mut visitor);
-            assert_eq!(
-                visitor.discharged_args, 0,
-                "Got confused about `GenericArgs` locations"
-            );
         }
     }
 }
diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs
index 06b9d1ec..1b586cad 100644
--- a/charon/src/transform/ctx.rs
+++ b/charon/src/transform/ctx.rs
@@ -18,6 +18,8 @@ pub struct TransformOptions {
     pub hide_marker_traits: bool,
     /// Do not merge the chains of gotos.
     pub no_merge_goto_chains: bool,
+    /// Print the llbc just after control-flow reconstruction.
+    pub print_built_llbc: bool,
     /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
     /// field.
     pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs
index 92bb7875..41d5a32e 100644
--- a/charon/src/transform/index_to_function_calls.rs
+++ b/charon/src/transform/index_to_function_calls.rs
@@ -70,7 +70,7 @@ impl<'a> IndexVisitor<'a> {
         } else {
             TyKind::Adt(
                 TypeId::Builtin(BuiltinTy::Slice),
-                GenericArgs::new_from_types(vec![elem_ty].into()),
+                GenericArgs::new_for_builtin(vec![elem_ty].into()),
             )
             .into_ty()
         };
diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs
index 5a04bdf0..00c7864f 100644
--- a/charon/src/transform/insert_assign_return_unit.rs
+++ b/charon/src/transform/insert_assign_return_unit.rs
@@ -12,7 +12,12 @@ fn transform_st(locals: &Locals, st: &mut Statement) -> Vec<Statement> {
     if let RawStatement::Return = &mut st.content {
         let ret_place = locals.return_place();
         let unit_value = Rvalue::Aggregate(
-            AggregateKind::Adt(TypeId::Tuple, None, None, GenericArgs::empty()),
+            AggregateKind::Adt(
+                TypeId::Tuple,
+                None,
+                None,
+                GenericArgs::empty(GenericsSource::Builtin),
+            ),
             Vec::new(),
         );
         let assign_st = Statement::new(st.span, RawStatement::Assign(ret_place, unit_value));
diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs
index 7ba3daf3..3eb339d9 100644
--- a/charon/src/transform/mod.rs
+++ b/charon/src/transform/mod.rs
@@ -34,14 +34,25 @@ pub use ctx::TransformCtx;
 use ctx::{LlbcPass, TransformPass, UllbcPass};
 use Pass::*;
 
-pub static ULLBC_PASSES: &[Pass] = &[
+/// Item and type cleanup passes.
+pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[
     // Move clauses on associated types to be parent clauses
     NonBody(&lift_associated_item_clauses::Transform),
+    // Check that all supplied generic types match the corresponding generic parameters.
+    NonBody(&check_generics::Check("after translation")),
     // # Micro-pass: hide some overly-common traits we don't need: Sized, Sync, Allocator, etc..
     NonBody(&hide_marker_traits::Transform),
     // # Micro-pass: filter the trait impls that were marked invisible since we couldn't filter
     // them out earlier.
     NonBody(&filter_invisible_trait_impls::Transform),
+    // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
+    // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove
+    // some sources of mutual recursion.
+    UnstructuredBody(&skip_trait_refs_when_known::Transform),
+];
+
+/// Body cleanup passes on the ullbc.
+pub static ULLBC_PASSES: &[Pass] = &[
     // # Micro-pass: merge single-origin gotos into their parent. This drastically reduces the
     // graph size of the CFG.
     UnstructuredBody(&merge_goto_chains::Transform),
@@ -62,10 +73,6 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // # Micro-pass: desugar the constants to other values/operands as much
     // as possible.
     UnstructuredBody(&simplify_constants::Transform),
-    // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
-    // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove
-    // some sources of mutual recursion.
-    UnstructuredBody(&skip_trait_refs_when_known::Transform),
     // # Micro-pass: the first local variable of closures is the
     // closure itself. This is not consistent with the closure signature,
     // which ignores this first variable. This micro-pass updates this.
@@ -89,7 +96,10 @@ pub static ULLBC_PASSES: &[Pass] = &[
     UnstructuredBody(&filter_unreachable_blocks::Transform),
 ];
 
+/// Body cleanup passes after control flow reconstruction.
 pub static LLBC_PASSES: &[Pass] = &[
+    // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing the control flow.
+    NonBody(&ullbc_to_llbc::Transform),
     // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans
     // those up.
     StructuredBody(&inline_local_panic_functions::Transform),
@@ -124,8 +134,17 @@ pub static LLBC_PASSES: &[Pass] = &[
     // statements. This must be last after all the statement-affecting passes to avoid losing
     // comments.
     StructuredBody(&recover_body_comments::Transform),
+    // # Reorder the graph of dependencies and compute the strictly connex components to:
+    // - compute the order in which to extract the definitions
+    // - find the recursive definitions
+    // - group the mutually recursive definitions
+    NonBody(&reorder_decls::Transform),
+];
+
+/// Final passes to run at the end.
+pub static FINAL_CLEANUP_PASSES: &[Pass] = &[
     // Check that all supplied generic types match the corresponding generic parameters.
-    NonBody(&check_generics::Check),
+    NonBody(&check_generics::Check("after transformations")),
     // Use `DeBruijnVar::Free` for the variables bound in item signatures.
     NonBody(&unbind_item_vars::Check),
 ];
diff --git a/charon/src/transform/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs
index 64fa918b..478db494 100644
--- a/charon/src/transform/ops_to_function_calls.rs
+++ b/charon/src/transform/ops_to_function_calls.rs
@@ -23,6 +23,7 @@ fn transform_st(s: &mut Statement) {
                 vec![ty.clone()].into(),
                 vec![cg.clone()].into(),
                 vec![].into(),
+                GenericsSource::Builtin,
             );
             let func = FnOperand::Regular(FnPtr { func, generics });
             s.content = RawStatement::Call(Call {
@@ -42,6 +43,7 @@ fn transform_st(s: &mut Statement) {
                 vec![ty.clone()].into(),
                 vec![cg.clone()].into(),
                 vec![].into(),
+                GenericsSource::Builtin,
             );
             let func = FnOperand::Regular(FnPtr { func, generics });
             s.content = RawStatement::Call(Call {
diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs
index 13656fa1..0807eaa2 100644
--- a/charon/src/transform/reorder_decls.rs
+++ b/charon/src/transform/reorder_decls.rs
@@ -12,6 +12,8 @@ use serde::{Deserialize, Serialize};
 use std::fmt::{Debug, Display, Error};
 use std::vec::Vec;
 
+use super::ctx::TransformPass;
+
 /// A (group of) top-level declaration(s), properly reordered.
 /// "G" stands for "generic"
 #[derive(
@@ -483,7 +485,7 @@ fn group_declarations_from_scc(
     reordered_decls
 }
 
-pub fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups {
+fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups {
     trace!();
 
     // Step 1: explore the declarations to build the graph
@@ -516,6 +518,14 @@ pub fn compute_reordered_decls(ctx: &TransformCtx) -> DeclarationsGroups {
     reordered_decls
 }
 
+pub struct Transform;
+impl TransformPass for Transform {
+    fn transform_ctx(&self, ctx: &mut TransformCtx) {
+        let reordered_decls = compute_reordered_decls(&ctx);
+        ctx.translated.ordered_decls = Some(reordered_decls);
+    }
+}
+
 #[cfg(test)]
 mod tests {
     #[test]
diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs
index 57faa6e5..c6d7c167 100644
--- a/charon/src/transform/ullbc_to_llbc.rs
+++ b/charon/src/transform/ullbc_to_llbc.rs
@@ -36,6 +36,8 @@ use petgraph::Direction;
 use std::cmp::Ordering;
 use std::collections::{BTreeSet, HashMap, HashSet, VecDeque};
 
+use super::ctx::TransformPass;
+
 /// Control-Flow Graph
 type Cfg = DiGraphMap<src::BlockId, ()>;
 
@@ -1742,28 +1744,34 @@ fn translate_body(ctx: &mut TransformCtx, no_code_duplication: bool, body: &mut
     *body = Structured(tgt_body);
 }
 
-/// Translate the functions by reconstructing the control-flow.
-pub fn translate_functions(ctx: &mut TransformCtx) {
-    // Translate the bodies one at a time.
-    ctx.for_each_body(|ctx, body| {
-        translate_body(ctx, ctx.options.no_code_duplication, body);
-    });
+pub struct Transform;
+impl TransformPass for Transform {
+    fn transform_ctx(&self, ctx: &mut TransformCtx) {
+        // Translate the bodies one at a time.
+        ctx.for_each_body(|ctx, body| {
+            translate_body(ctx, ctx.options.no_code_duplication, body);
+        });
 
-    // Print the functions
-    let fmt_ctx = ctx.into_fmt();
-    for fun in &ctx.translated.fun_decls {
-        trace!(
-            "# Signature:\n{}\n\n# Function definition:\n{}\n",
-            fmt_ctx.format_object(&fun.signature),
-            fmt_ctx.format_object(fun),
-        );
-    }
-    // Print the global variables
-    for global in &ctx.translated.global_decls {
-        trace!(
-            "# Type:\n{}\n\n# Global definition:\n{}\n",
-            fmt_ctx.format_object(&global.ty),
-            fmt_ctx.format_object(global)
-        );
+        // Print the functions
+        let fmt_ctx = ctx.into_fmt();
+        for fun in &ctx.translated.fun_decls {
+            trace!(
+                "# Signature:\n{}\n\n# Function definition:\n{}\n",
+                fmt_ctx.format_object(&fun.signature),
+                fmt_ctx.format_object(fun),
+            );
+        }
+        // Print the global variables
+        for global in &ctx.translated.global_decls {
+            trace!(
+                "# Type:\n{}\n\n# Global definition:\n{}\n",
+                fmt_ctx.format_object(&global.ty),
+                fmt_ctx.format_object(global)
+            );
+        }
+
+        if ctx.options.print_built_llbc {
+            info!("# LLBC resulting from control-flow reconstruction:\n\n{ctx}\n",);
+        }
     }
 }
diff --git a/charon/tests/test-rust-name-matcher.rs b/charon/tests/test-rust-name-matcher.rs
index af49648d..bdd10369 100644
--- a/charon/tests/test-rust-name-matcher.rs
+++ b/charon/tests/test-rust-name-matcher.rs
@@ -45,7 +45,7 @@ fn test_name_matcher() -> anyhow::Result<()> {
             .filter_map(|a| parse_pattern_attr(a))
             .collect_vec();
         for (pass, pat) in patterns {
-            let passes = pat.matches(&crate_data, name);
+            let passes = pat.matches_item(&crate_data, item);
             if passes != pass {
                 if passes {
                     panic!(
diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs
index 9902bfb5..0eb6bb21 100644
--- a/charon/tests/ui.rs
+++ b/charon/tests/ui.rs
@@ -8,6 +8,7 @@ use anyhow::{anyhow, bail};
 use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt};
 use indoc::indoc as unindent;
 use libtest_mimic::Trial;
+use snapbox::filter::Filter as _;
 use std::{
     error::Error,
     fs::read_to_string,
@@ -233,6 +234,12 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> {
         }
         TestKind::PrettyLlbc => {
             if !output.status.success() {
+                if output.status.code() != Some(101) {
+                    // Write output file anyway to make debugging easier.
+                    let actual = snapbox::Data::text(stdout);
+                    let actual = snapbox::filter::FilterNewlines.filter(actual);
+                    actual.write_to_path(&test_case.expected)?;
+                }
                 bail!("Compilation failed: {stderr}")
             }
             stdout
diff --git a/charon/tests/ui/rust-name-matcher-tests.rs b/charon/tests/ui/rust-name-matcher-tests.rs
index 7f5c642f..5aca0f72 100644
--- a/charon/tests/ui/rust-name-matcher-tests.rs
+++ b/charon/tests/ui/rust-name-matcher-tests.rs
@@ -16,15 +16,16 @@ mod foo {
 
 #[pattern::pass("test_crate::Trait")]
 #[pattern::fail("test_crate::Trait<_>")]
-#[pattern::fail("test_crate::Trait<_, _>")]
+#[pattern::pass("test_crate::Trait<_, _>")]
 trait Trait<T> {
     #[pattern::pass("test_crate::Trait::method")]
-    #[pattern::fail("test_crate::Trait<_>::method")]
+    #[pattern::pass("test_crate::Trait<_>::method")]
     fn method<U>();
 }
 
 #[pattern::pass("test_crate::{impl test_crate::Trait<_> for _}")]
 #[pattern::pass("test_crate::{impl test_crate::Trait<_, _>}")]
+#[pattern::fail("test_crate::{impl test_crate::Trait<_>}")]
 #[pattern::fail("test_crate::{impl test_crate::Trait<_, _> for _}")]
 #[pattern::pass(
     "test_crate::{impl test_crate::Trait<core::option::Option<_>> for alloc::boxed::Box<_>}"