Handle recursive TAIT item bounds

[amirHdev]

Fixes rust-lang/trait-system-refactor-initiative#288.

While checking an opaque's item bounds we may legitimately need to normalize the same opaque again and use its provisional hidden type
the actual problem is that re-entering opaque normalization also schedules the same item bounds again and the proof recurses through another copy of obligations that are already part of the current proof and keeps those two things separate which having the opaque equation available and already having its item bounds scheduled in the current proof

[rustbot]

r? @khyperia

rustbot has assigned @khyperia.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

Why was this reviewer chosen?

The reviewer was selected based on:

• Owners of files modified in this PR: compiler
• compiler expanded to 75 candidates
• Random selection from 19 candidates

[khyperia]

sorry, I'm not quite confident enough with t-types yet to know if this is the right approach or not

r? types

[oli-obk]

I don't know enough about the next solver's opaque type handling yet to review this properly. My gut feeling on reading the diff is that the changes are solving the problem in a very brute force way, which may be the required way, but I'd basically need to debug this from scratch to understand it.

Can you explain a bit about how you got to this solution? Just looking at logs and checking where things start going wrong?

The fast path should probably be a separate commit and ideally have some (local is fine) benchmarks showing it's necessary at all

r? @lcnr

[lcnr]

My gut feeling on reading the diff is that the changes are solving the problem in a very brute force way, which may be the required way, but I'd basically need to debug this from scratch to understand it.

Can you explain a bit about how you got to this solution? Just looking at logs and checking where things start going wrong?

yeah, I am very worried about adding special cases or different paths to the behavior of the trait solver without a clear reason for why it is necessary and correct. I don't think this issue is particularly important to fix right now as to my knowledge it does not block stabilization and does not cause breakage to stable code in the wild here.

You could look into why exactly your PR changes things. I would expect this to be a larger underlying issue related to cyclic reasoning and maybe it should actually not be a productive cycle

[amirHdev]

You could look into why exactly your PR changes things. I would expect this to be a larger underlying issue related to cyclic reasoning and maybe it should actually not be a productive cycle

The SolverRelating change has nothing to do with #288. the eval_ctxt change alone fixes the original reproducer.
while checking Foo := Bar we need to prove Bar: PartialEq<(Foo, i32)> which already matches the impl directly. eagerly normalizing the recursive Foo reenters normalize_opaque_type and creates an unnecessary cycle
I tried a separate case where proving the bound would require normalizing Foo to Bar and the current solver rejects that case too and this does not appear to be a productive cycle
the second reproducer is a separate generic overflow caused by shallow_resolve not resolving inference variables nested inside aliases

remaining question is whether preventing this normalization while checking an opaque's own item bounds is the right layer for the fix.

[lcnr]

The SolverRelating change has nothing to do with #288. the eval_ctxt change alone fixes the original reproducer.
while checking Foo := Bar we need to prove Bar: PartialEq<(Foo, i32)> which already matches the impl directly. eagerly normalizing the recursive Foo reenters normalize_opaque_type and creates an unnecessary cycle

I personally feel hesitant about something being an "unnecessary cycle". We should generally be free to normalize things whereever we are, so either this cycle should actually be productive, or the cycle does actually matter somewhere.

That's what I am unsure about, why exactly this cycle should or should not be accepted.

It's hard to explain, but your change to normalization is something that "does not easily fit into a more theoretical model of what Rust is". Explaining what exactly this means is hard, but I want the behavior of the core type system to be as close to the its platonic ideal as possible

[amirHdev]

The path that matters here is the one where we are checking the opaque’s own item bounds
while normalizing Foo::{opaque#0} during post-typeck the bound still contains the free alias Foo and that alias resolves back to the same underlying opaque Foo::{opaque#0} as I could trace

I don’t think the interesting part here is just overflows and the overflow comes from normalizing the same opaque again while we are already proving its own bounds
once the hidden type is known the useful obligation is on the hidden type for example:

Bar: PartialEq<(Foo, i32)>

if we normalize the recursive Foo inside that obligation we just reenter opaque normalization and create the cycle again and this also lines up with the existing comment in add_item_bounds_for_hidden_type recursive references to the opaque whose item bounds we are currently proving should be preserved because normalizing them may recursively normalize the same opaque while proving its own bounds
Given that I think this is the fix for this path while proving an opaque’s own item bounds recursive references to that same opaque should stay opaque instead of being normalized again.

the broader opaque cycle-semantics question still exists but this case does not seem to need a more general cycle mechanism to make progress

[lcnr]

Given that I think this is the fix for this path while proving an opaque’s own item bounds recursive references to that same opaque should stay opaque instead of being normalized again.

the broader opaque cycle-semantics question still exists but this case does not seem to need a more general cycle mechanism to make progress

"keep an alias as rigid even though it can be normalized" also falls under

It's hard to explain, but your change to normalization is something that "does not easily fit into a more theoretical model of what Rust is". Explaining what exactly this means is hard, but I want the behavior of the core type system to be as close to the its platonic ideal as possible

If you change the PathKind when proving the item bounds during opaque type normalziation to Coinductive, does that allow this example to compile?

rust/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs

Line 438 in a4c1445

pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {

[amirHdev]

If you change the PathKind when proving the item bounds during opaque type normalization to Coinductive, does that allow this example to compile?

Yes, this works.

Would it make sense to introduce a more specific goal source for the opaque item-bound case instead of making all AliasWellFormed goals coinductive?

[rustbot]

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

[rustbot]

This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

[amirHdev]

Tightened this up
OpaqueTypeBound is coinductive while ordinary AliasWellFormed stays unchanged

r? lcnr

@rustbot ready

[rustbot]

Requested reviewer is already assigned to this pull request.

Please choose another assignee.