Skip to content

Commit 9e0be6c

Browse files
matthiaskrgrmatthiaskrgr
authored
Rollup merge of rust-lang#139900 - lcnr:normalizes-to-where-bounds-unproductive, r=compiler-errors
stepping into impls for normalization is unproductive See the inline comment. This builds on the reasoning from rust-lang#136824 (https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5). Fixes rust-lang/trait-system-refactor-initiative#176. Looking at the end of the gist: > The only ways to project out of a constructor are the following: > - accessing an associated item, either its type or its item bounds > - accessing super predicates Detecting cases where we accessing the type of an associated item is easy, it's simply when we normalize. I don't yet know how to detect whether we step out of an impl by accessing item bounds. Once we also detect these cases we should be able to soundly support arbitrary coinductive traits. Luckily this does not matter for this PR :> r? `@compiler-errors` cc `@nikomatsakis`
2 parents 848ec58 + 48e119e commit 9e0be6c

File tree

6 files changed

+201
-8
lines changed

6 files changed

+201
-8
lines changed

‎compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -286,18 +286,23 @@ where
286286
// fixing it may cause inference breakage or introduce ambiguity.
287287
GoalSource::Misc => PathKind::Unknown,
288288
GoalSource::NormalizeGoal(path_kind) => path_kind,
289-
GoalSource::ImplWhereBound => {
289+
GoalSource::ImplWhereBound => match self.current_goal_kind {
290290
// We currently only consider a cycle coinductive if it steps
291291
// into a where-clause of a coinductive trait.
292+
CurrentGoalKind::CoinductiveTrait => PathKind::Coinductive,
293+
// While normalizing via an impl does step into a where-clause of
294+
// an impl, accessing the associated item immediately steps out of
295+
// it again. This means cycles/recursive calls are not guarded
296+
// by impls used for normalization.
292297
//
298+
// See tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.rs
299+
// for how this can go wrong.
300+
CurrentGoalKind::NormalizesTo => PathKind::Inductive,
293301
// We probably want to make all traits coinductive in the future,
294-
// so we treat cycles involving their where-clauses as ambiguous.
295-
if let CurrentGoalKind::CoinductiveTrait = self.current_goal_kind {
296-
PathKind::Coinductive
297-
} else {
298-
PathKind::Unknown
299-
}
300-
}
302+
// so we treat cycles involving where-clauses of not-yet coinductive
303+
// traits as ambiguous for now.
304+
CurrentGoalKind::Misc => PathKind::Unknown,
305+
},
301306
// Relating types is always unproductive. If we were to map proof trees to
302307
// corecursive functions as explained in #136824, relating types never
303308
// introduces a constructor which could cause the recursion to be guarded.

‎tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive-2.rs‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
//@ revisions: current next
2+
//@ ignore-compare-mode-next-solver (explicit revisions)
3+
//@[next] compile-flags: -Znext-solver
4+
//@ check-pass
5+
6+
// Regression test for trait-system-refactor-initiative#176.
7+
//
8+
// Normalizing `<Vec<T> as IntoIterator>::IntoIter` has two candidates
9+
// inside of the function:
10+
// - `impl<T> IntoIterator for Vec<T>` which trivially applies
11+
// - `impl<I: Iterator> IntoIterator for I`
12+
// - requires `Vec<T>: Iterator`
13+
// - where-clause requires `<Vec<T> as IntoIterator>::IntoIter eq Vec<T>`
14+
// - normalize `<Vec<T> as IntoIterator>::IntoIter` again, cycle
15+
//
16+
// We need to treat this cycle as an error to be able to use the actual impl.
17+
18+
fn test<T>()
19+
where
20+
<Vec<T> as IntoIterator>::IntoIter: Iterator,
21+
{
22+
}
23+
24+
fn main() {}

‎tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.current.stderr‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
2+
--> $DIR/normalizes-to-is-not-productive.rs:41:1
3+
|
4+
LL | / fn generic<T>()
5+
LL | | where
6+
LL | | <Foo as Trait<T>>::Assoc: Bound,
7+
| |____________________________________^ the trait `Bound` is not implemented for `Foo`
8+
|
9+
= help: the trait `Bound` is implemented for `u32`
10+
note: required for `Foo` to implement `Trait<T>`
11+
--> $DIR/normalizes-to-is-not-productive.rs:24:19
12+
|
13+
LL | impl<T: Bound, U> Trait<U> for T {
14+
| ----- ^^^^^^^^ ^
15+
| |
16+
| unsatisfied trait bound introduced here
17+
18+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
19+
--> $DIR/normalizes-to-is-not-productive.rs:41:4
20+
|
21+
LL | fn generic<T>()
22+
| ^^^^^^^ the trait `Bound` is not implemented for `Foo`
23+
|
24+
= help: the trait `Bound` is implemented for `u32`
25+
note: required for `Foo` to implement `Trait<T>`
26+
--> $DIR/normalizes-to-is-not-productive.rs:24:19
27+
|
28+
LL | impl<T: Bound, U> Trait<U> for T {
29+
| ----- ^^^^^^^^ ^
30+
| |
31+
| unsatisfied trait bound introduced here
32+
33+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
34+
--> $DIR/normalizes-to-is-not-productive.rs:48:19
35+
|
36+
LL | impls_bound::<Foo>();
37+
| ^^^ the trait `Bound` is not implemented for `Foo`
38+
|
39+
= help: the trait `Bound` is implemented for `u32`
40+
note: required by a bound in `impls_bound`
41+
--> $DIR/normalizes-to-is-not-productive.rs:28:19
42+
|
43+
LL | fn impls_bound<T: Bound>() {
44+
| ^^^^^ required by this bound in `impls_bound`
45+
46+
error: aborting due to 3 previous errors
47+
48+
For more information about this error, try `rustc --explain E0277`.

‎tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.next.stderr‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
2+
--> $DIR/normalizes-to-is-not-productive.rs:43:31
3+
|
4+
LL | <Foo as Trait<T>>::Assoc: Bound,
5+
| ^^^^^ the trait `Bound` is not implemented for `Foo`
6+
|
7+
= help: the trait `Bound` is implemented for `u32`
8+
note: required for `Foo` to implement `Trait<T>`
9+
--> $DIR/normalizes-to-is-not-productive.rs:24:19
10+
|
11+
LL | impl<T: Bound, U> Trait<U> for T {
12+
| ----- ^^^^^^^^ ^
13+
| |
14+
| unsatisfied trait bound introduced here
15+
16+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
17+
--> $DIR/normalizes-to-is-not-productive.rs:48:19
18+
|
19+
LL | impls_bound::<Foo>();
20+
| ^^^ the trait `Bound` is not implemented for `Foo`
21+
|
22+
= help: the trait `Bound` is implemented for `u32`
23+
note: required by a bound in `impls_bound`
24+
--> $DIR/normalizes-to-is-not-productive.rs:28:19
25+
|
26+
LL | fn impls_bound<T: Bound>() {
27+
| ^^^^^ required by this bound in `impls_bound`
28+
29+
error: aborting due to 2 previous errors
30+
31+
For more information about this error, try `rustc --explain E0277`.

‎tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.rs‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
//@ ignore-compare-mode-next-solver (explicit)
2+
//@ compile-flags: -Znext-solver
3+
4+
// Make sure that stepping into impl where-clauses of `NormalizesTo`
5+
// goals is unproductive. This must not compile, see the inline
6+
// comments.
7+
8+
trait Bound {
9+
fn method();
10+
}
11+
impl Bound for u32 {
12+
fn method() {}
13+
}
14+
trait Trait<T> {
15+
type Assoc: Bound;
16+
}
17+
18+
struct Foo;
19+
20+
impl Trait<u32> for Foo {
21+
type Assoc = u32;
22+
}
23+
impl<T: Bound, U> Trait<U> for T {
24+
type Assoc = T;
25+
}
26+
27+
fn impls_bound<T: Bound>() {
28+
T::method();
29+
}
30+
31+
// The where-clause requires `Foo: Trait<T>` to hold to be wf.
32+
// If stepping into where-clauses during normalization is considered
33+
// to be productive, this would be the case:
34+
//
35+
// - `Foo: Trait<T>`
36+
// - via blanket impls, requires `Foo: Bound`
37+
// - via where-bound, requires `Foo eq <Foo as Trait<T>>::Assoc`
38+
// - normalize `<Foo as Trait<T>>::Assoc`
39+
// - via blanket impl, requires where-clause `Foo: Bound` -> cycle
40+
fn generic<T>()
41+
where
42+
<Foo as Trait<T>>::Assoc: Bound,
43+
//~^ ERROR the trait bound `Foo: Bound` is not satisfied
44+
{
45+
// Requires proving `Foo: Bound` by normalizing
46+
// `<Foo as Trait<T>>::Assoc` to `Foo`.
47+
impls_bound::<Foo>();
48+
//~^ ERROR the trait bound `Foo: Bound` is not satisfied
49+
}
50+
fn main() {
51+
// Requires proving `<Foo as Trait<u32>>::Assoc: Bound`.
52+
// This is trivially true.
53+
generic::<u32>();
54+
}

‎tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.stderr‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
2+
--> $DIR/normalizes-to-is-not-productive.rs:42:31
3+
|
4+
LL | <Foo as Trait<T>>::Assoc: Bound,
5+
| ^^^^^ the trait `Bound` is not implemented for `Foo`
6+
|
7+
= help: the trait `Bound` is implemented for `u32`
8+
note: required for `Foo` to implement `Trait<T>`
9+
--> $DIR/normalizes-to-is-not-productive.rs:23:19
10+
|
11+
LL | impl<T: Bound, U> Trait<U> for T {
12+
| ----- ^^^^^^^^ ^
13+
| |
14+
| unsatisfied trait bound introduced here
15+
16+
error[E0277]: the trait bound `Foo: Bound` is not satisfied
17+
--> $DIR/normalizes-to-is-not-productive.rs:47:19
18+
|
19+
LL | impls_bound::<Foo>();
20+
| ^^^ the trait `Bound` is not implemented for `Foo`
21+
|
22+
= help: the trait `Bound` is implemented for `u32`
23+
note: required by a bound in `impls_bound`
24+
--> $DIR/normalizes-to-is-not-productive.rs:27:19
25+
|
26+
LL | fn impls_bound<T: Bound>() {
27+
| ^^^^^ required by this bound in `impls_bound`
28+
29+
error: aborting due to 2 previous errors
30+
31+
For more information about this error, try `rustc --explain E0277`.

0 commit comments

Comments
 (0)