Rollup merge of #121193 - compiler-errors:coherence-fulfillment, r=lcnr

Use fulfillment in next trait solver coherence

Use fulfillment in the new trait solver's `impl_intersection_has_impossible_obligation` routine. This means that inference that falls out of processing other obligations can influence whether we can determine if an obligation is impossible to satisfy. See the committed test.

This should be completely sound, since evaluation and fulfillment both respect intercrate mode equally.

We run the risk of breaking coherence later if we were to change the rules of fulfillment and/or inference during coherence, but this is a problem which affects evaluation, as nested obligations from a trait goal are processed together and can influence each other in the same way.

r? lcnr
cc #114862

Also changed obligationctxt -> fulfillmentctxt because it feels kind of redundant to use an ocx here. I don't really care enough and can change it back if it really matters much.
This commit is contained in:
Matthias Krüger
2024-02-17 18:47:42 +01:00
committed by GitHub
5 changed files with 95 additions and 35 deletions

View File

@@ -223,8 +223,10 @@ impl<'tcx> InferCtxt<'tcx> {
goal: Goal<'tcx, ty::Predicate<'tcx>>,
visitor: &mut V,
) -> ControlFlow<V::BreakTy> {
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))
self.probe(|_| {
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))
})
}
}