diff --git a/charon-pin b/charon-pin
index afc5bfae7..d27a488d0 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-e0bf68d674edbb154fe2343b2315ccac325a0c7a
+cccc38353eec92c32c0f7a755fcef4ab5b1ae863
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 90a1714fa..dc1aa67d2 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -94,16 +94,15 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
+  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
+      trait_instance_id_is_local_clause id
   | TraitImpl _
   | BuiltinOrAuto _
-  | TraitRef _
   | UnknownTrait _
   | FnPointer _
   | Closure _
   | Unsolved _
   | Dyn _ -> false
-  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
-      trait_instance_id_is_local_clause id
 
 (** About the conversion functions: for now we need them (TODO: merge ety, rty, etc.),
     but they should be applied to types without regions.
@@ -149,6 +148,10 @@ let trait_ref_to_string (ctx : norm_ctx) (x : trait_ref) : string =
   let ctx = norm_ctx_to_fmt_env ctx in
   Print.Types.trait_ref_to_string ctx x
 
+let trait_decl_ref_to_string (ctx : norm_ctx) (x : trait_decl_ref) : string =
+  let ctx = norm_ctx_to_fmt_env ctx in
+  Print.Types.trait_decl_ref_to_string ctx x
+
 let trait_instance_id_to_string (ctx : norm_ctx) (x : trait_instance_id) :
     string =
   let ctx = norm_ctx_to_fmt_env ctx in
@@ -247,23 +250,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
       let ty : ty =
         match trait_ref.trait_id with
-        | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ }
-          ->
-            cassert_opt_span __FILE__ __LINE__
-              (ref_generics = empty_generic_args)
-              ctx.span "Higher order trait types are not supported yet";
-            log#ldebug
-              (lazy
-                ("norm_ctx_normalize_ty: trait type: trait ref: "
-               ^ ty_to_string ctx ty));
-            (* Lookup the type *)
-            let ty =
-              norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics
-                type_name
-            in
-            (* Normalize *)
-            norm_ctx_normalize_ty ctx ty
-        | TraitImpl impl_id ->
+        | TraitImpl (impl_id, generics) ->
             log#ldebug
               (lazy
                 ("norm_ctx_normalize_ty (trait impl):\n- trait type: "
@@ -278,8 +265,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
             *)
             (* Lookup the type *)
             let ty =
-              norm_ctx_lookup_trait_impl_ty ctx impl_id trait_ref.generics
-                type_name
+              norm_ctx_lookup_trait_impl_ty ctx impl_id generics type_name
             in
             (* Normalize *)
             norm_ctx_normalize_ty ctx ty
@@ -350,27 +336,22 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
         over it.
  *)
 and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
-    (id : trait_instance_id) : trait_instance_id * trait_ref option =
+    (id : trait_instance_id) : trait_instance_id =
   match id with
-  | Self -> (id, None)
-  | TraitImpl _ ->
+  | Self -> id
+  | TraitImpl (impl_id, generics) ->
       (* The [TraitImpl] shouldn't be inside any projection - we check this
          elsewhere by asserting that whenever we return [None] for the impl
          trait ref, then the id actually refers to a local clause. *)
-      (id, None)
-  | Clause _ -> (id, None)
-  | BuiltinOrAuto _ -> (id, None)
-  | ParentClause (inst_id, decl_id, clause_id) -> (
-      let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in
+      let generics = norm_ctx_normalize_generic_args ctx generics in
+      TraitImpl (impl_id, generics)
+  | Clause _ -> id
+  | BuiltinOrAuto _ -> id
+  | ParentClause (inst_id, decl_id, clause_id) -> begin
+      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
       (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match impl with
-      | None ->
-          (* This is actually a local clause *)
-          sanity_check_opt_span __FILE__ __LINE__
-            (trait_instance_id_is_local_clause inst_id)
-            ctx.span;
-          (ParentClause (inst_id, decl_id, clause_id), None)
-      | Some impl ->
+      match inst_id with
+      | TraitImpl (impl_id, generics) ->
           (* We figure out the parent clause by doing the following:
              {[
                // The implementation we are looking at
@@ -383,27 +364,24 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
              ]}
           *)
           (* Lookup the clause *)
-          let impl_id =
-            TypesUtils.trait_instance_id_as_trait_impl impl.trait_id
-          in
           let clause =
-            norm_ctx_lookup_trait_impl_parent_clause ctx impl_id impl.generics
+            norm_ctx_lookup_trait_impl_parent_clause ctx impl_id generics
               clause_id
           in
           (* Normalize the clause *)
-          let clause = norm_ctx_normalize_trait_ref ctx clause in
-          (TraitRef clause, Some clause))
-  | ItemClause (inst_id, decl_id, item_name, clause_id) -> (
-      let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in
-      (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match impl with
-      | None ->
+          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
+      | _ ->
           (* This is actually a local clause *)
           sanity_check_opt_span __FILE__ __LINE__
             (trait_instance_id_is_local_clause inst_id)
             ctx.span;
-          (ItemClause (inst_id, decl_id, item_name, clause_id), None)
-      | Some impl ->
+          ParentClause (inst_id, decl_id, clause_id)
+    end
+  | ItemClause (inst_id, decl_id, item_name, clause_id) -> begin
+      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
+      (* Check if the inst_id refers to a specific implementation, if yes project *)
+      match inst_id with
+      | TraitImpl (impl_id, generics) ->
           (* We figure out the item clause by doing the following:
              {[
                // The implementation we are looking at
@@ -416,49 +394,30 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
              ]}
           *)
           (* Lookup the impl *)
-          let impl_id =
-            TypesUtils.trait_instance_id_as_trait_impl impl.trait_id
-          in
           let clause =
-            norm_ctx_lookup_trait_impl_item_clause ctx impl_id impl.generics
+            norm_ctx_lookup_trait_impl_item_clause ctx impl_id generics
               item_name clause_id
           in
           (* Normalize the clause *)
-          let clause = norm_ctx_normalize_trait_ref ctx clause in
-          (TraitRef clause, Some clause))
-  | TraitRef { trait_id = TraitImpl trait_id; generics; trait_decl_ref } ->
-      (* We can't simplify the id *yet* : we will simplify it when projecting.
-         However, we have an implementation to return *)
-      (* Normalize the generics *)
-      let generics = norm_ctx_normalize_generic_args ctx generics in
-      let trait_decl_ref =
-        norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref
-      in
-      let trait_ref : trait_ref =
-        { trait_id = TraitImpl trait_id; generics; trait_decl_ref }
-      in
-      (TraitRef trait_ref, Some trait_ref)
-  | TraitRef trait_ref ->
-      (* The trait instance id necessarily refers to a local sub-clause. We
-         can't project over it and can only peel off the [TraitRef] wrapper *)
-      sanity_check_opt_span __FILE__ __LINE__
-        (trait_instance_id_is_local_clause trait_ref.trait_id)
-        ctx.span;
-      sanity_check_opt_span __FILE__ __LINE__
-        (trait_ref.generics = empty_generic_args)
-        ctx.span;
-      (trait_ref.trait_id, None)
+          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
+      | _ ->
+          (* This is actually a local clause *)
+          sanity_check_opt_span __FILE__ __LINE__
+            (trait_instance_id_is_local_clause inst_id)
+            ctx.span;
+          ItemClause (inst_id, decl_id, item_name, clause_id)
+    end
   | FnPointer ty ->
       let ty = norm_ctx_normalize_ty ctx ty in
       (* TODO: we might want to return the ref to the function pointer,
          in order to later normalize a call to this function pointer *)
-      (FnPointer ty, None)
+      FnPointer ty
   | Closure (fid, generics) ->
       let generics = norm_ctx_normalize_generic_args ctx generics in
-      (Closure (fid, generics), None)
+      Closure (fid, generics)
   | Unsolved _ | UnknownTrait _ ->
       (* This is actually an error case *)
-      (id, None)
+      id
   | Dyn _ ->
       craise_opt_span __FILE__ __LINE__ ctx.span
         "Dynamic trait types are not supported yet"
@@ -477,31 +436,16 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) :
       ("norm_ctx_normalize_trait_ref: "
       ^ trait_ref_to_string ctx trait_ref
       ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
-  let { trait_id; generics; trait_decl_ref } = trait_ref in
+  let { trait_id; trait_decl_ref } = trait_ref in
+
   (* Check if the id is an impl, otherwise normalize it *)
-  let trait_id, norm_trait_ref =
-    norm_ctx_normalize_trait_instance_id ctx trait_id
-  in
-  match norm_trait_ref with
-  | None ->
-      log#ldebug
-        (lazy
-          ("norm_ctx_normalize_trait_ref: no norm: "
-          ^ trait_instance_id_to_string ctx trait_id));
-      let generics = norm_ctx_normalize_generic_args ctx generics in
-      let trait_decl_ref =
-        norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref
-      in
-      { trait_id; generics; trait_decl_ref }
-  | Some trait_ref ->
-      log#ldebug
-        (lazy
-          ("norm_ctx_normalize_trait_ref: normalized to: "
-          ^ trait_ref_to_string ctx trait_ref));
-      sanity_check_opt_span __FILE__ __LINE__
-        (generics = empty_generic_args)
-        ctx.span;
-      trait_ref
+  let trait_id = norm_ctx_normalize_trait_instance_id ctx trait_id in
+  let trait_decl_ref = norm_ctx_normalize_trait_decl_ref ctx trait_decl_ref in
+  log#ldebug
+    (lazy
+      ("norm_ctx_normalize_trait_ref: no norm: "
+      ^ trait_instance_id_to_string ctx trait_id));
+  { trait_id; trait_decl_ref }
 
 (* Not sure this one is really necessary *)
 and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 52a163ebd..c3f6fa591 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1641,9 +1641,9 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
         (fun (c : Types.trait_clause) -> c.clause_id = clause_id)
         clauses
     in
-    let trait_id = clause.trait_id in
+    let trait_id = clause.trait.trait_decl_id in
     let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
-    let args = clause.clause_generics in
+    let args = clause.trait.decl_generics in
     trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
       impl_trait_decl.item_meta.name params args
   in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 6b1965482..aac399240 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -587,9 +587,6 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            sanity_check __FILE__ __LINE__
-              (trait_ref.generics = empty_generic_args)
-              span;
             extract_trait_instance_id_with_dot span ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
@@ -606,28 +603,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
 and extract_trait_ref (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
     (tr : trait_ref) : unit =
-  let use_brackets = tr.generics <> empty_generic_args && inside in
-  if use_brackets then F.pp_print_string fmt "(";
-  (* We may need to filter the parameters if the trait is builtin *)
-  let generics =
-    match tr.trait_id with
-    | TraitImpl id -> (
-        match
-          TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map
-        with
-        | None -> tr.generics
-        | Some filter ->
-            let types =
-              List.filter_map
-                (fun (b, x) -> if b then Some x else None)
-                (List.combine filter tr.generics.types)
-            in
-            { tr.generics with types })
-    | _ -> tr.generics
-  in
-  extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id;
-  extract_generic_args span ctx fmt no_params_tys generics;
-  if use_brackets then F.pp_print_string fmt ")"
+  extract_trait_instance_id span ctx fmt no_params_tys inside tr.trait_id
 
 and extract_trait_decl_ref (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
@@ -715,9 +691,27 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
          (associated type, etc.). We should have caught this elsewhere. *)
       save_error __FILE__ __LINE__ (Some span) "Unexpected occurrence of `Self`";
       F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
-  | TraitImpl id ->
+  | TraitImpl (id, generics) ->
+      (* We may need to filter the parameters if the trait is builtin *)
+      let generics =
+        match
+          TraitImplId.Map.find_opt id ctx.trait_impls_filter_type_args_map
+        with
+        | None -> generics
+        | Some filter ->
+            let types =
+              List.filter_map
+                (fun (b, x) -> if b then Some x else None)
+                (List.combine filter generics.types)
+            in
+            { generics with types }
+      in
       let name = ctx_get_trait_impl span id ctx in
-      F.pp_print_string fmt name
+      let use_brackets = generics <> empty_generic_args && inside in
+      if use_brackets then F.pp_print_string fmt "(";
+      F.pp_print_string fmt name;
+      extract_generic_args span ctx fmt no_params_tys generics;
+      if use_brackets then F.pp_print_string fmt ")"
   | Clause id ->
       let name = ctx_get_local_trait_clause span id ctx in
       F.pp_print_string fmt name
@@ -733,8 +727,6 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
       in
       extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
-  | TraitRef trait_ref ->
-      extract_trait_ref span ctx fmt no_params_tys inside trait_ref
   | UnknownTrait _ ->
       (* This is an error case *)
       craise __FILE__ __LINE__ span "Unexpected"
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 3d665de6b..91613eebe 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -133,17 +133,15 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
       List.fold_left_map
         (fun tr_map (c : trait_clause) ->
           let subst = mk_subst tr_map in
-          let { trait_id = trait_decl_id; clause_generics; _ } = c in
+          let { trait_decl_id; decl_generics; _ } = c.trait in
           let generics =
-            Substitute.generic_args_substitute subst clause_generics
+            Substitute.generic_args_substitute subst decl_generics
           in
           let trait_decl_ref = { trait_decl_id; decl_generics = generics } in
           (* Note that because we directly refer to the clause, we give it
              empty generics *)
           let trait_id = Clause c.clause_id in
-          let trait_ref =
-            { trait_id; generics = empty_generic_args; trait_decl_ref }
-          in
+          let trait_ref = { trait_id; trait_decl_ref } in
           (* Update the traits map *)
           let tr_map = TraitClauseId.Map.add c.clause_id trait_id tr_map in
           (tr_map, trait_ref))
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index cf104d778..c4f260083 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -753,7 +753,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
              depending on whethere we call a top-level trait method impl or the
              method from a local clause *)
           match trait_ref.trait_id with
-          | TraitImpl impl_id -> (
+          | TraitImpl (impl_id, generics) -> (
               (* Lookup the trait impl *)
               let trait_impl = ctx_lookup_trait_impl ctx impl_id in
               log#ldebug
@@ -770,11 +770,9 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                   let method_def = ctx_lookup_fun_decl ctx id in
                   (* We have to concatenate the generics for the impl
                      and the generics for the method *)
-                  let generics =
-                    merge_generic_args trait_ref.generics func.generics
-                  in
+                  let generics = merge_generic_args generics func.generics in
                   (* Instantiate *)
-                  let tr_self = TraitRef trait_ref in
+                  let tr_self = trait_ref.trait_id in
                   let fid : fun_id = FRegular id in
                   let regions_hierarchy =
                     LlbcAstUtils.FunIdMap.find fid
@@ -847,7 +845,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                     LlbcAstUtils.FunIdMap.find (FRegular method_id)
                       ctx.fun_ctx.regions_hierarchies
                   in
-                  let tr_self = TraitRef trait_ref in
+                  let tr_self = trait_ref.trait_id in
                   let inst_sg =
                     instantiate_fun_sig span ctx all_generics tr_self
                       method_def.signature regions_hierarchy
@@ -891,7 +889,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                 LlbcAstUtils.FunIdMap.find (FRegular method_id)
                   ctx.fun_ctx.regions_hierarchies
               in
-              let tr_self = TraitRef trait_ref in
+              let tr_self = trait_ref.trait_id in
               let inst_sg =
                 instantiate_fun_sig span ctx generics tr_self
                   method_def.signature regions_hierarchy
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index a142aa8fb..3d679622d 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -177,26 +177,31 @@ and generic_args_to_string (env : fmt_env) (generics : generic_args) : string =
 
 and trait_ref_to_string (env : fmt_env) (inside : bool) (tr : trait_ref) :
     string =
-  let trait_id = trait_instance_id_to_string env false tr.trait_id in
-  let generics = generic_args_to_string env tr.generics in
-  let s = trait_id ^ generics in
-  if tr.generics = empty_generic_args || not inside then s else "(" ^ s ^ ")"
+  let trait_id = trait_instance_id_to_string env tr.trait_id in
+  let generics_are_empty =
+    match tr.trait_id with
+    | TraitImpl (_, generics) -> generics = empty_generic_args
+    | _ -> true
+  in
+  if generics_are_empty || not inside then trait_id else "(" ^ trait_id ^ ")"
 
-and trait_instance_id_to_string (env : fmt_env) (inside : bool)
-    (id : trait_instance_id) : string =
+and trait_instance_id_to_string (env : fmt_env) (id : trait_instance_id) :
+    string =
   match id with
   | Self -> "Self"
-  | TraitImpl id -> trait_impl_id_to_string env id
+  | TraitImpl (impl_id, generics) ->
+      let generics = generic_args_to_string env generics in
+      let impl_id = trait_impl_id_to_string env impl_id in
+      impl_id ^ generics
   | Clause id -> trait_clause_id_to_string env id
   | ParentClause (inst_id, _decl_id, clause_id) ->
-      let inst_id = trait_instance_id_to_string env false inst_id in
+      let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
       "parent(" ^ inst_id ^ ")::" ^ clause_id
   | ItemClause (inst_id, _decl_id, item_name, clause_id) ->
-      let inst_id = trait_instance_id_to_string env false inst_id in
+      let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
       "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
-  | TraitRef tr -> trait_ref_to_string env inside tr
   | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
 
 let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 2754eaac8..0575dce1c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -290,7 +290,6 @@ type ty =
 
 and trait_ref = {
   trait_id : trait_instance_id;
-  generics : generic_args;
   trait_decl_ref : trait_decl_ref;
 }
 
@@ -307,12 +306,11 @@ and generic_args = {
 
 and trait_instance_id =
   | Self
-  | TraitImpl of trait_impl_id
+  | TraitImpl of trait_impl_id * generic_args
   | Clause of trait_clause_id
   | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
   | ItemClause of
       trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id
-  | TraitRef of trait_ref
   | UnknownTrait of string
 [@@deriving
   show,
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 579b3dd54..818e4f8bc 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -163,7 +163,7 @@ let make_const_generic_subst (vars : const_generic_var list)
 let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) :
     TraitClauseId.id -> trait_instance_id =
   let clauses = List.map (fun x -> x.clause_id) clauses in
-  let refs = List.map (fun x -> TraitRef x) refs in
+  let refs = List.map (fun (x : trait_ref) -> x.trait_id) refs in
   let ls = List.combine clauses refs in
   let mp =
     List.fold_left
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index df1f0642a..29af3efcb 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -422,11 +422,10 @@ let rec translate_generic_args (span : Meta.span) (translate_ty : T.ty -> ty)
 and translate_trait_ref (span : Meta.span) (translate_ty : T.ty -> ty)
     (tr : T.trait_ref) : trait_ref =
   let trait_id = translate_trait_instance_id span translate_ty tr.trait_id in
-  let generics = translate_generic_args span translate_ty tr.generics in
   let trait_decl_ref =
     translate_trait_decl_ref span translate_ty tr.trait_decl_ref
   in
-  { trait_id; generics; trait_decl_ref }
+  { trait_id; trait_decl_ref }
 
 and translate_trait_decl_ref (span : Meta.span) (translate_ty : T.ty -> ty)
     (tr : T.trait_decl_ref) : trait_decl_ref =
@@ -442,7 +441,9 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
   in
   match id with
   | T.Self -> Self
-  | TraitImpl id -> TraitImpl id
+  | TraitImpl (id, generics) ->
+      let generics = translate_generic_args span translate_ty generics in
+      TraitImpl (id, generics)
   | BuiltinOrAuto _ ->
       (* We should have eliminated those in the prepasses *)
       craise __FILE__ __LINE__ span "Unreachable"
@@ -453,7 +454,6 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
   | ItemClause (inst_id, decl_id, item_name, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
       ItemClause (inst_id, decl_id, item_name, clause_id)
-  | TraitRef tr -> TraitRef (translate_trait_ref span translate_ty tr)
   | FnPointer _ | Closure _ ->
       craise __FILE__ __LINE__ span "Closures are not supported yet"
   | Dyn _ ->
@@ -518,9 +518,9 @@ and translate_strait_instance_id (span : Meta.span) (id : T.trait_instance_id) :
 
 let translate_trait_clause (span : Meta.span) (clause : T.trait_clause) :
     trait_clause =
-  let { T.clause_id; span = _; trait_id; clause_generics } = clause in
-  let generics = translate_sgeneric_args span clause_generics in
-  { clause_id; trait_id; generics }
+  let { T.clause_id; span = _; trait } = clause in
+  let generics = translate_sgeneric_args span trait.decl_generics in
+  { clause_id; trait_id = trait.trait_decl_id; generics }
 
 let translate_strait_type_constraint (span : Meta.span)
     (ttc : T.trait_type_constraint) : trait_type_constraint =
@@ -3576,11 +3576,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
             let trait_decl_ref =
               { trait_decl_id = c.trait_id; decl_generics = empty_generic_args }
             in
-            {
-              trait_id = Clause c.clause_id;
-              generics = empty_generic_args;
-              trait_decl_ref;
-            })
+            { trait_id = Clause c.clause_id; trait_decl_ref })
           trait_clauses
       in
       { types; const_generics; trait_refs }
diff --git a/flake.lock b/flake.lock
index 8ee729788..4f5b189af 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1719994894,
-        "narHash": "sha256-RhSc57vv/xORPkjqnL4jcupcyV6DTfgm8KqRiOI1ruA=",
+        "lastModified": 1720447930,
+        "narHash": "sha256-U5Tz1Pz7pmeFTrheZS90K3iRmfnlHvi47UexXflwV2o=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "e0bf68d674edbb154fe2343b2315ccac325a0c7a",
+        "rev": "cccc38353eec92c32c0f7a755fcef4ab5b1ae863",
         "type": "github"
       },
       "original": {
@@ -272,11 +272,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1719973106,
-        "narHash": "sha256-IGCdN/m7DfwUfxZjFnlTiTtpwSHCb01P/LWavAKD2jw=",
+        "lastModified": 1720405186,
+        "narHash": "sha256-7D57KwmTIbsopE/1g8hFeIbVoeJGgU3wfuGYvTlNQG4=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "fb733500aead50880b9b301f34a0061bf997d6f2",
+        "rev": "f0ca58b37ff4179ce4587589c32205764d9b4a4f",
         "type": "github"
       },
       "original": {