diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index a169d78a..5da7620a 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -138,10 +138,10 @@ impl BodyTransCtx<'_, '_> {
                         // declares them.
                         let id = self.register_global_decl_id(item_span, item_def_id);
                         let generics_target = GenericsSource::item(id);
-                        let gref = GlobalDeclRef {
-                            id,
-                            generics: self.the_only_binder().params.identity_args(generics_target),
-                        };
+                        let mut generics =
+                            self.the_only_binder().params.identity_args(generics_target);
+                        generics.trait_refs.push(self_trait_ref.clone());
+                        let gref = GlobalDeclRef { id, generics };
                         const_defaults.insert(item_name.clone(), gref);
                     };
                     let ty = self.translate_ty(item_span, ty)?;
@@ -238,6 +238,16 @@ impl BodyTransCtx<'_, '_> {
             )?;
             TraitDeclRef { trait_id, generics }
         };
+        // A `TraitRef` that points to this impl with the correct generics.
+        let self_predicate = TraitRef {
+            kind: TraitRefKind::TraitImpl(
+                def_id,
+                self.the_only_binder()
+                    .params
+                    .identity_args(GenericsSource::item(def_id)),
+            ),
+            trait_decl_ref: RegionBinder::empty(implemented_trait.clone()),
+        };
 
         // The trait refs which implement the parent clauses of the implemented trait decl.
         let parent_trait_refs = self.translate_trait_impl_exprs(span, &required_impl_exprs)?;
@@ -322,10 +332,14 @@ impl BodyTransCtx<'_, '_> {
                         Provided { .. } => {
                             self.the_only_binder().params.identity_args(generics_target)
                         }
-                        _ => implemented_trait
-                            .generics
-                            .clone()
-                            .with_target(generics_target),
+                        _ => {
+                            let mut generics = implemented_trait
+                                .generics
+                                .clone()
+                                .with_target(generics_target);
+                            generics.trait_refs.push(self_predicate.clone());
+                            generics
+                        }
                     };
                     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 57e2d0ca..e923eb94 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -593,9 +593,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             | Variant { .. } => {
                 let parent_def_id = def.parent.as_ref().unwrap();
                 let parent_def = self.t_ctx.hax_def(parent_def_id)?;
-                let explicit_self_clause = matches!(def.kind(), AssocFn { .. })
-                    && matches!(parent_def.kind(), Trait { .. });
-                // Add an explicit `Self` clause to trait method declarations.
+                // Add an explicit `Self` clause to trait item declarations.
+                let explicit_self_clause = matches!(parent_def.kind(), Trait { .. });
                 self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?;
             }
             _ => {}
diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs
index cbc7f706..9a07fb90 100644
--- a/charon/tests/crate_data.rs
+++ b/charon/tests/crate_data.rs
@@ -612,14 +612,10 @@ fn declaration_groups() -> anyhow::Result<()> {
         "#,
     )?;
 
-    // There are two function ids registered, but only one is nonempty. `functions.len() == 2` as
-    // `len()` counts the empty slots too.
-    let decl_groups = crate_data.ordered_decls.unwrap();
+    // There are two function items: one for `foo`, one for the initializer of `Trait::FOO`.
     assert_eq!(crate_data.fun_decls.iter().count(), 2);
+    let decl_groups = crate_data.ordered_decls.unwrap();
     assert_eq!(decl_groups.len(), 5);
-    assert!(decl_groups
-        .iter()
-        .all(|group| group.to_mixed_group().is_non_rec()));
 
     Ok(())
 }
diff --git a/charon/tests/ui/assoc-const-with-generics.out b/charon/tests/ui/assoc-const-with-generics.out
index 37a92291..0740684d 100644
--- a/charon/tests/ui/assoc-const-with-generics.out
+++ b/charon/tests/ui/assoc-const-with-generics.out
@@ -94,6 +94,8 @@ where
 }
 
 fn test_crate::HasDefaultLen::LEN<Self, const M : usize>() -> usize
+where
+    [@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
 {
     let @0: usize; // return
 
@@ -101,7 +103,10 @@ fn test_crate::HasDefaultLen::LEN<Self, const M : usize>() -> usize
     return
 }
 
-global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize = test_crate::HasDefaultLen::LEN()
+global test_crate::HasDefaultLen::LEN<Self, const M : usize>: usize
+  where
+      [@TraitClause0]: test_crate::HasDefaultLen<Self, const M : usize>,
+ = test_crate::HasDefaultLen::LEN()
 
 trait test_crate::HasDefaultLen<Self, const M : usize>
 {
@@ -110,7 +115,7 @@ trait test_crate::HasDefaultLen<Self, const M : usize>
 
 impl<const N : usize> test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize> : test_crate::HasDefaultLen<Array<(), const N : usize>, const N : usize>
 {
-    const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>
+    const LEN = test_crate::HasDefaultLen::LEN<Array<(), const N : usize>, const N : usize>[test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<(), const N : usize>}#4<const N : usize>]
 }
 
 fn test_crate::{impl test_crate::HasDefaultLen<const N : usize> for Array<bool, const N : usize>}#5::LEN<const N : usize>() -> usize
@@ -137,14 +142,19 @@ impl<const N : usize> test_crate::{impl test_crate::HasDefaultLen<const N : usiz
 }
 
 fn test_crate::AlsoHasLen::ALSO_LEN<Self>() -> usize
+where
+    [@TraitClause0]: test_crate::AlsoHasLen<Self>,
 {
     let @0: usize; // return
 
-    @0 := const (Self::parent_clause0::LEN) + const (1 : usize)
+    @0 := const (@TraitClause0::parent_clause0::LEN) + const (1 : usize)
     return
 }
 
-global test_crate::AlsoHasLen::ALSO_LEN<Self>: usize = test_crate::AlsoHasLen::ALSO_LEN()
+global test_crate::AlsoHasLen::ALSO_LEN<Self>: usize
+  where
+      [@TraitClause0]: test_crate::AlsoHasLen<Self>,
+ = test_crate::AlsoHasLen::ALSO_LEN()
 
 trait test_crate::AlsoHasLen<Self>
 {
@@ -155,7 +165,7 @@ trait test_crate::AlsoHasLen<Self>
 impl<const N : usize> test_crate::{impl test_crate::AlsoHasLen for Array<(), const N : usize>}#6<const N : usize> : test_crate::AlsoHasLen<Array<(), const N : usize>>
 {
     parent_clause0 = test_crate::{impl test_crate::HasLen for Array<(), const N : usize>}#1<const N : usize>
-    const ALSO_LEN = test_crate::AlsoHasLen::ALSO_LEN<Array<(), const N : usize>>
+    const ALSO_LEN = test_crate::AlsoHasLen::ALSO_LEN<Array<(), const N : usize>>[test_crate::{impl test_crate::AlsoHasLen for Array<(), const N : usize>}#6<const N : usize>]
 }
 
 
diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out
index 91cd09ca..06a1fdad 100644
--- a/charon/tests/ui/traits.out
+++ b/charon/tests/ui/traits.out
@@ -488,6 +488,8 @@ where
 }
 
 fn test_crate::WithConstTy::LEN2<Self, const LEN : usize>() -> usize
+where
+    [@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
 {
     let @0: usize; // return
 
@@ -495,7 +497,10 @@ fn test_crate::WithConstTy::LEN2<Self, const LEN : usize>() -> usize
     return
 }
 
-global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize = test_crate::WithConstTy::LEN2()
+global test_crate::WithConstTy::LEN2<Self, const LEN : usize>: usize
+  where
+      [@TraitClause0]: test_crate::WithConstTy<Self, const LEN : usize>,
+ = test_crate::WithConstTy::LEN2()
 
 trait test_crate::WithConstTy<Self, const LEN : usize>
 {
@@ -538,7 +543,7 @@ impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8 : test_cr
     parent_clause1 = test_crate::{impl test_crate::ToU64 for u64}#2
     parent_clause2 = core::marker::Sized<u64>
     const LEN1 = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1
-    const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>
+    const LEN2 = test_crate::WithConstTy::LEN2<bool, 32 : usize>[test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8]
     type V = u8
     type W = u64
     fn f<'_0, '_1> = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0_0, '_0_1>