-
Notifications
You must be signed in to change notification settings - Fork 13.5k
try evaluate nested goals with reduced depth first #143638
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
base: master
Are you sure you want to change the base?
Conversation
The job Click to see the possible cause of the failure (guessed by this bot)
|
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.
just nits, still trying to understand what's going on here
let _span = debug_span!("inject_normalize_to_rigid_candidate"); | ||
let _span = _span.enter(); |
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.
do we need this still? can't we just #[instrument]
the inject fn?
// FIXME: This match is a bit ugly, it might be nice to change the inspect | ||
// stuff to use a closure instead. which should hopefully simplify this a bit. | ||
match self.evaluate_added_goals_step() { | ||
for i in 0..FIXPOINT_STEP_LIMIT { |
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.
i'm tempted to say we should just unroll this loop somehow lol
@@ -1380,7 +1380,12 @@ where | |||
.map(|c| c.result) | |||
.collect(); | |||
return if let Some(response) = self.try_merge_responses(&where_bounds) { | |||
Ok((response, Some(TraitGoalProvenVia::ParamEnv))) | |||
let proven_via = if response.value.certainty == Certainty::Yes { |
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.
🤔 ?
r? @compiler-errors
This enables us to compile rayon, it's still quite hacky and just entirely yeets the provisional cache which is definitely wrong.
At its core the trait solver simply recursively evaluates nested goals. When encountering a goal on the stack we return a provisional result. This result depends on the path kind from the stack entry its usage during the first iteration and the result of the previous iteration when rerunning this cyclic goal until we're reaching a fixpoint.
We assume that the final result of all cycle participants stays the same regardless of where in the cycle they occur. The result of B in BAB and in ABA should be the same. We need to cache the result of evaluating subtrees, even if they depend on entries currently on the stack. We need to keep these entries around even after we've popped some of their cycle heads or have some of their nested goals on stack.
We also need to reuse results from previous fixpoint steps to avoid exponential blowup. The core question is whether provisional cache entries are still valid given the change in provisional result. Importantly, to avoid exponential blowup, reevaluating some goal must not result is separate uses of some other cycle head.
The only cache entries which can depend on the previous provisional result are cache entries created while evaluating the current goal which depend on that goal as a cycle head.
To avoid exponential blowup when rerunning goals we could only lazily reevaluate goals whose nested goals changed. This avoids exponential blowup as long as lazily rerunning the hanged goals does not add additional dependency edges to other cycle heads.
This holds for Case 1 of rayon: https://rust.godbolt.org/z/E17j9GTM7 rust-lang/trait-system-refactor-initiative#109 (comment)
This is a problem for Case 2 of rayon: https://rust.godbolt.org/z/3K9r7PaxY rust-lang/trait-system-refactor-initiative#109 (comment)
When checking the
Box<B>: ParallelIterator
goal we have aParamEnv
candidate for each$T::Iter: ParallelIterator
where-clause. Each candidate starts out as overflow during the first iteration and then changes toErr(NoSolution)
in the rerun. This means we actually need to recheckBox<B>: ParallelIterator
for all combinations of provisional results.To avoid this we'd need the search graph to be able to somehow reason about candidate merging to know that
[maybe, maybe, error]
and[maybe, error, error]
both result in ambiguity to allow us to not rerun both instances of it. Detected this is really involved and I don't know how to do that.We need to support the pattern from Case 2. The reason the cycles start out as ambiguous is that the cycle is stepping into a where-clause of a trait goal. In case
ParallelIterator
were a coinductive trait we'd consider the cycle to hold in the first iteration. This is already the case for auto-traits andSized
:NormalizesTo(<Vec<()> as Trait<Node<Vec<()>>>::Assoc)
Node<Vec<()>>: Sized
<Vec<()> as Trait<Node<Vec<()>>>::Assoc: Sized
NormalizesTo(<Vec<()> as Trait<Node<Vec<()>>>::Assoc)
cycleLazily rerunning goals on changed provisional results is therefore insufficient.
Rayon actually ends up completely ignoring the impl candidates, so there's an easier way to avoid its exponential blowup: simply do not consider impl candidates if there's a
ParamEnv
one: #141226.This only works as long as
ParamEnv
candidates always fully shadow impl candidates. Relying on this to avoid hangs means that it'll be significantly more difficult to weaken shadowing in the future. I believe we want to weaken shadowing in the future so this feels quite undesirable.There's a more general approach to avoid unnecessary work: we can initially evaluate nested goals at a lower depth and only evaluate them at their full depth if this succeeds or stays ambiguous. This handles impl candidates which get ignored as the
ParamEnv
candidate should hold with a lower required depth. It also avoids fully recomputing nested goals ofNormalizesTo
goals in case the parentAliasRelate
fails.There exist hangs which are not caused by unnecessarily recursing into impl candidates, e.g. rust-lang/trait-system-refactor-initiative#210. Like Case 1 of rayon, we rerun
NormalizesTo
goals going fromNoSolution
to a rigid alias. However, because of nested aliases we end up withAliasRelate
goals where there's an alias on the rhs and lhs, causing the rerun of the parentAliasRelate
to also normalize another alias which depends on the current and on cycle heads. We currently fully reevaluate that normalization. I don't know whether the strongest possible lazily evaluation scheme I've considered up until now would be sufficient to avoid the hang here.