Skip to content

Commit

Permalink
Auto merge of #795 - lowr:fix/clauses-for-assoc-placeholders, r=jackh726
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@bors
bors committed Jun 14, 2023
2 parents 88fd1c2 + 52b52cf commit e856e21
Show file tree
Hide file tree
Showing 3 changed files with 99 additions and 10 deletions.
9 changes: 9 additions & 0 deletions chalk-solve/src/clauses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
53 changes: 43 additions & 10 deletions chalk-solve/src/clauses/program_clauses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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.
//
Expand All @@ -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),
Expand All @@ -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());
}
});
}

Expand Down
47 changes: 47 additions & 0 deletions tests/test/projection.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]"#]]
}
}
}

0 comments on commit e856e21

Please sign in to comment.