From 52cc0219bec4d33b3a83f1c78cfb561cc4791918 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 17 Dec 2024 16:41:50 +0100
Subject: [PATCH] Only include direct parent bounds for associated types in
 traits.

---
 frontend/exporter/src/types/hir.rs                    | 11 ++++++++---
 .../src/snapshots/toolchain__traits into-fstar.snap   | 11 +++++------
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index 307120076..1c8a23399 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -840,10 +840,15 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene
     };
 
     let clauses: Vec<ty::Clause<'tcx>> = if use_item_bounds {
-        tcx.item_bounds(s.owner_id())
+        tcx.explicit_item_bounds(s.owner_id())
+            .map_bound(|clauses| {
+                clauses
+                    .iter()
+                    .map(|(x, _span)| x)
+                    .copied()
+                    .collect::<Vec<_>>()
+            })
             .instantiate_identity()
-            .iter()
-            .collect()
     } else {
         predicates_defined_on(tcx, s.owner_id())
             .predicates
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index fcc166dc9..2568c7d3d 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -614,7 +614,6 @@ let use_impl_trait (_: Prims.unit) : Prims.unit =
 class t_Foo (v_Self: Type0) = {
   f_AssocType:Type0;
   f_AssocType_15012754260415912210:t_SuperTrait f_AssocType;
-  f_AssocType_3242921639065184873:Core.Clone.t_Clone f_AssocType;
   f_N:usize;
   f_assoc_f_pre:Prims.unit -> Type0;
   f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
@@ -624,12 +623,12 @@ class t_Foo (v_Self: Type0) = {
   f_method_f_post:v_Self -> Prims.unit -> Type0;
   f_method_f:x0: v_Self
     -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result);
-  f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Type0;
-  f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> Type0;
-  f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType
+  f_assoc_type_pre:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Type0;
+  f_assoc_type_post:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> Type0;
+  f_assoc_type:{| i2: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType
     -> Prims.Pure Prims.unit
-        (f_assoc_type_pre #i3 x0)
-        (fun result -> f_assoc_type_post #i3 x0 result)
+        (f_assoc_type_pre #i2 x0)
+        (fun result -> f_assoc_type_post #i2 x0 result)
 }
 
 class t_Lang (v_Self: Type0) = {