From 5ffee10b889be5fa05a2c37fa88b98162e603934 Mon Sep 17 00:00:00 2001 From: Ryo Yoshida Date: Sun, 30 Apr 2023 22:32:20 +0900 Subject: [PATCH] Generate clauses for placeholder associated types --- chalk-solve/src/clauses.rs | 9 ++++ chalk-solve/src/clauses/program_clauses.rs | 53 ++++++++++++++++++---- tests/test/projection.rs | 47 +++++++++++++++++++ 3 files changed, 99 insertions(+), 10 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index a0ede39df7c..a0a23597e06 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -440,6 +440,11 @@ pub fn program_clauses_that_could_match( .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. @@ -524,6 +529,10 @@ pub fn program_clauses_that_could_match( 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. diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 19811ff8b30..e1fec223d06 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -768,6 +768,24 @@ impl ToProgramClauses for AssociatedTyDatum { /// `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 where WC; + /// } + /// ``` + /// + /// we generate + /// + /// ```notrust + /// forall { + /// Implemented((Foo::Assoc<'a, T>): Bar) :- WC. + /// AliasEq(<<(Foo::Assoc<'a, T>)> as Bar>::U = Ty) :- WC. + /// } + /// ``` + /// /// We also generate rules specific to WF requirements and implied bounds: /// /// ```notrust @@ -818,11 +836,11 @@ impl ToProgramClauses for AssociatedTyDatum { // Construct an application from the projection. So if we have `::Item`, // we would produce `(Iterator::Item)`. - 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 ToProgramClauses for AssociatedTyDatum { // WellFormed((Foo::Assoc)) :- 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::>(interner)) .chain( where_clauses @@ -856,7 +874,10 @@ impl ToProgramClauses for AssociatedTyDatum { // forall { // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)). // } - 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 ToProgramClauses for AssociatedTyDatum { 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 { - // FromEnv(::Assoc: Bounds) :- FromEnv(Self: Foo), WC - // } for quantified_bound in bounds { builder.push_binders(quantified_bound, |builder, bound| { + // Reverse rule for implied bounds. + // + // forall { + // FromEnv(::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 ToProgramClauses for AssociatedTyDatum { .chain(where_clauses.iter().cloned().casted(interner)), ); } + + // Rules for the corresponding placeholder type. + // + // When `Foo::Assoc` has a bound `type Assoc: Trait`, we generate: + // + // forall { + // Implemented((Foo::Assoc): Trait) :- WC + // AliasEq(<(Foo::Assoc) as Trait>::T = Ty) :- WC + // } + for wc in bound.into_where_clauses(interner, placeholder_ty.clone()) { + builder.push_clause(wc, where_clauses.iter().cloned()); + } }); } diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 021aba29972..049b760229f 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -1158,3 +1158,50 @@ fn projection_to_opaque() { } } } + +#[test] +fn clauses_for_placeholder_projection_types() { + test! { + program { + trait Iterator { type Item; } + trait IntoIterator { + type Item; + type IntoIter: Iterator::Item>; + } + + struct Vec { } + impl IntoIterator for Vec { + type Item = T; + type IntoIter = Iter; + } + + struct Iter { } + impl Iterator for Iter { + type Item = T; + } + + opaque type Opaque: IntoIterator = Vec; + } + + goal { + forall { + as IntoIterator>::IntoIter: Iterator + } + } yields { + expect![[r#"Unique"#]] + } + + goal { + forall { + exists { + < 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]"#]] + } + } +}