Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

change definitely unproductive cycles to error #137314

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 43 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,39 @@ 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 an inductive variant in the future.
//
// Having unknown cycles is always the safer option, as changing that to either
// succeed or hard error is backwards compatible. If we incorrectly treat a cycle
// as inductive even though it should not be, it may be unsound during coherence and
// fixing it may cause inference breakage or introduce ambiguity.
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,
// Relating types is always unproductive. If we were to map proof trees to
// corecursive functions as explained in #136824, relating types never
// introduces a constructor which could cause the recursion to be guarded.
GoalSource::TypeRelating => PathKind::Inductive,
// Instantiating a higher ranked goal can never cause the recursion to be
// guarded and is therefore unproductive.
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 +633,7 @@ where

let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
GoalEvaluationKind::Nested,
GoalSource::Misc,
GoalSource::TypeRelating,
unconstrained_goal,
)?;
// Add the nested goals from normalization to our own nested goals.
Expand Down Expand Up @@ -683,7 +710,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::TypeRelating,
goal.param_env,
));
self.inspect.add_normalizes_to_goal(self.delegate, self.max_input_universe, goal);
Expand Down Expand Up @@ -939,7 +966,15 @@ 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:?}"),
}
}
}
self.add_goals(GoalSource::TypeRelating, 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::TypeRelating,
goal.with(delegate.cx(), goal.predicate),
);
}
Expand Down
4 changes: 3 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,9 @@ where
ty::AliasRelationDirection::Equate,
),
);
self.add_goal(GoalSource::Misc, alias_relate_goal);
// We normalize the self type to be able to relate it with
// types from candidates.
self.add_goal(GoalSource::TypeRelating, 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);
// A projection goal holds if the alias is equal to the expected term.
self.add_goal(GoalSource::TypeRelating, goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
}
30 changes: 21 additions & 9 deletions compiler/rustc_next_trait_solver/src/solve/search_graph.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
use std::convert::Infallible;
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 rustc_type_ir::{Interner, TypingMode};

use super::inspect::ProofTreeBuilder;
use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
Expand Down Expand Up @@ -47,7 +47,24 @@ 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)),
// Even though we know these cycles to be unproductive, we still return
// overflow during coherence. This is both as we are not 100% confident in
// the implementation yet and any incorrect errors would be unsound there.
// The affected cases are also fairly artificial and not necessarily desirable
// so keeping this as ambiguity is fine for now.
//
// See `tests/ui/traits/next-solver/cycles/unproductive-in-coherence.rs` for an
// example where this would matter. We likely should change these cycles to `NoSolution`
// even in coherence once this is a bit more settled.
PathKind::Inductive => match input.typing_mode {
TypingMode::Coherence => {
response_no_constraints(cx, input, Certainty::overflow(false))
}
TypingMode::Analysis { .. }
| TypingMode::PostBorrowckAnalysis { .. }
| TypingMode::PostAnalysis => Err(NoSolution),
},
}
}

Expand All @@ -57,12 +74,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,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
match (child_mode, nested_goal.source()) {
(
ChildMode::Trait(_) | ChildMode::Host(_),
GoalSource::Misc | GoalSource::NormalizeGoal(_),
GoalSource::Misc | GoalSource::TypeRelating | GoalSource::NormalizeGoal(_),
) => {
continue;
}
Expand Down
Loading
Loading