Clean up program_clauses_that_could_match

- Use a single match on the TyKind for Implemented goals
- Normalize TyKind::Alias self types

Author: matthewjasper

chalk-ir/src/lib.rs

@@ -1346,12 +1346,7 @@ impl<I: Interner> AliasTy<I> {
     /// Gets the type parameters of the `Self` type in this alias type.
     pub fn self_type_parameter(&self, interner: &I) -> Ty<I> {
         match self {
-            AliasTy::Projection(projection_ty) => projection_ty
-                .substitution
-                .iter(interner)
-                .find_map(move |p| p.ty(interner))
-                .unwrap()
-                .clone(),
+            AliasTy::Projection(projection_ty) => projection_ty.self_type_parameter(interner),
             _ => todo!(),
         }
     }
@@ -1368,6 +1363,17 @@ pub struct ProjectionTy<I: Interner> {
 
 impl<I: Interner> Copy for ProjectionTy<I> where I::InternedSubstitution: Copy {}
 
+impl<I: Interner> ProjectionTy<I> {
+    /// Gets the type parameters of the `Self` type in this alias type.
+    pub fn self_type_parameter(&self, interner: &I) -> Ty<I> {
+        self.substitution
+            .iter(interner)
+            .find_map(move |p| p.ty(interner))
+            .unwrap()
+            .clone()
+    }
+}
+
 /// An opaque type `opaque type T<..>: Trait = HiddenTy`.
 #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]
 pub struct OpaqueTy<I: Interner> {

chalk-solve/src/clauses.rs

@@ -389,20 +389,56 @@ fn program_clauses_that_could_match<I: Interner>(
 
     match goal {
         DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => {
-            let trait_id = trait_ref.trait_id;
+            let self_ty = trait_ref.self_type_parameter(interner);
 
+            let trait_id = trait_ref.trait_id;
             let trait_datum = db.trait_datum(trait_id);
 
-            if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() {
-                let self_ty = trait_ref.self_type_parameter(interner);
+            match self_ty.kind(interner) {
+                TyKind::Alias(alias) => {
+                    // An alias could normalize to anything, including `dyn trait`
+                    // or an opaque type, so push a clause that asks for the
+                    // self type to be normalized and return.
+                    push_alias_implemented_clause(builder, trait_ref, alias);
+                    return Ok(clauses);
+                }
 
-                if let TyKind::Alias(AliasTy::Opaque(opaque_ty)) = self_ty.kind(interner) {
-                    if trait_datum.is_auto_trait() {
-                        push_auto_trait_impls_opaque(builder, trait_id, opaque_ty.opaque_ty_id)
+                _ if self_ty.is_general_var(interner, binders) => {
+                    if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() {
+                        return Err(Floundered);
                     }
-                } else if self_ty.is_general_var(interner, binders) {
-                    return Err(Floundered);
                 }
+
+                TyKind::OpaqueType(opaque_ty_id, _) => {
+                    db.opaque_ty_data(*opaque_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.
+                    // FIXME: This is presently rather wasteful, in that we don't check that the
+                    // these program clauses we are generating are actually relevant to the goal
+                    // `goal` that we are actually *trying* to prove (though there is some later
+                    // code that will screen out irrelevant stuff).
+                    //
+                    // In other words, if we were trying to prove `Implemented(dyn
+                    // Fn(&u8): Clone)`, we would still generate two clauses that are
+                    // totally irrelevant to that goal, because they let us prove other
+                    // things but not `Clone`.
+                    dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone())
+                }
+
+                // We don't actually do anything here, but we need to record the types when logging
+                TyKind::Adt(adt_id, _) => {
+                    let _ = db.adt_datum(*adt_id);
+                }
+
+                TyKind::FnDef(fn_def_id, _) => {
+                    let _ = db.fn_def_datum(*fn_def_id);
+                }
+
+                _ => {}
             }
 
             // This is needed for the coherence related impls, as well
@@ -429,42 +465,6 @@ fn program_clauses_that_could_match<I: Interner>(
                 })?;
             }
 
-            // If the self type is a `dyn trait` type, generate program-clauses
-            // that indicates that it implements its own traits.
-            // FIXME: This is presently rather wasteful, in that we don't check that the
-            // these program clauses we are generating are actually relevant to the goal
-            // `goal` that we are actually *trying* to prove (though there is some later
-            // code that will screen out irrelevant stuff).
-            //
-            // In other words, if we were trying to prove `Implemented(dyn
-            // Fn(&u8): Clone)`, we would still generate two clauses that are
-            // totally irrelevant to that goal, because they let us prove other
-            // things but not `Clone`.
-            let self_ty = trait_ref.self_type_parameter(interner);
-            if let TyKind::Dyn(_) = self_ty.kind(interner) {
-                dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone())
-            }
-
-            match self_ty.kind(interner) {
-                TyKind::OpaqueType(opaque_ty_id, _)
-                | TyKind::Alias(AliasTy::Opaque(OpaqueTy { opaque_ty_id, .. })) => {
-                    db.opaque_ty_data(*opaque_ty_id)
-                        .to_program_clauses(builder, environment);
-                }
-                _ => {}
-            }
-
-            // We don't actually do anything here, but we need to record the types it when logging
-            match self_ty.kind(interner) {
-                TyKind::Adt(adt_id, _) => {
-                    let _ = db.adt_datum(*adt_id);
-                }
-                TyKind::FnDef(fn_def_id, _) => {
-                    let _ = db.fn_def_datum(*fn_def_id);
-                }
-                _ => {}
-            }
-
             if let Some(well_known) = trait_datum.well_known {
                 builtin_traits::add_builtin_program_clauses(
                     db, builder, well_known, trait_ref, binders,
@@ -478,21 +478,26 @@ fn program_clauses_that_could_match<I: Interner>(
                     .self_type_parameter(interner);
 
                 match trait_self_ty.kind(interner) {
-                    TyKind::OpaqueType(opaque_ty_id, _)
-                    | TyKind::Alias(AliasTy::Opaque(OpaqueTy { opaque_ty_id, .. })) => {
+                    TyKind::Alias(alias) => {
+                        // An alias could normalize to anything, including an
+                        // opaque type, so push a clause that asks for the self
+                        // type to be normalized and return.
+                        push_alias_alias_eq_clause(builder, proj, &alias_eq.ty, alias);
+                        return Ok(clauses);
+                    }
+                    TyKind::OpaqueType(opaque_ty_id, _) => {
                         db.opaque_ty_data(*opaque_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.
+                    TyKind::Dyn(_) => {
+                        dyn_ty::build_dyn_self_ty_clauses(db, builder, trait_self_ty.clone())
+                    }
                     _ => {}
                 }
 
-                // 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.
-                if let TyKind::Dyn(_) = trait_self_ty.kind(interner) {
-                    dyn_ty::build_dyn_self_ty_clauses(db, builder, trait_self_ty.clone())
-                }
-
                 db.associated_ty_data(proj.associated_ty_id)
                     .to_program_clauses(builder, environment)
             }
@@ -708,6 +713,97 @@ fn push_program_clauses_for_associated_type_values_in_impls_of<I: Interner>(
     }
 }
 
+fn push_alias_implemented_clause<I: Interner>(
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    alias: &AliasTy<I>,
+) {
+    let interner = builder.interner();
+    assert_eq!(
+        *trait_ref.self_type_parameter(interner).kind(interner),
+        TyKind::Alias(alias.clone())
+    );
+
+    let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
+
+    // forall<..., T> {
+    //      <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
+    // }
+    builder.push_binders(&binders, |builder, bound_var| {
+        let fresh_self_subst = Substitution::from_iter(
+            interner,
+            std::iter::once(bound_var.clone().cast(interner)).chain(
+                trait_ref.substitution.as_slice(interner)[1..]
+                    .iter()
+                    .cloned(),
+            ),
+        );
+        let fresh_self_trait_ref = TraitRef {
+            trait_id: trait_ref.trait_id,
+            substitution: fresh_self_subst,
+        };
+        builder.push_clause(
+            DomainGoal::Holds(WhereClause::Implemented(trait_ref.clone())),
+            &[
+                DomainGoal::Holds(WhereClause::Implemented(fresh_self_trait_ref)),
+                DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
+                    alias: alias.clone(),
+                    ty: bound_var,
+                })),
+            ],
+        );
+    });
+}
+
+fn push_alias_alias_eq_clause<I: Interner>(
+    builder: &mut ClauseBuilder<'_, I>,
+    projection_ty: &ProjectionTy<I>,
+    ty: &Ty<I>,
+    alias: &AliasTy<I>,
+) {
+    let interner = builder.interner();
+    assert_eq!(
+        *projection_ty.self_type_parameter(interner).kind(interner),
+        TyKind::Alias(alias.clone())
+    );
+
+    let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
+
+    // forall<..., T> {
+    //      <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
+    // }
+    builder.push_binders(&binders, |builder, bound_var| {
+        let fresh_self_subst = Substitution::from_iter(
+            interner,
+            std::iter::once(bound_var.clone().cast(interner)).chain(
+                projection_ty.substitution.as_slice(interner)[1..]
+                    .iter()
+                    .cloned(),
+            ),
+        );
+        let fresh_alias = AliasTy::Projection(ProjectionTy {
+            associated_ty_id: projection_ty.associated_ty_id,
+            substitution: fresh_self_subst,
+        });
+        builder.push_clause(
+            DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
+                alias: AliasTy::Projection(projection_ty.clone()),
+                ty: ty.clone(),
+            })),
+            &[
+                DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
+                    alias: fresh_alias,
+                    ty: ty.clone(),
+                })),
+                DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
+                    alias: alias.clone(),
+                    ty: bound_var,
+                })),
+            ],
+        );
+    });
+}
+
 /// Examine `T` and push clauses that may be relevant to proving the
 /// following sorts of goals (and maybe others):
 ///

tests/test/projection.rs

@@ -1043,3 +1043,67 @@ fn guidance_for_projection_on_flounder() {
         }
     }
 }
+
+#[test]
+fn projection_to_dyn() {
+    test! {
+        program {
+            trait AsDyn {
+                type Dyn;
+            }
+
+            #[object_safe]
+            trait Debug {}
+
+            impl AsDyn for () {
+                type Dyn = dyn Debug + 'static;
+            }
+        }
+
+        goal {
+            <() as AsDyn>::Dyn: Debug
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn projection_to_opaque() {
+    test! {
+        program {
+            #[non_enumerable]
+            trait Debug {
+                type Output;
+            }
+
+            impl Debug for () {
+                type Output = ();
+            }
+
+            opaque type OpaqueDebug: Debug<Output = ()> = ();
+
+            struct A {}
+
+            trait AsProj {
+                type Proj;
+            }
+
+            impl AsProj for A {
+                type Proj = OpaqueDebug;
+            }
+        }
+
+        goal {
+            <A as AsProj>::Proj: Debug
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            <<A as AsProj>::Proj as Debug>::Output = ()
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}