1
Fork 0

elaborate unknowable goals

if a trait is unknowable, but its super trait
is definitely not implemented, then the trait
itself is definitely also not implemented.
This commit is contained in:
lcnr 2024-07-10 16:03:20 +02:00
parent 0fdfb61795
commit fe0bd76a8b
11 changed files with 122 additions and 2 deletions

View file

@ -699,6 +699,18 @@ where
if ecx.trait_ref_is_knowable(goal.param_env, trait_ref)? {
Err(NoSolution)
} else {
// While the trait bound itself may be unknowable, we may be able to
// prove that a super trait is not implemented. For this, we recursively
// prove the super trait bounds of the current goal.
//
// We skip the goal itself as that one would cycle.
let predicate: I::Predicate = trait_ref.upcast(cx);
ecx.add_goals(
GoalSource::Misc,
elaborate::elaborate(cx, [predicate])
.skip(1)
.map(|predicate| goal.with(cx, predicate)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
},