Auto merge of #117278 - lcnr:try-normalize-ty, r=compiler-errors

new solver normalization improvements

cool beans

At the core of this PR is a `try_normalize_ty` which stops for rigid aliases by using `commit_if_ok`.

Reworks alias-relate to fully normalize both the lhs and rhs and then equate the resulting rigid (or inference) types. This fixes https://github.com/rust-lang/trait-system-refactor-initiative/issues/68 by avoiding the exponential blowup. Also supersedes #116369 by only defining opaque types if the hidden type is rigid.

I removed the stability check in `EvalCtxt::evaluate_goal` due to https://github.com/rust-lang/trait-system-refactor-initiative/issues/75. While I personally have opinions on how to fix it, that still requires further t-types/`@nikomatsakis` buy-in, so I removed that for now. Once we've decided on our approach there, we can revert this commit.

r? `@compiler-errors`
This commit is contained in:
bors
2023-11-17 10:16:41 +00:00
30 changed files with 411 additions and 317 deletions

View File

@@ -120,7 +120,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
for step in &probe.steps {
match step {
&inspect::ProbeStep::AddGoal(goal) => nested_goals.push(goal),
inspect::ProbeStep::EvaluateGoals(_) => (),
inspect::ProbeStep::NestedProbe(ref probe) => {
// Nested probes have to prove goals added in their parent
// but do not leak them, so we truncate the added goals
@@ -129,13 +128,17 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
self.candidates_recur(candidates, nested_goals, probe);
nested_goals.truncate(num_goals);
}
inspect::ProbeStep::EvaluateGoals(_)
| inspect::ProbeStep::CommitIfOkStart
| inspect::ProbeStep::CommitIfOkSuccess => (),
}
}
match probe.kind {
inspect::ProbeKind::NormalizedSelfTyAssembly
| inspect::ProbeKind::UnsizeAssembly
| inspect::ProbeKind::UpcastProjectionCompatibility => (),
| inspect::ProbeKind::UpcastProjectionCompatibility
| inspect::ProbeKind::CommitIfOk => (),
// We add a candidate for the root evaluation if there
// is only one way to prove a given goal, e.g. for `WellFormed`.
//

View File

@@ -219,6 +219,8 @@ enum WipProbeStep<'tcx> {
AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>),
CommitIfOkStart,
CommitIfOkSuccess,
}
impl<'tcx> WipProbeStep<'tcx> {
@@ -227,6 +229,8 @@ impl<'tcx> WipProbeStep<'tcx> {
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
WipProbeStep::CommitIfOkStart => inspect::ProbeStep::CommitIfOkStart,
WipProbeStep::CommitIfOkSuccess => inspect::ProbeStep::CommitIfOkSuccess,
}
}
}
@@ -459,6 +463,29 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}
/// Used by `EvalCtxt::commit_if_ok` to flatten the work done inside
/// of the probe into the parent.
pub fn integrate_snapshot(&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::CommitIfOkStart);
assert_eq!(probe.kind, None);
steps.extend(probe.steps);
steps.push(WipProbeStep::CommitIfOkSuccess);
}
_ => unreachable!(),
}
}
}
pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
self.nested(|| WipAddedGoalsEvaluation { evaluations: vec![], result: None })
}