Correctly consider depth when visiting WF goals

This commit is contained in:
Michael Goulet 2024-06-14 17:19:47 -04:00
parent 93ee07c756
commit 0562064959
2 changed files with 18 additions and 3 deletions

View file

@ -520,8 +520,9 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
if let Some(ty::PredicateKind::AliasRelate(lhs, rhs, _)) = pred_kind.no_bound_vars() {
if let Some(obligation) = goal
.infcx()
.visit_proof_tree(
.visit_proof_tree_at_depth(
goal.goal().with(goal.infcx().tcx, ty::ClauseKind::WellFormed(lhs.into())),
goal.depth() + 1,
self,
)
.break_value()
@ -529,8 +530,9 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
return ControlFlow::Break(obligation);
} else if let Some(obligation) = goal
.infcx()
.visit_proof_tree(
.visit_proof_tree_at_depth(
goal.goal().with(goal.infcx().tcx, ty::ClauseKind::WellFormed(rhs.into())),
goal.depth() + 1,
self,
)
.break_value()

View file

@ -278,6 +278,10 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
self.source
}
pub fn depth(&self) -> usize {
self.depth
}
fn candidates_recur(
&'a self,
candidates: &mut Vec<InspectCandidate<'a, 'tcx>>,
@ -435,9 +439,18 @@ impl<'tcx> InferCtxt<'tcx> {
&self,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
visitor: &mut V,
) -> V::Result {
self.visit_proof_tree_at_depth(goal, 0, visitor)
}
fn visit_proof_tree_at_depth<V: ProofTreeVisitor<'tcx>>(
&self,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
depth: usize,
visitor: &mut V,
) -> V::Result {
let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
let proof_tree = proof_tree.unwrap();
visitor.visit_goal(&InspectGoal::new(self, 0, proof_tree, None, GoalSource::Misc))
visitor.visit_goal(&InspectGoal::new(self, depth, proof_tree, None, GoalSource::Misc))
}
}