Rollup merge of #119613 - gavinleroy:expose-obligations, r=lcnr

Expose Obligations created during type inference.

This PR is a first pass at exposing the trait obligations generated and solved for during the type-check progress. Exposing these obligations allows for rustc plugins to use the public interface for proof trees (provided by the next gen trait solver).

The changes proposed track *all* obligations during the type-check process, this is desirable to not only look at the trees of failed obligations, but also those of successfully proved obligations. This feature is placed behind an unstable compiler option `track-trait-obligations` which should be used together with the `next-solver` option. I should note that the main interface is the function `inspect_typeck` made public in `rustc_hir_typeck/src/lib.rs` which allows the caller to provide a callback granting access to the `FnCtxt`.

r? `@lcnr`
This commit is contained in:
Matthias Krüger 2024-01-20 09:37:26 +01:00 committed by GitHub
commit 2de5ca25d2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 121 additions and 64 deletions

View file

@ -11,7 +11,7 @@ use rustc_middle::ty;
use rustc_middle::ty::error::{ExpectedFound, TypeError};
use super::eval_ctxt::GenerateProofTree;
use super::{Certainty, InferCtxtEvalExt};
use super::{Certainty, Goal, InferCtxtEvalExt};
/// A trait engine using the new trait solver.
///
@ -43,6 +43,21 @@ impl<'tcx> FulfillmentCtxt<'tcx> {
);
FulfillmentCtxt { obligations: Vec::new(), usable_in_snapshot: infcx.num_open_snapshots() }
}
fn inspect_evaluated_obligation(
&self,
infcx: &InferCtxt<'tcx>,
obligation: &PredicateObligation<'tcx>,
result: &Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
) {
if let Some(inspector) = infcx.obligation_inspector.get() {
let result = match result {
Ok((_, c, _)) => Ok(*c),
Err(NoSolution) => Err(NoSolution),
};
(inspector)(infcx, &obligation, result);
}
}
}
impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
@ -100,65 +115,66 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
let mut has_changed = false;
for obligation in mem::take(&mut self.obligations) {
let goal = obligation.clone().into();
let (changed, certainty, nested_goals) =
match infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0 {
Ok(result) => result,
Err(NoSolution) => {
errors.push(FulfillmentError {
obligation: obligation.clone(),
code: match goal.predicate.kind().skip_binder() {
ty::PredicateKind::Clause(ty::ClauseKind::Projection(_)) => {
FulfillmentErrorCode::ProjectionError(
// FIXME: This could be a `Sorts` if the term is a type
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::NormalizesTo(..) => {
FulfillmentErrorCode::ProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::AliasRelate(_, _, _) => {
FulfillmentErrorCode::ProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::Subtype(pred) => {
let (a, b) = infcx.instantiate_binder_with_placeholders(
goal.predicate.kind().rebind((pred.a, pred.b)),
);
let expected_found = ExpectedFound::new(true, a, b);
FulfillmentErrorCode::SubtypeError(
expected_found,
TypeError::Sorts(expected_found),
)
}
ty::PredicateKind::Coerce(pred) => {
let (a, b) = infcx.instantiate_binder_with_placeholders(
goal.predicate.kind().rebind((pred.a, pred.b)),
);
let expected_found = ExpectedFound::new(false, a, b);
FulfillmentErrorCode::SubtypeError(
expected_found,
TypeError::Sorts(expected_found),
)
}
ty::PredicateKind::Clause(_)
| ty::PredicateKind::ObjectSafe(_)
| ty::PredicateKind::Ambiguous => {
FulfillmentErrorCode::SelectionError(
SelectionError::Unimplemented,
)
}
ty::PredicateKind::ConstEquate(..) => {
bug!("unexpected goal: {goal:?}")
}
},
root_obligation: obligation,
});
continue;
}
};
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
self.inspect_evaluated_obligation(infcx, &obligation, &result);
let (changed, certainty, nested_goals) = match result {
Ok(result) => result,
Err(NoSolution) => {
errors.push(FulfillmentError {
obligation: obligation.clone(),
code: match goal.predicate.kind().skip_binder() {
ty::PredicateKind::Clause(ty::ClauseKind::Projection(_)) => {
FulfillmentErrorCode::ProjectionError(
// FIXME: This could be a `Sorts` if the term is a type
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::NormalizesTo(..) => {
FulfillmentErrorCode::ProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::AliasRelate(_, _, _) => {
FulfillmentErrorCode::ProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::Subtype(pred) => {
let (a, b) = infcx.instantiate_binder_with_placeholders(
goal.predicate.kind().rebind((pred.a, pred.b)),
);
let expected_found = ExpectedFound::new(true, a, b);
FulfillmentErrorCode::SubtypeError(
expected_found,
TypeError::Sorts(expected_found),
)
}
ty::PredicateKind::Coerce(pred) => {
let (a, b) = infcx.instantiate_binder_with_placeholders(
goal.predicate.kind().rebind((pred.a, pred.b)),
);
let expected_found = ExpectedFound::new(false, a, b);
FulfillmentErrorCode::SubtypeError(
expected_found,
TypeError::Sorts(expected_found),
)
}
ty::PredicateKind::Clause(_)
| ty::PredicateKind::ObjectSafe(_)
| ty::PredicateKind::Ambiguous => {
FulfillmentErrorCode::SelectionError(
SelectionError::Unimplemented,
)
}
ty::PredicateKind::ConstEquate(..) => {
bug!("unexpected goal: {goal:?}")
}
},
root_obligation: obligation,
});
continue;
}
};
// Push any nested goals that we get from unifying our canonical response
// with our obligation onto the fulfillment context.
self.obligations.extend(nested_goals.into_iter().map(|goal| {