mirror of
https://github.com/rust-lang/rust.git
synced 2024-11-22 14:55:26 +00:00
proof trees: use for intercrate_ambiguity_causes
This commit is contained in:
parent
4fda889bf8
commit
de53877f8b
@ -1,30 +1,70 @@
|
||||
//! Data structure used to inspect trait solver behavior.
|
||||
//!
|
||||
//! During trait solving we optionally build "proof trees", the root of
|
||||
//! which is a [GoalEvaluation] with [GoalEvaluationKind::Root]. These
|
||||
//! trees are used to improve the debug experience and are also used by
|
||||
//! the compiler itself to provide necessary context for error messages.
|
||||
//!
|
||||
//! Because each nested goal in the solver gets [canonicalized] separately
|
||||
//! and we discard inference progress via "probes", we cannot mechanically
|
||||
//! use proof trees without somehow "lifting up" data local to the current
|
||||
//! `InferCtxt`. Any data used mechanically is therefore canonicalized and
|
||||
//! stored as [CanonicalState]. As printing canonicalized data worsens the
|
||||
//! debugging dumps, we do not simply canonicalize everything.
|
||||
//!
|
||||
//! This means proof trees contain inference variables and placeholders
|
||||
//! local to a different `InferCtxt` which must not be used with the
|
||||
//! current one.
|
||||
//!
|
||||
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
|
||||
|
||||
use super::{
|
||||
CandidateSource, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution, QueryInput,
|
||||
QueryResult,
|
||||
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution,
|
||||
QueryInput, QueryResult,
|
||||
};
|
||||
use crate::ty;
|
||||
use crate::{infer::canonical::CanonicalVarValues, ty};
|
||||
use format::ProofTreeFormatter;
|
||||
use std::fmt::{Debug, Write};
|
||||
|
||||
mod format;
|
||||
|
||||
/// Some `data` together with information about how they relate to the input
|
||||
/// of the canonical query.
|
||||
///
|
||||
/// This is only ever used as [CanonicalState]. Any type information in proof
|
||||
/// trees used mechanically has to be canonicalized as we otherwise leak
|
||||
/// inference variables from a nested `InferCtxt`.
|
||||
#[derive(Debug, Clone, Copy, Eq, PartialEq, TypeFoldable, TypeVisitable)]
|
||||
pub struct State<'tcx, T> {
|
||||
pub var_values: CanonicalVarValues<'tcx>,
|
||||
pub data: T,
|
||||
}
|
||||
|
||||
pub type CanonicalState<'tcx, T> = Canonical<'tcx, State<'tcx, T>>;
|
||||
|
||||
#[derive(Debug, Eq, PartialEq)]
|
||||
pub enum CacheHit {
|
||||
Provisional,
|
||||
Global,
|
||||
}
|
||||
|
||||
/// When evaluating the root goals we also store the
|
||||
/// original values for the `CanonicalVarValues` of the
|
||||
/// canonicalized goal. We use this to map any [CanonicalState]
|
||||
/// from the local `InferCtxt` of the solver query to
|
||||
/// the `InferCtxt` of the caller.
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub enum GoalEvaluationKind {
|
||||
Root,
|
||||
pub enum GoalEvaluationKind<'tcx> {
|
||||
Root { orig_values: Vec<ty::GenericArg<'tcx>> },
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub struct GoalEvaluation<'tcx> {
|
||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
pub kind: GoalEvaluationKind,
|
||||
pub kind: GoalEvaluationKind<'tcx>,
|
||||
pub evaluation: CanonicalGoalEvaluation<'tcx>,
|
||||
/// The nested goals from instantiating the query response.
|
||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||
}
|
||||
|
||||
@ -66,6 +106,7 @@ pub struct GoalEvaluationStep<'tcx> {
|
||||
/// of a goal.
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub struct Probe<'tcx> {
|
||||
/// What happened inside of this probe in chronological order.
|
||||
pub steps: Vec<ProbeStep<'tcx>>,
|
||||
pub kind: ProbeKind<'tcx>,
|
||||
}
|
||||
@ -78,12 +119,21 @@ impl Debug for Probe<'_> {
|
||||
|
||||
#[derive(Eq, PartialEq)]
|
||||
pub enum ProbeStep<'tcx> {
|
||||
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
|
||||
/// We added a goal to the `EvalCtxt` which will get proven
|
||||
/// the next time `EvalCtxt::try_evaluate_added_goals` is called.
|
||||
AddGoal(CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
|
||||
/// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
|
||||
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
|
||||
/// A call to `probe` while proving the current goal. This is
|
||||
/// used whenever there are multiple candidates to prove the
|
||||
/// current goalby .
|
||||
NestedProbe(Probe<'tcx>),
|
||||
}
|
||||
|
||||
#[derive(Debug, PartialEq, Eq)]
|
||||
/// What kind of probe we're in. In case the probe represents a candidate, or
|
||||
/// the final result of the current goal - via [ProbeKind::Root] - we also
|
||||
/// store the [QueryResult].
|
||||
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
|
||||
pub enum ProbeKind<'tcx> {
|
||||
/// The root inference context while proving a goal.
|
||||
Root { result: QueryResult<'tcx> },
|
||||
|
@ -41,7 +41,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
||||
|
||||
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
|
||||
let goal_text = match eval.kind {
|
||||
GoalEvaluationKind::Root => "ROOT GOAL",
|
||||
GoalEvaluationKind::Root { orig_values: _ } => "ROOT GOAL",
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack } => match is_normalizes_to_hack {
|
||||
IsNormalizesToHack::No => "GOAL",
|
||||
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
|
||||
|
@ -344,7 +344,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
|
||||
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
||||
let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, goal_evaluation_kind);
|
||||
let mut goal_evaluation =
|
||||
self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
|
||||
let encountered_overflow = self.search_graph.encountered_overflow();
|
||||
let canonical_response = EvalCtxt::evaluate_canonical_goal(
|
||||
self.tcx(),
|
||||
@ -568,7 +569,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
|
||||
unconstrained_goal,
|
||||
)?;
|
||||
self.add_goals(instantiate_goals);
|
||||
self.nested_goals.goals.extend(instantiate_goals);
|
||||
|
||||
// Finally, equate the goal's RHS with the unconstrained var.
|
||||
// We put the nested goals from this into goals instead of
|
||||
@ -605,7 +606,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
|
||||
goal,
|
||||
)?;
|
||||
self.add_goals(instantiate_goals);
|
||||
self.nested_goals.goals.extend(instantiate_goals);
|
||||
if has_changed {
|
||||
unchanged_certainty = None;
|
||||
}
|
||||
@ -613,7 +614,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
match certainty {
|
||||
Certainty::Yes => {}
|
||||
Certainty::Maybe(_) => {
|
||||
self.add_goal(goal);
|
||||
self.nested_goals.goals.push(goal);
|
||||
unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
|
||||
}
|
||||
}
|
||||
|
@ -10,17 +10,21 @@
|
||||
//! [c]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
|
||||
use super::{CanonicalInput, Certainty, EvalCtxt, Goal};
|
||||
use crate::solve::canonicalize::{CanonicalizeMode, Canonicalizer};
|
||||
use crate::solve::{response_no_constraints_raw, CanonicalResponse, QueryResult, Response};
|
||||
use crate::solve::{
|
||||
inspect, response_no_constraints_raw, CanonicalResponse, QueryResult, Response,
|
||||
};
|
||||
use rustc_data_structures::fx::FxHashSet;
|
||||
use rustc_index::IndexVec;
|
||||
use rustc_infer::infer::canonical::query_response::make_query_region_constraints;
|
||||
use rustc_infer::infer::canonical::CanonicalVarValues;
|
||||
use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
|
||||
use rustc_infer::infer::InferCtxt;
|
||||
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
|
||||
use rustc_middle::infer::canonical::Canonical;
|
||||
use rustc_middle::traits::query::NoSolution;
|
||||
use rustc_middle::traits::solve::{
|
||||
ExternalConstraintsData, MaybeCause, PredefinedOpaquesData, QueryInput,
|
||||
};
|
||||
use rustc_middle::traits::ObligationCause;
|
||||
use rustc_middle::ty::{
|
||||
self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable, TypeFolder, TypeSuperFoldable,
|
||||
TypeVisitableExt,
|
||||
@ -29,6 +33,22 @@ use rustc_span::DUMMY_SP;
|
||||
use std::iter;
|
||||
use std::ops::Deref;
|
||||
|
||||
trait ResponseT<'tcx> {
|
||||
fn var_values(&self) -> CanonicalVarValues<'tcx>;
|
||||
}
|
||||
|
||||
impl<'tcx> ResponseT<'tcx> for Response<'tcx> {
|
||||
fn var_values(&self) -> CanonicalVarValues<'tcx> {
|
||||
self.var_values
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx, T> ResponseT<'tcx> for inspect::State<'tcx, T> {
|
||||
fn var_values(&self) -> CanonicalVarValues<'tcx> {
|
||||
self.var_values
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
/// Canonicalizes the goal remembering the original values
|
||||
/// for each bound variable.
|
||||
@ -188,12 +208,14 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
original_values: Vec<ty::GenericArg<'tcx>>,
|
||||
response: CanonicalResponse<'tcx>,
|
||||
) -> Result<(Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
|
||||
let substitution = self.compute_query_response_substitution(&original_values, &response);
|
||||
let substitution =
|
||||
Self::compute_query_response_substitution(self.infcx, &original_values, &response);
|
||||
|
||||
let Response { var_values, external_constraints, certainty } =
|
||||
response.substitute(self.tcx(), &substitution);
|
||||
|
||||
let nested_goals = self.unify_query_var_values(param_env, &original_values, var_values)?;
|
||||
let nested_goals =
|
||||
Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values)?;
|
||||
|
||||
let ExternalConstraintsData { region_constraints, opaque_types } =
|
||||
external_constraints.deref();
|
||||
@ -206,21 +228,21 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
/// This returns the substitutions to instantiate the bound variables of
|
||||
/// the canonical response. This depends on the `original_values` for the
|
||||
/// bound variables.
|
||||
fn compute_query_response_substitution(
|
||||
&self,
|
||||
fn compute_query_response_substitution<T: ResponseT<'tcx>>(
|
||||
infcx: &InferCtxt<'tcx>,
|
||||
original_values: &[ty::GenericArg<'tcx>],
|
||||
response: &CanonicalResponse<'tcx>,
|
||||
response: &Canonical<'tcx, T>,
|
||||
) -> CanonicalVarValues<'tcx> {
|
||||
// FIXME: Longterm canonical queries should deal with all placeholders
|
||||
// created inside of the query directly instead of returning them to the
|
||||
// caller.
|
||||
let prev_universe = self.infcx.universe();
|
||||
let prev_universe = infcx.universe();
|
||||
let universes_created_in_query = response.max_universe.index();
|
||||
for _ in 0..universes_created_in_query {
|
||||
self.infcx.create_next_universe();
|
||||
infcx.create_next_universe();
|
||||
}
|
||||
|
||||
let var_values = response.value.var_values;
|
||||
let var_values = response.value.var_values();
|
||||
assert_eq!(original_values.len(), var_values.len());
|
||||
|
||||
// If the query did not make progress with constraining inference variables,
|
||||
@ -254,13 +276,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
let var_values = self.tcx().mk_args_from_iter(response.variables.iter().enumerate().map(
|
||||
let var_values = infcx.tcx.mk_args_from_iter(response.variables.iter().enumerate().map(
|
||||
|(index, info)| {
|
||||
if info.universe() != ty::UniverseIndex::ROOT {
|
||||
// A variable from inside a binder of the query. While ideally these shouldn't
|
||||
// exist at all (see the FIXME at the start of this method), we have to deal with
|
||||
// them for now.
|
||||
self.infcx.instantiate_canonical_var(DUMMY_SP, info, |idx| {
|
||||
infcx.instantiate_canonical_var(DUMMY_SP, info, |idx| {
|
||||
ty::UniverseIndex::from(prev_universe.index() + idx.index())
|
||||
})
|
||||
} else if info.is_existential() {
|
||||
@ -274,7 +296,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
if let Some(v) = opt_values[BoundVar::from_usize(index)] {
|
||||
v
|
||||
} else {
|
||||
self.infcx.instantiate_canonical_var(DUMMY_SP, info, |_| prev_universe)
|
||||
infcx.instantiate_canonical_var(DUMMY_SP, info, |_| prev_universe)
|
||||
}
|
||||
} else {
|
||||
// For placeholders which were already part of the input, we simply map this
|
||||
@ -287,9 +309,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
CanonicalVarValues { var_values }
|
||||
}
|
||||
|
||||
#[instrument(level = "debug", skip(self, param_env), ret)]
|
||||
#[instrument(level = "debug", skip(infcx, param_env), ret)]
|
||||
fn unify_query_var_values(
|
||||
&self,
|
||||
infcx: &InferCtxt<'tcx>,
|
||||
param_env: ty::ParamEnv<'tcx>,
|
||||
original_values: &[ty::GenericArg<'tcx>],
|
||||
var_values: CanonicalVarValues<'tcx>,
|
||||
@ -298,7 +320,18 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
|
||||
let mut nested_goals = vec![];
|
||||
for (&orig, response) in iter::zip(original_values, var_values.var_values) {
|
||||
nested_goals.extend(self.eq_and_get_goals(param_env, orig, response)?);
|
||||
nested_goals.extend(
|
||||
infcx
|
||||
.at(&ObligationCause::dummy(), param_env)
|
||||
.eq(DefineOpaqueTypes::No, orig, response)
|
||||
.map(|InferOk { value: (), obligations }| {
|
||||
obligations.into_iter().map(|o| Goal::from(o))
|
||||
})
|
||||
.map_err(|e| {
|
||||
debug!(?e, "failed to equate");
|
||||
NoSolution
|
||||
})?,
|
||||
);
|
||||
}
|
||||
|
||||
Ok(nested_goals)
|
||||
@ -403,3 +436,35 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for EagerResolver<'_, 'tcx> {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> inspect::ProofTreeBuilder<'tcx> {
|
||||
pub fn make_canonical_state<T: TypeFoldable<TyCtxt<'tcx>>>(
|
||||
ecx: &EvalCtxt<'_, 'tcx>,
|
||||
data: T,
|
||||
) -> inspect::CanonicalState<'tcx, T> {
|
||||
let state = inspect::State { var_values: ecx.var_values, data };
|
||||
let state = state.fold_with(&mut EagerResolver { infcx: ecx.infcx });
|
||||
Canonicalizer::canonicalize(
|
||||
ecx.infcx,
|
||||
CanonicalizeMode::Response { max_input_universe: ecx.max_input_universe },
|
||||
&mut vec![],
|
||||
state,
|
||||
)
|
||||
}
|
||||
|
||||
pub fn instantiate_canonical_state<T: TypeFoldable<TyCtxt<'tcx>>>(
|
||||
infcx: &InferCtxt<'tcx>,
|
||||
param_env: ty::ParamEnv<'tcx>,
|
||||
original_values: &[ty::GenericArg<'tcx>],
|
||||
state: inspect::CanonicalState<'tcx, T>,
|
||||
) -> Result<(Vec<Goal<'tcx, ty::Predicate<'tcx>>>, T), NoSolution> {
|
||||
let substitution =
|
||||
EvalCtxt::compute_query_response_substitution(infcx, original_values, &state);
|
||||
|
||||
let inspect::State { var_values, data } = state.substitute(infcx.tcx, &substitution);
|
||||
|
||||
let nested_goals =
|
||||
EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values)?;
|
||||
Ok((nested_goals, data))
|
||||
}
|
||||
}
|
||||
|
226
compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
Normal file
226
compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
Normal file
@ -0,0 +1,226 @@
|
||||
/// An infrastructure to mechanically analyse proof trees.
|
||||
///
|
||||
/// It is unavoidable that this representation is somewhat
|
||||
/// lossy as it should hide quite a few semantically relevant things,
|
||||
/// e.g. canonicalization and the order of nested goals.
|
||||
///
|
||||
/// @lcnr: However, a lot of the weirdness here is not strictly necessary
|
||||
/// and could be improved in the future. This is mostly good enough for
|
||||
/// coherence right now and was annoying to implement, so I am leaving it
|
||||
/// as is until we start using it for something else.
|
||||
use std::ops::ControlFlow;
|
||||
|
||||
use rustc_infer::infer::InferCtxt;
|
||||
use rustc_middle::traits::query::NoSolution;
|
||||
use rustc_middle::traits::solve::{inspect, QueryResult};
|
||||
use rustc_middle::traits::solve::{Certainty, Goal};
|
||||
use rustc_middle::ty;
|
||||
|
||||
use crate::solve::inspect::ProofTreeBuilder;
|
||||
use crate::solve::{GenerateProofTree, InferCtxtEvalExt, UseGlobalCache};
|
||||
|
||||
pub struct InspectGoal<'a, 'tcx> {
|
||||
infcx: &'a InferCtxt<'tcx>,
|
||||
depth: usize,
|
||||
orig_values: &'a [ty::GenericArg<'tcx>],
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
evaluation: &'a inspect::GoalEvaluation<'tcx>,
|
||||
}
|
||||
|
||||
pub struct InspectCandidate<'a, 'tcx> {
|
||||
goal: &'a InspectGoal<'a, 'tcx>,
|
||||
kind: inspect::ProbeKind<'tcx>,
|
||||
nested_goals: Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
||||
result: QueryResult<'tcx>,
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
|
||||
pub fn infcx(&self) -> &'a InferCtxt<'tcx> {
|
||||
self.goal.infcx
|
||||
}
|
||||
|
||||
pub fn kind(&self) -> inspect::ProbeKind<'tcx> {
|
||||
self.kind
|
||||
}
|
||||
|
||||
pub fn result(&self) -> Result<Certainty, NoSolution> {
|
||||
self.result.map(|c| c.value.certainty)
|
||||
}
|
||||
|
||||
/// Visit the nested goals of this candidate.
|
||||
///
|
||||
/// FIXME(@lcnr): we have to slightly adapt this API
|
||||
/// to also use it to compute the most relevant goal
|
||||
/// for fulfillment errors. Will do that once we actually
|
||||
/// need it.
|
||||
pub fn visit_nested<V: ProofTreeVisitor<'tcx>>(
|
||||
&self,
|
||||
visitor: &mut V,
|
||||
) -> ControlFlow<V::BreakTy> {
|
||||
// HACK: An arbitrary cutoff to avoid dealing with overflow and cycles.
|
||||
if self.goal.depth >= 10 {
|
||||
let infcx = self.goal.infcx;
|
||||
infcx.probe(|_| {
|
||||
let mut instantiated_goals = vec![];
|
||||
for goal in &self.nested_goals {
|
||||
let goal = match ProofTreeBuilder::instantiate_canonical_state(
|
||||
infcx,
|
||||
self.goal.goal.param_env,
|
||||
self.goal.orig_values,
|
||||
*goal,
|
||||
) {
|
||||
Ok((_goals, goal)) => goal,
|
||||
Err(NoSolution) => {
|
||||
warn!(
|
||||
"unexpected failure when instantiating {:?}: {:?}",
|
||||
goal, self.nested_goals
|
||||
);
|
||||
return ControlFlow::Continue(());
|
||||
}
|
||||
};
|
||||
instantiated_goals.push(goal);
|
||||
}
|
||||
|
||||
for &goal in &instantiated_goals {
|
||||
let (_, proof_tree) =
|
||||
infcx.evaluate_root_goal(goal, GenerateProofTree::Yes(UseGlobalCache::No));
|
||||
let proof_tree = proof_tree.unwrap();
|
||||
visitor.visit_goal(&InspectGoal::new(
|
||||
infcx,
|
||||
self.goal.depth + 1,
|
||||
&proof_tree,
|
||||
))?;
|
||||
}
|
||||
|
||||
ControlFlow::Continue(())
|
||||
})?;
|
||||
}
|
||||
ControlFlow::Continue(())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
||||
pub fn infcx(&self) -> &'a InferCtxt<'tcx> {
|
||||
self.infcx
|
||||
}
|
||||
|
||||
pub fn goal(&self) -> Goal<'tcx, ty::Predicate<'tcx>> {
|
||||
self.goal
|
||||
}
|
||||
|
||||
pub fn result(&self) -> Result<Certainty, NoSolution> {
|
||||
self.evaluation.evaluation.result.map(|c| c.value.certainty)
|
||||
}
|
||||
|
||||
fn candidates_recur(
|
||||
&'a self,
|
||||
candidates: &mut Vec<InspectCandidate<'a, 'tcx>>,
|
||||
nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
|
||||
probe: &inspect::Probe<'tcx>,
|
||||
) {
|
||||
for step in &probe.steps {
|
||||
match step {
|
||||
&inspect::ProbeStep::AddGoal(goal) => nested_goals.push(goal),
|
||||
inspect::ProbeStep::EvaluateGoals(_) => (),
|
||||
inspect::ProbeStep::NestedProbe(ref probe) => {
|
||||
let num_goals = nested_goals.len();
|
||||
self.candidates_recur(candidates, nested_goals, probe);
|
||||
nested_goals.truncate(num_goals);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
match probe.kind {
|
||||
inspect::ProbeKind::Root { result: _ }
|
||||
| inspect::ProbeKind::NormalizedSelfTyAssembly
|
||||
| inspect::ProbeKind::UnsizeAssembly
|
||||
| inspect::ProbeKind::UpcastProjectionCompatibility => (),
|
||||
inspect::ProbeKind::MiscCandidate { name: _, result }
|
||||
| inspect::ProbeKind::TraitCandidate { source: _, result } => {
|
||||
candidates.push(InspectCandidate {
|
||||
goal: self,
|
||||
kind: probe.kind,
|
||||
nested_goals: nested_goals.clone(),
|
||||
result,
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> {
|
||||
let mut candidates = vec![];
|
||||
let last_eval_step = match self.evaluation.evaluation.kind {
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
| inspect::CanonicalGoalEvaluationKind::CacheHit(_) => {
|
||||
warn!("unexpected root evaluation: {:?}", self.evaluation);
|
||||
return vec![];
|
||||
}
|
||||
inspect::CanonicalGoalEvaluationKind::Uncached { ref revisions } => {
|
||||
if let Some(last) = revisions.last() {
|
||||
last
|
||||
} else {
|
||||
return vec![];
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
let mut nested_goals = vec![];
|
||||
self.candidates_recur(&mut candidates, &mut nested_goals, &last_eval_step.evaluation);
|
||||
|
||||
if candidates.is_empty() {
|
||||
candidates.push(InspectCandidate {
|
||||
goal: self,
|
||||
kind: last_eval_step.evaluation.kind,
|
||||
nested_goals,
|
||||
result: self.evaluation.evaluation.result,
|
||||
});
|
||||
}
|
||||
|
||||
candidates
|
||||
}
|
||||
|
||||
fn new(
|
||||
infcx: &'a InferCtxt<'tcx>,
|
||||
depth: usize,
|
||||
root: &'a inspect::GoalEvaluation<'tcx>,
|
||||
) -> Self {
|
||||
match root.kind {
|
||||
inspect::GoalEvaluationKind::Root { ref orig_values } => InspectGoal {
|
||||
infcx,
|
||||
depth,
|
||||
orig_values,
|
||||
goal: infcx.resolve_vars_if_possible(root.uncanonicalized_goal),
|
||||
evaluation: root,
|
||||
},
|
||||
inspect::GoalEvaluationKind::Nested { .. } => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// The public API to interact with proof trees.
|
||||
pub trait ProofTreeVisitor<'tcx> {
|
||||
type BreakTy;
|
||||
|
||||
fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> ControlFlow<Self::BreakTy>;
|
||||
}
|
||||
|
||||
pub trait ProofTreeInferCtxtExt<'tcx> {
|
||||
fn visit_proof_tree<V: ProofTreeVisitor<'tcx>>(
|
||||
&self,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
visitor: &mut V,
|
||||
) -> ControlFlow<V::BreakTy>;
|
||||
}
|
||||
|
||||
impl<'tcx> ProofTreeInferCtxtExt<'tcx> for InferCtxt<'tcx> {
|
||||
fn visit_proof_tree<V: ProofTreeVisitor<'tcx>>(
|
||||
&self,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
visitor: &mut V,
|
||||
) -> ControlFlow<V::BreakTy> {
|
||||
let (_, proof_tree) =
|
||||
self.evaluate_root_goal(goal, GenerateProofTree::Yes(UseGlobalCache::No));
|
||||
let proof_tree = proof_tree.unwrap();
|
||||
visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree))
|
||||
}
|
||||
}
|
@ -1,153 +1,53 @@
|
||||
//! Building proof trees incrementally during trait solving.
|
||||
//!
|
||||
//! This code is *a bit* of a mess and can hopefully be
|
||||
//! mostly ignored. For a general overview of how it works,
|
||||
//! see the comment on [ProofTreeBuilder].
|
||||
use rustc_middle::traits::query::NoSolution;
|
||||
use rustc_middle::traits::solve::inspect::{self, CacheHit, ProbeKind};
|
||||
use rustc_middle::traits::solve::{
|
||||
CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult,
|
||||
};
|
||||
use rustc_middle::ty::{self, TyCtxt};
|
||||
use rustc_session::config::DumpSolverProofTree;
|
||||
|
||||
use super::eval_ctxt::UseGlobalCache;
|
||||
use super::{GenerateProofTree, GoalEvaluationKind};
|
||||
use crate::solve::eval_ctxt::UseGlobalCache;
|
||||
use crate::solve::{self, inspect, EvalCtxt, GenerateProofTree};
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipGoalEvaluation<'tcx> {
|
||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
pub kind: WipGoalEvaluationKind,
|
||||
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||
/// The core data structure when building proof trees.
|
||||
///
|
||||
/// In case the current evaluation does not generate a proof
|
||||
/// tree, `state` is simply `None` and we avoid any work.
|
||||
///
|
||||
/// The possible states of the solver are represented via
|
||||
/// variants of [DebugSolver]. For any nested computation we call
|
||||
/// `ProofTreeBuilder::new_nested_computation_kind` which
|
||||
/// creates a new `ProofTreeBuilder` to temporarily replace the
|
||||
/// current one. Once that nested computation is done,
|
||||
/// `ProofTreeBuilder::nested_computation_kind` is called
|
||||
/// to add the finished nested evaluation to the parent.
|
||||
///
|
||||
/// We provide additional information to the current state
|
||||
/// by calling methods such as `ProofTreeBuilder::probe_kind`.
|
||||
///
|
||||
/// The actual structure closely mirrors the finished proof
|
||||
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
|
||||
/// is called to recursively convert the whole structure to a
|
||||
/// finished proof tree.
|
||||
pub(in crate::solve) struct ProofTreeBuilder<'tcx> {
|
||||
state: Option<Box<BuilderData<'tcx>>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||
pub fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
|
||||
inspect::GoalEvaluation {
|
||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||
kind: match self.kind {
|
||||
WipGoalEvaluationKind::Root => inspect::GoalEvaluationKind::Root,
|
||||
WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||
}
|
||||
},
|
||||
evaluation: self.evaluation.unwrap().finalize(),
|
||||
returned_goals: self.returned_goals,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipGoalEvaluationKind {
|
||||
Root,
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipCanonicalGoalEvaluationKind {
|
||||
Overflow,
|
||||
CacheHit(CacheHit),
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipCanonicalGoalEvaluation<'tcx> {
|
||||
pub goal: CanonicalInput<'tcx>,
|
||||
pub kind: Option<WipCanonicalGoalEvaluationKind>,
|
||||
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
||||
pub result: Option<QueryResult<'tcx>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
||||
pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
|
||||
let kind = match self.kind {
|
||||
Some(WipCanonicalGoalEvaluationKind::Overflow) => {
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
}
|
||||
Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
|
||||
inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
|
||||
}
|
||||
None => inspect::CanonicalGoalEvaluationKind::Uncached {
|
||||
revisions: self
|
||||
.revisions
|
||||
.into_iter()
|
||||
.map(WipGoalEvaluationStep::finalize)
|
||||
.collect(),
|
||||
},
|
||||
};
|
||||
|
||||
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipAddedGoalsEvaluation<'tcx> {
|
||||
pub evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
|
||||
pub result: Option<Result<Certainty, NoSolution>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
||||
pub fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
|
||||
inspect::AddedGoalsEvaluation {
|
||||
evaluations: self
|
||||
.evaluations
|
||||
.into_iter()
|
||||
.map(|evaluations| {
|
||||
evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
|
||||
})
|
||||
.collect(),
|
||||
result: self.result.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipGoalEvaluationStep<'tcx> {
|
||||
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||
|
||||
pub evaluation: WipProbe<'tcx>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||
pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
|
||||
let evaluation = self.evaluation.finalize();
|
||||
match evaluation.kind {
|
||||
ProbeKind::Root { .. } => (),
|
||||
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
|
||||
}
|
||||
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub struct WipProbe<'tcx> {
|
||||
pub steps: Vec<WipProbeStep<'tcx>>,
|
||||
pub kind: Option<ProbeKind<'tcx>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipProbe<'tcx> {
|
||||
pub fn finalize(self) -> inspect::Probe<'tcx> {
|
||||
inspect::Probe {
|
||||
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
||||
kind: self.kind.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub enum WipProbeStep<'tcx> {
|
||||
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
|
||||
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
||||
NestedProbe(WipProbe<'tcx>),
|
||||
}
|
||||
|
||||
impl<'tcx> WipProbeStep<'tcx> {
|
||||
pub fn finalize(self) -> inspect::ProbeStep<'tcx> {
|
||||
match self {
|
||||
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
|
||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||
}
|
||||
}
|
||||
struct BuilderData<'tcx> {
|
||||
tree: DebugSolver<'tcx>,
|
||||
use_global_cache: UseGlobalCache,
|
||||
}
|
||||
|
||||
/// The current state of the proof tree builder, at most places
|
||||
/// in the code, only one or two variants are actually possible.
|
||||
///
|
||||
/// We simply ICE in case that assumption is broken.
|
||||
#[derive(Debug)]
|
||||
pub enum DebugSolver<'tcx> {
|
||||
enum DebugSolver<'tcx> {
|
||||
Root,
|
||||
GoalEvaluation(WipGoalEvaluation<'tcx>),
|
||||
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
|
||||
@ -186,13 +86,143 @@ impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
pub struct ProofTreeBuilder<'tcx> {
|
||||
state: Option<Box<BuilderData<'tcx>>>,
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
struct WipGoalEvaluation<'tcx> {
|
||||
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
pub kind: WipGoalEvaluationKind<'tcx>,
|
||||
pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
|
||||
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||
}
|
||||
|
||||
struct BuilderData<'tcx> {
|
||||
tree: DebugSolver<'tcx>,
|
||||
use_global_cache: UseGlobalCache,
|
||||
impl<'tcx> WipGoalEvaluation<'tcx> {
|
||||
fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
|
||||
inspect::GoalEvaluation {
|
||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||
kind: match self.kind {
|
||||
WipGoalEvaluationKind::Root { orig_values } => {
|
||||
inspect::GoalEvaluationKind::Root { orig_values }
|
||||
}
|
||||
WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||
}
|
||||
},
|
||||
evaluation: self.evaluation.unwrap().finalize(),
|
||||
returned_goals: self.returned_goals,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub(in crate::solve) enum WipGoalEvaluationKind<'tcx> {
|
||||
Root { orig_values: Vec<ty::GenericArg<'tcx>> },
|
||||
Nested { is_normalizes_to_hack: IsNormalizesToHack },
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind {
|
||||
Overflow,
|
||||
CacheHit(inspect::CacheHit),
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
struct WipCanonicalGoalEvaluation<'tcx> {
|
||||
goal: CanonicalInput<'tcx>,
|
||||
kind: Option<WipCanonicalGoalEvaluationKind>,
|
||||
revisions: Vec<WipGoalEvaluationStep<'tcx>>,
|
||||
result: Option<QueryResult<'tcx>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
|
||||
fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
|
||||
let kind = match self.kind {
|
||||
Some(WipCanonicalGoalEvaluationKind::Overflow) => {
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
}
|
||||
Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
|
||||
inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
|
||||
}
|
||||
None => inspect::CanonicalGoalEvaluationKind::Uncached {
|
||||
revisions: self
|
||||
.revisions
|
||||
.into_iter()
|
||||
.map(WipGoalEvaluationStep::finalize)
|
||||
.collect(),
|
||||
},
|
||||
};
|
||||
|
||||
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
struct WipAddedGoalsEvaluation<'tcx> {
|
||||
evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
|
||||
result: Option<Result<Certainty, NoSolution>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
|
||||
fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
|
||||
inspect::AddedGoalsEvaluation {
|
||||
evaluations: self
|
||||
.evaluations
|
||||
.into_iter()
|
||||
.map(|evaluations| {
|
||||
evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
|
||||
})
|
||||
.collect(),
|
||||
result: self.result.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
struct WipGoalEvaluationStep<'tcx> {
|
||||
instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
|
||||
|
||||
evaluation: WipProbe<'tcx>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipGoalEvaluationStep<'tcx> {
|
||||
fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
|
||||
let evaluation = self.evaluation.finalize();
|
||||
match evaluation.kind {
|
||||
inspect::ProbeKind::Root { .. } => (),
|
||||
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
|
||||
}
|
||||
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
struct WipProbe<'tcx> {
|
||||
pub steps: Vec<WipProbeStep<'tcx>>,
|
||||
pub kind: Option<inspect::ProbeKind<'tcx>>,
|
||||
}
|
||||
|
||||
impl<'tcx> WipProbe<'tcx> {
|
||||
fn finalize(self) -> inspect::Probe<'tcx> {
|
||||
inspect::Probe {
|
||||
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
|
||||
kind: self.kind.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, PartialEq, Debug)]
|
||||
enum WipProbeStep<'tcx> {
|
||||
AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
|
||||
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
|
||||
NestedProbe(WipProbe<'tcx>),
|
||||
}
|
||||
|
||||
impl<'tcx> WipProbeStep<'tcx> {
|
||||
fn finalize(self) -> inspect::ProbeStep<'tcx> {
|
||||
match self {
|
||||
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
|
||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
@ -273,16 +303,19 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
self.state.is_none()
|
||||
}
|
||||
|
||||
pub(super) fn new_goal_evaluation(
|
||||
pub(in crate::solve) fn new_goal_evaluation(
|
||||
&mut self,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
kind: GoalEvaluationKind,
|
||||
orig_values: &[ty::GenericArg<'tcx>],
|
||||
kind: solve::GoalEvaluationKind,
|
||||
) -> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipGoalEvaluation {
|
||||
uncanonicalized_goal: goal,
|
||||
kind: match kind {
|
||||
GoalEvaluationKind::Root => WipGoalEvaluationKind::Root,
|
||||
GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
solve::GoalEvaluationKind::Root => {
|
||||
WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
|
||||
}
|
||||
solve::GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
|
||||
WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
|
||||
}
|
||||
},
|
||||
@ -379,7 +412,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
self.nested(|| WipProbe { steps: vec![], kind: None })
|
||||
}
|
||||
|
||||
pub fn probe_kind(&mut self, probe_kind: ProbeKind<'tcx>) {
|
||||
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::Probe(this) => {
|
||||
@ -390,18 +423,22 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||
evaluation: WipProbe { steps, .. },
|
||||
..
|
||||
})
|
||||
| DebugSolver::Probe(WipProbe { steps, .. }) => {
|
||||
steps.push(WipProbeStep::AddGoal(goal))
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
pub fn add_goal(ecx: &mut EvalCtxt<'_, 'tcx>, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
|
||||
// Can't use `if let Some(this) = ecx.inspect.as_mut()` here because
|
||||
// we have to immutably use the `EvalCtxt` for `make_canonical_state`.
|
||||
if ecx.inspect.is_noop() {
|
||||
return;
|
||||
}
|
||||
|
||||
let goal = Self::make_canonical_state(ecx, goal);
|
||||
|
||||
match ecx.inspect.as_mut().unwrap() {
|
||||
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
|
||||
evaluation: WipProbe { steps, .. },
|
||||
..
|
||||
})
|
||||
| DebugSolver::Probe(WipProbe { steps, .. }) => steps.push(WipProbeStep::AddGoal(goal)),
|
||||
s => unreachable!("tried to add {goal:?} to {s:?}"),
|
||||
}
|
||||
}
|
||||
|
||||
@ -471,7 +508,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
|
||||
}
|
||||
DebugSolver::GoalEvaluationStep(evaluation_step) => {
|
||||
assert_eq!(
|
||||
evaluation_step.evaluation.kind.replace(ProbeKind::Root { result }),
|
||||
evaluation_step
|
||||
.evaluation
|
||||
.kind
|
||||
.replace(inspect::ProbeKind::Root { result }),
|
||||
None
|
||||
);
|
||||
}
|
7
compiler/rustc_trait_selection/src/solve/inspect/mod.rs
Normal file
7
compiler/rustc_trait_selection/src/solve/inspect/mod.rs
Normal file
@ -0,0 +1,7 @@
|
||||
pub use rustc_middle::traits::solve::inspect::*;
|
||||
|
||||
mod build;
|
||||
pub(in crate::solve) use build::*;
|
||||
|
||||
mod analyse;
|
||||
pub use analyse::*;
|
@ -235,7 +235,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||
|
||||
#[instrument(level = "debug", skip(self))]
|
||||
fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
|
||||
self.inspect.add_goal(goal);
|
||||
inspect::ProofTreeBuilder::add_goal(self, goal);
|
||||
self.nested_goals.goals.push(goal);
|
||||
}
|
||||
|
||||
|
@ -6,9 +6,15 @@
|
||||
|
||||
use crate::infer::outlives::env::OutlivesEnvironment;
|
||||
use crate::infer::InferOk;
|
||||
use crate::solve::inspect;
|
||||
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
|
||||
use crate::traits::engine::TraitEngineExt;
|
||||
use crate::traits::outlives_bounds::InferCtxtExt as _;
|
||||
use crate::traits::query::evaluate_obligation::InferCtxtExt;
|
||||
use crate::traits::select::{IntercrateAmbiguityCause, TreatInductiveCycleAs};
|
||||
use crate::traits::structural_normalize::StructurallyNormalizeExt;
|
||||
use crate::traits::util::impl_subject_and_oblig;
|
||||
use crate::traits::NormalizeExt;
|
||||
use crate::traits::SkipLeakCheck;
|
||||
use crate::traits::{
|
||||
self, Obligation, ObligationCause, ObligationCtxt, PredicateObligation, PredicateObligations,
|
||||
@ -18,10 +24,13 @@ use rustc_data_structures::fx::FxIndexSet;
|
||||
use rustc_errors::Diagnostic;
|
||||
use rustc_hir::def_id::{DefId, CRATE_DEF_ID, LOCAL_CRATE};
|
||||
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
|
||||
use rustc_infer::traits::util;
|
||||
use rustc_infer::traits::{util, TraitEngine};
|
||||
use rustc_middle::traits::query::NoSolution;
|
||||
use rustc_middle::traits::solve::{Certainty, Goal};
|
||||
use rustc_middle::traits::specialization_graph::OverlapMode;
|
||||
use rustc_middle::traits::DefiningAnchor;
|
||||
use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
|
||||
use rustc_middle::ty::print::with_no_trimmed_paths;
|
||||
use rustc_middle::ty::visit::{TypeVisitable, TypeVisitableExt};
|
||||
use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitor};
|
||||
use rustc_session::lint::builtin::COINDUCTIVE_OVERLAP_IN_COHERENCE;
|
||||
@ -31,9 +40,6 @@ use std::fmt::Debug;
|
||||
use std::iter;
|
||||
use std::ops::ControlFlow;
|
||||
|
||||
use super::query::evaluate_obligation::InferCtxtExt;
|
||||
use super::NormalizeExt;
|
||||
|
||||
/// Whether we do the orphan check relative to this crate or
|
||||
/// to some remote crate.
|
||||
#[derive(Copy, Clone, Debug)]
|
||||
@ -205,72 +211,79 @@ fn overlap<'tcx>(
|
||||
|
||||
// Equate the headers to find their intersection (the general type, with infer vars,
|
||||
// that may apply both impls).
|
||||
let equate_obligations = equate_impl_headers(selcx.infcx, &impl1_header, &impl2_header)?;
|
||||
let mut obligations = equate_impl_headers(selcx.infcx, &impl1_header, &impl2_header)?;
|
||||
debug!("overlap: unification check succeeded");
|
||||
|
||||
if overlap_mode.use_implicit_negative() {
|
||||
for mode in [TreatInductiveCycleAs::Ambig, TreatInductiveCycleAs::Recur] {
|
||||
if let Some(failing_obligation) = selcx.with_treat_inductive_cycle_as(mode, |selcx| {
|
||||
impl_intersection_has_impossible_obligation(
|
||||
selcx,
|
||||
param_env,
|
||||
&impl1_header,
|
||||
&impl2_header,
|
||||
&equate_obligations,
|
||||
)
|
||||
}) {
|
||||
if matches!(mode, TreatInductiveCycleAs::Recur) {
|
||||
let first_local_impl = impl1_header
|
||||
.impl_def_id
|
||||
.as_local()
|
||||
.or(impl2_header.impl_def_id.as_local())
|
||||
.expect("expected one of the impls to be local");
|
||||
infcx.tcx.struct_span_lint_hir(
|
||||
COINDUCTIVE_OVERLAP_IN_COHERENCE,
|
||||
infcx.tcx.local_def_id_to_hir_id(first_local_impl),
|
||||
infcx.tcx.def_span(first_local_impl),
|
||||
format!(
|
||||
"implementations {} will conflict in the future",
|
||||
match impl1_header.trait_ref {
|
||||
Some(trait_ref) => {
|
||||
let trait_ref = infcx.resolve_vars_if_possible(trait_ref);
|
||||
format!(
|
||||
"of `{}` for `{}`",
|
||||
trait_ref.print_only_trait_path(),
|
||||
trait_ref.self_ty()
|
||||
)
|
||||
}
|
||||
None => format!(
|
||||
"for `{}`",
|
||||
infcx.resolve_vars_if_possible(impl1_header.self_ty)
|
||||
),
|
||||
},
|
||||
),
|
||||
|lint| {
|
||||
lint.note(
|
||||
"impls that are not considered to overlap may be considered to \
|
||||
overlap in the future",
|
||||
)
|
||||
.span_label(
|
||||
infcx.tcx.def_span(impl1_header.impl_def_id),
|
||||
"the first impl is here",
|
||||
)
|
||||
.span_label(
|
||||
infcx.tcx.def_span(impl2_header.impl_def_id),
|
||||
"the second impl is here",
|
||||
);
|
||||
lint.note(format!(
|
||||
"`{}` may be considered to hold in future releases, \
|
||||
causing the impls to overlap",
|
||||
infcx.resolve_vars_if_possible(failing_obligation.predicate)
|
||||
));
|
||||
lint
|
||||
},
|
||||
);
|
||||
}
|
||||
if !overlap_mode.use_implicit_negative() {
|
||||
let impl_header = selcx.infcx.resolve_vars_if_possible(impl1_header);
|
||||
return Some(OverlapResult {
|
||||
impl_header,
|
||||
intercrate_ambiguity_causes: Default::default(),
|
||||
involves_placeholder: false,
|
||||
});
|
||||
};
|
||||
|
||||
return None;
|
||||
obligations.extend(
|
||||
[&impl1_header.predicates, &impl2_header.predicates].into_iter().flatten().map(
|
||||
|&predicate| Obligation::new(infcx.tcx, ObligationCause::dummy(), param_env, predicate),
|
||||
),
|
||||
);
|
||||
|
||||
for mode in [TreatInductiveCycleAs::Ambig, TreatInductiveCycleAs::Recur] {
|
||||
if let Some(failing_obligation) = selcx.with_treat_inductive_cycle_as(mode, |selcx| {
|
||||
impl_intersection_has_impossible_obligation(selcx, &obligations)
|
||||
}) {
|
||||
if matches!(mode, TreatInductiveCycleAs::Recur) {
|
||||
let first_local_impl = impl1_header
|
||||
.impl_def_id
|
||||
.as_local()
|
||||
.or(impl2_header.impl_def_id.as_local())
|
||||
.expect("expected one of the impls to be local");
|
||||
infcx.tcx.struct_span_lint_hir(
|
||||
COINDUCTIVE_OVERLAP_IN_COHERENCE,
|
||||
infcx.tcx.local_def_id_to_hir_id(first_local_impl),
|
||||
infcx.tcx.def_span(first_local_impl),
|
||||
format!(
|
||||
"implementations {} will conflict in the future",
|
||||
match impl1_header.trait_ref {
|
||||
Some(trait_ref) => {
|
||||
let trait_ref = infcx.resolve_vars_if_possible(trait_ref);
|
||||
format!(
|
||||
"of `{}` for `{}`",
|
||||
trait_ref.print_only_trait_path(),
|
||||
trait_ref.self_ty()
|
||||
)
|
||||
}
|
||||
None => format!(
|
||||
"for `{}`",
|
||||
infcx.resolve_vars_if_possible(impl1_header.self_ty)
|
||||
),
|
||||
},
|
||||
),
|
||||
|lint| {
|
||||
lint.note(
|
||||
"impls that are not considered to overlap may be considered to \
|
||||
overlap in the future",
|
||||
)
|
||||
.span_label(
|
||||
infcx.tcx.def_span(impl1_header.impl_def_id),
|
||||
"the first impl is here",
|
||||
)
|
||||
.span_label(
|
||||
infcx.tcx.def_span(impl2_header.impl_def_id),
|
||||
"the second impl is here",
|
||||
);
|
||||
lint.note(format!(
|
||||
"`{}` may be considered to hold in future releases, \
|
||||
causing the impls to overlap",
|
||||
infcx.resolve_vars_if_possible(failing_obligation.predicate)
|
||||
));
|
||||
lint
|
||||
},
|
||||
);
|
||||
}
|
||||
|
||||
return None;
|
||||
}
|
||||
}
|
||||
|
||||
@ -281,7 +294,12 @@ fn overlap<'tcx>(
|
||||
return None;
|
||||
}
|
||||
|
||||
let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
|
||||
let intercrate_ambiguity_causes = if infcx.next_trait_solver() {
|
||||
compute_intercrate_ambiguity_causes(&infcx, &obligations)
|
||||
} else {
|
||||
selcx.take_intercrate_ambiguity_causes()
|
||||
};
|
||||
|
||||
debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
|
||||
let involves_placeholder = infcx
|
||||
.inner
|
||||
@ -335,34 +353,24 @@ fn equate_impl_headers<'tcx>(
|
||||
/// of the two impls above to be empty.
|
||||
///
|
||||
/// Importantly, this works even if there isn't a `impl !Error for MyLocalType`.
|
||||
fn impl_intersection_has_impossible_obligation<'cx, 'tcx>(
|
||||
fn impl_intersection_has_impossible_obligation<'a, 'cx, 'tcx>(
|
||||
selcx: &mut SelectionContext<'cx, 'tcx>,
|
||||
param_env: ty::ParamEnv<'tcx>,
|
||||
impl1_header: &ty::ImplHeader<'tcx>,
|
||||
impl2_header: &ty::ImplHeader<'tcx>,
|
||||
obligations: &PredicateObligations<'tcx>,
|
||||
) -> Option<PredicateObligation<'tcx>> {
|
||||
obligations: &'a [PredicateObligation<'tcx>],
|
||||
) -> Option<&'a PredicateObligation<'tcx>> {
|
||||
let infcx = selcx.infcx;
|
||||
|
||||
[&impl1_header.predicates, &impl2_header.predicates]
|
||||
.into_iter()
|
||||
.flatten()
|
||||
.map(|&predicate| {
|
||||
Obligation::new(infcx.tcx, ObligationCause::dummy(), param_env, predicate)
|
||||
})
|
||||
.chain(obligations.into_iter().cloned())
|
||||
.find(|obligation: &PredicateObligation<'tcx>| {
|
||||
if infcx.next_trait_solver() {
|
||||
infcx.evaluate_obligation(obligation).map_or(false, |result| !result.may_apply())
|
||||
} else {
|
||||
// We use `evaluate_root_obligation` to correctly track intercrate
|
||||
// ambiguity clauses. We cannot use this in the new solver.
|
||||
selcx.evaluate_root_obligation(obligation).map_or(
|
||||
false, // Overflow has occurred, and treat the obligation as possibly holding.
|
||||
|result| !result.may_apply(),
|
||||
)
|
||||
}
|
||||
})
|
||||
obligations.iter().find(|obligation| {
|
||||
if infcx.next_trait_solver() {
|
||||
infcx.evaluate_obligation(obligation).map_or(false, |result| !result.may_apply())
|
||||
} else {
|
||||
// We use `evaluate_root_obligation` to correctly track intercrate
|
||||
// ambiguity clauses. We cannot use this in the new solver.
|
||||
selcx.evaluate_root_obligation(obligation).map_or(
|
||||
false, // Overflow has occurred, and treat the obligation as possibly holding.
|
||||
|result| !result.may_apply(),
|
||||
)
|
||||
}
|
||||
})
|
||||
}
|
||||
|
||||
/// Check if both impls can be satisfied by a common type by considering whether
|
||||
@ -882,3 +890,142 @@ where
|
||||
ControlFlow::Continue(())
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute the `intercrate_ambiguity_causes` for the new solver using
|
||||
/// "proof trees".
|
||||
///
|
||||
/// This is a bit scuffed but seems to be good enough, at least
|
||||
/// when looking at UI tests. Given that it is only used to improve
|
||||
/// diagnostics this is good enough. We can always improve it once there
|
||||
/// are test cases where it is currently not enough.
|
||||
fn compute_intercrate_ambiguity_causes<'tcx>(
|
||||
infcx: &InferCtxt<'tcx>,
|
||||
obligations: &[PredicateObligation<'tcx>],
|
||||
) -> FxIndexSet<IntercrateAmbiguityCause> {
|
||||
let mut causes: FxIndexSet<IntercrateAmbiguityCause> = Default::default();
|
||||
|
||||
for obligation in obligations {
|
||||
search_ambiguity_causes(infcx, obligation.clone().into(), &mut causes);
|
||||
}
|
||||
|
||||
causes
|
||||
}
|
||||
|
||||
struct AmbiguityCausesVisitor<'a> {
|
||||
causes: &'a mut FxIndexSet<IntercrateAmbiguityCause>,
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a> {
|
||||
type BreakTy = !;
|
||||
fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> ControlFlow<Self::BreakTy> {
|
||||
let infcx = goal.infcx();
|
||||
for cand in goal.candidates() {
|
||||
cand.visit_nested(self)?;
|
||||
}
|
||||
// When searching for intercrate ambiguity causes, we only need to look
|
||||
// at ambiguous goals, as for others the coherence unknowable candidate
|
||||
// was irrelevant.
|
||||
match goal.result() {
|
||||
Ok(Certainty::Maybe(_)) => {}
|
||||
Ok(Certainty::Yes) | Err(NoSolution) => return ControlFlow::Continue(()),
|
||||
}
|
||||
|
||||
let Goal { param_env, predicate } = goal.goal();
|
||||
|
||||
let trait_ref = match predicate.kind().no_bound_vars() {
|
||||
Some(ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr))) => tr.trait_ref,
|
||||
Some(ty::PredicateKind::Clause(ty::ClauseKind::Projection(proj))) => {
|
||||
proj.projection_ty.trait_ref(infcx.tcx)
|
||||
}
|
||||
_ => return ControlFlow::Continue(()),
|
||||
};
|
||||
|
||||
let mut ambiguity_cause = None;
|
||||
for cand in goal.candidates() {
|
||||
match cand.result() {
|
||||
Ok(Certainty::Maybe(_)) => {}
|
||||
// We only add intercrate ambiguity causes if the goal would
|
||||
// otherwise result in an error.
|
||||
//
|
||||
// FIXME: this isn't quite right. Changing a goal from YES with
|
||||
// inference contraints to AMBIGUOUS can also cause a goal to not
|
||||
// fail.
|
||||
Ok(Certainty::Yes) => {
|
||||
ambiguity_cause = None;
|
||||
break;
|
||||
}
|
||||
Err(NoSolution) => continue,
|
||||
}
|
||||
|
||||
// FIXME: boiiii, using string comparisions here sure is scuffed.
|
||||
if let inspect::ProbeKind::MiscCandidate { name: "coherence unknowable", result: _ } =
|
||||
cand.kind()
|
||||
{
|
||||
let lazily_normalize_ty = |ty: Ty<'tcx>| {
|
||||
let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx);
|
||||
if matches!(ty.kind(), ty::Alias(..)) {
|
||||
// FIXME(-Ztrait-solver=next-coherence): we currently don't
|
||||
// normalize opaque types here, resulting in diverging behavior
|
||||
// for TAITs.
|
||||
match infcx
|
||||
.at(&ObligationCause::dummy(), param_env)
|
||||
.structurally_normalize(ty, &mut *fulfill_cx)
|
||||
{
|
||||
Ok(ty) => Ok(ty),
|
||||
Err(_errs) => Err(()),
|
||||
}
|
||||
} else {
|
||||
Ok(ty)
|
||||
}
|
||||
};
|
||||
|
||||
infcx.probe(|_| {
|
||||
match trait_ref_is_knowable(infcx.tcx, trait_ref, lazily_normalize_ty) {
|
||||
Err(()) => {}
|
||||
Ok(Ok(())) => warn!("expected an unknowable trait ref: {trait_ref:?}"),
|
||||
Ok(Err(conflict)) => {
|
||||
if !trait_ref.references_error() {
|
||||
let self_ty = trait_ref.self_ty();
|
||||
let (trait_desc, self_desc) = with_no_trimmed_paths!({
|
||||
let trait_desc = trait_ref.print_only_trait_path().to_string();
|
||||
let self_desc = self_ty
|
||||
.has_concrete_skeleton()
|
||||
.then(|| self_ty.to_string());
|
||||
(trait_desc, self_desc)
|
||||
});
|
||||
ambiguity_cause = Some(match conflict {
|
||||
Conflict::Upstream => {
|
||||
IntercrateAmbiguityCause::UpstreamCrateUpdate {
|
||||
trait_desc,
|
||||
self_desc,
|
||||
}
|
||||
}
|
||||
Conflict::Downstream => {
|
||||
IntercrateAmbiguityCause::DownstreamCrate {
|
||||
trait_desc,
|
||||
self_desc,
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
if let Some(ambiguity_cause) = ambiguity_cause {
|
||||
self.causes.insert(ambiguity_cause);
|
||||
}
|
||||
|
||||
ControlFlow::Continue(())
|
||||
}
|
||||
}
|
||||
|
||||
fn search_ambiguity_causes<'tcx>(
|
||||
infcx: &InferCtxt<'tcx>,
|
||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||
causes: &mut FxIndexSet<IntercrateAmbiguityCause>,
|
||||
) {
|
||||
infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes });
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user