Skip to content

Commit

Permalink
how to handle non infer var_values
Browse files Browse the repository at this point in the history
  • Loading branch information
@lcnr
lcnr committed Jan 29, 2024
1 parent 9ab7ed3 commit 213a42f
Show file tree
Hide file tree
Showing 11 changed files with 131 additions and 184 deletions.
7 changes: 6 additions & 1 deletion compiler/rustc_infer/src/infer/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,12 @@ impl<'tcx> InferCtxtInner<'tcx> {
}

#[inline]
fn type_variables(&mut self) -> type_variable::TypeVariableTable<'_, 'tcx> {
pub fn instantiate_const_var(&mut self, var: ConstVid, value: ty::Const<'tcx>) {
self.const_unification_table().union_value(var, ConstVariableValue::Known { value })
}

#[inline]
pub fn type_variables(&mut self) -> type_variable::TypeVariableTable<'_, 'tcx> {
self.type_variable_storage.with_log(&mut self.undo_log)
}

Expand Down
2 changes: 0 additions & 2 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,6 @@ pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
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>>>,
}

#[derive(Eq, PartialEq)]
Expand Down
15 changes: 1 addition & 14 deletions compiler/rustc_middle/src/traits/solve/inspect/format.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
},
};
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
if eval.returned_goals.len() > 0 {
writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
self.nested(|this| {
for goal in eval.returned_goals.iter() {
writeln!(this.f, "ADDED GOAL: {goal:?},")?;
}
Ok(())
})?;

writeln!(self.f, "]")
} else {
Ok(())
}
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
}

pub(super) fn format_canonical_goal_evaluation(
Expand Down
28 changes: 20 additions & 8 deletions compiler/rustc_next_trait_solver/src/canonicalizer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,21 +107,22 @@ impl<'a, Infcx: InferCtxtLike<Interner = I>, I: Interner> Canonicalizer<'a, Infc
// universes `n`, this algorithm compresses them in place so that:
//
// - the new universe indices are as small as possible
// - we only create a new universe if we would otherwise put a placeholder in
// the same compressed universe as an existential which cannot name it
// - we create a new universe if we would otherwise
// 1. put existentials from a different universe into the same one
// 2. put a placeholder in the same universe as an existential which cannot name it
//
// Let's walk through an example:
// - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 0, next_orig_uv: 0
// - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 0, next_orig_uv: 1
// - var_infos: [E0, U1, E5, U2, E2, E6, U6], curr_compressed_uv: 1, next_orig_uv: 2
// - var_infos: [E0, U1, E5, U1, E1, E6, U6], curr_compressed_uv: 1, next_orig_uv: 5
// - var_infos: [E0, U1, E1, U1, E1, E6, U6], curr_compressed_uv: 1, next_orig_uv: 6
// - var_infos: [E0, U1, E1, U1, E1, E2, U2], curr_compressed_uv: 2, next_orig_uv: -
// - var_infos: [E0, U1, E2, U1, E1, E6, U6], curr_compressed_uv: 2, next_orig_uv: 6
// - var_infos: [E0, U1, E1, U1, E1, E3, U3], curr_compressed_uv: 2, next_orig_uv: -
//
// This algorithm runs in `O(n²)` where `n` is the number of different universe
// indices in the input. This should be fine as `n` is expected to be small.
let mut curr_compressed_uv = ty::UniverseIndex::ROOT;
let mut existential_in_new_uv = false;
let mut existential_in_new_uv = None;
let mut next_orig_uv = Some(ty::UniverseIndex::ROOT);
while let Some(orig_uv) = next_orig_uv.take() {
let mut update_uv = |var: &mut CanonicalVarInfo<I>, orig_uv, is_existential| {
Expand All @@ -130,14 +131,25 @@ impl<'a, Infcx: InferCtxtLike<Interner = I>, I: Interner> Canonicalizer<'a, Infc
Ordering::Less => (), // Already updated
Ordering::Equal => {
if is_existential {
existential_in_new_uv = true;
} else if existential_in_new_uv {
if existential_in_new_uv.is_some_and(|uv| uv < orig_uv) {
// Condition 1.
//
// We already put an existential from a outer universe
// into the current compressed universe, so we need to
// create a new one.
curr_compressed_uv = curr_compressed_uv.next_universe();
}

existential_in_new_uv = next_orig_uv;
} else if existential_in_new_uv.is_some() {
// Condition 2.
//
// `var` is a placeholder from a universe which is not nameable
// by an existential which we already put into the compressed
// universe `curr_compressed_uv`. We therefore have to create a
// new universe for `var`.
curr_compressed_uv = curr_compressed_uv.next_universe();
existential_in_new_uv = false;
existential_in_new_uv = None;
}

*var = var.with_updated_universe(curr_compressed_uv);
Expand Down
94 changes: 61 additions & 33 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/canonical.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,22 +191,20 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
param_env: ty::ParamEnv<'tcx>,
original_values: Vec<ty::GenericArg<'tcx>>,
response: CanonicalResponse<'tcx>,
) -> Result<(Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
) -> Certainty {
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(self.infcx, param_env, &original_values, var_values)?;
Self::unify_query_var_values(self.infcx, param_env, &original_values, var_values);

let ExternalConstraintsData { region_constraints, opaque_types } =
external_constraints.deref();
self.register_region_constraints(region_constraints);
self.register_opaque_types(param_env, opaque_types)?;

Ok((certainty, nested_goals))
self.register_new_opaque_types(param_env, opaque_types);
certainty
}

/// This returns the substitutions to instantiate the bound variables of
Expand Down Expand Up @@ -299,26 +297,61 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
param_env: ty::ParamEnv<'tcx>,
original_values: &[ty::GenericArg<'tcx>],
var_values: CanonicalVarValues<'tcx>,
) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, NoSolution> {
) {
assert_eq!(original_values.len(), var_values.len());

let mut nested_goals = vec![];
for (&orig, response) in iter::zip(original_values, var_values.var_values) {
nested_goals.extend(
infcx
EvalCtxt::unify_var_value(infcx, param_env, orig, response);
}
}

fn unify_var_value(
infcx: &InferCtxt<'tcx>,
param_env: ty::ParamEnv<'tcx>,
orig: ty::GenericArg<'tcx>,
response: ty::GenericArg<'tcx>,
) {
let orig = infcx.shallow_resolve(orig);
match (orig.unpack(), response.unpack()) {
(ty::GenericArgKind::Lifetime(orig), ty::GenericArgKind::Lifetime(response)) => {
let InferOk { value: (), obligations } = 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
})?,
);
.unwrap();
assert!(obligations.is_empty());
}
(ty::GenericArgKind::Type(orig), ty::GenericArgKind::Type(response)) => {
if let ty::Infer(ty::TyVar(orig)) = *orig.kind()
&& !response.is_ty_or_numeric_infer()
{
infcx.inner.borrow_mut().type_variables().instantiate(orig, response);
} else {
let InferOk { value: (), obligations } = infcx
.at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::No, orig, response)
.unwrap();
assert!(obligations.is_empty());
}
}
(ty::GenericArgKind::Const(orig), ty::GenericArgKind::Const(response)) => {
if let ty::ConstKind::Infer(ty::InferConst::Var(orig)) = orig.kind()
&& !response.is_ct_infer()
{
infcx.inner.borrow_mut().instantiate_const_var(orig, response);
} else {
let InferOk { value: (), obligations } = infcx
.at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::No, orig, response)
.unwrap();
assert!(obligations.is_empty());
}
}
(
ty::GenericArgKind::Lifetime(_)
| ty::GenericArgKind::Type(_)
| ty::GenericArgKind::Const(_),
_,
) => unreachable!(),
}

Ok(nested_goals)
}

fn register_region_constraints(&mut self, region_constraints: &QueryRegionConstraints<'tcx>) {
Expand All @@ -330,21 +363,17 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}
}

for member_constraint in &region_constraints.member_constraints {
// FIXME: Deal with member constraints :<
let _ = member_constraint;
}
assert!(region_constraints.member_constraints.is_empty());
}

fn register_opaque_types(
fn register_new_opaque_types(
&mut self,
param_env: ty::ParamEnv<'tcx>,
opaque_types: &[(ty::OpaqueTypeKey<'tcx>, Ty<'tcx>)],
) -> Result<(), NoSolution> {
) {
for &(key, ty) in opaque_types {
self.insert_hidden_type(key, param_env, ty)?;
self.insert_hidden_type(key, param_env, ty).unwrap();
}
Ok(())
}
}

Expand All @@ -368,14 +397,13 @@ impl<'tcx> inspect::ProofTreeBuilder<'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> {
) -> T {
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))
EvalCtxt::unify_query_var_values(infcx, param_env, original_values, var_values);
data
}
}
55 changes: 17 additions & 38 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,7 @@ pub trait InferCtxtEvalExt<'tcx> {
&self,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
generate_proof_tree: GenerateProofTree,
) -> (
Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
Option<inspect::GoalEvaluation<'tcx>>,
);
) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<'tcx>>);
}

impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
Expand All @@ -152,10 +149,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
&self,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
generate_proof_tree: GenerateProofTree,
) -> (
Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
Option<inspect::GoalEvaluation<'tcx>>,
) {
) -> (Result<(bool, Certainty), NoSolution>, Option<inspect::GoalEvaluation<'tcx>>) {
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
})
Expand Down Expand Up @@ -337,7 +331,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
goal_evaluation_kind: GoalEvaluationKind,
source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
) -> Result<(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 @@ -355,26 +349,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
Ok(response) => response,
};

let (certainty, has_changed, nested_goals) = match self
.instantiate_response_discarding_overflow(
goal.param_env,
source,
orig_values,
canonical_response,
) {
Err(e) => {
self.inspect.goal_evaluation(goal_evaluation);
return Err(e);
}
Ok(response) => response,
};
goal_evaluation.returned_goals(&nested_goals);
let (certainty, has_changed) = self.instantiate_response_discarding_overflow(
goal.param_env,
source,
orig_values,
canonical_response,
);
self.inspect.goal_evaluation(goal_evaluation);

if !has_changed && !nested_goals.is_empty() {
bug!("an unchanged goal shouldn't have any side-effects on instantiation");
}

// FIXME: We previously had an assert here that checked that recomputing
// a goal after applying its constraints did not change its response.
//
Expand All @@ -385,7 +366,7 @@ 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, nested_goals))
Ok((has_changed, certainty))
}

fn instantiate_response_discarding_overflow(
Expand All @@ -394,7 +375,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
source: GoalSource,
original_values: Vec<ty::GenericArg<'tcx>>,
response: CanonicalResponse<'tcx>,
) -> Result<(Certainty, bool, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
) -> (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
Expand All @@ -415,14 +396,14 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
};

if response.value.certainty == Certainty::OVERFLOW && !keep_overflow_constraints() {
Ok((Certainty::OVERFLOW, false, Vec::new()))
(Certainty::OVERFLOW, false)
} else {
let has_changed = !response.value.var_values.is_identity_modulo_regions()
|| !response.value.external_constraints.opaque_types.is_empty();

let (certainty, nested_goals) =
self.instantiate_and_apply_query_response(param_env, original_values, response)?;
Ok((certainty, has_changed, nested_goals))
let certainty =
self.instantiate_and_apply_query_response(param_env, original_values, response);
(certainty, has_changed)
}
}

Expand Down Expand Up @@ -546,12 +527,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
ty::NormalizesTo { alias: goal.predicate.alias, term: unconstrained_rhs },
);

let (_, certainty, instantiate_goals) = self.evaluate_goal(
let (_, certainty) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
GoalSource::Misc,
unconstrained_goal,
)?;
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));

// Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of
Expand Down Expand Up @@ -582,12 +562,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}

for (source, goal) in goals.goals.drain(..) {
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
let (has_changed, certainty) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
source,
goal,
)?;
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
if has_changed {
unchanged_certainty = None;
}
Expand Down
Loading

0 comments on commit 213a42f

Please sign in to comment.