bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Rollup merge of #139900 - lcnr:normalizes-to-where-bounds-unproductive, r=compiler-errors

Browse source 
stepping into impls for normalization is unproductive

See the inline comment. This builds on the reasoning from #136824 (https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5). Fixes https://github.com/rust-lang/trait-system-refactor-initiative/issues/176.

Looking at the end of the gist:
> The only ways to project out of a constructor are the following:
> - accessing an associated item, either its type or its item bounds
> - accessing super predicates

Detecting cases where we accessing the type of an associated item is easy, it's simply when we normalize. I don't yet know how to detect whether we step out of an impl by accessing item bounds. Once we also detect these cases we should be able to soundly support arbitrary coinductive traits. Luckily this does not matter for this PR :>

r? `@compiler-errors` cc `@nikomatsakis`
This commit is contained in:
Matthias Krüger 2025-04-17 00:16:24 +02:00 • committed by GitHub
commit 9e0be6c15b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 201 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

21
compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
View file

@ -286,18 +286,23 @@ where
// fixing it may cause inference breakage or introduce ambiguity.
GoalSource::Misc => PathKind::Unknown,
GoalSource::NormalizeGoal(path_kind) => path_kind,
GoalSource::ImplWhereBound => {
GoalSource::ImplWhereBound => match self.current_goal_kind {
// We currently only consider a cycle coinductive if it steps
// into a where-clause of a coinductive trait.
CurrentGoalKind::CoinductiveTrait => PathKind::Coinductive,
// While normalizing via an impl does step into a where-clause of
// an impl, accessing the associated item immediately steps out of
// it again. This means cycles/recursive calls are not guarded
// by impls used for normalization.
//
// See tests/ui/traits/next-solver/cycles/normalizes-to-is-not-productive.rs
// for how this can go wrong.
CurrentGoalKind::NormalizesTo => PathKind::Inductive,
// 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
}
}
// so we treat cycles involving where-clauses of not-yet coinductive
// traits as ambiguous for now.
CurrentGoalKind::Misc => PathKind::Unknown,
},
// 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.