Only ImplExprAtom::Concrete needs nested ImplExprs

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 }

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 {
@@ -108,8 +110,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 {
@@ -83,8 +85,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
@@ -360,23 +360,21 @@ 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_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 +400,9 @@ impl<'tcx> PredicateSearcher<'tcx> {
                     }
                 }
             }
-            Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => {
-                nested = vec![];
-                ImplExprAtom::Dyn
-            }
-            Ok(ImplSource::Builtin(_, _)) => {
-                // Builtin impls currently don't need nested predicates.
-                nested = vec![];
-                ImplExprAtom::Builtin { r#trait: *tref }
-            }
+            Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn,
+            Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref },
             Err(e) => {
-                nested = vec![];
                 let msg = format!(
                     "Could not find a clause for `{tref:?}` in the current context: `{e:?}`"
                 );
@@ -423,7 +413,6 @@ impl<'tcx> PredicateSearcher<'tcx> {
 
         Ok(ImplExpr {
             r#impl: atom,
-            args: nested,
             r#trait: *tref,
         })
     }