Next-generation trait solver

[nikomatsakis]

Metadata
Owner(s)	@lcnr
Team(s)	rust-analyzer, types
Goal document	2024h2/next-solver

Summary

In the next 6 months we plan to extend the next-generation trait solver as follows:

• stabilize the use of the next-generation trait solver in coherence checking
• use the new implementation in rustdoc and lints where applicable
• share the solver with rust-analyser
• successfully bootstrap the compiler when exclusively using the new implementation and run crater

Tasks and status

• Discussion and moral support (types )
• Stabilize next-generation solver in coherence
  • Prototype implementation (@lcnr, @compiler-errors)
  • Standard reviews (types )
  • Resolve hang with complex auto-trait cycles
  • Stabilization PR merged (types )
  • Address performance impacton nalgebra
  • Stabilization decision (types )
• Support next-generation solver in rust-analyzer
  • Implementation (library side) (@compiler-errors)
  • Implementation (rust-analyzer side) ()
  • Standard reviews (types )
  • Standard reviews (rust-analyzer )

[nikomatsakis]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

[lcnr]

I am currently working on caching in the trait solver. The current implementation results in hangs when encountering complex auto-trait cycles. See https://rust-lang.zulipchat.com/#narrow/stream/364551-t-types.2Ftrait-system-refactor/topic/Fuchsia.20hanging.20on.20.60-Znext-solver.3Dcoherence.60 for the progress here. We now have an approach which fixes the performance regression. It'll still take at least multiple weeks until it's ready for merge however.

The librarification of the trait solver is in a very good state thanks to a lot of work by @compiler-errors. We're currently discussing its use in r-a on zulip: https://rust-lang.zulipchat.com/#narrow/stream/185405-t-compiler.2Frust-analyzer/topic/New.20Trait.20Solver. While there are still components we intend to move from rustc into the shared library to enable their reuse, all major ones have already been moved by now.

[lcnr]

Since the last update, we've landed the new caching optimization in rust-lang/rust#128828 and hope to land the -Znext-solver=coherence stabilization PR this week.

There has been one other bug fix in the last month, see https://github.com/rust-lang/rust/pulls?q=is%3Apr+is%3Amerged+label%3AWG-trait-system-refactor+-label%3Arollup+closed%3A%3C2024-09-02+-closed%3A%3C2024-08-01 for the full list of PRs.

[lcnr]

We've tried to stabilize -Znext-solver=coherence in rust-lang/rust#121848 which we had to revert later (rust-lang/rust#130249) as it caused a hang in nalgebra.

We mostly fixed this hang with rust-lang/rust#130617 and rust-lang/rust#130821. As nalgebra still ends up hitting the recursion limit with a quite wide search graph, the performance impact of enabling -Znext-solver=coherence is quite bad rust-lang/rust#130654 (comment).

There haven't been any other significant changes to the new solver during the last month.

[lcnr]

We stabilized -Znext-solver=coherence again in rust-lang/rust#130654. It's looking like the stabilization will actually go through this time.

We're currently refactoring the way the current "typing mode" is tracked, cc rust-lang/types-team#128. This is necessary to fix rust-lang/trait-system-refactor-initiative#106. I also started an FCP to clean up the way we merge candidates when proving trait goals: rust-lang/rust#132325. I intend to pretty much exactly match this behavior in the new solver as well, so I expect all of our issues there to be resolved.

[lcnr]

The -Znext-solver=coherence stabilization didn't encounter any issues and is now on beta. Published a new update blogpost. We've made significant progress on bootstrap with -Znext-solver=globally this last month. I finished the core of the "typing mode" refactor with rust-lang/rust#133242 which then allowed me to unblock bootstrap via rust-lang/rust#133501. There has been a lot of work by @compiler-errors and myself with significant help from @lqd since then.

We're now able to bootstrap using exclusively the new solver. This allowed us to finish the first @bors try-run and run the benchmark suite for the first time. There are 3 remaining benchmarks which fail to compile and quite a few with very significant performance regressions. I am now working towards proper support for defining uses of opaque types inside of closures to fix wg-grammar.