Generate clauses for placeholder associated types

Author: lowr

chalk-solve/src/clauses.rs

@@ -440,6 +440,11 @@ pub fn program_clauses_that_could_match<I: Interner>(
                         .to_program_clauses(builder, environment);
                 }
 
+                TyKind::AssociatedType(assoc_ty_id, _) => {
+                    db.associated_ty_data(*assoc_ty_id)
+                        .to_program_clauses(builder, environment);
+                }
+
                 TyKind::Dyn(_) => {
                     // If the self type is a `dyn trait` type, generate program-clauses
                     // that indicates that it implements its own traits.
@@ -519,6 +524,10 @@ pub fn program_clauses_that_could_match<I: Interner>(
                         db.opaque_ty_data(*opaque_ty_id)
                             .to_program_clauses(builder, environment);
                     }
+                    TyKind::AssociatedType(assoc_ty_id, _) => {
+                        db.associated_ty_data(*assoc_ty_id)
+                            .to_program_clauses(builder, environment);
+                    }
                     // If the self type is a `dyn trait` type, generate program-clauses
                     // for any associated type bindings it contains.
                     // FIXME: see the fixme for the analogous code for Implemented goals.

chalk-solve/src/clauses/program_clauses.rs

@@ -768,6 +768,24 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
     /// `AliasEq` to fallback *or* normalize it. So instead we
     /// handle this kind of reasoning through the `FromEnv` predicate.
     ///
+    /// Another set of clauses we generate for each associated type is about placeholder associated
+    /// types (i.e. `TyKind::AssociatedType`). Given
+    ///
+    /// ```notrust
+    /// trait Foo {
+    ///     type Assoc<'a, T>: Bar<U = Ty> where WC;
+    /// }
+    /// ```
+    ///
+    /// we generate
+    ///
+    /// ```notrust
+    /// forall<Self, 'a, T> {
+    ///     Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
+    ///     AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
+    /// }
+    /// ```
+    ///
     /// We also generate rules specific to WF requirements and implied bounds:
     ///
     /// ```notrust
@@ -818,11 +836,11 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
 
                 // Construct an application from the projection. So if we have `<T as Iterator>::Item`,
                 // we would produce `(Iterator::Item)<T>`.
-                let ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
+                let placeholder_ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
 
                 let projection_eq = AliasEq {
                     alias: AliasTy::Projection(projection.clone()),
-                    ty: ty.clone(),
+                    ty: placeholder_ty.clone(),
                 };
 
                 // Fallback rule. The solver uses this to move between the projection
@@ -839,7 +857,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
                 //        WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC).
                 //    }
                 builder.push_clause(
-                    WellFormed::Ty(ty.clone()),
+                    WellFormed::Ty(placeholder_ty.clone()),
                     iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner))
                         .chain(
                             where_clauses
@@ -856,7 +874,10 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
                 //    forall<Self> {
                 //        FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
                 //    }
-                builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env()));
+                builder.push_clause(
+                    FromEnv::Trait(trait_ref.clone()),
+                    Some(placeholder_ty.from_env()),
+                );
 
                 // Reverse rule for where clauses.
                 //
@@ -869,18 +890,18 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
                     builder.push_binders(qwc.clone(), |builder, wc| {
                         builder.push_clause(
                             wc.into_from_env_goal(interner),
-                            Some(FromEnv::Ty(ty.clone())),
+                            Some(FromEnv::Ty(placeholder_ty.clone())),
                         );
                     });
                 }
 
-                // Reverse rule for implied bounds.
-                //
-                //    forall<Self> {
-                //        FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
-                //    }
                 for quantified_bound in bounds {
                     builder.push_binders(quantified_bound, |builder, bound| {
+                        // Reverse rule for implied bounds.
+                        //
+                        //    forall<Self> {
+                        //        FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
+                        //    }
                         for wc in bound.into_where_clauses(interner, projection_ty.clone()) {
                             builder.push_clause(
                                 wc.into_from_env_goal(interner),
@@ -890,6 +911,18 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
                                 .chain(where_clauses.iter().cloned().casted(interner)),
                             );
                         }
+
+                        // Rules for the corresponding placeholder type.
+                        //
+                        // When `Foo::Assoc` has a bound `type Assoc: Trait<T = Ty>`, we generate:
+                        //
+                        //    forall<Self> {
+                        //        Implemented((Foo::Assoc)<Self>: Trait) :- WC
+                        //        AliasEq(<(Foo::Assoc)<Self> as Trait>::T = Ty) :- WC
+                        //    }
+                        for wc in bound.into_where_clauses(interner, placeholder_ty.clone()) {
+                            builder.push_clause(wc, where_clauses.iter().cloned());
+                        }
                     });
                 }
 

tests/test/projection.rs

@@ -1226,3 +1226,50 @@ fn nested_proj_eq_nested_proj_should_flounder() {
         }
     }
 }
+
+#[test]
+fn clauses_for_placeholder_projection_types() {
+    test! {
+        program {
+            trait Iterator { type Item; }
+            trait IntoIterator {
+                type Item;
+                type IntoIter: Iterator<Item = <Self as IntoIterator>::Item>;
+            }
+
+            struct Vec<T> { }
+            impl<T> IntoIterator for Vec<T> {
+                type Item = T;
+                type IntoIter = Iter<T>;
+            }
+
+            struct Iter<T> { }
+            impl<T> Iterator for Iter<T> {
+                type Item = T;
+            }
+
+            opaque type Opaque<T>: IntoIterator<Item = T> = Vec<T>;
+        }
+
+        goal {
+            forall<T> {
+                <Opaque<T> as IntoIterator>::IntoIter: Iterator
+            }
+        } yields {
+            expect![[r#"Unique"#]]
+        }
+
+        goal {
+            forall<T> {
+                exists<U> {
+                    <<Opaque<T> as IntoIterator>::IntoIter as Iterator>::Item = U
+                }
+            }
+        } yields[SolverChoice::slg_default()] {
+            // FIXME: chalk#234?
+            expect![[r#"Ambiguous; no inference guidance"#]]
+        } yields[SolverChoice::recursive_default()] {
+            expect![[r#"Unique; substitution [?0 := !1_0]"#]]
+        }
+    }
+}