diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 5884d425..ec7deac4 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -816,7 +816,7 @@ dependencies = [
 [[package]]
 name = "hax-adt-into"
 version = "0.1.0-rc.1"
-source = "git+https://github.com/hacspec/hax?branch=main#de59826b832befc82905286d052c8a961c31f3cd"
+source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -827,7 +827,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.1.0-rc.1"
-source = "git+https://github.com/hacspec/hax?branch=main#de59826b832befc82905286d052c8a961c31f3cd"
+source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502"
 dependencies = [
  "extension-traits",
  "hax-adt-into",
@@ -844,7 +844,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.1.0-rc.1"
-source = "git+https://github.com/hacspec/hax?branch=main#de59826b832befc82905286d052c8a961c31f3cd"
+source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502"
 dependencies = [
  "hax-adt-into",
  "schemars",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index 6046ff56..223c206e 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -76,7 +76,8 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] }
 wait-timeout = { version = "0.2.0", optional = true }
 which = "7.0"
 
-hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-call-generics", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 
diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs
index 75143455..7f29b2e3 100644
--- a/charon/src/ast/types.rs
+++ b/charon/src/ast/types.rs
@@ -242,7 +242,7 @@ pub struct Binder<T> {
 /// be filled. We group in a different place the predicates which are not
 /// trait clauses, because those enforce constraints but do not need to
 /// be filled with witnesses/instances.
-#[derive(Debug, Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct GenericParams {
     pub regions: Vector<RegionId, RegionVar>,
     pub types: Vector<TypeVarId, TypeVar>,
diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs
index 10fdeda9..ef2afb7b 100644
--- a/charon/src/ast/types_utils.rs
+++ b/charon/src/ast/types_utils.rs
@@ -190,11 +190,11 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs,
-        } = &mut self;
-        regions.extend(other.regions.iter().cloned());
-        types.extend(other.types.iter().cloned());
-        const_generics.extend(other.const_generics.iter().cloned());
-        trait_refs.extend(other.trait_refs.iter().cloned());
+        } = 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
     }
 }
diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs
index f58ca93e..544b21ce 100644
--- a/charon/src/ast/visitor.rs
+++ b/charon/src/ast/visitor.rs
@@ -44,12 +44,12 @@ use index_vec::Idx;
         CastKind, ClosureInfo, ClosureKind, ConstantExpr, ConstGenericVar, ConstGenericVarId,
         Disambiguator, ExistentialPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue,
         FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
-        llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Statement, llbc_ast::Switch,
+        llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr,
         RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName,
         TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId,
         ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
-        ullbc_ast::RawTerminator, ullbc_ast::Statement, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
+        ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
         UnOp, Var, Variant, VariantId, VarId,
         for<T: AstVisitable> Box<T>,
         for<T: AstVisitable> Option<T>,
@@ -67,6 +67,7 @@ use index_vec::Idx;
         for<T: AstVisitable + Idx> DeBruijnVar<T>,
         for<T: AstVisitable> RegionBinder<T>,
         for<T: AstVisitable> Binder<T>,
+        llbc_statement: llbc_ast::Statement, ullbc_statement: ullbc_ast::Statement,
         AggregateKind, FnPtr, ItemKind, ItemMeta, Span,
         BodyId, FunDeclId, GlobalDeclId, TypeDeclId, TraitDeclId, TraitImplId,
         FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl,
diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
index 19e52e1e..2c394e5c 100644
--- a/charon/src/bin/charon-driver/translate/translate_constants.rs
+++ b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -112,9 +112,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     generics,
                     trait_refs
                 );
-                let used_params = None;
-                let generics =
-                    self.translate_generic_args(span, used_params, generics, trait_refs, None)?;
+                let generics = self.translate_generic_args(span, generics, trait_refs, None)?;
 
                 let global_id = self.register_global_decl_id(span, id);
                 RawConstantExpr::Global(GlobalDeclRef {
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 2d9e48e2..32401bff 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
@@ -131,7 +131,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     impl_id: self.register_trait_impl_id(span, impl_id),
                     generics: self.translate_generic_args(
                         span,
-                        None,
                         impl_generics,
                         impl_required_impl_exprs,
                         None,
@@ -669,7 +668,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
                         // Translate the substitution
                         let generics =
-                            self.translate_generic_args(span, None, substs, trait_refs, None)?;
+                            self.translate_generic_args(span, substs, trait_refs, None)?;
 
                         let type_id = self.translate_type_id(span, adt_id)?;
                         // Sanity check
@@ -688,21 +687,20 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         let akind = AggregateKind::Adt(type_id, variant_id, field_id, generics);
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
-                    hax::AggregateKind::Closure(def_id, substs, trait_refs, sig) => {
-                        trace!("Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}", def_id, sig);
+                    hax::AggregateKind::Closure(def_id, closure_args) => {
+                        trace!(
+                            "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
+                            def_id,
+                            closure_args.tupled_sig
+                        );
 
                         // Retrieve the late-bound variables.
-                        let binder = match self.t_ctx.hax_def(def_id)?.kind() {
-                            hax::FullDefKind::Closure { args, .. } => args.sig.as_ref().rebind(()),
-                            _ => unreachable!(),
-                        };
-
+                        let binder = closure_args.tupled_sig.as_ref().rebind(());
                         // Translate the substitution
                         let generics = self.translate_generic_args(
                             span,
-                            None,
-                            substs,
-                            trait_refs,
+                            &closure_args.parent_args,
+                            &closure_args.parent_trait_refs,
                             Some(binder),
                         )?;
 
@@ -785,7 +783,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         };
 
         // Translate the type parameters
-        let generics = self.translate_generic_args(span, None, substs, trait_refs, binder)?;
+        let generics = self.translate_generic_args(span, substs, trait_refs, binder)?;
 
         // Translate the arguments
         let args = args
@@ -1005,26 +1003,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             TerminatorKind::Call {
                 fun,
-                generics,
                 args,
                 destination,
                 target,
-                trait_refs,
-                trait_info,
                 unwind: _, // We model unwinding as an effet, we don't represent it in control flow
-                call_source: _,
                 fn_span: _,
-            } => self.translate_function_call(
-                statements,
-                span,
-                fun,
-                generics,
-                args,
-                destination,
-                target,
-                trait_refs,
-                trait_info,
-            )?,
+                ..
+            } => self.translate_function_call(statements, span, fun, args, destination, target)?,
             TerminatorKind::Assert {
                 cond,
                 expected,
@@ -1127,12 +1112,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         statements: &mut Vec<Statement>,
         span: Span,
         fun: &hax::FunOperand,
-        generics: &Vec<hax::GenericArg>,
         args: &Vec<hax::Spanned<hax::Operand>>,
         destination: &hax::Place,
         target: &Option<hax::BasicBlock>,
-        trait_refs: &Vec<hax::ImplExpr>,
-        trait_info: &Option<hax::ImplExpr>,
     ) -> Result<RawTerminator, Error> {
         trace!();
         // There are two cases, depending on whether this is a "regular"
@@ -1141,7 +1123,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         let lval = self.translate_place(span, destination)?;
         let next_block = target.map(|target| self.translate_basic_block_id(target));
         let (fn_operand, args) = match fun {
-            hax::FunOperand::Id(def_id) => {
+            hax::FunOperand::Static {
+                def_id,
+                generics,
+                trait_refs,
+                trait_info,
+            } => {
                 // Translate the function operand - should be a constant: we don't
                 // support closures for now
                 trace!("func: {:?}", def_id);
@@ -1171,7 +1158,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     }
                 }
             }
-            hax::FunOperand::Move(p) => {
+            hax::FunOperand::DynamicMove(p) => {
                 // Call to a local function pointer
                 // The function
                 let p = self.translate_place(span, p)?;
@@ -1418,7 +1405,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         self.translate_def_generics(span, def)?;
 
         let signature = match &def.kind {
-            hax::FullDefKind::Closure { args, .. } => &args.sig,
+            hax::FullDefKind::Closure { args, .. } => &args.tupled_sig,
             hax::FullDefKind::Fn { sig, .. } => sig,
             hax::FullDefKind::AssocFn { sig, .. } => sig,
             hax::FullDefKind::Ctor {
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index e2867244..771faa95 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -44,8 +44,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> 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, None, &trait_ref.generic_args, &[], None)?;
+            let generics = ctx.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
             Ok(TraitDeclRef { trait_id, generics })
         })
     }
@@ -67,8 +66,7 @@ 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, None, &trait_ref.generic_args, &[], None)?;
+        let generics = self.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
         Ok(TraitDeclRef { trait_id, generics })
     }
 
@@ -225,7 +223,7 @@ 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, None, generics, nested, None)?;
+                let generics = self.translate_generic_args(span, generics, nested, None)?;
                 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 cfa578b3..86b1e8d1 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -192,13 +192,8 @@ 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,
-                None,
-                &implemented_trait.generic_args,
-                &[],
-                None,
-            )?;
+            let generics =
+                self.translate_generic_args(span, &implemented_trait.generic_args, &[], None)?;
             TraitDeclRef { trait_id, generics }
         };
 
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index d32d65a6..d7a8447e 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -144,19 +144,25 @@ 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)?;
 
-                // Retrieve the list of used arguments
-                let used_params = if let TypeId::Builtin(builtin_ty) = type_id {
-                    Some(builtins::type_to_used_params(builtin_ty))
-                } else {
-                    None
-                };
-
-                // Translate the type parameters instantiation
-                let generics =
-                    self.translate_generic_args(span, used_params, substs, trait_refs, None)?;
+                // Filter the type arguments.
+                // TODO: do this in a micro-pass
+                if let TypeId::Builtin(builtin_ty) = type_id {
+                    let used_args = builtins::type_to_used_params(builtin_ty);
+                    error_assert!(self, span, generics.types.len() == used_args.len());
+                    let types = std::mem::take(&mut generics.types)
+                        .into_iter()
+                        .zip(used_args)
+                        .filter(|(_, used)| *used)
+                        .map(|(ty, _)| ty)
+                        .collect();
+                    generics.types = types;
+                }
 
                 // Return the instantiated ADT
                 TyKind::Adt(type_id, generics)
@@ -262,7 +268,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 trace!("PlaceHolder");
                 error_or_panic!(self, span, "Unsupported type: placeholder")
             }
-            hax::TyKind::Arrow(box sig) => {
+            hax::TyKind::Arrow(box sig)
+            | hax::TyKind::Closure(
+                _,
+                hax::ClosureArgs {
+                    untupled_sig: sig, ..
+                },
+            ) => {
                 trace!("Arrow");
                 trace!("bound vars: {:?}", sig.bound_vars);
                 let sig = self.translate_region_binder(span, sig, |ctx, sig| {
@@ -295,7 +307,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     pub fn translate_generic_args(
         &mut self,
         span: Span,
-        used_params: Option<Vec<bool>>,
         substs: &[hax::GenericArg],
         trait_refs: &[hax::ImplExpr],
         late_bound: Option<hax::Binder<()>>,
@@ -303,23 +314,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         use hax::GenericArg::*;
         trace!("{:?}", substs);
 
-        // Filter the parameters
-        let substs: Vec<&hax::GenericArg> = match used_params {
-            None => substs.iter().collect(),
-            Some(used_args) => {
-                error_assert!(self, span, substs.len() == used_args.len());
-                substs
-                    .iter()
-                    .zip(used_args.into_iter())
-                    .filter_map(|(param, used)| if used { Some(param) } else { None })
-                    .collect()
-            }
-        };
-
         let mut regions = Vector::new();
         let mut types = Vector::new();
         let mut const_generics = Vector::new();
-        for param in substs.iter() {
+        for param in substs {
             match param {
                 Type(param_ty) => {
                     types.push(self.translate_ty(span, param_ty)?);
@@ -663,7 +661,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
         // parameters here.
         let signature = match &def.kind {
-            hax::FullDefKind::Closure { args, .. } => Some(&args.sig),
+            hax::FullDefKind::Closure { args, .. } => Some(&args.tupled_sig),
             hax::FullDefKind::Fn { sig, .. } => Some(sig),
             hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
             _ => None,
diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs
index ad47ec64..542b7c70 100644
--- a/charon/src/ids/vector.rs
+++ b/charon/src/ids/vector.rs
@@ -118,6 +118,14 @@ where
         self.push_all(it).for_each(|_| ())
     }
 
+    pub fn extend_from_slice(&mut self, other: &Self)
+    where
+        T: Clone,
+    {
+        self.vector.extend_from_slice(&other.vector);
+        self.real_len += other.real_len;
+    }
+
     /// Map each entry to a new one, keeping the same ids.
     pub fn map<U>(self, mut f: impl FnMut(T) -> U) -> Vector<I, U> {
         Vector {
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index 698a2446..e0414df6 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -392,6 +392,21 @@ impl GenericParams {
         };
         (params, clauses)
     }
+
+    pub fn fmt_with_ctx_single_line<C>(&self, ctx: &C) -> String
+    where
+        C: AstFormatter,
+    {
+        let params = self
+            .format_params(ctx)
+            .chain(self.format_clauses(ctx))
+            .join(", ");
+        if params.is_empty() {
+            String::new()
+        } else {
+            format!("<{}>", params)
+        }
+    }
 }
 
 impl<T, C> FmtWithCtx<C> for GExprBody<T>
@@ -1559,12 +1574,24 @@ impl std::fmt::Display for GenericArgs {
     }
 }
 
+impl std::fmt::Display for GenericParams {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
+        write!(f, "{}", self.fmt_with_ctx_single_line(&FmtCtx::new()))
+    }
+}
+
 impl std::fmt::Debug for GenericArgs {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
         write!(f, "{}", self)
     }
 }
 
+impl std::fmt::Debug for GenericParams {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
+        write!(f, "{}", self)
+    }
+}
+
 impl std::fmt::Display for Literal {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> {
         match self {
diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs
index 8b112f47..5702e0e9 100644
--- a/charon/src/transform/check_generics.rs
+++ b/charon/src/transform/check_generics.rs
@@ -2,7 +2,7 @@
 use derive_generic_visitor::*;
 use std::fmt::Display;
 
-use crate::{ast::*, errors::ErrorCtx, register_error_or_panic};
+use crate::{errors::ErrorCtx, llbc_ast::*, register_error_or_panic};
 
 use super::{ctx::TransformPass, TransformCtx};
 
@@ -66,19 +66,29 @@ impl VisitAst for CheckGenericsVisitor<'_> {
             AggregateKind::Adt(kind, _, _, args) => {
                 self.check_typeid_generics(args, kind);
             }
-            AggregateKind::Closure(id, args) => {
-                self.generics_should_match_item(args, *id);
+            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) {
-        let args = &fn_ptr.generics;
         match &fn_ptr.func {
-            FunIdOrTraitMethodRef::Fun(FunId::Regular(id))
-            | FunIdOrTraitMethodRef::Trait(_, _, id) => {
+            FunIdOrTraitMethodRef::Fun(FunId::Regular(id)) => {
+                let args = &fn_ptr.generics;
                 self.generics_should_match_item(args, *id);
             }
+            FunIdOrTraitMethodRef::Trait(tref, _, id) => {
+                let args = tref
+                    .trait_decl_ref
+                    .skip_binder
+                    .generics
+                    .clone()
+                    .concat(&fn_ptr.generics);
+                self.generics_should_match_item(&args, *id);
+            }
             FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {
                 // TODO: check generics for built-in types
                 self.discharged_one_generics()
@@ -147,6 +157,14 @@ impl VisitAst for CheckGenericsVisitor<'_> {
             self.error("The methods supplied by the trait impl don't match the trait decl.")
         }
     }
+
+    fn visit_llbc_statement(&mut self, st: &Statement) -> ControlFlow<Self::Break> {
+        let old_span = self.item_span;
+        self.item_span = st.span;
+        self.visit_inner(st)?;
+        self.item_span = old_span;
+        Continue(())
+    }
 }
 
 pub struct Check;
@@ -164,6 +182,13 @@ impl TransformPass for Check {
                 visitor.discharged_args, 0,
                 "Got confused about `GenericArgs` locations"
             );
+            if let AnyTransItem::Fun(d) = item {
+                if let Ok(body_id) = d.body {
+                    if let Some(body) = ctx.translated.bodies.get(body_id) {
+                        body.drive(&mut visitor);
+                    }
+                }
+            }
         }
     }
 }
diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out
index 8384f3b6..b455dddf 100644
--- a/charon/tests/ui/issue-378-ctor-as-fn.out
+++ b/charon/tests/ui/issue-378-ctor-as-fn.out
@@ -18,7 +18,7 @@ fn test_crate::F() -> fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>
 {
     let @0: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // return
 
-    @0 := cast<fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>], fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]>(const (core::option::Option::Some<u8>))
+    @0 := cast<fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>], fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]>(const (core::option::Option::Some<u8>[core::marker::Sized<u8>]))
     return
 }
 
@@ -86,10 +86,10 @@ fn test_crate::main()
     let @17: i32; // anonymous local
     let @18: (); // anonymous local
 
-    f@1 := const (core::option::Option::Some<u8>)
+    f@1 := const (core::option::Option::Some<u8>[core::marker::Sized<u8>])
     @fake_read(f@1)
     @3 := copy (f@1)
-    @2 := core::option::Option::Some<u8>(const (42 : u8))
+    @2 := core::option::Option::Some<u8>[core::marker::Sized<u8>](const (42 : u8))
     drop @3
     @fake_read(@2)
     drop @2
@@ -112,13 +112,13 @@ fn test_crate::main()
     @fake_read(@9)
     drop @9
     drop @9
-    f@12 := const (test_crate::Bar::Variant<'_, i32>)
+    f@12 := const (test_crate::Bar::Variant<'_, i32>[core::marker::Sized<i32>])
     @fake_read(f@12)
     @14 := copy (f@12)
     @17 := const (42 : i32)
     @16 := &@17
     @15 := &*(@16)
-    @13 := test_crate::Bar::Variant<'_, i32>(move (@15))
+    @13 := test_crate::Bar::Variant<'_, i32>[core::marker::Sized<i32>](move (@15))
     drop @15
     drop @14
     @fake_read(@13)
diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out
index 54304f28..5983f7dc 100644
--- a/charon/tests/ui/issue-4-slice-try-into-array.out
+++ b/charon/tests/ui/issue-4-slice-try-into-array.out
@@ -40,7 +40,7 @@ trait core::marker::Copy<Self>
     parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
 }
 
-fn core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7::try_from<'_0, '_1, T, const N : usize>(@1: &'_1 (Slice<T>)) -> core::result::Result<Array<T, const N : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<T, const N : usize>>, core::marker::Sized<core::array::TryFromSliceError>]
+fn core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice<T>)) -> core::result::Result<Array<T, const N : usize>, core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, T, const N : usize>[@TraitClause0, @TraitClause1]::Error>[core::marker::Sized<Array<T, const N : usize>>, core::marker::Sized<core::array::TryFromSliceError>]
 where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::marker::Copy<T>,
diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out
index 54304f28..5983f7dc 100644
--- a/charon/tests/ui/issue-4-traits.out
+++ b/charon/tests/ui/issue-4-traits.out
@@ -40,7 +40,7 @@ trait core::marker::Copy<Self>
     parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
 }
 
-fn core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7::try_from<'_0, '_1, T, const N : usize>(@1: &'_1 (Slice<T>)) -> core::result::Result<Array<T, const N : usize>, core::array::TryFromSliceError>[core::marker::Sized<Array<T, const N : usize>>, core::marker::Sized<core::array::TryFromSliceError>]
+fn core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice<T>)) -> core::result::Result<Array<T, const N : usize>, core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, T, const N : usize>[@TraitClause0, @TraitClause1]::Error>[core::marker::Sized<Array<T, const N : usize>>, core::marker::Sized<core::array::TryFromSliceError>]
 where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::marker::Copy<T>,
diff --git a/charon/tests/ui/issue-70-override-provided-method.3.out b/charon/tests/ui/issue-70-override-provided-method.3.out
index 47c9914c..a410dbbe 100644
--- a/charon/tests/ui/issue-70-override-provided-method.3.out
+++ b/charon/tests/ui/issue-70-override-provided-method.3.out
@@ -80,19 +80,19 @@ where
 
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn test_crate::{impl test_crate::GenericTrait<core::option::Option<T>[@TraitClause0]> for test_crate::Override<T>[@TraitClause0]}::provided<T, U>(@1: T, @2: U)
+fn test_crate::{impl test_crate::GenericTrait<core::option::Option<T>[@TraitClause0]> for test_crate::Override<T>[@TraitClause0]}::provided<T, U>(@1: core::option::Option<T>[@TraitClause0], @2: U)
 where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::marker::Copy<T>,
     [@TraitClause2]: core::marker::Sized<U>,
-    [@TraitClause3]: core::cmp::PartialEq<U, T>,
+    [@TraitClause3]: core::cmp::PartialEq<U, core::option::Option<T>[@TraitClause0]>,
 {
     let @0: (); // return
-    let x@1: T; // arg #1
+    let x@1: core::option::Option<T>[@TraitClause0]; // arg #1
     let y@2: U; // arg #2
     let @3: bool; // anonymous local
     let @4: &'_ (U); // anonymous local
-    let @5: &'_ (T); // anonymous local
+    let @5: &'_ (core::option::Option<T>[@TraitClause0]); // anonymous local
     let @6: (); // anonymous local
 
     @4 := &y@2
diff --git a/charon/tests/ui/issue-70-override-provided-method.3.rs b/charon/tests/ui/issue-70-override-provided-method.3.rs
index cd6ce100..9c1905d5 100644
--- a/charon/tests/ui/issue-70-override-provided-method.3.rs
+++ b/charon/tests/ui/issue-70-override-provided-method.3.rs
@@ -14,7 +14,7 @@ trait GenericTrait<T: Clone> {
 struct Override<T>(T);
 impl<T: Copy> GenericTrait<Option<T>> for Override<T> {
     fn other_method() {}
-    fn provided<U: PartialEq<T>>(x: T, y: U) {
+    fn provided<U: PartialEq<Option<T>>>(x: Option<T>, y: U) {
         if y == x {
             Self::other_method()
         }
diff --git a/charon/tests/ui/method-impl-generalization.out b/charon/tests/ui/method-impl-generalization.out
new file mode 100644
index 00000000..9287e354
--- /dev/null
+++ b/charon/tests/ui/method-impl-generalization.out
@@ -0,0 +1,192 @@
+# Final LLBC before serialization:
+
+trait core::marker::Sized<Self>
+
+trait core::clone::Clone<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    fn clone : core::clone::Clone::clone
+    fn clone_from : core::clone::Clone::clone_from
+}
+
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
+trait test_crate::Trait<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    fn method1 : test_crate::Trait::method1
+    fn method2 : test_crate::Trait::method2
+}
+
+fn test_crate::{impl test_crate::Trait for ()}::method1(@1: (), @2: &'static (u32)) -> bool
+{
+    let @0: bool; // return
+    let self@1: (); // arg #1
+    let _other@2: &'_ (u32); // arg #2
+
+    @0 := const (true)
+    return
+}
+
+fn test_crate::{impl test_crate::Trait for ()}::method2<T>(@1: (), @2: T)
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+{
+    let @0: (); // return
+    let self@1: (); // arg #1
+    let _other@2: T; // arg #2
+    let @3: (); // anonymous local
+
+    @3 := ()
+    @0 := move (@3)
+    drop _other@2
+    @0 := ()
+    return
+}
+
+impl test_crate::{impl test_crate::Trait for ()} : test_crate::Trait<()>
+{
+    parent_clause0 = core::marker::Sized<()>
+    fn method1 = test_crate::{impl test_crate::Trait for ()}::method1
+    fn method2 = test_crate::{impl test_crate::Trait for ()}::method2
+}
+
+trait test_crate::MyCompare<Self, Other>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Other>
+    fn compare : test_crate::MyCompare::compare
+}
+
+fn test_crate::{impl test_crate::MyCompare<&'a (())> for &'a (())}#1::compare<'a>(@1: &'a (()), @2: &'a (())) -> bool
+{
+    let @0: bool; // return
+    let self@1: &'_ (()); // arg #1
+    let _other@2: &'_ (()); // arg #2
+
+    @0 := const (true)
+    return
+}
+
+impl<'a> test_crate::{impl test_crate::MyCompare<&'a (())> for &'a (())}#1<'a> : test_crate::MyCompare<&'a (()), &'a (())>
+{
+    parent_clause0 = core::marker::Sized<&'_ (())>
+    parent_clause1 = core::marker::Sized<&'_ (())>
+    fn compare = test_crate::{impl test_crate::MyCompare<&'a (())> for &'a (())}#1::compare
+}
+
+fn test_crate::main()
+{
+    let @0: (); // return
+    let @1: bool; // anonymous local
+    let @2: (); // anonymous local
+    let @3: &'_ (u32); // anonymous local
+    let @4: &'_ (u32); // anonymous local
+    let @5: u32; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: &'_ (()); // anonymous local
+    let @8: (); // anonymous local
+    let @9: &'_ (()); // anonymous local
+    let @10: &'_ (()); // anonymous local
+    let @11: (); // anonymous local
+    let @12: (); // anonymous local
+
+    @2 := ()
+    @5 := const (1 : u32)
+    @4 := &@5
+    @3 := &*(@4)
+    @1 := test_crate::{impl test_crate::Trait for ()}::method1(move (@2), move (@3))
+    drop @3
+    drop @2
+    @fake_read(@1)
+    drop @5
+    drop @4
+    drop @1
+    // TODO: this gives incorrect predicates
+    // let _ = ().method2(false);
+    // Not allowed to use the more precise signature.
+    // let _ = ().method2(String::new());
+    @8 := ()
+    @7 := &@8
+    @11 := ()
+    @10 := &@11
+    @9 := &*(@10)
+    @6 := test_crate::{impl test_crate::MyCompare<&'a (())> for &'a (())}#1::compare<'_>(move (@7), move (@9))
+    drop @9
+    drop @7
+    @fake_read(@6)
+    drop @11
+    drop @10
+    drop @8
+    drop @6
+    @12 := ()
+    @0 := move (@12)
+    @0 := ()
+    return
+}
+
+trait test_crate::Foo<Self>
+{
+    fn foo : test_crate::Foo::foo
+}
+
+fn test_crate::{impl test_crate::Foo for ()}#2::foo<'a, 'b>(@1: &'b (()), @2: &'a (())) -> &'b (())
+{
+    let @0: &'_ (()); // return
+    let x@1: &'_ (()); // arg #1
+    let y@2: &'_ (()); // arg #2
+
+    @0 := copy (x@1)
+    return
+}
+
+impl test_crate::{impl test_crate::Foo for ()}#2 : test_crate::Foo<()>
+{
+    fn foo = test_crate::{impl test_crate::Foo for ()}#2::foo
+}
+
+fn test_crate::call_foo<'e>(@1: &'e (())) -> &'e (())
+{
+    let @0: &'_ (()); // return
+    let x@1: &'_ (()); // arg #1
+    let @2: &'_ (()); // anonymous local
+    let @3: &'_ (()); // anonymous local
+    let @4: &'_ (()); // anonymous local
+    let @5: &'_ (()); // anonymous local
+    let @6: (); // anonymous local
+
+    // Calls have erased lifetimes so we can't notice the discrepancy if there is one.
+    @3 := &*(x@1)
+    @6 := ()
+    @5 := &@6
+    @4 := &*(@5)
+    @2 := test_crate::{impl test_crate::Foo for ()}#2::foo<'_, '_>(move (@3), move (@4))
+    @0 := &*(@2)
+    drop @4
+    drop @3
+    drop @6
+    drop @5
+    drop @2
+    return
+}
+
+fn test_crate::Trait::method1<Self>(@1: Self, @2: &'static (u32)) -> bool
+
+fn test_crate::Trait::method2<Self, T>(@1: Self, @2: T)
+where
+    [@TraitClause0]: core::marker::Sized<T>,
+    [@TraitClause1]: core::marker::Copy<T>,
+
+fn test_crate::MyCompare::compare<Self, Other>(@1: Self, @2: Other) -> bool
+
+fn test_crate::Foo::foo<'a, 'b, Self>(@1: &'a (()), @2: &'b (())) -> &'a (())
+
+fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+
+fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
+
+
+
diff --git a/charon/tests/ui/method-impl-generalization.rs b/charon/tests/ui/method-impl-generalization.rs
new file mode 100644
index 00000000..c0721631
--- /dev/null
+++ b/charon/tests/ui/method-impl-generalization.rs
@@ -0,0 +1,54 @@
+//! Implemented methods are allowed to have more general types than the declared method. This
+//! causes subtleties in translation.
+trait Trait: Sized {
+    fn method1(self, other: &'static u32) -> bool;
+    fn method2<T: Copy>(self, other: T);
+}
+
+impl Trait for () {
+    // This implementation is more general because it works for non-static refs.
+    fn method1(self, _other: &u32) -> bool {
+        true
+    }
+    // This implementation is more general because it works for non-`Copy` `T`s. We can't call
+    // it with its more general type however.
+    fn method2<T>(self, _other: T) {}
+}
+
+trait MyCompare<Other>: Sized {
+    fn compare(self, other: Other) -> bool;
+}
+
+impl<'a> MyCompare<&'a ()> for &'a () {
+    // This implementation is more general because it works for non-`'a` refs. Note that only
+    // late-bound vars may differ in this way.
+    // If we used this signature when translating, we'd need unification to map from the expected
+    // trait method generics to the actual impl method generics.
+    fn compare<'b>(self, _other: &'b ()) -> bool {
+        true
+    }
+}
+
+fn main() {
+    let _ = ().method1(&1u32);
+    // TODO: this gives incorrect predicates
+    // let _ = ().method2(false);
+    // Not allowed to use the more precise signature.
+    // let _ = ().method2(String::new());
+    let _ = ().compare(&());
+}
+
+trait Foo {
+    fn foo<'a, 'b>(x: &'a (), y: &'b ()) -> &'a ();
+}
+impl Foo for () {
+    // Lifetimes declared in opposite order despite having the same names.
+    // TODO: make sure we substitute the right lifetimes.
+    fn foo<'a, 'b>(x: &'b (), y: &'a ()) -> &'b () {
+        x
+    }
+}
+fn call_foo<'e>(x: &'e ()) -> &'e () {
+    // Calls have erased lifetimes so we can't notice the discrepancy if there is one.
+    <() as Foo>::foo(x, &())
+}
diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out
index a3e6fc24..0efe48b5 100644
--- a/charon/tests/ui/polonius_map.out
+++ b/charon/tests/ui/polonius_map.out
@@ -154,7 +154,13 @@ where
     [@TraitClause4]: core::hash::Hash<K>,
     [@TraitClause5]: core::hash::BuildHasher<S>,
 
-fn std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]}#9::index<'_0, '_1, '_2, K, Q, V, S>(@1: &'_1 (std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]), @2: &'_2 (Q)) -> &'_1 (V)
+trait core::ops::index::Index<Self, Idx>
+{
+    type Output
+    fn index : core::ops::index::Index::index
+}
+
+fn std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]}#9::index<'_0, '_1, K, Q, V, S>(@1: &'_1 (std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]), @2: &'_0 (Q)) -> &'_1 (std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]}#9<'_, K, Q, V, S>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause4, @TraitClause5, @TraitClause6, @TraitClause7, @TraitClause8]::Output)
 where
     [@TraitClause0]: core::marker::Sized<K>,
     [@TraitClause1]: core::marker::Sized<V>,
@@ -227,12 +233,6 @@ fn test_crate::get_or_insert<'_0>(@1: &'_0 mut (std::collections::hash::map::Has
 
 fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output)
 
-trait core::ops::index::Index<Self, Idx>
-{
-    type Output
-    fn index : core::ops::index::Index::index
-}
-
 impl<'_0, K, Q, V, S> std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2]}#9<'_0, K, Q, V, S> : core::ops::index::Index<std::collections::hash::map::HashMap<K, V, S>[@TraitClause0, @TraitClause1, @TraitClause2], &'_0 (Q)>
 where
     [@TraitClause0]: core::marker::Sized<K>,
diff --git a/charon/tests/ui/region-inference-vars.out b/charon/tests/ui/region-inference-vars.out
index 42e2a8f2..2ea9810b 100644
--- a/charon/tests/ui/region-inference-vars.out
+++ b/charon/tests/ui/region-inference-vars.out
@@ -19,7 +19,7 @@ trait test_crate::MyTryFrom<Self, T>
     fn from : test_crate::MyTryFrom::from
 }
 
-fn test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}::from<'_0, '_1>(@1: &'_1 (bool)) -> core::result::Result<bool, test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}<'_>::Error>[core::marker::Sized<bool>, core::marker::Sized<()>]
+fn test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result<bool, test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}<'_>::Error>[core::marker::Sized<bool>, core::marker::Sized<()>]
 {
     let @0: core::result::Result<bool, ()>[core::marker::Sized<bool>, core::marker::Sized<()>]; // return
     let v@1: &'_ (bool); // arg #1
diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out
index 3d4748f5..32cfdc21 100644
--- a/charon/tests/ui/trait-instance-id.out
+++ b/charon/tests/ui/trait-instance-id.out
@@ -688,7 +688,7 @@ where
     fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked
 }
 
-fn core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_0, '_1, '_2>(@1: &'_1 mut (i32), @2: &'_2 (i32))
+fn core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_0, '_1>(@1: &'_1 mut (i32), @2: &'_0 (i32))
 
 fn core::slice::{Slice<T>}::chunks<'_0, T>(@1: &'_0 (Slice<T>), @2: usize) -> core::slice::iter::Chunks<'_0, T>[@TraitClause0]
 where
diff --git a/charon/tests/ui/traits_special.out b/charon/tests/ui/traits_special.out
index 018cb4b0..19d23707 100644
--- a/charon/tests/ui/traits_special.out
+++ b/charon/tests/ui/traits_special.out
@@ -19,7 +19,7 @@ trait test_crate::From<Self, T>
     fn from : test_crate::From::from
 }
 
-fn test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from<'_0, '_1>(@1: &'_1 (bool)) -> core::result::Result<bool, test_crate::{impl test_crate::From<&'_0 (bool)> for bool}<'_>::Error>[core::marker::Sized<bool>, core::marker::Sized<()>]
+fn test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result<bool, test_crate::{impl test_crate::From<&'_0 (bool)> for bool}<'_>::Error>[core::marker::Sized<bool>, core::marker::Sized<()>]
 {
     let @0: core::result::Result<bool, ()>[core::marker::Sized<bool>, core::marker::Sized<()>]; // return
     let v@1: &'_ (bool); // arg #1