-
Notifications
You must be signed in to change notification settings - Fork 13.2k
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
change definitely unproductive cycles to error #137314
Conversation
This comment has been minimized.
This comment has been minimized.
908a6ad
to
25621e4
Compare
☔ The latest upstream changes (presumably #137466) made this pull request unmergeable. Please resolve the merge conflicts. |
dc88ce2
to
da01707
Compare
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
c6ab624
to
fa26c12
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- better document
Inductive
goal sources, explain WHY that's correct and the that it's safer to beUnknown
- this impacts coherence, write test
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 |
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`
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`
233fd9a
to
18809a2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ty for the comments
@bors r+ |
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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`
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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``
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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```
Rollup of 16 pull requests Successful merges: - rust-lang#126856 (remove deprecated tool `rls`) - rust-lang#136932 (Reduce formatting `width` and `precision` to 16 bits) - rust-lang#137314 (change definitely unproductive cycles to error) - rust-lang#137612 (Update bootstrap to edition 2024) - rust-lang#138002 (Disable CFI for weakly linked syscalls) - rust-lang#138052 (strip `-Wlinker-messages` wrappers from `rust-lld` rmake test) - rust-lang#138063 (Improve `-Zunpretty=hir` for parsed attrs) - rust-lang#138109 (make precise capturing args in rustdoc Json typed) - rust-lang#138147 (Add maintainers for powerpc64le-unknown-linux-gnu) - rust-lang#138245 (stabilize `ci_rustc_if_unchanged_logic` test for local environments) - rust-lang#138296 (Remove `AdtFlags::IS_ANONYMOUS` and `Copy`/`Clone` condition for anonymous ADT) - rust-lang#138300 (add tracking issue for unqualified_local_imports) - rust-lang#138307 (Allow specifying glob patterns for try jobs) - rust-lang#138313 (Update books) - rust-lang#138315 (use next_back() instead of last() on DoubleEndedIterator) - rust-lang#138318 (Rustdoc: remove a bunch of `@ts-expect-error` from main.js) r? `@ghost` `@rustbot` modify labels: rollup
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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````
Rollup of 18 pull requests Successful merges: - rust-lang#126856 (remove deprecated tool `rls`) - rust-lang#137314 (change definitely unproductive cycles to error) - rust-lang#137504 (Move methods from Map to TyCtxt, part 4.) - rust-lang#137701 (Convert `ShardedHashMap` to use `hashbrown::HashTable`) - rust-lang#137967 ([AIX] Fix hangs during testing) - rust-lang#138002 (Disable CFI for weakly linked syscalls) - rust-lang#138052 (strip `-Wlinker-messages` wrappers from `rust-lld` rmake test) - rust-lang#138063 (Improve `-Zunpretty=hir` for parsed attrs) - rust-lang#138109 (make precise capturing args in rustdoc Json typed) - rust-lang#138147 (Add maintainers for powerpc64le-unknown-linux-gnu) - rust-lang#138245 (stabilize `ci_rustc_if_unchanged_logic` test for local environments) - rust-lang#138296 (Remove `AdtFlags::IS_ANONYMOUS` and `Copy`/`Clone` condition for anonymous ADT) - rust-lang#138300 (add tracking issue for unqualified_local_imports) - rust-lang#138307 (Allow specifying glob patterns for try jobs) - rust-lang#138313 (Update books) - rust-lang#138315 (use next_back() instead of last() on DoubleEndedIterator) - rust-lang#138318 (Rustdoc: remove a bunch of `@ts-expect-error` from main.js) - rust-lang#138330 (Remove unnecessary `[lints.rust]` sections.) Failed merges: - rust-lang#137147 (Add exclude to config.toml) r? `@ghost` `@rustbot` modify labels: rollup
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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`````
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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``````
Rollup of 25 pull requests Successful merges: - rust-lang#134076 (Stabilize `std::io::ErrorKind::InvalidFilename`) - rust-lang#136842 (Add libstd support for Trusty targets) - rust-lang#137314 (change definitely unproductive cycles to error) - rust-lang#137504 (Move methods from Map to TyCtxt, part 4.) - rust-lang#137621 (Add std support to cygwin target) - rust-lang#137701 (Convert `ShardedHashMap` to use `hashbrown::HashTable`) - rust-lang#138109 (make precise capturing args in rustdoc Json typed) - rust-lang#138161 (Add PeekMut::refresh) - rust-lang#138162 (Update the standard library to Rust 2024) - rust-lang#138174 (Elaborate trait assumption in `receiver_is_dispatchable`) - rust-lang#138175 (Support rmeta inputs for --crate-type=bin --emit=obj) - rust-lang#138269 (uefi: fs: Implement FileType, FilePermissions and FileAttr) - rust-lang#138313 (Update books) - rust-lang#138318 (Rustdoc: remove a bunch of `@ts-expect-error` from main.js) - rust-lang#138331 (Use `RUSTC_LINT_FLAGS` more) - rust-lang#138333 (Rebuild llvm spuriously less frequently) - rust-lang#138343 (Enable `f16` tests for `powf`) - rust-lang#138345 (Some autodiff cleanups) - rust-lang#138346 (naked functions: on windows emit `.endef` without the symbol name) - rust-lang#138347 (Reduce `kw::Empty` usage, part 2) - rust-lang#138360 (Fix false-positive in `expr_or_init` and in the `invalid_from_utf8` lint) - rust-lang#138371 (Update compiletest's `has_asm_support` to match rustc) - rust-lang#138372 (Refactor `pick2_mut` & `pick3_mut` to use `get_disjoint_mut`) - rust-lang#138376 (Item-related cleanups) - rust-lang#138377 (Remove unnecessary lifetime from `PatInfo`.) r? `@ghost` `@rustbot` modify labels: rollup
…ompiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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```````
…iaskrgr Rollup of 8 pull requests Successful merges: - rust-lang#137314 (change definitely unproductive cycles to error) - rust-lang#137701 (Convert `ShardedHashMap` to use `hashbrown::HashTable`) - rust-lang#138269 (uefi: fs: Implement FileType, FilePermissions and FileAttr) - rust-lang#138331 (Use `RUSTC_LINT_FLAGS` more) - rust-lang#138345 (Some autodiff cleanups) - rust-lang#138387 (intrinsics: remove unnecessary leading underscore from argument names) - rust-lang#138389 (use `expect` instead of `allow`) - rust-lang#138390 (fix incorrect tracing log) r? `@ghost` `@rustbot` modify labels: rollup
…iaskrgr Rollup of 7 pull requests Successful merges: - rust-lang#137314 (change definitely unproductive cycles to error) - rust-lang#137701 (Convert `ShardedHashMap` to use `hashbrown::HashTable`) - rust-lang#138269 (uefi: fs: Implement FileType, FilePermissions and FileAttr) - rust-lang#138331 (Use `RUSTC_LINT_FLAGS` more) - rust-lang#138345 (Some autodiff cleanups) - rust-lang#138387 (intrinsics: remove unnecessary leading underscore from argument names) - rust-lang#138390 (fix incorrect tracing log) r? `@ghost` `@rustbot` modify labels: rollup
Rollup merge of rust-lang#137314 - lcnr:cycles-with-unknown-kind, r=compiler-errors change definitely unproductive cycles to error builds on top of rust-lang#136824 by adding a third variant to `PathKind` for 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````````
builds on top of #136824 by adding a third variant to
PathKind
for 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