Skip to content

Commit e856e21

Browse files
borsbors
committed
Auto merge of #795 - lowr:fix/clauses-for-assoc-placeholders, r=jackh726
Generate clauses for placeholder associated types Currently, we don't generate clauses for placeholder associated types (`TyKind::AssociatedType`) except for some `FromEnv`s. This leads to `NoSolution` for goals like `(IntoIterator::IntoIter)<Opaque>: Iterator` where `Opaque = impl IntoIterator`. For every associated type in a trait definition ```rust trait Foo { type Assoc<'a, T>: Bar<U = Ty> where WC; } ``` chalk with this patch generates ```rust forall<Self, 'a, T> { Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC. AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC. } ``` To be honest, I'm not entirely sure if `AssociatedTyDatum::to_program_clauses()` is the best place to generate those clauses in, but analogous clauses for placeholder opaque types are generated in `OpaqueTyDatum::to_program_clauses()`, which I modeled after. Spotted in rust-lang/rust-analyzer#14680.
2 parents 88fd1c2 + 52b52cf commit e856e21

File tree

3 files changed

+99
-10
lines changed

3 files changed

+99
-10
lines changed

‎chalk-solve/src/clauses.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -440,6 +440,11 @@ pub fn program_clauses_that_could_match<I: Interner>(
440440
.to_program_clauses(builder, environment);
441441
}
442442

443+
TyKind::AssociatedType(assoc_ty_id, _) => {
444+
db.associated_ty_data(*assoc_ty_id)
445+
.to_program_clauses(builder, environment);
446+
}
447+
443448
TyKind::Dyn(_) => {
444449
// If the self type is a `dyn trait` type, generate program-clauses
445450
// that indicates that it implements its own traits.
@@ -519,6 +524,10 @@ pub fn program_clauses_that_could_match<I: Interner>(
519524
db.opaque_ty_data(*opaque_ty_id)
520525
.to_program_clauses(builder, environment);
521526
}
527+
TyKind::AssociatedType(assoc_ty_id, _) => {
528+
db.associated_ty_data(*assoc_ty_id)
529+
.to_program_clauses(builder, environment);
530+
}
522531
// If the self type is a `dyn trait` type, generate program-clauses
523532
// for any associated type bindings it contains.
524533
// FIXME: see the fixme for the analogous code for Implemented goals.

‎chalk-solve/src/clauses/program_clauses.rs

Lines changed: 43 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -768,6 +768,24 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
768768
/// `AliasEq` to fallback *or* normalize it. So instead we
769769
/// handle this kind of reasoning through the `FromEnv` predicate.
770770
///
771+
/// Another set of clauses we generate for each associated type is about placeholder associated
772+
/// types (i.e. `TyKind::AssociatedType`). Given
773+
///
774+
/// ```notrust
775+
/// trait Foo {
776+
/// type Assoc<'a, T>: Bar<U = Ty> where WC;
777+
/// }
778+
/// ```
779+
///
780+
/// we generate
781+
///
782+
/// ```notrust
783+
/// forall<Self, 'a, T> {
784+
/// Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
785+
/// AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
786+
/// }
787+
/// ```
788+
///
771789
/// We also generate rules specific to WF requirements and implied bounds:
772790
///
773791
/// ```notrust
@@ -818,11 +836,11 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
818836

819837
// Construct an application from the projection. So if we have `<T as Iterator>::Item`,
820838
// we would produce `(Iterator::Item)<T>`.
821-
let ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
839+
let placeholder_ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
822840

823841
let projection_eq = AliasEq {
824842
alias: AliasTy::Projection(projection.clone()),
825-
ty: ty.clone(),
843+
ty: placeholder_ty.clone(),
826844
};
827845

828846
// Fallback rule. The solver uses this to move between the projection
@@ -839,7 +857,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
839857
// WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC).
840858
// }
841859
builder.push_clause(
842-
WellFormed::Ty(ty.clone()),
860+
WellFormed::Ty(placeholder_ty.clone()),
843861
iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner))
844862
.chain(
845863
where_clauses
@@ -856,7 +874,10 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
856874
// forall<Self> {
857875
// FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
858876
// }
859-
builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env()));
877+
builder.push_clause(
878+
FromEnv::Trait(trait_ref.clone()),
879+
Some(placeholder_ty.from_env()),
880+
);
860881

861882
// Reverse rule for where clauses.
862883
//
@@ -869,18 +890,18 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
869890
builder.push_binders(qwc.clone(), |builder, wc| {
870891
builder.push_clause(
871892
wc.into_from_env_goal(interner),
872-
Some(FromEnv::Ty(ty.clone())),
893+
Some(FromEnv::Ty(placeholder_ty.clone())),
873894
);
874895
});
875896
}
876897

877-
// Reverse rule for implied bounds.
878-
//
879-
// forall<Self> {
880-
// FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
881-
// }
882898
for quantified_bound in bounds {
883899
builder.push_binders(quantified_bound, |builder, bound| {
900+
// Reverse rule for implied bounds.
901+
//
902+
// forall<Self> {
903+
// FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
904+
// }
884905
for wc in bound.into_where_clauses(interner, projection_ty.clone()) {
885906
builder.push_clause(
886907
wc.into_from_env_goal(interner),
@@ -890,6 +911,18 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
890911
.chain(where_clauses.iter().cloned().casted(interner)),
891912
);
892913
}
914+
915+
// Rules for the corresponding placeholder type.
916+
//
917+
// When `Foo::Assoc` has a bound `type Assoc: Trait<T = Ty>`, we generate:
918+
//
919+
// forall<Self> {
920+
// Implemented((Foo::Assoc)<Self>: Trait) :- WC
921+
// AliasEq(<(Foo::Assoc)<Self> as Trait>::T = Ty) :- WC
922+
// }
923+
for wc in bound.into_where_clauses(interner, placeholder_ty.clone()) {
924+
builder.push_clause(wc, where_clauses.iter().cloned());
925+
}
893926
});
894927
}
895928

‎tests/test/projection.rs

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1226,3 +1226,50 @@ fn nested_proj_eq_nested_proj_should_flounder() {
12261226
}
12271227
}
12281228
}
1229+
1230+
#[test]
1231+
fn clauses_for_placeholder_projection_types() {
1232+
test! {
1233+
program {
1234+
trait Iterator { type Item; }
1235+
trait IntoIterator {
1236+
type Item;
1237+
type IntoIter: Iterator<Item = <Self as IntoIterator>::Item>;
1238+
}
1239+
1240+
struct Vec<T> { }
1241+
impl<T> IntoIterator for Vec<T> {
1242+
type Item = T;
1243+
type IntoIter = Iter<T>;
1244+
}
1245+
1246+
struct Iter<T> { }
1247+
impl<T> Iterator for Iter<T> {
1248+
type Item = T;
1249+
}
1250+
1251+
opaque type Opaque<T>: IntoIterator<Item = T> = Vec<T>;
1252+
}
1253+
1254+
goal {
1255+
forall<T> {
1256+
<Opaque<T> as IntoIterator>::IntoIter: Iterator
1257+
}
1258+
} yields {
1259+
expect![[r#"Unique"#]]
1260+
}
1261+
1262+
goal {
1263+
forall<T> {
1264+
exists<U> {
1265+
<<Opaque<T> as IntoIterator>::IntoIter as Iterator>::Item = U
1266+
}
1267+
}
1268+
} yields[SolverChoice::slg_default()] {
1269+
// FIXME: chalk#234?
1270+
expect![[r#"Ambiguous; no inference guidance"#]]
1271+
} yields[SolverChoice::recursive_default()] {
1272+
expect![[r#"Unique; substitution [?0 := !1_0]"#]]
1273+
}
1274+
}
1275+
}

0 commit comments

Comments
 (0)