search graph: improve rebasing and add forced ambiguity support

[lcnr]

Based on #142774

This slightly strengthens rebasing and actually checks for the property we want to maintain. There are two additional optimizations we can and should do here:

• we should be able to just always rebase if cycle heads already have a provisional result from a previous iteration
• we currently only apply provisional cache entries if the path_to_entry matches exactly. We should be able to extend this e.g. if you have an entry for B in ABA where the path BA is coinductive, then we can use this entry even if the current path from A to B is inductive.

---

I've also added support for PathKind::ForcedAmbiguity which always forced the initial provisional result to be ambiguous. A am using this for cycles involving negative reasons, which is currently only used by the fuzzer in https://github.com/lcnr/search_graph_fuzz. Consider the following setup: A goal A which only holds if B does not hold, and B which only holds if A does not hold.

• A only holds if B does not hold, results in X
  • B only holds if A does not hold, results in !X
    • A cycle, provisional result X
• B only holds if A does not hold, results in X
  • A only holds if B does not hold, results in !X
    • B cycle, provisional result X

With negative reasoning, the result of cycle participants depends on their position in the cycle. This means using cache entries while other entries are on the stack/have been popped is wrong. It's also generally just kinda iffy. By always forcing the initial provisional result of such cycles to be ambiguity, we can avoid this, as "not maybe" is just "maybe" again.

Rust kind of has negative reasoning due to incompleteness, consider the following setup:

• T::Foo eq u32
  • normalize T::Foo
    • via impl -> u32
    • via param_env -> T
      • nested goals...

T::Foo eq u32 holds exactly if the nested goals of the param_env candidate do not hold, as preferring that candidate over the impl causes the alias-relate to fail. This means the current provisional cache may cause us to ignore param_env preference in rare cases. This is not unsound and I don't care about it, as we already have this behavior when rerunning on changed fixpoint results:

• T: Trait
  • via impl ok
  • via env
    • T: Trait non-productive cycle
• result OK, rerun changed provisional result
• T: Trait
  • via impl ok
  • via env
    • T: Trait using the provisional result, can be thought of as recursively expanding the proof tree
      • via impl ok
      • via env <don't care>
• prefer the env candidate, reached fixpoint

---

One could imaging changing ParamEnv candidates or the impl shadowing check to use PathKind::ForcedAmbiguity to make the search graph less observable instead of only using it for fuzzing. However, incomplete candidate preference isn't really negative reasoning and doing this is a breaking change rust-lang/trait-system-refactor-initiative#114

r? @compiler-errors

[rustbot]

Some changes occurred to the core trait solver

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

[lcnr]

@bors2 try @rust-timer queue

[rust-bors]

⌛ Trying commit ff3254b with merge a07e3de…

To cancel the try build, run the command @bors2 try cancel.

[rust-bors]

☀️ Try build successful (CI)
Build commit: a07e3de (a07e3de733ec6c6ec4f2988cbd06487ff09094c4, parent: 8f21a5c92ea55c348c275a1bc4fedbdf181e0d64)

[bors]

☔ The latest upstream changes (presumably #142774) made this pull request unmergeable. Please resolve the merge conflicts.

[rust-timer]

Finished benchmarking commit (a07e3de): comparison URL.

Overall result: ✅ improvements - no action needed

Benchmarking this pull request means it may be perf-sensitive – we'll automatically label it not fit for rolling up. You can override this, but we strongly advise not to, due to possible changes in compiler perf.

@bors rollup=never
@rustbot label: -S-waiting-on-perf -perf-regression

Instruction count

Our most reliable metric. Used to determine the overall result above. However, even this metric can be noisy.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	-	-	0
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-0.3%	[-0.5%, -0.2%]	11
All ❌✅ (primary)	-	-	0

Max RSS (memory usage)

Results (primary 5.1%, secondary 2.7%)

A less reliable metric. May be of interest, but not used to determine the overall result above.

	mean	range	count
Regressions ❌ (primary)	5.1%	[2.6%, 9.4%]	3
Regressions ❌ (secondary)	2.7%	[2.6%, 2.8%]	2
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-	-	0
All ❌✅ (primary)	5.1%	[2.6%, 9.4%]	3

Cycles

Results (secondary -8.0%)

A less reliable metric. May be of interest, but not used to determine the overall result above.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	-	-	0
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-8.0%	[-9.8%, -3.3%]	7
All ❌✅ (primary)	-	-	0

Binary size

This benchmark run did not return any relevant results for this metric.

Bootstrap: 691.142s -> 688.194s (-0.43%)
Artifact size: 372.05 MiB -> 372.03 MiB (-0.01%)