elaborate obligations in coherence #124532
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This comment was marked as outdated.
This comment was marked as outdated.
rustbot
added
S-waiting-on-review
compiler-errors
added
T-types
compiler-errors
approved these changes
Apr 29, 2024
|
@rfcbot fcp merge |
|
Team member @compiler-errors has proposed to merge this. The next step is review by the rest of the tagged team members: No concerns currently listed. Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up! See this document for info about what commands tagged team members can give me. |
rfcbot
added
proposed-final-comment-period
This comment has been minimized.
This comment has been minimized.
rust-cloud-vms
bot
force-pushed
the
elaborate-coherence
branch
3 times, most recently
from
f9ab26e
to
cbee778
Compare
lcnr
added
I-types-nominated
rust-cloud-vms
bot
force-pushed
the
elaborate-coherence
branch
from
cbee778
to
7b1add4
Compare
|
@rfcbot reviewed Notably it's already a breaking change to remove a supertrait. |
compiler-errors
added
S-waiting-on-fcp
rfcbot
added
final-comment-period
|
🔔 This is now entering its final comment period, as per the review above. 🔔 |
|
do we want to skip the 10 day waiting period so that this is included in the same beta bumps as new solver in coherence stabilization? |
|
the last beta bump was on the 26th of April, so this PR and the stabilization PR will definitely be on the same beta version unless we somehow delay this PR by 5 weeks |
rfcbot
added
finished-final-comment-period
|
The final comment period, with a disposition to merge, as per the review above, is now complete. As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed. This will be merged soon. |
rust-cloud-vms
bot
force-pushed
the
elaborate-coherence
branch
from
7b1add4
to
3a131e1
Compare
This comment has been minimized.
This comment has been minimized.
rustbot
added
A-testsuite
This comment has been minimized.
This comment has been minimized.
rust-cloud-vms
bot
force-pushed
the
elaborate-coherence
branch
from
dd72952
to
03d9e84
Compare
|
@bors r+ |
bors
added
the
S-waiting-on-bors
fmease
added a commit
to fmease/rust
that referenced
this pull request
May 13, 2024
…er-errors
elaborate obligations in coherence
The following test currently does not pass coherence:
```rust
trait Super {}
trait Sub<T>: Super {}
trait Overlap<T> {}
impl<T, U: Sub<T>> Overlap<T> for U {}
impl<T> Overlap<T> for () {}
fn main() {}
```
We check whether `(): Sub<?t>` holds. This stalls with ambiguity as downstream crates may add an impl for `(): Sub<Local>`. However, its super trait bound `(): Super` cannot be implemented downstream, so this one is known not to hold.
By elaborating the bounds in the implicit negative overlap check, this now compiles. This is necessary to prevent breakage from enabling `-Znext-solver=coherence` (rust-lang#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details.
r? `@compiler-errors`
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this pull request
May 13, 2024
…er-errors
elaborate obligations in coherence
The following test currently does not pass coherence:
```rust
trait Super {}
trait Sub<T>: Super {}
trait Overlap<T> {}
impl<T, U: Sub<T>> Overlap<T> for U {}
impl<T> Overlap<T> for () {}
fn main() {}
```
We check whether `(): Sub<?t>` holds. This stalls with ambiguity as downstream crates may add an impl for `(): Sub<Local>`. However, its super trait bound `(): Super` cannot be implemented downstream, so this one is known not to hold.
By elaborating the bounds in the implicit negative overlap check, this now compiles. This is necessary to prevent breakage from enabling `-Znext-solver=coherence` (rust-lang#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details.
r? ``@compiler-errors``
bors
added a commit
to rust-lang-ci/rust
that referenced
this pull request
May 13, 2024
…iaskrgr Rollup of 5 pull requests Successful merges: - rust-lang#119515 (style-guide: Format single associated type `where` clauses on the same line) - rust-lang#119959 ([meta] Clarify prioritization alert) - rust-lang#123817 (Stabilize `seek_seek_relative`) - rust-lang#124532 (elaborate obligations in coherence) - rust-lang#125063 (Don't call `env::set_var` in `rustc_driver::install_ice_hook`) r? `@ghost` `@rustbot` modify labels: rollup
bors
added
S-waiting-on-author
|
☔ The latest upstream changes (presumably #125179) made this pull request unmergeable. Please resolve the merge conflicts. |
|
closing in favor of #127574 |
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this pull request
Jul 30, 2024
…=compiler-errors elaborate unknowable goals A reimplemented version of rust-lang#124532 affecting only the new solver. Always trying to prove super traits ends up causing a fatal overflow error in diesel, so we cannot land this in the old solver. The following test currently does not pass coherence: ```rust trait Super {} trait Sub<T>: Super {} trait Overlap<T> {} impl<T, U: Sub<T>> Overlap<T> for U {} impl<T> Overlap<T> for () {} fn main() {} ``` We check whether `(): Sub<?t>` holds. This stalls with ambiguity as downstream crates may add an impl for `(): Sub<Local>`. However, its super trait bound `(): Super` cannot be implemented downstream, so this one is known not to hold. By trying to prove that all the super bounds of a trait before adding a coherence unknowable candidate, this compiles. This is necessary to prevent breakage from enabling `-Znext-solver=coherence` (rust-lang#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details. The idea is that while there may be an impl of the trait itself we don't know about, if we're able to prove that a super trait is definitely not implemented, then that impl would also never apply/not be well-formed. This approach is different from rust-lang#124532 as it allows tests/ui/coherence/super-traits/super-trait-knowable-3.rs to compile. The approach in rust-lang#124532 only elaborating the root obligations while this approach tries it for all unknowable trait goals. r? `@compiler-errors`
rust-timer
added a commit
to rust-lang-ci/rust
that referenced
this pull request
Jul 30, 2024
Rollup merge of rust-lang#127574 - lcnr:coherence-check-supertrait, r=compiler-errors elaborate unknowable goals A reimplemented version of rust-lang#124532 affecting only the new solver. Always trying to prove super traits ends up causing a fatal overflow error in diesel, so we cannot land this in the old solver. The following test currently does not pass coherence: ```rust trait Super {} trait Sub<T>: Super {} trait Overlap<T> {} impl<T, U: Sub<T>> Overlap<T> for U {} impl<T> Overlap<T> for () {} fn main() {} ``` We check whether `(): Sub<?t>` holds. This stalls with ambiguity as downstream crates may add an impl for `(): Sub<Local>`. However, its super trait bound `(): Super` cannot be implemented downstream, so this one is known not to hold. By trying to prove that all the super bounds of a trait before adding a coherence unknowable candidate, this compiles. This is necessary to prevent breakage from enabling `-Znext-solver=coherence` (rust-lang#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details. The idea is that while there may be an impl of the trait itself we don't know about, if we're able to prove that a super trait is definitely not implemented, then that impl would also never apply/not be well-formed. This approach is different from rust-lang#124532 as it allows tests/ui/coherence/super-traits/super-trait-knowable-3.rs to compile. The approach in rust-lang#124532 only elaborating the root obligations while this approach tries it for all unknowable trait goals. r? `@compiler-errors`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The following test currently does not pass coherence:
We check whether
(): Sub<?t>holds. This stalls with ambiguity as downstream crates may add an impl for(): Sub<Local>. However, its super trait bound(): Supercannot be implemented downstream, so this one is known not to hold.By elaborating the bounds in the implicit negative overlap check, this now compiles. This is necessary to prevent breakage from enabling
-Znext-solver=coherence(#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details.r? @compiler-errors