change definitely unproductive cycles to error #137314
Open
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
rustbot
added
S-waiting-on-review
This comment has been minimized.
This comment has been minimized.
lcnr
force-pushed
the
cycles-with-unknown-kind
branch
from
908a6ad to
25621e4
Compare
This was referenced Feb 20, 2025
|
☔ The latest upstream changes (presumably #137466) made this pull request unmergeable. Please resolve the merge conflicts. |
lcnr
changed the title
lcnr
force-pushed
the
cycles-with-unknown-kind
branch
3 times, most recently
from
dc88ce2 to
da01707
Compare
|
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
lcnr
force-pushed
the
cycles-with-unknown-kind
branch
3 times, most recently
from
c6ab624 to
fa26c12
Compare
4 tasks
lcnr
commented
Feb 27, 2025
A cycle was previously coinductive if all steps were coinductive. Change this to instead considerm cycles to be coinductive if they step through at least one where-bound of an impl of a coinductive trait goal.
they don't detect any bugs in the search graph. We instead check for these via `search_graph_fuzz`.
lcnr
force-pushed
the
cycles-with-unknown-kind
branch
from
fa26c12 to
958909a
Compare
lcnr
force-pushed
the
cycles-with-unknown-kind
branch
from
b81c189 to
fc8a474
Compare
|
I've changed the approach to keep known inductive cycles as ambig as coherence and added a test which will be affected if we change this in the future. As coherence is already stable I would like to give this some time to make sure we're confident in the approach and to allow us to iterate further here without needing to FCP each change while it's still in flux. I would like to do one 'complete' FCP for cycle handling before stabilizing |
jieyouxu
added a commit
to jieyouxu/rust
that referenced
this pull request
Feb 28, 2025
solver cycles are coinductive once they have one coinductive step Implements the new cycle semantics in the new solver, dealing with the fallout from rust-lang/trait-system-refactor-initiative#10. The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz. A trait solver cycle is now coinductive if it has at least one *coinductive step*. A step is only considered coinductive if it's a where-clause of an impl of a coinductive trait. The only coinductive traits are `Sized` and auto traits. This differs from the current stable because where a cycle had to consist of exclusively coinductive goals. This is overly limiting and wasn't properly enforced as it (mostly) ignored all non-trait goals. A more in-depth explanation of my reasoning can be found in this separate doc: https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5. A summary: - imagine using dictionary passing style: map where-bounds to additional "dictonary" fn arguments instead of monomorphization - impls are the only source of truth and introduce a *constructor* of the dictionary type - a trait goal holds if mapping its proof tree to dictionary passing style results in a valid corecursive function - a corecursive function is valid if it is guarded: matching on it should result in a constructor in a finite amount of time. This property should recursively hold for all fields of the constructor - a function is guarded if the recursive call is *behind* a constructor - **and** this constructor is not *moved out of*, e.g. by accessing a field of the dictionary - the "not moved out of" condition is difficult to guarantee in general, e.g. for item bounds of associated types. However, there is no way to *move out* of an auto trait as there is no information you can get from *the inside of* an auto trait bound in the trait system - if we encounter a cycle/recursive call which involves an auto trait, we can always convert the proof tree into a non-recursive function which calls a corecursive function whose first step is the construction of the auto trait dict and which only recursively depends on itself (by inlining the original function until they reach the uses of the auto trait) **we can therefore make any cycle during which we step into an auto trait (or `Sized`) impl coinductive** ---- To fix rust-lang/trait-system-refactor-initiative#10 we could go with a more restrictive version which tries to restrict cycles to only allow code already supported on stable, potentially forcing cycles to be ambiguous if they step through an impl-where clause of a non-coinductive trait. `PathKind` should be a strictly ordered set to allow merging paths without worry. We could therefore add another variant `PathKind::ForceUnknown` which is greater than `PathKind::Coinductive`. We already have to add such a third `PathKind` in rust-lang#137314 anyways. I am not doing this here due to multiple reasons: - I cannot think of a principled reason why cycles using an impl to normalize differ in any way from simply using that impl to prove a trait bound. It feels unnecessary and like it makes it more difficult to reason about our cycle semantics :< - This PR does not affect stable as coherence doesn't care about whether a goal holds or is ambiguous. So we don't yet have to make a final decision r? `@compiler-errors` `@nikomatsakis`
rust-timer
added a commit
to rust-lang-ci/rust
that referenced
this pull request
Feb 28, 2025
Rollup merge of rust-lang#136824 - lcnr:yeet, r=compiler-errors solver cycles are coinductive once they have one coinductive step Implements the new cycle semantics in the new solver, dealing with the fallout from rust-lang/trait-system-refactor-initiative#10. The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz. A trait solver cycle is now coinductive if it has at least one *coinductive step*. A step is only considered coinductive if it's a where-clause of an impl of a coinductive trait. The only coinductive traits are `Sized` and auto traits. This differs from the current stable because where a cycle had to consist of exclusively coinductive goals. This is overly limiting and wasn't properly enforced as it (mostly) ignored all non-trait goals. A more in-depth explanation of my reasoning can be found in this separate doc: https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5. A summary: - imagine using dictionary passing style: map where-bounds to additional "dictonary" fn arguments instead of monomorphization - impls are the only source of truth and introduce a *constructor* of the dictionary type - a trait goal holds if mapping its proof tree to dictionary passing style results in a valid corecursive function - a corecursive function is valid if it is guarded: matching on it should result in a constructor in a finite amount of time. This property should recursively hold for all fields of the constructor - a function is guarded if the recursive call is *behind* a constructor - **and** this constructor is not *moved out of*, e.g. by accessing a field of the dictionary - the "not moved out of" condition is difficult to guarantee in general, e.g. for item bounds of associated types. However, there is no way to *move out* of an auto trait as there is no information you can get from *the inside of* an auto trait bound in the trait system - if we encounter a cycle/recursive call which involves an auto trait, we can always convert the proof tree into a non-recursive function which calls a corecursive function whose first step is the construction of the auto trait dict and which only recursively depends on itself (by inlining the original function until they reach the uses of the auto trait) **we can therefore make any cycle during which we step into an auto trait (or `Sized`) impl coinductive** ---- To fix rust-lang/trait-system-refactor-initiative#10 we could go with a more restrictive version which tries to restrict cycles to only allow code already supported on stable, potentially forcing cycles to be ambiguous if they step through an impl-where clause of a non-coinductive trait. `PathKind` should be a strictly ordered set to allow merging paths without worry. We could therefore add another variant `PathKind::ForceUnknown` which is greater than `PathKind::Coinductive`. We already have to add such a third `PathKind` in rust-lang#137314 anyways. I am not doing this here due to multiple reasons: - I cannot think of a principled reason why cycles using an impl to normalize differ in any way from simply using that impl to prove a trait bound. It feels unnecessary and like it makes it more difficult to reason about our cycle semantics :< - This PR does not affect stable as coherence doesn't care about whether a goal holds or is ambiguous. So we don't yet have to make a final decision r? `@compiler-errors` `@nikomatsakis`
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.
builds on top of #136824 by adding a third variant to
PathKindfor paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.
r? @compiler-errors @nikomatsakis