hir typeck: look into nested goals

uses a `ProofTreeVisitor` to look into nested
goals when looking at the pending obligations
during hir typeck. Used by closure signature
inference, coercion, and for async functions.
This commit is contained in:
lcnr 2024-03-12 14:26:30 +01:00
parent 662eadbafb
commit 03878c682a
23 changed files with 642 additions and 327 deletions

View file

@ -1,7 +1,7 @@
//! Code shared by trait and projection goals for candidate assembly.
use super::{EvalCtxt, SolverMode};
use crate::solve::GoalSource;
use crate::solve::{inspect, EvalCtxt, SolverMode};
use crate::traits::coherence;
use rustc_hir::def_id::DefId;
use rustc_infer::traits::query::NoSolution;
@ -16,6 +16,7 @@ use rustc_middle::ty::{fast_reject, TypeFoldable};
use rustc_middle::ty::{ToPredicate, TypeVisitableExt};
use rustc_span::{ErrorGuaranteed, DUMMY_SP};
use std::fmt::Debug;
use std::mem;
pub(super) mod structural_traits;
@ -315,20 +316,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}
fn forced_ambiguity(&mut self, cause: MaybeCause) -> Vec<Candidate<'tcx>> {
let source = CandidateSource::BuiltinImpl(BuiltinImplSource::Misc);
let certainty = Certainty::Maybe(cause);
// This may fail if `try_evaluate_added_goals` overflows because it
// fails to reach a fixpoint but ends up getting an error after
// running for some additional step.
//
// FIXME: Add a test for this. It seems to be necessary for typenum but
// is incredibly hard to minimize as it may rely on being inside of a
// trait solver cycle.
let result = self.evaluate_added_goals_and_make_canonical_response(certainty);
let mut dummy_probe = self.inspect.new_probe();
dummy_probe.probe_kind(ProbeKind::TraitCandidate { source, result });
self.inspect.finish_probe(dummy_probe);
if let Ok(result) = result { vec![Candidate { source, result }] } else { vec![] }
// cc trait-system-refactor-initiative#105
let source = CandidateSource::BuiltinImpl(BuiltinImplSource::Misc);
let certainty = Certainty::Maybe(cause);
let result = self
.probe_trait_candidate(source)
.enter(|this| this.evaluate_added_goals_and_make_canonical_response(certainty));
if let Ok(cand) = result { vec![cand] } else { vec![] }
}
#[instrument(level = "debug", skip_all)]
@ -813,6 +811,11 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
goal: Goal<'tcx, G>,
candidates: &mut Vec<Candidate<'tcx>>,
) {
// HACK: We temporarily remove the `ProofTreeBuilder` to
// avoid adding `Trait` candidates to the candidates used
// to prove the current goal.
let inspect = mem::replace(&mut self.inspect, inspect::ProofTreeBuilder::new_noop());
let tcx = self.tcx();
let trait_goal: Goal<'tcx, ty::TraitPredicate<'tcx>> =
goal.with(tcx, goal.predicate.trait_ref(tcx));
@ -846,6 +849,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}
}
}
self.inspect = inspect;
}
/// If there are multiple ways to prove a trait or projection goal, we have

View file

@ -19,9 +19,12 @@ 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::resolve::EagerResolver;
use rustc_infer::infer::type_variable::TypeVariableOrigin;
use rustc_infer::infer::RegionVariableOrigin;
use rustc_infer::infer::{InferCtxt, InferOk};
use rustc_infer::traits::solve::NestedNormalizationGoals;
use rustc_middle::infer::canonical::Canonical;
use rustc_middle::infer::unify_key::ConstVariableOrigin;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{
ExternalConstraintsData, MaybeCause, PredefinedOpaquesData, QueryInput,
@ -29,7 +32,7 @@ use rustc_middle::traits::solve::{
use rustc_middle::traits::ObligationCause;
use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable};
use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
use rustc_span::DUMMY_SP;
use rustc_span::{Span, DUMMY_SP};
use std::assert_matches::assert_matches;
use std::iter;
use std::ops::Deref;
@ -374,36 +377,70 @@ impl<'tcx> EvalCtxt<'_, '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::new(ecx.infcx));
Canonicalizer::canonicalize(
ecx.infcx,
CanonicalizeMode::Response { max_input_universe: ecx.max_input_universe },
&mut vec![],
state,
)
}
/// Instantiate a `CanonicalState`. This assumes that unifying the var values
/// trivially succeeds. Adding any inference constraints which weren't present when
/// originally computing the canonical query can result in bugs.
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>,
) -> T {
let instantiation =
EvalCtxt::compute_query_response_instantiation_values(infcx, original_values, &state);
let inspect::State { var_values, data } = state.instantiate(infcx.tcx, &instantiation);
EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values);
data
}
/// Used by proof trees to be able to recompute intermediate actions while
/// evaluating a goal. The `var_values` not only include the bound variables
/// of the query input, but also contain all unconstrained inference vars
/// created while evaluating this goal.
pub(in crate::solve) fn make_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
infcx: &InferCtxt<'tcx>,
var_values: &[ty::GenericArg<'tcx>],
max_input_universe: ty::UniverseIndex,
data: T,
) -> inspect::CanonicalState<'tcx, T> {
let var_values = CanonicalVarValues { var_values: infcx.tcx.mk_args(var_values) };
let state = inspect::State { var_values, data };
let state = state.fold_with(&mut EagerResolver::new(infcx));
Canonicalizer::canonicalize(
infcx,
CanonicalizeMode::Response { max_input_universe },
&mut vec![],
state,
)
}
/// Instantiate a `CanonicalState`.
///
/// Unlike for query responses, `CanonicalState` also track fresh inference
/// variables created while evaluating a goal. When creating two separate
/// `CanonicalState` during a single evaluation both may reference this
/// fresh inference variable. When instantiating them we now create separate
/// inference variables for it and have to unify them somehow. We do this
/// by extending the `var_values` while building the proof tree.
///
/// This currently assumes that unifying the var values trivially succeeds.
/// Adding any inference constraints which weren't present when originally
/// computing the canonical query can result in bugs.
pub(in crate::solve) fn instantiate_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
infcx: &InferCtxt<'tcx>,
span: Span,
param_env: ty::ParamEnv<'tcx>,
orig_values: &mut Vec<ty::GenericArg<'tcx>>,
state: inspect::CanonicalState<'tcx, T>,
) -> T {
// In case any fresh inference variables have been created between `state`
// and the previous instantiation, extend `orig_values` for it.
assert!(orig_values.len() <= state.value.var_values.len());
for i in orig_values.len()..state.value.var_values.len() {
let unconstrained = match state.value.var_values.var_values[i].unpack() {
ty::GenericArgKind::Lifetime(_) => {
infcx.next_region_var(RegionVariableOrigin::MiscVariable(span)).into()
}
ty::GenericArgKind::Type(_) => {
infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span }).into()
}
ty::GenericArgKind::Const(ct) => infcx
.next_const_var(ct.ty(), ConstVariableOrigin { param_def_id: None, span })
.into(),
};
orig_values.push(unconstrained);
}
let instantiation =
EvalCtxt::compute_query_response_instantiation_values(infcx, orig_values, &state);
let inspect::State { var_values, data } = state.instantiate(infcx.tcx, &instantiation);
EvalCtxt::unify_query_var_values(infcx, param_env, orig_values, var_values);
data
}

View file

@ -34,7 +34,7 @@ use super::{search_graph::SearchGraph, Goal};
use super::{GoalSource, SolverMode};
pub use select::InferCtxtSelectExt;
mod canonical;
pub(super) mod canonical;
mod probe;
mod select;
@ -84,7 +84,7 @@ pub struct EvalCtxt<'a, 'tcx> {
pub(super) search_graph: &'a mut SearchGraph<'tcx>,
pub(super) nested_goals: NestedGoals<'tcx>,
nested_goals: NestedGoals<'tcx>,
// Has this `EvalCtxt` errored out with `NoSolution` in `try_evaluate_added_goals`?
//
@ -161,7 +161,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
/// Creates a root evaluation context and search graph. This should only be
/// used from outside of any evaluation, and other methods should be preferred
/// over using this manually (such as [`InferCtxtEvalExt::evaluate_root_goal`]).
fn enter_root<R>(
pub(super) fn enter_root<R>(
infcx: &InferCtxt<'tcx>,
generate_proof_tree: GenerateProofTree,
f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
@ -242,7 +242,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
search_graph,
nested_goals: NestedGoals::new(),
tainted: Ok(()),
inspect: canonical_goal_evaluation.new_goal_evaluation_step(input),
inspect: canonical_goal_evaluation.new_goal_evaluation_step(var_values, input),
};
for &(key, ty) in &input.predefined_opaques_in_body.opaque_types {
@ -255,7 +255,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
let result = f(&mut ecx, input.goal);
ecx.inspect.probe_final_state(ecx.infcx, ecx.max_input_universe);
canonical_goal_evaluation.goal_evaluation_step(ecx.inspect);
// When creating a query response we clone the opaque type constraints
@ -338,7 +338,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
/// storage.
// FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
// be necessary once we implement the new coinduction approach.
fn evaluate_goal_raw(
pub(super) fn evaluate_goal_raw(
&mut self,
goal_evaluation_kind: GoalEvaluationKind,
_source: GoalSource,
@ -458,13 +458,23 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
}
#[instrument(level = "debug", skip(self))]
pub(super) fn add_normalizes_to_goal(&mut self, goal: Goal<'tcx, ty::NormalizesTo<'tcx>>) {
self.inspect.add_normalizes_to_goal(self.infcx, self.max_input_universe, goal);
self.nested_goals.normalizes_to_goals.push(goal);
}
#[instrument(level = "debug", skip(self))]
pub(super) fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
self.inspect.add_goal(self.infcx, self.max_input_universe, source, goal);
self.nested_goals.goals.push((source, goal));
}
// Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
// the certainty of all the goals.
#[instrument(level = "debug", skip(self))]
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
let inspect = self.inspect.new_evaluate_added_goals();
let inspect = core::mem::replace(&mut self.inspect, inspect);
self.inspect.start_evaluate_added_goals();
let mut response = Ok(Certainty::overflow(false));
for _ in 0..FIXPOINT_STEP_LIMIT {
// FIXME: This match is a bit ugly, it might be nice to change the inspect
@ -482,15 +492,12 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
}
self.inspect.eval_added_goals_result(response);
self.inspect.evaluate_added_goals_result(response);
if response.is_err() {
self.tainted = Err(NoSolution);
}
let goal_evaluations = std::mem::replace(&mut self.inspect, inspect);
self.inspect.added_goals_evaluation(goal_evaluations);
response
}
@ -499,10 +506,9 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
/// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
let tcx = self.tcx();
self.inspect.start_evaluate_added_goals_step();
let mut goals = core::mem::take(&mut self.nested_goals);
self.inspect.evaluate_added_goals_loop_start();
// If this loop did not result in any progress, what's our final certainty.
let mut unchanged_certainty = Some(Certainty::Yes);
for goal in goals.normalizes_to_goals {
@ -586,17 +592,23 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
self.infcx.tcx
}
pub(super) fn next_ty_infer(&self) -> Ty<'tcx> {
self.infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span: DUMMY_SP })
pub(super) fn next_ty_infer(&mut self) -> Ty<'tcx> {
let ty = self.infcx.next_ty_var(TypeVariableOrigin { param_def_id: None, span: DUMMY_SP });
self.inspect.add_var_value(ty);
ty
}
pub(super) fn next_const_infer(&self, ty: Ty<'tcx>) -> ty::Const<'tcx> {
self.infcx.next_const_var(ty, ConstVariableOrigin { param_def_id: None, span: DUMMY_SP })
pub(super) fn next_const_infer(&mut self, ty: Ty<'tcx>) -> ty::Const<'tcx> {
let ct = self
.infcx
.next_const_var(ty, ConstVariableOrigin { param_def_id: None, span: DUMMY_SP });
self.inspect.add_var_value(ct);
ct
}
/// Returns a ty infer or a const infer depending on whether `kind` is a `Ty` or `Const`.
/// If `kind` is an integer inference variable this will still return a ty infer var.
pub(super) fn next_term_infer_of_kind(&self, kind: ty::Term<'tcx>) -> ty::Term<'tcx> {
pub(super) fn next_term_infer_of_kind(&mut self, kind: ty::Term<'tcx>) -> ty::Term<'tcx> {
match kind.unpack() {
ty::TermKind::Ty(_) => self.next_ty_infer().into(),
ty::TermKind::Const(ct) => self.next_const_infer(ct.ty()).into(),

View file

@ -20,23 +20,29 @@ where
pub(in crate::solve) fn enter(self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
let ProbeCtxt { ecx: outer_ecx, probe_kind, _result } = self;
let infcx = outer_ecx.infcx;
let max_input_universe = outer_ecx.max_input_universe;
let mut nested_ecx = EvalCtxt {
infcx: outer_ecx.infcx,
infcx,
variables: outer_ecx.variables,
var_values: outer_ecx.var_values,
is_normalizes_to_goal: outer_ecx.is_normalizes_to_goal,
predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
max_input_universe: outer_ecx.max_input_universe,
max_input_universe,
search_graph: outer_ecx.search_graph,
nested_goals: outer_ecx.nested_goals.clone(),
tainted: outer_ecx.tainted,
inspect: outer_ecx.inspect.new_probe(),
inspect: outer_ecx.inspect.take_and_enter_probe(),
};
let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
if !outer_ecx.inspect.is_noop() {
let r = nested_ecx.infcx.probe(|_| {
let r = f(&mut nested_ecx);
nested_ecx.inspect.probe_final_state(infcx, max_input_universe);
r
});
if !nested_ecx.inspect.is_noop() {
let probe_kind = probe_kind(&r);
nested_ecx.inspect.probe_kind(probe_kind);
outer_ecx.inspect.finish_probe(nested_ecx.inspect);
outer_ecx.inspect = nested_ecx.inspect.finish_probe();
}
r
}

View file

@ -11,15 +11,24 @@
use rustc_ast_ir::try_visit;
use rustc_ast_ir::visit::VisitorResult;
use rustc_infer::infer::InferCtxt;
use rustc_infer::infer::type_variable::TypeVariableOrigin;
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, InferOk};
use rustc_middle::infer::unify_key::ConstVariableOrigin;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{inspect, QueryResult};
use rustc_middle::traits::solve::{Certainty, Goal};
use rustc_middle::traits::ObligationCause;
use rustc_middle::ty;
use rustc_span::Span;
use crate::solve::inspect::ProofTreeBuilder;
use crate::solve::eval_ctxt::canonical;
use crate::solve::{EvalCtxt, GoalEvaluationKind, GoalSource};
use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
pub struct InspectConfig {
pub max_depth: usize,
}
pub struct InspectGoal<'a, 'tcx> {
infcx: &'a InferCtxt<'tcx>,
depth: usize,
@ -32,14 +41,11 @@ 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>>>>,
final_state: inspect::CanonicalState<'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
}
@ -48,55 +54,88 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
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) -> V::Result {
// HACK: An arbitrary cutoff to avoid dealing with overflow and cycles.
if self.goal.depth <= 10 {
/// Visit all nested goals of this candidate without rolling
/// back their inference constraints. This function modifies
/// the state of the `infcx`.
pub fn visit_nested_no_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
if self.goal.depth < visitor.config().max_depth {
let infcx = self.goal.infcx;
infcx.probe(|_| {
let mut instantiated_goals = vec![];
for goal in &self.nested_goals {
let goal = ProofTreeBuilder::instantiate_canonical_state(
infcx,
self.goal.goal.param_env,
self.goal.orig_values,
*goal,
);
instantiated_goals.push(goal);
}
let param_env = self.goal.goal.param_env;
let mut orig_values = self.goal.orig_values.to_vec();
let mut instantiated_goals = vec![];
for goal in &self.nested_goals {
let goal = canonical::instantiate_canonical_state(
infcx,
visitor.span(),
param_env,
&mut orig_values,
*goal,
);
instantiated_goals.push(goal);
}
for goal in instantiated_goals.iter().copied() {
// We need to be careful with `NormalizesTo` goals as the
// expected term has to be replaced with an unconstrained
// inference variable.
if let Some(kind) = goal.predicate.kind().no_bound_vars()
&& let ty::PredicateKind::NormalizesTo(predicate) = kind
&& !predicate.alias.is_opaque(infcx.tcx)
{
// FIXME: We currently skip these goals as
// `fn evaluate_root_goal` ICEs if there are any
// `NestedNormalizationGoals`.
continue;
};
let (_, proof_tree) = infcx.evaluate_root_goal(goal, GenerateProofTree::Yes);
let proof_tree = proof_tree.unwrap();
try_visit!(visitor.visit_goal(&InspectGoal::new(
infcx,
self.goal.depth + 1,
&proof_tree,
)));
}
let () = canonical::instantiate_canonical_state(
infcx,
visitor.span(),
param_env,
&mut orig_values,
self.final_state,
);
V::Result::output()
})
} else {
V::Result::output()
for &goal in &instantiated_goals {
let proof_tree = match goal.predicate.kind().no_bound_vars() {
Some(ty::PredicateKind::NormalizesTo(ty::NormalizesTo { alias, term })) => {
let unconstrained_term = match term.unpack() {
ty::TermKind::Ty(_) => infcx
.next_ty_var(TypeVariableOrigin {
param_def_id: None,
span: visitor.span(),
})
.into(),
ty::TermKind::Const(ct) => infcx
.next_const_var(
ct.ty(),
ConstVariableOrigin {
param_def_id: None,
span: visitor.span(),
},
)
.into(),
};
let goal = goal
.with(infcx.tcx, ty::NormalizesTo { alias, term: unconstrained_term });
let proof_tree =
EvalCtxt::enter_root(infcx, GenerateProofTree::Yes, |ecx| {
ecx.evaluate_goal_raw(
GoalEvaluationKind::Root,
GoalSource::Misc,
goal,
)
})
.1;
let InferOk { value: (), obligations: _ } = infcx
.at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::Yes, term, unconstrained_term)
.unwrap();
proof_tree
}
_ => infcx.evaluate_root_goal(goal, GenerateProofTree::Yes).1,
};
try_visit!(visitor.visit_goal(&InspectGoal::new(
infcx,
self.goal.depth + 1,
&proof_tree.unwrap(),
)));
}
}
V::Result::output()
}
/// Visit all nested goals of this candidate, rolling back
/// all inference constraints.
pub fn visit_nested_in_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
self.goal.infcx.probe(|_| self.visit_nested_no_probe(visitor))
}
}
@ -119,6 +158,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
nested_goals: &mut Vec<inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>>,
probe: &inspect::Probe<'tcx>,
) {
let num_candidates = candidates.len();
for step in &probe.steps {
match step {
&inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
@ -144,23 +184,25 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
// FIXME: This is currently wrong if we don't even try any
// candidates, e.g. for a trait goal, as in this case `candidates` is
// actually supposed to be empty.
inspect::ProbeKind::Root { result } => {
if candidates.is_empty() {
inspect::ProbeKind::Root { result }
| inspect::ProbeKind::TryNormalizeNonRigid { result } => {
if candidates.len() == num_candidates {
candidates.push(InspectCandidate {
goal: self,
kind: probe.kind,
nested_goals: nested_goals.clone(),
final_state: probe.final_state,
result,
});
})
}
}
inspect::ProbeKind::TryNormalizeNonRigid { result }
| inspect::ProbeKind::MiscCandidate { name: _, result }
inspect::ProbeKind::MiscCandidate { name: _, result }
| inspect::ProbeKind::TraitCandidate { source: _, result } => {
candidates.push(InspectCandidate {
goal: self,
kind: probe.kind,
nested_goals: nested_goals.clone(),
final_state: probe.final_state,
result,
});
}
@ -191,6 +233,17 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
candidates
}
/// Returns the single candidate applicable for the current goal, if it exists.
///
/// Returns `None` if there are either no or multiple applicable candidates.
pub fn unique_applicable_candidate(&'a self) -> Option<InspectCandidate<'a, 'tcx>> {
// FIXME(-Znext-solver): This does not handle impl candidates
// hidden by env candidates.
let mut candidates = self.candidates();
candidates.retain(|c| c.result().is_ok());
candidates.pop().filter(|_| candidates.is_empty())
}
fn new(
infcx: &'a InferCtxt<'tcx>,
depth: usize,
@ -213,6 +266,12 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
pub trait ProofTreeVisitor<'tcx> {
type Result: VisitorResult = ();
fn span(&self) -> Span;
fn config(&self) -> InspectConfig {
InspectConfig { max_depth: 10 }
}
fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) -> Self::Result;
}
@ -223,10 +282,8 @@ impl<'tcx> InferCtxt<'tcx> {
goal: Goal<'tcx, ty::Predicate<'tcx>>,
visitor: &mut V,
) -> V::Result {
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))
})
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))
}
}

View file

@ -5,6 +5,8 @@
//! see the comment on [ProofTreeBuilder].
use std::mem;
use rustc_infer::infer::InferCtxt;
use rustc_middle::infer::canonical::CanonicalVarValues;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
@ -12,7 +14,8 @@ use rustc_middle::traits::solve::{
use rustc_middle::ty::{self, TyCtxt};
use rustc_session::config::DumpSolverProofTree;
use crate::solve::{self, inspect, EvalCtxt, GenerateProofTree};
use crate::solve::eval_ctxt::canonical;
use crate::solve::{self, inspect, GenerateProofTree};
/// The core data structure when building proof trees.
///
@ -47,9 +50,7 @@ enum DebugSolver<'tcx> {
Root,
GoalEvaluation(WipGoalEvaluation<'tcx>),
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
Probe(WipProbe<'tcx>),
}
impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
@ -64,24 +65,12 @@ impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
}
}
impl<'tcx> From<WipAddedGoalsEvaluation<'tcx>> for DebugSolver<'tcx> {
fn from(g: WipAddedGoalsEvaluation<'tcx>) -> DebugSolver<'tcx> {
DebugSolver::AddedGoalsEvaluation(g)
}
}
impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
fn from(g: WipGoalEvaluationStep<'tcx>) -> DebugSolver<'tcx> {
DebugSolver::GoalEvaluationStep(g)
}
}
impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
fn from(p: WipProbe<'tcx>) -> DebugSolver<'tcx> {
DebugSolver::Probe(p)
}
}
#[derive(Eq, PartialEq, Debug)]
struct WipGoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
@ -184,12 +173,41 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
#[derive(Eq, PartialEq, Debug)]
struct WipGoalEvaluationStep<'tcx> {
/// Unlike `EvalCtxt::var_values`, we append a new
/// generic arg here whenever we create a new inference
/// variable.
///
/// This is necessary as we otherwise don't unify these
/// vars when instantiating multiple `CanonicalState`.
var_values: Vec<ty::GenericArg<'tcx>>,
instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
probe_depth: usize,
evaluation: WipProbe<'tcx>,
}
impl<'tcx> WipGoalEvaluationStep<'tcx> {
fn current_evaluation_scope(&mut self) -> &mut WipProbe<'tcx> {
let mut current = &mut self.evaluation;
for _ in 0..self.probe_depth {
match current.steps.last_mut() {
Some(WipProbeStep::NestedProbe(p)) => current = p,
_ => bug!(),
}
}
current
}
fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<'tcx> {
let mut current = &mut self.evaluation;
loop {
match current.steps.last_mut() {
Some(WipProbeStep::NestedProbe(p)) => current = p,
Some(WipProbeStep::EvaluateGoals(evaluation)) => return evaluation,
_ => bug!(),
}
}
}
fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
let evaluation = self.evaluation.finalize();
match evaluation.kind {
@ -202,8 +220,10 @@ impl<'tcx> WipGoalEvaluationStep<'tcx> {
#[derive(Eq, PartialEq, Debug)]
struct WipProbe<'tcx> {
pub steps: Vec<WipProbeStep<'tcx>>,
pub kind: Option<inspect::ProbeKind<'tcx>>,
initial_num_var_values: usize,
steps: Vec<WipProbeStep<'tcx>>,
kind: Option<inspect::ProbeKind<'tcx>>,
final_state: Option<inspect::CanonicalState<'tcx, ()>>,
}
impl<'tcx> WipProbe<'tcx> {
@ -211,6 +231,7 @@ impl<'tcx> WipProbe<'tcx> {
inspect::Probe {
steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
kind: self.kind.unwrap(),
final_state: self.final_state.unwrap(),
}
}
}
@ -245,6 +266,12 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
self.state.as_deref_mut()
}
pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<'tcx> {
let mut nested = ProofTreeBuilder { state: self.state.take() };
nested.enter_probe();
nested
}
pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
match *self.state? {
DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
@ -362,11 +389,14 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
if let Some(this) = self.as_mut() {
match (this, *goal_evaluation.state.unwrap()) {
(
DebugSolver::AddedGoalsEvaluation(WipAddedGoalsEvaluation {
evaluations, ..
}),
DebugSolver::GoalEvaluationStep(state),
DebugSolver::GoalEvaluation(goal_evaluation),
) => evaluations.last_mut().unwrap().push(goal_evaluation),
) => state
.added_goals_evaluation()
.evaluations
.last_mut()
.unwrap()
.push(goal_evaluation),
(this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
_ => unreachable!(),
}
@ -375,13 +405,22 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
pub fn new_goal_evaluation_step(
&mut self,
var_values: CanonicalVarValues<'tcx>,
instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
) -> ProofTreeBuilder<'tcx> {
self.nested(|| WipGoalEvaluationStep {
var_values: var_values.var_values.to_vec(),
instantiated_goal,
evaluation: WipProbe { steps: vec![], kind: None },
evaluation: WipProbe {
initial_num_var_values: var_values.len(),
steps: vec![],
kind: None,
final_state: None,
},
probe_depth: 0,
})
}
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
if let Some(this) = self.as_mut() {
match (this, *goal_evaluation_step.state.unwrap()) {
@ -396,112 +435,146 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}
pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
self.nested(|| WipProbe { steps: vec![], kind: None })
pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
state.var_values.push(arg.into());
}
Some(s) => bug!("tried to add var values to {s:?}"),
}
}
pub fn enter_probe(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let initial_num_var_values = state.var_values.len();
state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
initial_num_var_values,
steps: vec![],
kind: None,
final_state: None,
}));
state.probe_depth += 1;
}
Some(s) => bug!("tried to start probe to {s:?}"),
}
}
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
if let Some(this) = self.as_mut() {
match this {
DebugSolver::Probe(this) => {
assert_eq!(this.kind.replace(probe_kind), None)
}
_ => unreachable!(),
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let prev = state.current_evaluation_scope().kind.replace(probe_kind);
assert_eq!(prev, None);
}
_ => bug!(),
}
}
pub fn probe_final_state(
&mut self,
infcx: &InferCtxt<'tcx>,
max_input_universe: ty::UniverseIndex,
) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let final_state = canonical::make_canonical_state(
infcx,
&state.var_values,
max_input_universe,
(),
);
let prev = state.current_evaluation_scope().final_state.replace(final_state);
assert_eq!(prev, None);
}
_ => bug!(),
}
}
pub fn add_normalizes_to_goal(
ecx: &mut EvalCtxt<'_, 'tcx>,
&mut self,
infcx: &InferCtxt<'tcx>,
max_input_universe: ty::UniverseIndex,
goal: Goal<'tcx, ty::NormalizesTo<'tcx>>,
) {
if ecx.inspect.is_noop() {
return;
}
Self::add_goal(ecx, GoalSource::Misc, goal.with(ecx.tcx(), goal.predicate));
self.add_goal(
infcx,
max_input_universe,
GoalSource::Misc,
goal.with(infcx.tcx, goal.predicate),
);
}
pub fn add_goal(
ecx: &mut EvalCtxt<'_, 'tcx>,
&mut self,
infcx: &InferCtxt<'tcx>,
max_input_universe: ty::UniverseIndex,
source: GoalSource,
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(source, goal))
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let goal = canonical::make_canonical_state(
infcx,
&state.var_values,
max_input_universe,
goal,
);
state.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal))
}
s => unreachable!("tried to add {goal:?} to {s:?}"),
_ => bug!(),
}
}
pub fn finish_probe(&mut self, probe: ProofTreeBuilder<'tcx>) {
if let Some(this) = self.as_mut() {
match (this, *probe.state.unwrap()) {
(
DebugSolver::Probe(WipProbe { steps, .. })
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
evaluation: WipProbe { steps, .. },
..
}),
DebugSolver::Probe(probe),
) => steps.push(WipProbeStep::NestedProbe(probe)),
_ => unreachable!(),
pub fn finish_probe(mut self) -> ProofTreeBuilder<'tcx> {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
assert_ne!(state.probe_depth, 0);
let num_var_values = state.current_evaluation_scope().initial_num_var_values;
state.var_values.truncate(num_var_values);
state.probe_depth -= 1;
}
_ => bug!(),
}
self
}
pub fn start_evaluate_added_goals(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
state.current_evaluation_scope().steps.push(WipProbeStep::EvaluateGoals(
WipAddedGoalsEvaluation { evaluations: vec![], result: None },
));
}
_ => bug!(),
}
}
pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
self.nested(|| WipAddedGoalsEvaluation { evaluations: vec![], result: None })
}
pub fn evaluate_added_goals_loop_start(&mut self) {
if let Some(this) = self.as_mut() {
match this {
DebugSolver::AddedGoalsEvaluation(this) => {
this.evaluations.push(vec![]);
}
_ => unreachable!(),
pub fn start_evaluate_added_goals_step(&mut self) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
state.added_goals_evaluation().evaluations.push(vec![]);
}
_ => bug!(),
}
}
pub fn eval_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
if let Some(this) = self.as_mut() {
match this {
DebugSolver::AddedGoalsEvaluation(this) => {
assert_eq!(this.result.replace(result), None);
}
_ => unreachable!(),
}
}
}
pub fn added_goals_evaluation(&mut self, added_goals_evaluation: ProofTreeBuilder<'tcx>) {
if let Some(this) = self.as_mut() {
match (this, *added_goals_evaluation.state.unwrap()) {
(
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
evaluation: WipProbe { steps, .. },
..
})
| DebugSolver::Probe(WipProbe { steps, .. }),
DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
_ => unreachable!(),
pub fn evaluate_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
match self.as_mut() {
None => {}
Some(DebugSolver::GoalEvaluationStep(state)) => {
let prev = state.added_goals_evaluation().result.replace(result);
assert_eq!(prev, None);
}
_ => bug!(),
}
}

View file

@ -200,18 +200,6 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
impl<'tcx> EvalCtxt<'_, 'tcx> {
#[instrument(level = "debug", skip(self))]
fn add_normalizes_to_goal(&mut self, goal: Goal<'tcx, ty::NormalizesTo<'tcx>>) {
inspect::ProofTreeBuilder::add_normalizes_to_goal(self, goal);
self.nested_goals.normalizes_to_goals.push(goal);
}
#[instrument(level = "debug", skip(self))]
fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
inspect::ProofTreeBuilder::add_goal(self, source, goal);
self.nested_goals.goals.push((source, goal));
}
#[instrument(level = "debug", skip(self, goals))]
fn add_goals(
&mut self,

View file

@ -30,7 +30,7 @@ use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
use rustc_middle::ty::visit::{TypeVisitable, TypeVisitableExt};
use rustc_middle::ty::{self, Ty, TyCtxt, TypeSuperVisitable, TypeVisitor};
use rustc_span::symbol::sym;
use rustc_span::DUMMY_SP;
use rustc_span::{Span, DUMMY_SP};
use std::fmt::Debug;
use std::ops::ControlFlow;
@ -1022,10 +1022,14 @@ struct AmbiguityCausesVisitor<'a, 'tcx> {
}
impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
fn span(&self) -> Span {
DUMMY_SP
}
fn visit_goal(&mut self, goal: &InspectGoal<'_, 'tcx>) {
let infcx = goal.infcx();
for cand in goal.candidates() {
cand.visit_nested(self);
cand.visit_nested_in_probe(self);
}
// When searching for intercrate ambiguity causes, we only need to look
// at ambiguous goals, as for others the coherence unknowable candidate
@ -1157,5 +1161,5 @@ fn search_ambiguity_causes<'tcx>(
goal: Goal<'tcx, ty::Predicate<'tcx>>,
causes: &mut FxIndexSet<IntercrateAmbiguityCause<'tcx>>,
) {
infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes });
infcx.probe(|_| infcx.visit_proof_tree(goal, &mut AmbiguityCausesVisitor { causes }));
}