Skip to content

Commit

Permalink
change definitely non-productive cycles to error
Browse files Browse the repository at this point in the history
  • Loading branch information
lcnr committed Feb 27, 2025
1 parent 35fbaf1 commit fa26c12
Show file tree
Hide file tree
Showing 19 changed files with 231 additions and 204 deletions.
45 changes: 37 additions & 8 deletions compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -271,12 +271,32 @@ where
/// and will need to clearly document it in the rustc-dev-guide before
/// stabilization.
pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
match (self.current_goal_kind, source) {
(_, GoalSource::NormalizeGoal(step_kind)) => step_kind,
(CurrentGoalKind::CoinductiveTrait, GoalSource::ImplWhereBound) => {
PathKind::Coinductive
match source {
// We treat these goals as unknown for now. It is likely that most miscellaneous
// nested goals will be converted to `GoalSource::MiscKnownInductive` over time.
GoalSource::Misc => PathKind::Unknown,
GoalSource::NormalizeGoal(path_kind) => path_kind,
GoalSource::ImplWhereBound => {
// We currently only consider a cycle coinductive if it steps
// into a where-clause of a coinductive trait.
//
// We probably want to make all traits coinductive in the future,
// so we treat cycles involving their where-clauses as ambiguous.
if let CurrentGoalKind::CoinductiveTrait = self.current_goal_kind {
PathKind::Coinductive
} else {
PathKind::Unknown
}
}
_ => PathKind::Inductive,
// A step which is clearly unproductive. Cycles exclusively involving such steps
// result in `Err(NoSolution)`.
GoalSource::MiscKnownInductive | GoalSource::InstantiateHigherRanked => {
PathKind::Inductive
}
// These goal sources are likely unproductive and can be changed to
// `PathKind::Inductive`. Keeping them as unknown until we're confident
// about this and have an example where it is necessary.
GoalSource::AliasBoundConstCondition | GoalSource::AliasWellFormed => PathKind::Unknown,
}
}

Expand Down Expand Up @@ -606,7 +626,7 @@ where

let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
GoalEvaluationKind::Nested,
GoalSource::Misc,
GoalSource::normalizes_to(),
unconstrained_goal,
)?;
// Add the nested goals from normalization to our own nested goals.
Expand Down Expand Up @@ -683,7 +703,7 @@ where
pub(super) fn add_normalizes_to_goal(&mut self, mut goal: Goal<I, ty::NormalizesTo<I>>) {
goal.predicate = goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(
self,
GoalSource::Misc,
GoalSource::normalizes_to(),
goal.param_env,
));
self.inspect.add_normalizes_to_goal(self.delegate, self.max_input_universe, goal);
Expand Down Expand Up @@ -939,7 +959,16 @@ where
rhs: T,
) -> Result<(), NoSolution> {
let goals = self.delegate.relate(param_env, lhs, variance, rhs, self.origin_span)?;
self.add_goals(GoalSource::Misc, goals);
if cfg!(debug_assertions) {
for g in goals.iter() {
match g.predicate.kind().skip_binder() {
ty::PredicateKind::Subtype { .. } | ty::PredicateKind::AliasRelate(..) => {}
p => unreachable!("unexpected nested goal in `relate`: {p:?}"),
}
}
}
// Relating types is always unproductive.
self.add_goals(GoalSource::MiscKnownInductive, goals);
Ok(())
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -421,7 +421,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
self.add_goal(
delegate,
max_input_universe,
GoalSource::Misc,
GoalSource::normalizes_to(),
goal.with(delegate.cx(), goal.predicate),
);
}
Expand Down
3 changes: 2 additions & 1 deletion compiler/rustc_next_trait_solver/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -313,7 +313,8 @@ where
ty::AliasRelationDirection::Equate,
),
);
self.add_goal(GoalSource::Misc, alias_relate_goal);
// Normalization is always unproductive.
self.add_goal(GoalSource::MiscKnownInductive, alias_relate_goal);
self.try_evaluate_added_goals()?;
Ok(self.resolve_vars_if_possible(normalized_term))
} else {
Expand Down
3 changes: 2 additions & 1 deletion compiler/rustc_next_trait_solver/src/solve/project_goals.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ where
ty::AliasRelationDirection::Equate,
),
);
self.add_goal(GoalSource::Misc, goal);
// Normalization is always unproductive.
self.add_goal(GoalSource::MiscKnownInductive, goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
}
12 changes: 4 additions & 8 deletions compiler/rustc_next_trait_solver/src/solve/search_graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use std::marker::PhantomData;

use rustc_type_ir::Interner;
use rustc_type_ir::search_graph::{self, PathKind};
use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};

use super::inspect::ProofTreeBuilder;
use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
Expand Down Expand Up @@ -47,7 +47,8 @@ where
) -> QueryResult<I> {
match kind {
PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
PathKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
PathKind::Unknown => response_no_constraints(cx, input, Certainty::overflow(false)),
PathKind::Inductive => Err(NoSolution),
}
}

Expand All @@ -57,12 +58,7 @@ where
input: CanonicalInput<I>,
result: QueryResult<I>,
) -> bool {
match kind {
PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
PathKind::Inductive => {
response_no_constraints(cx, input, Certainty::overflow(false)) == result
}
}
Self::initial_provisional_result(cx, kind, input) == result
}

fn on_stack_overflow(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -440,7 +440,9 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
match (child_mode, nested_goal.source()) {
(
ChildMode::Trait(_) | ChildMode::Host(_),
GoalSource::Misc | GoalSource::NormalizeGoal(_),
GoalSource::Misc
| GoalSource::MiscKnownInductive
| GoalSource::NormalizeGoal(_),
) => {
continue;
}
Expand Down
Loading

0 comments on commit fa26c12

Please sign in to comment.