Move substitution into push_binders

Author: detrumi

chalk-integration/src/lowering.rs

@@ -388,9 +388,13 @@ impl LowerProgram for Program {
                             .map(|k| k.lower())
                             .collect::<Vec<_>>();
 
+                        // Introduce the parameters declared on the opaque type definition.
+                        // So if we have `type Foo<P1..Pn> = impl Trait<T1..Tn>`, this would introduce `P1..Pn`
                         let binders = empty_env.in_binders(parameter_kinds, |env| {
                             let hidden_ty = opaque_ty.ty.lower(&env)?;
 
+                            // Introduce a variable to represent the hidden "self type". This will be used in the bounds.
+                            // So the `impl Trait<T1..Tn>` will be lowered to `exists<Self> { Self: Trait<T1..Tn> }`.
                             let bounds: chalk_ir::Binders<Vec<chalk_ir::Binders<_>>> = env
                                 .in_binders(
                                     Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))),
@@ -401,6 +405,7 @@ impl LowerProgram for Program {
                                             .lower(&env1)?
                                             .iter()
                                             .flat_map(|qil| {
+                                                // Instantiate the bounds with the innermost bound variable, which represents Self, as the self type.
                                                 qil.into_where_clauses(
                                                     interner,
                                                     chalk_ir::TyData::BoundVar(BoundVar::new(

chalk-solve/src/clauses/program_clauses.rs

@@ -130,22 +130,22 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
     /// ```
     /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`.
     fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) {
-        let interner = builder.interner();
-        let substitution = builder.substitution_in_scope();
-        let alias = AliasTy::Opaque(OpaqueTy {
-            opaque_ty_id: self.opaque_ty_id,
-            substitution: substitution.clone(),
-        });
+        builder.push_binders(&self.bound, |builder, opaque_ty_bound| {
+            let interner = builder.interner();
+            let substitution = builder.substitution_in_scope();
+            let alias = AliasTy::Opaque(OpaqueTy {
+                opaque_ty_id: self.opaque_ty_id,
+                substitution: substitution.clone(),
+            });
 
-        let alias_ty = Ty::new(
-            interner,
-            ApplicationTy {
-                name: TypeName::OpaqueType(self.opaque_ty_id),
-                substitution,
-            },
-        );
+            let alias_placeholder_ty = Ty::new(
+                interner,
+                ApplicationTy {
+                    name: TypeName::OpaqueType(self.opaque_ty_id),
+                    substitution,
+                },
+            );
 
-        builder.push_binders(&self.bound, |builder, opaque_ty_bound| {
             // AliasEq(T<..> = HiddenTy) :- Reveal.
             builder.push_clause(
                 DomainGoal::Holds(
@@ -162,17 +162,19 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
             builder.push_fact(DomainGoal::Holds(
                 AliasEq {
                     alias: alias.clone(),
-                    ty: alias_ty.clone(),
+                    ty: alias_placeholder_ty.clone(),
                 }
                 .cast(interner),
             ));
 
             for bound in &opaque_ty_bound.bounds {
                 // Implemented(!T<..>: Bound).
-                builder.push_binders(&bound, |builder, bound| {
-                    builder.push_binders(&bound, |builder, bound| {
-                        builder.push_fact(bound.into_well_formed_goal(interner));
-                    });
+                let bound_with_placeholder_ty = bound.substitute(
+                    interner,
+                    &Substitution::from1(interner, alias_placeholder_ty.clone()),
+                );
+                builder.push_binders(&bound_with_placeholder_ty, |builder, bound| {
+                    builder.push_fact(bound.into_well_formed_goal(interner));
                 });
             }
 
@@ -181,7 +183,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
                 builder.push_clause(
                     TraitRef {
                         trait_id: auto_trait_id,
-                        substitution: Substitution::from1(interner, alias_ty.clone()),
+                        substitution: Substitution::from1(interner, alias_placeholder_ty.clone()),
                     },
                     iter::once(TraitRef {
                         trait_id: auto_trait_id,