1
Fork 0
This commit is contained in:
lcnr 2025-02-26 14:28:44 +01:00
parent fe874cd99b
commit ef771b8450
6 changed files with 36 additions and 22 deletions

View file

@ -4,7 +4,6 @@ use rustc_data_structures::intern::Interned;
use rustc_hir::def_id::DefId; use rustc_hir::def_id::DefId;
use rustc_macros::{HashStable, extension}; use rustc_macros::{HashStable, extension};
use rustc_type_ir as ir; use rustc_type_ir as ir;
use tracing::instrument;
use crate::ty::{ use crate::ty::{
self, DebruijnIndex, EarlyBinder, PredicatePolarity, Ty, TyCtxt, TypeFlags, Upcast, UpcastFrom, self, DebruijnIndex, EarlyBinder, PredicatePolarity, Ty, TyCtxt, TypeFlags, Upcast, UpcastFrom,
@ -115,19 +114,6 @@ impl<'tcx> Predicate<'tcx> {
Some(tcx.mk_predicate(kind)) Some(tcx.mk_predicate(kind))
} }
/// Only used by the old solver to decide whether a predicate is accepted
/// in a coinductive trait solver cycle.
#[instrument(level = "debug", skip(tcx), ret)]
pub fn is_coinductive(self, tcx: TyCtxt<'tcx>) -> bool {
match self.kind().skip_binder() {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(data)) => {
tcx.trait_is_coinductive(data.def_id())
}
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(_)) => true,
_ => false,
}
}
/// Whether this projection can be soundly normalized. /// Whether this projection can be soundly normalized.
/// ///
/// Wf predicates must not be normalized, as normalization /// Wf predicates must not be normalized, as normalization

View file

@ -262,6 +262,14 @@ where
self.delegate.typing_mode() self.delegate.typing_mode()
} }
/// Computes the `PathKind` for the step from the current goal to the
/// nested goal required due to `source`.
///
/// See #136824 for a more detailed reasoning for this behavior. We
/// consider cycles to be coinductive if they 'step into' a where-clause
/// of a coinductive trait. We will likely extend this function in the future
/// 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 { pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
match (self.current_goal_kind, source) { match (self.current_goal_kind, source) {
(_, GoalSource::NormalizeGoal(step_kind)) => step_kind, (_, GoalSource::NormalizeGoal(step_kind)) => step_kind,
@ -1099,6 +1107,13 @@ where
/// ///
/// This is a performance optimization to more eagerly detect cycles during trait /// This is a performance optimization to more eagerly detect cycles during trait
/// solving. See tests/ui/traits/next-solver/cycles/cycle-modulo-ambig-aliases.rs. /// solving. See tests/ui/traits/next-solver/cycles/cycle-modulo-ambig-aliases.rs.
///
/// The emitted goals get evaluated in the context of the parent goal; by
/// replacing aliases in nested goals we essentially pull the normalization out of
/// the nested goal. We want to treat the goal as if the normalization still happens
/// inside of the nested goal by inheriting the `step_kind` of the nested goal and
/// storing it in the `GoalSource` of the emitted `AliasRelate` goals.
/// This is necessary for tests/ui/sized/coinductive-1.rs to compile.
struct ReplaceAliasWithInfer<'me, 'a, D, I> struct ReplaceAliasWithInfer<'me, 'a, D, I>
where where
D: SolverDelegate<Interner = I>, D: SolverDelegate<Interner = I>,

View file

@ -1225,15 +1225,21 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
/// that recursion is ok. This routine returns `true` if the top of the /// that recursion is ok. This routine returns `true` if the top of the
/// stack (`cycle[0]`): /// stack (`cycle[0]`):
/// ///
/// - is a defaulted trait, /// - is a coinductive trait: an auto-trait or `Sized`,
/// - it also appears in the backtrace at some position `X`, /// - it also appears in the backtrace at some position `X`,
/// - all the predicates at positions `X..` between `X` and the top are /// - all the predicates at positions `X..` between `X` and the top are
/// also defaulted traits. /// also coinductive traits.
pub(crate) fn coinductive_match<I>(&mut self, mut cycle: I) -> bool pub(crate) fn coinductive_match<I>(&mut self, mut cycle: I) -> bool
where where
I: Iterator<Item = ty::Predicate<'tcx>>, I: Iterator<Item = ty::Predicate<'tcx>>,
{ {
cycle.all(|predicate| predicate.is_coinductive(self.tcx())) cycle.all(|p| match p.kind().skip_binder() {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(data)) => {
self.infcx.tcx.trait_is_coinductive(data.def_id())
}
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(_)) => true,
_ => false,
})
} }
/// Further evaluates `candidate` to decide whether all type parameters match and whether nested /// Further evaluates `candidate` to decide whether all type parameters match and whether nested

View file

@ -83,9 +83,8 @@ pub enum GoalSource {
/// In case normalizing aliases in nested goals cycles, eagerly normalizing these /// In case normalizing aliases in nested goals cycles, eagerly normalizing these
/// aliases in the context of the parent may incorrectly change the cycle kind. /// aliases in the context of the parent may incorrectly change the cycle kind.
/// Normalizing aliases in goals therefore tracks the original path kind for this /// Normalizing aliases in goals therefore tracks the original path kind for this
/// nested goal. /// nested goal. See the comment of the `ReplaceAliasWithInfer` visitor for more
/// /// details.
/// This is necessary for tests/ui/sized/coinductive-1.rs to compile.
NormalizeGoal(PathKind), NormalizeGoal(PathKind),
} }

View file

@ -1,11 +1,11 @@
error[E0275]: overflow evaluating the requirement `Foo<T>: SendIndir` error[E0275]: overflow evaluating the requirement `Foo<T>: SendIndir`
--> $DIR/only-one-coinductive-step-needed.rs:9:15 --> $DIR/only-one-coinductive-step-needed.rs:17:15
| |
LL | struct Foo<T>(<Foo<T> as Trait>::Assoc); LL | struct Foo<T>(<Foo<T> as Trait>::Assoc);
| ^^^^^^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^^^^^^
| |
note: required for `Foo<T>` to implement `Trait` note: required for `Foo<T>` to implement `Trait`
--> $DIR/only-one-coinductive-step-needed.rs:18:20 --> $DIR/only-one-coinductive-step-needed.rs:26:20
| |
LL | impl<T: SendIndir> Trait for T { LL | impl<T: SendIndir> Trait for T {
| --------- ^^^^^ ^ | --------- ^^^^^ ^

View file

@ -5,6 +5,14 @@
// #136824 changed cycles to be coinductive if they have at least // #136824 changed cycles to be coinductive if they have at least
// one productive step, causing this test to pass with the new solver. // one productive step, causing this test to pass with the new solver.
//
// The cycle in the test is the following:
// - `Foo<T>: Send`, builtin auto-trait impl requires
// - `<Foo<T> as Trait>::Assoc: Send`, requires normalizing self type via impl, requires
// - `Foo<T>: SendIndir`, via impl requires
// - `Foo<T>: Send` cycle
//
// The old solver treats this cycle as inductive due to the `Foo<T>: SendIndir` step.
struct Foo<T>(<Foo<T> as Trait>::Assoc); struct Foo<T>(<Foo<T> as Trait>::Assoc);
//[current]~^ ERROR overflow evaluating the requirement `Foo<T>: SendIndir` //[current]~^ ERROR overflow evaluating the requirement `Foo<T>: SendIndir`