Skip to content

Commit

Permalink
NormalizesTo return nested goals
Browse files Browse the repository at this point in the history
  • Loading branch information
lcnr committed Mar 18, 2024
1 parent 33c274f commit 1ae8d1d
Show file tree
Hide file tree
Showing 13 changed files with 176 additions and 94 deletions.
23 changes: 21 additions & 2 deletions compiler/rustc_middle/src/traits/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,19 @@ pub struct ExternalConstraintsData<'tcx> {
// FIXME: implement this.
pub region_constraints: QueryRegionConstraints<'tcx>,
pub opaque_types: Vec<(ty::OpaqueTypeKey<'tcx>, Ty<'tcx>)>,
pub normalization_nested_goals: NestedNormalizationGoals<'tcx>,
}

#[derive(Debug, PartialEq, Eq, Clone, Hash, HashStable, Default, TypeVisitable, TypeFoldable)]
pub struct NestedNormalizationGoals<'tcx>(pub Vec<(GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)>);
impl<'tcx> NestedNormalizationGoals<'tcx> {
pub fn empty() -> Self {
NestedNormalizationGoals(vec![])
}

pub fn is_empty(&self) -> bool {
self.0.is_empty()
}
}

// FIXME: Having to clone `region_constraints` for folding feels bad and
Expand All @@ -183,21 +196,27 @@ impl<'tcx> TypeFoldable<TyCtxt<'tcx>> for ExternalConstraints<'tcx> {
.iter()
.map(|opaque| opaque.try_fold_with(folder))
.collect::<Result<_, F::Error>>()?,
normalization_nested_goals: self
.normalization_nested_goals
.clone()
.try_fold_with(folder)?,
}))
}

fn fold_with<F: TypeFolder<TyCtxt<'tcx>>>(self, folder: &mut F) -> Self {
TypeFolder::interner(folder).mk_external_constraints(ExternalConstraintsData {
region_constraints: self.region_constraints.clone().fold_with(folder),
opaque_types: self.opaque_types.iter().map(|opaque| opaque.fold_with(folder)).collect(),
normalization_nested_goals: self.normalization_nested_goals.clone().fold_with(folder),
})
}
}

impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for ExternalConstraints<'tcx> {
fn visit_with<V: TypeVisitor<TyCtxt<'tcx>>>(&self, visitor: &mut V) -> V::Result {
try_visit!(self.region_constraints.visit_with(visitor));
self.opaque_types.visit_with(visitor)
try_visit!(self.opaque_types.visit_with(visitor));
self.normalization_nested_goals.visit_with(visitor)
}
}

Expand Down Expand Up @@ -239,7 +258,7 @@ impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for PredefinedOpaques<'tcx> {
///
/// This is necessary as we treat nested goals different depending on
/// their source.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, HashStable, TypeVisitable, TypeFoldable)]
pub enum GoalSource {
Misc,
/// We're proving a where-bound of an impl.
Expand Down
44 changes: 32 additions & 12 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
//!
//! [c]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html
use super::{CanonicalInput, Certainty, EvalCtxt, Goal};
use crate::solve::eval_ctxt::NestedGoals;
use crate::solve::{
inspect, response_no_constraints_raw, CanonicalResponse, QueryResult, Response,
};
Expand All @@ -19,6 +20,7 @@ use rustc_infer::infer::canonical::CanonicalVarValues;
use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
use rustc_infer::infer::resolve::EagerResolver;
use rustc_infer::infer::{InferCtxt, InferOk};
use rustc_infer::traits::solve::NestedNormalizationGoals;
use rustc_middle::infer::canonical::Canonical;
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{
Expand Down Expand Up @@ -93,13 +95,26 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
previous call to `try_evaluate_added_goals!`"
);

let certainty = certainty.unify_with(goals_certainty);

let var_values = self.var_values;
let external_constraints = self.compute_external_query_constraints()?;

// When normalizing, we've replaced the expected term with an unconstrained
// inference variable. This means that we dropped information which could
// have been important. We handle this by instead returning the nested goals
// to the caller, where they are then handled.
//
// As we return all ambiguous nested goals, we can ignore the certainty returned
// by `try_evaluate_added_goals()`.
let (certainty, normalization_nested_goals) = if self.is_normalizes_to_goal {
let NestedGoals { normalizes_to_goals, goals } = std::mem::take(&mut self.nested_goals);
assert!(normalizes_to_goals.is_empty());
(certainty, NestedNormalizationGoals(goals))
} else {
let certainty = certainty.unify_with(goals_certainty);
(certainty, NestedNormalizationGoals::empty())
};

let external_constraints =
self.compute_external_query_constraints(normalization_nested_goals)?;
let (var_values, mut external_constraints) =
(var_values, external_constraints).fold_with(&mut EagerResolver::new(self.infcx));
(self.var_values, external_constraints).fold_with(&mut EagerResolver::new(self.infcx));
// Remove any trivial region constraints once we've resolved regions
external_constraints
.region_constraints
Expand Down Expand Up @@ -146,6 +161,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
#[instrument(level = "debug", skip(self), ret)]
fn compute_external_query_constraints(
&self,
normalization_nested_goals: NestedNormalizationGoals<'tcx>,
) -> Result<ExternalConstraintsData<'tcx>, NoSolution> {
// We only check for leaks from universes which were entered inside
// of the query.
Expand Down Expand Up @@ -176,7 +192,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
self.predefined_opaques_in_body.opaque_types.iter().all(|(pa, _)| pa != a)
});

Ok(ExternalConstraintsData { region_constraints, opaque_types })
Ok(ExternalConstraintsData { region_constraints, opaque_types, normalization_nested_goals })
}

/// After calling a canonical query, we apply the constraints returned
Expand All @@ -185,13 +201,14 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
/// This happens in three steps:
/// - we instantiate the bound variables of the query response
/// - we unify the `var_values` of the response with the `original_values`
/// - we apply the `external_constraints` returned by the query
/// - we apply the `external_constraints` returned by the query, returning
/// the `normalization_nested_goals`
pub(super) fn instantiate_and_apply_query_response(
&mut self,
param_env: ty::ParamEnv<'tcx>,
original_values: Vec<ty::GenericArg<'tcx>>,
response: CanonicalResponse<'tcx>,
) -> Certainty {
) -> (NestedNormalizationGoals<'tcx>, Certainty) {
let instantiation = Self::compute_query_response_instantiation_values(
self.infcx,
&original_values,
Expand All @@ -203,11 +220,14 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {

Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values);

let ExternalConstraintsData { region_constraints, opaque_types } =
external_constraints.deref();
let ExternalConstraintsData {
region_constraints,
opaque_types,
normalization_nested_goals,
} = external_constraints.deref();
self.register_region_constraints(region_constraints);
self.register_new_opaque_types(param_env, opaque_types);
certainty
(normalization_nested_goals.clone(), certainty)
}

/// This returns the canoncial variable values to instantiate the bound variables of
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
infcx: self.infcx,
variables: self.variables,
var_values: self.var_values,
is_normalizes_to_goal: self.is_normalizes_to_goal,
predefined_opaques_in_body: self.predefined_opaques_in_body,
max_input_universe: self.max_input_universe,
search_graph: self.search_graph,
Expand All @@ -25,6 +26,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
infcx: _,
variables: _,
var_values: _,
is_normalizes_to_goal: _,
predefined_opaques_in_body: _,
max_input_universe: _,
search_graph: _,
Expand Down
86 changes: 47 additions & 39 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use rustc_infer::infer::{
BoundRegionConversionTime, DefineOpaqueTypes, InferCtxt, InferOk, TyCtxtInferExt,
};
use rustc_infer::traits::query::NoSolution;
use rustc_infer::traits::solve::MaybeCause;
use rustc_infer::traits::solve::{MaybeCause, NestedNormalizationGoals};
use rustc_infer::traits::ObligationCause;
use rustc_middle::infer::canonical::CanonicalVarInfos;
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
Expand Down Expand Up @@ -61,6 +61,14 @@ pub struct EvalCtxt<'a, 'tcx> {
/// The variable info for the `var_values`, only used to make an ambiguous response
/// with no constraints.
variables: CanonicalVarInfos<'tcx>,
/// Whether we're currently computing a `NormalizesTo` goal. Unlike other goals,
/// `NormalizesTo` goals act like functions with the expected term always being
/// fully unconstrained. This would weaken inference however, as the nested goals
/// never get the inference constraints from the actual normalized-to type. Because
/// of this we return any ambiguous nested goals from `NormalizesTo` to the caller
/// when then adds these to its own context. The caller is always an `AliasRelate`
/// goal so this never leaks out of the solver.
is_normalizes_to_goal: bool,
pub(super) var_values: CanonicalVarValues<'tcx>,

predefined_opaques_in_body: PredefinedOpaques<'tcx>,
Expand Down Expand Up @@ -91,7 +99,7 @@ pub struct EvalCtxt<'a, 'tcx> {
pub(super) inspect: ProofTreeBuilder<'tcx>,
}

#[derive(Debug, Clone)]
#[derive(Default, Debug, Clone)]
pub(super) struct NestedGoals<'tcx> {
/// These normalizes-to goals are treated specially during the evaluation
/// loop. In each iteration we take the RHS of the projection, replace it with
Expand Down Expand Up @@ -153,6 +161,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
self.search_graph.solver_mode()
}

pub(super) fn set_is_normalizes_to_goal(&mut self) {
self.is_normalizes_to_goal = true;
}

/// 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`]).
Expand All @@ -165,8 +177,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let mut search_graph = search_graph::SearchGraph::new(mode);

let mut ecx = EvalCtxt {
search_graph: &mut search_graph,
infcx,
search_graph: &mut search_graph,
nested_goals: NestedGoals::new(),
inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),

Expand All @@ -178,6 +190,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
max_input_universe: ty::UniverseIndex::ROOT,
variables: ty::List::empty(),
var_values: CanonicalVarValues::dummy(),
is_normalizes_to_goal: false,
tainted: Ok(()),
};
let result = f(&mut ecx);
Expand Down Expand Up @@ -231,6 +244,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
infcx,
variables: canonical_input.variables,
var_values,
is_normalizes_to_goal: false,
predefined_opaques_in_body: input.predefined_opaques_in_body,
max_input_universe: canonical_input.max_universe,
search_graph,
Expand Down Expand Up @@ -317,6 +331,20 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty), NoSolution> {
let (normalization_nested_goals, has_changed, certainty) =
self.evaluate_goal_raw(goal_evaluation_kind, source, goal)?;
assert!(normalization_nested_goals.is_empty());
Ok((has_changed, certainty))
}

/// FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
/// be necessary once we implement the new coinduction approach.
fn evaluate_goal_raw(
&mut self,
goal_evaluation_kind: GoalEvaluationKind,
_source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(NestedNormalizationGoals<'tcx>, bool, Certainty), NoSolution> {
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
let mut goal_evaluation =
self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
Expand All @@ -334,12 +362,12 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
Ok(response) => response,
};

let (certainty, has_changed) = self.instantiate_response_discarding_overflow(
goal.param_env,
source,
orig_values,
canonical_response,
);
let (normalization_nested_goals, certainty, has_changed) = self
.instantiate_response_discarding_overflow(
goal.param_env,
orig_values,
canonical_response,
);
self.inspect.goal_evaluation(goal_evaluation);
// FIXME: We previously had an assert here that checked that recomputing
// a goal after applying its constraints did not change its response.
Expand All @@ -351,47 +379,25 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// Once we have decided on how to handle trait-system-refactor-initiative#75,
// we should re-add an assert here.

Ok((has_changed, certainty))
Ok((normalization_nested_goals, has_changed, certainty))
}

fn instantiate_response_discarding_overflow(
&mut self,
param_env: ty::ParamEnv<'tcx>,
source: GoalSource,
original_values: Vec<ty::GenericArg<'tcx>>,
response: CanonicalResponse<'tcx>,
) -> (Certainty, bool) {
// The old solver did not evaluate nested goals when normalizing.
// It returned the selection constraints allowing a `Projection`
// obligation to not hold in coherence while avoiding the fatal error
// from overflow.
//
// We match this behavior here by considering all constraints
// from nested goals which are not from where-bounds. We will already
// need to track which nested goals are required by impl where-bounds
// for coinductive cycles, so we simply reuse that here.
//
// While we could consider overflow constraints in more cases, this should
// not be necessary for backcompat and results in better perf. It also
// avoids a potential inconsistency which would otherwise require some
// tracking for root goals as well. See #119071 for an example.
let keep_overflow_constraints = || {
self.search_graph.current_goal_is_normalizes_to()
&& source != GoalSource::ImplWhereBound
};

if let Certainty::Maybe(MaybeCause::Overflow { .. }) = response.value.certainty
&& !keep_overflow_constraints()
{
return (response.value.certainty, false);
) -> (NestedNormalizationGoals<'tcx>, Certainty, bool) {
if let Certainty::Maybe(MaybeCause::Overflow { .. }) = response.value.certainty {
return (NestedNormalizationGoals::empty(), response.value.certainty, false);
}

let has_changed = !response.value.var_values.is_identity_modulo_regions()
|| !response.value.external_constraints.opaque_types.is_empty();

let certainty =
let (normalization_nested_goals, certainty) =
self.instantiate_and_apply_query_response(param_env, original_values, response);
(certainty, has_changed)
(normalization_nested_goals, certainty, has_changed)
}

fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
Expand Down Expand Up @@ -494,7 +500,7 @@ 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();
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());
let mut goals = core::mem::take(&mut self.nested_goals);

self.inspect.evaluate_added_goals_loop_start();

Expand All @@ -515,11 +521,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
ty::NormalizesTo { alias: goal.predicate.alias, term: unconstrained_rhs },
);

let (_, certainty) = self.evaluate_goal(
let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
GoalSource::Misc,
unconstrained_goal,
)?;
// Add the nested goals from normalization to our own nested goals.
goals.goals.extend(nested_goals);

// Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ where
infcx: outer_ecx.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,
search_graph: outer_ecx.search_graph,
Expand Down
13 changes: 7 additions & 6 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/select.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,12 +58,13 @@ impl<'tcx> InferCtxt<'tcx> {
}

let candidate = candidates.pop().unwrap();
let certainty = ecx.instantiate_and_apply_query_response(
trait_goal.param_env,
orig_values,
candidate.result,
);

let (normalization_nested_goals, certainty) = ecx
.instantiate_and_apply_query_response(
trait_goal.param_env,
orig_values,
candidate.result,
);
assert!(normalization_nested_goals.is_empty());
Ok(Some((candidate, certainty)))
});

Expand Down
Loading

0 comments on commit 1ae8d1d

Please sign in to comment.