Repository: cryspen/hax (language: rust)

Issue:
Super-parent bounds of associated types in impls are inlined
```rust
trait A{}
trait B{}
trait C:A+B{}

trait D {
   type T:C;
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/102ae9fdc9/gist=92dc559a6c2d45b8d440f4dc2aa977ed)

Here we translate to the following F*:
```fstar

class t_C (v_Self: Type0) = {
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_14273389043514592625:t_A
  v_Self;
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_14858733883632685556:t_B
  v_Self
}

class t_D (v_Self: Type0) = {
  f_T:Type0;
  f_T_16407784479303782286:t_C f_T;
  f_T_4589724874609156387:t_B f_T;
  f_T_3674199358433564065:t_A f_T
}
```

The bounds on `T` contain the super bounds of `C`, this is wrong.


Discussion / hints:

Fix patch:
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


Test patch:
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) = {