Skip to content

stepping into impls for normalization is unproductive #139900

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 17, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 13 additions & 8 deletions compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -286,18 +286,23 @@ where
// fixing it may cause inference breakage or introduce ambiguity.
GoalSource::Misc => PathKind::Unknown,
GoalSource::NormalizeGoal(path_kind) => path_kind,
GoalSource::ImplWhereBound => {
GoalSource::ImplWhereBound => match self.current_goal_kind {
// We currently only consider a cycle coinductive if it steps
// into a where-clause of a coinductive trait.
CurrentGoalKind::CoinductiveTrait => PathKind::Coinductive,
// While normalizing via an impl does step into a where-clause of
// an impl, accessing the associated item immediately steps out of
// it again. This means cycles/recursive calls are not guarded
// by impls used for normalization.
//
// See tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.rs
// for how this can go wrong.
CurrentGoalKind::NormalizesTo => PathKind::Inductive,
// We probably want to make all traits coinductive in the future,
// so we treat cycles involving their where-clauses as ambiguous.
if let CurrentGoalKind::CoinductiveTrait = self.current_goal_kind {
PathKind::Coinductive
} else {
PathKind::Unknown
}
}
// so we treat cycles involving where-clauses of not-yet coinductive
// traits as ambiguous for now.
CurrentGoalKind::Misc => PathKind::Unknown,
},
// Relating types is always unproductive. If we were to map proof trees to
// corecursive functions as explained in #136824, relating types never
// introduces a constructor which could cause the recursion to be guarded.
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@ check-pass

// Regression test for trait-system-refactor-initiative#176.
//
// Normalizing `<Vec<T> as IntoIterator>::IntoIter` has two candidates
// inside of the function:
// - `impl<T> IntoIterator for Vec<T>` which trivially applies
// - `impl<I: Iterator> IntoIterator for I`
// - requires `Vec<T>: Iterator`
// - where-clause requires `<Vec<T> as IntoIterator>::IntoIter eq Vec<T>`
// - normalize `<Vec<T> as IntoIterator>::IntoIter` again, cycle
//
// We need to treat this cycle as an error to be able to use the actual impl.

fn test<T>()
where
<Vec<T> as IntoIterator>::IntoIter: Iterator,
{
}

fn main() {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:41:1
|
LL | / fn generic<T>()
LL | | where
LL | | <Foo as Trait<T>>::Assoc: Bound,
| |____________________________________^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required for `Foo` to implement `Trait<T>`
--> $DIR/normalizes-to-is-not-productive.rs:24:19
|
LL | impl<T: Bound, U> Trait<U> for T {
| ----- ^^^^^^^^ ^
| |
| unsatisfied trait bound introduced here

error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:41:4
|
LL | fn generic<T>()
| ^^^^^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required for `Foo` to implement `Trait<T>`
--> $DIR/normalizes-to-is-not-productive.rs:24:19
|
LL | impl<T: Bound, U> Trait<U> for T {
| ----- ^^^^^^^^ ^
| |
| unsatisfied trait bound introduced here

error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:48:19
|
LL | impls_bound::<Foo>();
| ^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required by a bound in `impls_bound`
--> $DIR/normalizes-to-is-not-productive.rs:28:19
|
LL | fn impls_bound<T: Bound>() {
| ^^^^^ required by this bound in `impls_bound`

error: aborting due to 3 previous errors

For more information about this error, try `rustc --explain E0277`.
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:43:31
|
LL | <Foo as Trait<T>>::Assoc: Bound,
| ^^^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required for `Foo` to implement `Trait<T>`
--> $DIR/normalizes-to-is-not-productive.rs:24:19
|
LL | impl<T: Bound, U> Trait<U> for T {
| ----- ^^^^^^^^ ^
| |
| unsatisfied trait bound introduced here

error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:48:19
|
LL | impls_bound::<Foo>();
| ^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required by a bound in `impls_bound`
--> $DIR/normalizes-to-is-not-productive.rs:28:19
|
LL | fn impls_bound<T: Bound>() {
| ^^^^^ required by this bound in `impls_bound`

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0277`.
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
//@ ignore-compare-mode-next-solver (explicit)
//@ compile-flags: -Znext-solver

// Make sure that stepping into impl where-clauses of `NormalizesTo`
// goals is unproductive. This must not compile, see the inline
// comments.

trait Bound {
fn method();
}
impl Bound for u32 {
fn method() {}
}
trait Trait<T> {
type Assoc: Bound;
}

struct Foo;

impl Trait<u32> for Foo {
type Assoc = u32;
}
impl<T: Bound, U> Trait<U> for T {
type Assoc = T;
}

fn impls_bound<T: Bound>() {
T::method();
}

// The where-clause requires `Foo: Trait<T>` to hold to be wf.
// If stepping into where-clauses during normalization is considered
// to be productive, this would be the case:
//
// - `Foo: Trait<T>`
// - via blanket impls, requires `Foo: Bound`
// - via where-bound, requires `Foo eq <Foo as Trait<T>>::Assoc`
// - normalize `<Foo as Trait<T>>::Assoc`
// - via blanket impl, requires where-clause `Foo: Bound` -> cycle
fn generic<T>()
where
<Foo as Trait<T>>::Assoc: Bound,
//~^ ERROR the trait bound `Foo: Bound` is not satisfied
{
// Requires proving `Foo: Bound` by normalizing
// `<Foo as Trait<T>>::Assoc` to `Foo`.
impls_bound::<Foo>();
//~^ ERROR the trait bound `Foo: Bound` is not satisfied
}
fn main() {
// Requires proving `<Foo as Trait<u32>>::Assoc: Bound`.
// This is trivially true.
generic::<u32>();
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:42:31
|
LL | <Foo as Trait<T>>::Assoc: Bound,
| ^^^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required for `Foo` to implement `Trait<T>`
--> $DIR/normalizes-to-is-not-productive.rs:23:19
|
LL | impl<T: Bound, U> Trait<U> for T {
| ----- ^^^^^^^^ ^
| |
| unsatisfied trait bound introduced here

error[E0277]: the trait bound `Foo: Bound` is not satisfied
--> $DIR/normalizes-to-is-not-productive.rs:47:19
|
LL | impls_bound::<Foo>();
| ^^^ the trait `Bound` is not implemented for `Foo`
|
= help: the trait `Bound` is implemented for `u32`
note: required by a bound in `impls_bound`
--> $DIR/normalizes-to-is-not-productive.rs:27:19
|
LL | fn impls_bound<T: Bound>() {
| ^^^^^ required by this bound in `impls_bound`

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0277`.
Loading