Add more info to ImplExprAtom::Builtin

engine/lib/import_thir.ml

@@ -1099,11 +1099,12 @@ end) : EXPR = struct
   and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
     let goal = c_trait_ref span ie.trait.value in
     let impl = { kind = c_impl_expr_atom span ie.impl; goal } in
-    match ie.args with
-    | [] -> impl
-    | args ->
-        let args = List.map ~f:(c_impl_expr span) args in
+    match ie.impl with
+    | Concrete { impl_exprs = []; _ } -> impl
+    | Concrete { impl_exprs; _ } ->
+        let args = List.map ~f:(c_impl_expr span) impl_exprs in
         { kind = ImplApp { impl; args }; goal }
+    | _ -> impl
 
   and c_trait_ref span (tr : Thir.trait_ref) : trait_goal =
     let trait = Concrete_ident.of_def_id Trait tr.def_id in
@@ -1137,7 +1138,7 @@ end) : EXPR = struct
           Parent { impl = { kind = item_kind; goal = trait_ref }; ident }
     in
     match ie with
-    | Concrete { id; generics } ->
+    | Concrete { id; generics; _ } ->
         let trait = Concrete_ident.of_def_id Impl id in
         let args = List.map ~f:(c_generic_value span) generics in
         Concrete { trait; args }
@@ -1146,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

@@ -62,6 +62,8 @@ pub enum ImplExprAtom {
         #[from(def_id)]
         id: GlobalIdent,
         generics: Vec<GenericArg>,
+        /// The impl exprs that prove the clauses on the impl.
+        impl_exprs: Vec<ImplExpr>,
     },
     /// A context-bound clause like `where T: Trait`.
     LocalBound {
@@ -90,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),
 }
@@ -108,8 +120,6 @@ pub struct ImplExpr {
     pub r#trait: Binder<TraitRef>,
     /// The kind of implemention of the root of the tree.
     pub r#impl: ImplExprAtom,
-    /// A list of `ImplExpr`s required to fully specify the trait references in `impl`.
-    pub args: Vec<ImplExpr>,
 }
 
 /// Given a clause `clause` in the context of some impl block `impl_did`, susbts correctly `Self`

frontend/exporter/src/traits/resolution.rs

@@ -49,6 +49,8 @@ pub enum ImplExprAtom<'tcx> {
     Concrete {
         def_id: DefId,
         generics: GenericArgsRef<'tcx>,
+        /// The impl exprs that prove the clauses on the impl.
+        impl_exprs: Vec<ImplExpr<'tcx>>,
     },
     /// A context-bound clause like `where T: Trait`.
     LocalBound {
@@ -71,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),
 }
@@ -83,8 +95,6 @@ pub struct ImplExpr<'tcx> {
     pub r#trait: PolyTraitRef<'tcx>,
     /// The kind of implemention of the root of the tree.
     pub r#impl: ImplExprAtom<'tcx>,
-    /// A list of `ImplExpr`s required to fully specify the trait references in `impl`.
-    pub args: Vec<Self>,
 }
 
 /// Items have various predicates in scope. `path_to` uses them as a starting point for trait
@@ -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)| {
@@ -360,23 +370,22 @@ impl<'tcx> PredicateSearcher<'tcx> {
 
         let tcx = self.tcx;
         let impl_source = shallow_resolve_trait_ref(tcx, self.param_env, erased_tref);
-        let nested;
         let atom = match impl_source {
             Ok(ImplSource::UserDefined(ImplSourceUserDefinedData {
                 impl_def_id,
                 args: generics,
                 ..
             })) => {
                 // Resolve the predicates required by the impl.
-                nested = 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,
+                    impl_exprs,
                 }
             }
             Ok(ImplSource::Param(_)) => {
-                // Mentioning a local clause requires no extra predicates to hold.
-                nested = vec![];
                 match self.resolve_local(erased_tref.upcast(self.tcx), warn)? {
                     Some(candidate) => {
                         let path = candidate.path;
@@ -402,17 +411,45 @@ impl<'tcx> PredicateSearcher<'tcx> {
                     }
                 }
             }
-            Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => {
-                nested = vec![];
-                ImplExprAtom::Dyn
-            }
+            Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn,
             Ok(ImplSource::Builtin(_, _)) => {
-                // Builtin impls currently don't need nested predicates.
-                nested = vec![];
-                ImplExprAtom::Builtin { r#trait: *tref }
+                // 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) => {
-                nested = vec![];
                 let msg = format!(
                     "Could not find a clause for `{tref:?}` in the current context: `{e:?}`"
                 );
@@ -423,21 +460,45 @@ impl<'tcx> PredicateSearcher<'tcx> {
 
         Ok(ImplExpr {
             r#impl: atom,
-            args: nested,
             r#trait: *tref,
         })
     }
 
     /// 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);