solver cycles are coinductive once they have one coinductive step #136824

lcnr · 2025-02-10T16:36:55Z

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 #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

[DO NOT MERGE] bootstrap with `-Znext-solver=globally` A revival of rust-lang#124812. Current status: ~~`./x.py b --stage 2` passes 🎉~~ `try` builds succeed 🎉 🎉 🎉 [first perf run](rust-lang#133502 (comment)) 👻 ### in-flight changes - ce66d92 is a rebased version of rust-lang#125334, unsure whether I actually want to land this PR for now - rust-lang#136824 r? `@ghost`

lcnr · 2025-02-13T10:08:55Z

@bors try

bors · 2025-02-13T10:10:09Z

⌛ Trying commit 68f2802 with merge d5c3c24...

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. I am currently also changing inductive cycles back to an error instead of ambiguity outside of coherence to deal with rust-lang/trait-system-refactor-initiative#114. This should allow nalgebra to compile without affecting anything on stable. Whether a cycle results in ambiguity or success should not matter for coherence, as it only checks for errors. The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz. TODO: - [ ] fix issues from https://hackmd.io/JsblAvk4R5y30niSNQVYeA - [ ] add ui tests - [ ] explain this approach and why we believe it to be correct r? `@compiler-errors` `@nikomatsakis`

bors · 2025-02-13T11:59:37Z

☀️ Try build successful - checks-actions
Build commit: d5c3c24 (d5c3c24fef4826690d53e1b54dda32ac9008633b)

…rors rework rigid alias handling Necessary for rust-lang#136824 if we treat coinductive cycles as errors as we otherwise don't emit an error for ```rust trait Overflow { type Assoc; } impl<T> Overflow for T { type Assoc = <T as Overflow>::Assoc; } ``` The important part is that we only add a `RigidAlias` candidate in cases where the alias is actually supposed to be rigid: - its trait bound has been proven via a `ParamEnv` or `ItemBound` candidate - it's one of the special builtin traits which have a blanket impl with a `default` assoc type This means that we now more explicitly control which aliases should rigid to avoid accidentally accepting cyclic aliases. This requires changes to diagnostics as we no longer enter an explicit `RigidAlias` candidate for `NormalizesTo` goals whose trait bound doesn't hold. To fix this I've modified the `BestObligation` visitor always ignore `RigidAlias` candidates and to instead manually check these requirements if there are no applicable candidates. I also removed the hack for handling `structurally_normalize_ty` failures. This fixes rust-lang#134905 as we no longer continue to use the `EvalCtxt` even though a nested goal failed. r? `@compiler-errors`

…rors rework rigid alias handling Necessary for rust-lang#136824 if we treat coinductive cycles as errors as we otherwise don't emit an error for ```rust trait Overflow { type Assoc; } impl<T> Overflow for T { type Assoc = <T as Overflow>::Assoc; } ``` The important part is that we only add a `RigidAlias` candidate in cases where the alias is actually supposed to be rigid: - its trait bound has been proven via a `ParamEnv` or `ItemBound` candidate - it's one of the special builtin traits which have a blanket impl with a `default` assoc type This means that we now more explicitly control which aliases should rigid to avoid accidentally accepting cyclic aliases. This requires changes to diagnostics as we no longer enter an explicit `RigidAlias` candidate for `NormalizesTo` goals whose trait bound doesn't hold. To fix this I've modified the `BestObligation` visitor always ignore `RigidAlias` candidates and to instead manually check these requirements if there are no applicable candidates. I also removed the hack for handling `structurally_normalize_ty` failures. This fixes rust-lang#134905 as we no longer continue to use the `EvalCtxt` even though a nested goal failed. r? ``@compiler-errors``

Rollup merge of rust-lang#136863 - lcnr:treat-as-rigid, r=compiler-errors rework rigid alias handling Necessary for rust-lang#136824 if we treat coinductive cycles as errors as we otherwise don't emit an error for ```rust trait Overflow { type Assoc; } impl<T> Overflow for T { type Assoc = <T as Overflow>::Assoc; } ``` The important part is that we only add a `RigidAlias` candidate in cases where the alias is actually supposed to be rigid: - its trait bound has been proven via a `ParamEnv` or `ItemBound` candidate - it's one of the special builtin traits which have a blanket impl with a `default` assoc type This means that we now more explicitly control which aliases should rigid to avoid accidentally accepting cyclic aliases. This requires changes to diagnostics as we no longer enter an explicit `RigidAlias` candidate for `NormalizesTo` goals whose trait bound doesn't hold. To fix this I've modified the `BestObligation` visitor always ignore `RigidAlias` candidates and to instead manually check these requirements if there are no applicable candidates. I also removed the hack for handling `structurally_normalize_ty` failures. This fixes rust-lang#134905 as we no longer continue to use the `EvalCtxt` even though a nested goal failed. r? ``@compiler-errors``

rustbot · 2025-02-18T10:50:27Z

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

compiler-errors

LGTM, though could possibly use more info written as doc comments 🤔

tests/ui/traits/next-solver/cycles/coinduction/only-one-coinductive-step-needed.current.stderr

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

compiler/rustc_middle/src/ty/predicate.rs

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

compiler-errors

Add a test for a mixed cycle that only involves trait goals, r=me

compiler-errors · 2025-02-28T03:44:15Z

@rustbot author

lcnr · 2025-02-28T11:12:46Z

@bors r=compiler-errors rollup

bors · 2025-02-28T11:12:48Z

📌 Commit e0d862e has been approved by compiler-errors

It is now in the queue for this repository.

bors · 2025-02-28T11:12:49Z

🌲 The tree is currently closed for pull requests below priority 100. This pull request will be tested once the tree is reopened.

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 · 2025-02-28T11:17:09Z

@bors r=compiler-errors rollup

bors · 2025-02-28T11:17:12Z

📌 Commit 6a3b30f has been approved by compiler-errors

It is now in the queue for this repository.

bors · 2025-02-28T11:17:13Z

🌲 The tree is currently closed for pull requests below priority 100. This pull request will be tested once the tree is reopened.

Rollup of 9 pull requests Successful merges: - rust-lang#136424 (fix: overflowing bin hex) - rust-lang#136824 (solver cycles are coinductive once they have one coinductive step) - rust-lang#137220 (Support `rust.channel = "auto-detect"`) - rust-lang#137712 (Clean up TypeckResults::extract_binding_mode) - rust-lang#137713 (Fix enzyme build errors) - rust-lang#137748 (Fix method name in `TyCtxt::hir_crate()` documentation) - rust-lang#137778 (update enzyme to handle range metadata) - rust-lang#137780 (Fix typo in query expansion documentation) - rust-lang#137788 (Bump `rustc_{codegen_ssa,llvm}` `cc` to 1.2.16 to fix `x86` Windows jobs on newest Windows SDK) r? `@ghost` `@rustbot` modify labels: rollup

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`

rustbot assigned compiler-errors Feb 10, 2025

rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-trait-system-refactor The Rustc Trait System Refactor Initiative (-Znext-solver) labels Feb 10, 2025

lcnr force-pushed the yeet branch from a309253 to 4847609 Compare February 10, 2025 16:44

This comment has been minimized.

Sign in to view

lcnr force-pushed the yeet branch from 4847609 to 8f2920b Compare February 11, 2025 07:57

This comment has been minimized.

Sign in to view

This was referenced Feb 11, 2025

rework rigid alias handling #136863

Merged

[DO NOT MERGE] bootstrap with -Znext-solver=globally #133502

Draft

lcnr force-pushed the yeet branch from c3ebb53 to 7997ff6 Compare February 12, 2025 13:52

This comment has been minimized.

Sign in to view

lcnr force-pushed the yeet branch from 7997ff6 to b55f9c8 Compare February 12, 2025 15:00

lcnr force-pushed the yeet branch 4 times, most recently from e8a5870 to 4720589 Compare February 17, 2025 14:52

lcnr marked this pull request as ready for review February 18, 2025 10:50

lcnr mentioned this pull request Feb 18, 2025

search_graph_fuzz add unit test support and unit tests rust-lang/trait-system-refactor-initiative#163

Open

lcnr force-pushed the yeet branch from 4720589 to db5624f Compare February 19, 2025 10:05

lcnr mentioned this pull request Feb 20, 2025

change definitely unproductive cycles to error #137314

Open

compiler-errors reviewed Feb 25, 2025

View reviewed changes

lcnr force-pushed the yeet branch 2 times, most recently from c2e16f1 to c44ecdf Compare February 26, 2025 13:39

lcnr mentioned this pull request Feb 27, 2025

Next-generation trait solver rust-lang/rust-project-goals#113

Open

4 tasks

compiler-errors approved these changes Feb 27, 2025

View reviewed changes

rustbot added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Feb 28, 2025

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. labels Feb 28, 2025

lcnr added 8 commits February 28, 2025 12:16

rework cycle handling

46faf4b

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.

fix rustc_type_ir without the nightly feature

edadb54

fix typo

933d45f

remove useless tests

a7970c0

they don't detect any bugs in the search graph. We instead check for these via `search_graph_fuzz`.

normalizing where-clauses is also coinductive, add tests

7eb677e

add test for newly supported behavior

fe874cd

review

ef771b8

add test using only trait bounds

6a3b30f

lcnr force-pushed the yeet branch from e0d862e to 6a3b30f Compare February 28, 2025 11:16

jieyouxu mentioned this pull request Feb 28, 2025

Rollup of 9 pull requests #137790

Merged

bors merged commit 2ebf407 into rust-lang:master Feb 28, 2025
6 checks passed

rustbot added this to the 1.87.0 milestone Feb 28, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

solver cycles are coinductive once they have one coinductive step #136824

solver cycles are coinductive once they have one coinductive step #136824

lcnr commented Feb 10, 2025 •

edited

Loading

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

lcnr commented Feb 13, 2025

bors commented Feb 13, 2025

bors commented Feb 13, 2025

rustbot commented Feb 18, 2025

compiler-errors left a comment

compiler-errors left a comment

compiler-errors commented Feb 28, 2025

lcnr commented Feb 28, 2025

bors commented Feb 28, 2025

bors commented Feb 28, 2025

lcnr commented Feb 28, 2025

bors commented Feb 28, 2025

bors commented Feb 28, 2025

solver cycles are coinductive once they have one coinductive step #136824

solver cycles are coinductive once they have one coinductive step #136824

Conversation

lcnr commented Feb 10, 2025 • edited Loading

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

lcnr commented Feb 13, 2025

bors commented Feb 13, 2025

bors commented Feb 13, 2025

rustbot commented Feb 18, 2025

compiler-errors left a comment

Choose a reason for hiding this comment

compiler-errors left a comment

Choose a reason for hiding this comment

compiler-errors commented Feb 28, 2025

lcnr commented Feb 28, 2025

bors commented Feb 28, 2025

bors commented Feb 28, 2025

lcnr commented Feb 28, 2025

bors commented Feb 28, 2025

bors commented Feb 28, 2025

lcnr commented Feb 10, 2025 •

edited

Loading