Add more info to ImplExprAtom::Builtin

engine/lib/import_thir.ml

@@ -1147,7 +1147,7 @@ end) : EXPR = struct
         List.fold ~init ~f:browse_path path
     | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
-    | Builtin { trait } -> Builtin (c_trait_ref span trait.value)
+    | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value)
     | Error str -> failwith @@ "impl_expr_atom: Error " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

frontend/exporter/src/traits.rs

@@ -92,8 +92,18 @@ pub enum ImplExprAtom {
     /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
     /// built-in implementation.
     Dyn,
-    /// A built-in trait whose implementation is computed by the compiler, such as `Sync`.
-    Builtin { r#trait: Binder<TraitRef> },
+    /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
+    /// morally points to an invisible `impl` block; as such it contains the information we may
+    /// need from one.
+    Builtin {
+        r#trait: Binder<TraitRef>,
+        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
+        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
+        /// FnOnce`.
+        impl_exprs: Vec<ImplExpr>,
+        /// The values of the associated types for this trait.
+        types: Vec<(DefId, Ty)>,
+    },
     /// An error happened while resolving traits.
     Error(String),
 }

frontend/exporter/src/traits/resolution.rs

@@ -73,8 +73,18 @@ pub enum ImplExprAtom<'tcx> {
     /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
     /// built-in implementation.
     Dyn,
-    /// A built-in trait whose implementation is computed by the compiler, such as `Sync`.
-    Builtin { r#trait: PolyTraitRef<'tcx> },
+    /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
+    /// morally points to an invisible `impl` block; as such it contains the information we may
+    /// need from one.
+    Builtin {
+        r#trait: PolyTraitRef<'tcx>,
+        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
+        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
+        /// FnOnce`.
+        impl_exprs: Vec<ImplExpr<'tcx>>,
+        /// The values of the associated types for this trait.
+        types: Vec<(DefId, Ty<'tcx>)>,
+    },
     /// An error happened while resolving traits.
     Error(String),
 }
@@ -290,7 +300,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
 
         // Resolve predicates required to mention the item.
         let nested_impl_exprs =
-            self.resolve_item_predicates(alias_ty.def_id, alias_ty.args, warn)?;
+            self.resolve_item_required_predicates(alias_ty.def_id, alias_ty.args, warn)?;
 
         // Add all the bounds on the corresponding associated item.
         self.extend(item_bounds.map(|(index, pred)| {
@@ -367,7 +377,8 @@ impl<'tcx> PredicateSearcher<'tcx> {
                 ..
             })) => {
                 // Resolve the predicates required by the impl.
-                let impl_exprs = self.resolve_item_predicates(impl_def_id, generics, warn)?;
+                let impl_exprs =
+                    self.resolve_item_required_predicates(impl_def_id, generics, warn)?;
                 ImplExprAtom::Concrete {
                     def_id: impl_def_id,
                     generics,
@@ -401,7 +412,43 @@ impl<'tcx> PredicateSearcher<'tcx> {
                 }
             }
             Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn,
-            Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref },
+            Ok(ImplSource::Builtin(_, _)) => {
+                // Resolve the predicates implied by the trait.
+                let trait_def_id = erased_tref.skip_binder().def_id;
+                // If we wanted to not skip this binder, we'd have to instantiate the bound
+                // regions, solve, then wrap the result in a binder. And track  higher-kinded
+                // clauses better all over.
+                let impl_exprs = self.resolve_item_implied_predicates(
+                    trait_def_id,
+                    erased_tref.skip_binder().args,
+                    warn,
+                )?;
+                let types = tcx
+                    .associated_items(trait_def_id)
+                    .in_definition_order()
+                    .filter(|assoc| matches!(assoc.kind, AssocKind::Type))
+                    .filter_map(|assoc| {
+                        let ty = AliasTy::new(tcx, assoc.def_id, erased_tref.skip_binder().args)
+                            .to_ty(tcx);
+                        let ty = erase_and_norm(tcx, self.param_env, ty);
+                        if let TyKind::Alias(_, alias_ty) = ty.kind() {
+                            if alias_ty.def_id == assoc.def_id {
+                                warn(&format!("Failed to compute associated type {ty}"));
+                                // We can't return the unnormalized associated type as that would
+                                // make the trait ref contain itself, which would make hax's
+                                // `sinto` infrastructure loop.
+                                return None;
+                            }
+                        }
+                        Some((assoc.def_id, ty))
+                    })
+                    .collect();
+                ImplExprAtom::Builtin {
+                    r#trait: *tref,
+                    impl_exprs,
+                    types,
+                }
+            }
             Err(e) => {
                 let msg = format!(
                     "Could not find a clause for `{tref:?}` in the current context: `{e:?}`"
@@ -418,15 +465,40 @@ impl<'tcx> PredicateSearcher<'tcx> {
     }
 
     /// Resolve the predicates required by the given item.
-    pub fn resolve_item_predicates(
+    pub fn resolve_item_required_predicates(
+        &mut self,
+        def_id: DefId,
+        generics: GenericArgsRef<'tcx>,
+        // Call back into hax-related code to display a nice warning.
+        warn: &impl Fn(&str),
+    ) -> Result<Vec<ImplExpr<'tcx>>, String> {
+        let tcx = self.tcx;
+        self.resolve_predicates(generics, required_predicates(tcx, def_id), warn)
+    }
+
+    /// Resolve the predicates implied by the given item.
+    pub fn resolve_item_implied_predicates(
         &mut self,
         def_id: DefId,
         generics: GenericArgsRef<'tcx>,
         // Call back into hax-related code to display a nice warning.
         warn: &impl Fn(&str),
     ) -> Result<Vec<ImplExpr<'tcx>>, String> {
         let tcx = self.tcx;
-        required_predicates(tcx, def_id)
+        self.resolve_predicates(generics, implied_predicates(tcx, def_id), warn)
+    }
+
+    /// Apply the given generics to the provided clauses and resolve the trait references in the
+    /// current context.
+    pub fn resolve_predicates(
+        &mut self,
+        generics: GenericArgsRef<'tcx>,
+        predicates: GenericPredicates<'tcx>,
+        // Call back into hax-related code to display a nice warning.
+        warn: &impl Fn(&str),
+    ) -> Result<Vec<ImplExpr<'tcx>>, String> {
+        let tcx = self.tcx;
+        predicates
             .predicates
             .iter()
             .map(|(clause, _span)| *clause)

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -55,7 +55,7 @@ open FStar.Mul
 class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16210070100893052778:t_Bar v_Self f_U;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_13496126865352171029:t_Bar v_Self f_U;
   f_U:Type0
 }
 '''
@@ -408,7 +408,7 @@ class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
     v_TypeArg
     v_ConstArg;
   f_AssocType:Type0;
-  f_AssocType_7414800425644916102:t_Trait f_AssocType v_TypeArg v_ConstArg
+  f_AssocType_13704321474071752218:t_Trait f_AssocType v_TypeArg v_ConstArg
 }
 '''
 "Traits.Interlaced_consts_types.fst" = '''
@@ -485,7 +485,7 @@ open FStar.Mul
 
 class t_Trait1 (v_Self: Type0) = {
   f_T:Type0;
-  f_T_2328060197809802853:t_Trait1 f_T
+  f_T_2186006717281159153:t_Trait1 f_T
 }
 
 class t_Trait2 (v_Self: Type0) = {
@@ -630,7 +630,7 @@ let use_impl_trait (_: Prims.unit) : Prims.unit =
 
 class t_Foo (v_Self: Type0) = {
   f_AssocType:Type0;
-  f_AssocType_12248650268031145847:t_SuperTrait f_AssocType;
+  f_AssocType_16668910951696008497:t_SuperTrait f_AssocType;
   f_N:usize;
   f_assoc_f_pre:Prims.unit -> Type0;
   f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
@@ -667,7 +667,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
   {
     f_AssocType = i32;
-    f_AssocType_12248650268031145847 = FStar.Tactics.Typeclasses.solve;
+    f_AssocType_16668910951696008497 = FStar.Tactics.Typeclasses.solve;
     f_N = sz 32;
     f_assoc_f_pre = (fun (_: Prims.unit) -> true);
     f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);