Skip to content

don't ignore ambiguity during MIR type check - #164055

Open
lcnr wants to merge 2 commits into
rust-lang:mainfrom
lcnr:next-solver-soundness-bug
Open

lcnr wants to merge 2 commits into
rust-lang:mainfrom
lcnr:next-solver-soundness-bug

Conversation

@lcnr

@lcnr lcnr commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

fixes #164054

this was previously fixed in #116530 and later reverted in #118736.

It impacts the new solver more than the old one as the new solver depends significantly more on region identity, see the relevant stabilization report section.

The old solver has significantly less region identity dependence. It does rely on region identity when merging candidates during normalization:

// Duplicates can happen inside ParamEnv. In the case, we
// perform a lazy deduplication.
if current == &candidate {
return false;
}

This check results in additional ICE with the old solver while instead triggering the potentially region dependent goals check with the new one

let value = op(&ocx).map_err(|_| {
infcx.tcx.check_potentially_region_dependent_goals(root_def_id).err().unwrap_or_else(

r? types

@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-trait-system-refactor The Rustc Trait System Refactor Initiative (-Znext-solver) labels Oct 9, 2026
@lcnr lcnr added the I-types-nominated Nominated for discussion during a types team meeting. label Oct 9, 2026
@rustbot

rustbot commented Oct 9, 2026

Copy link
Copy Markdown
Collaborator

🤖 A dedicated #t-types/nominated topic has been opened for humans to discuss this issue 🤖

@rust-log-analyzer

This comment has been minimized.

@lcnr lcnr closed this Oct 9, 2026
@rustbot rustbot removed the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Oct 9, 2026
@lcnr lcnr reopened this Oct 9, 2026
@rustbot rustbot added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Oct 9, 2026
@rust-log-analyzer

This comment has been minimized.

@rustbot

This comment has been minimized.

@rust-log-analyzer

This comment has been minimized.

@rust-bors

This comment has been minimized.

@lcnr
lcnr force-pushed the next-solver-soundness-bug branch from 3eee062 to d5ef0a9 Compare October 28, 2026 14:43
@rustbot

rustbot commented Oct 28, 2026

Copy link
Copy Markdown
Collaborator

miri is developed in its own repository. If the Miri part of this change can be broken out, consider making this change to rust-lang/miri instead. However, if Miri needs adjusting for rustc changes, just ignore this message.

cc @rust-lang/miri

@lcnr lcnr removed the I-types-nominated Nominated for discussion during a types team meeting. label Oct 28, 2026
@rustbot

This comment has been minimized.

@@ -1,7 +1,10 @@
// Test for <https://github.com/rust-lang/rust/issues/135316>.

@RalfJung RalfJung Oct 28, 2026 •

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is a fail test the best test we can have now for #135316 ? It means we're not even hitting vtable generation any more.

View changes since the review

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

updated it

@jackh726 jackh726 left a comment •

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Several of these tests I wouldn't expect to error because I'm not understand what region constraints we're generating.

Seems like the (undesired, probably) fallback is basically all around dyn Trait? We don't get similar fallout from non-dyn multiple super traits?

Have we done crater with these changes yet? The breakage to the MIRI test has me worried about whether we may see this pop up often.

If there is undesired breakage here, I think we should mark those tests as known-bug.

View changes since this review

Comment on lines -502 to +509
(&() as &'static dyn for<'a> Trait<&'static (), &'a ()>
as &'static dyn Trait<&'static (), &'static ()>)
.say_hello(&0);
// We can't have `dyn Trait<&'static (), &'static ()>` directly here
// as that results in an ambiguity error in MIR borrowck.
fn generic<T: 'static>() {
(&() as &'static dyn for<'a> Trait<T, &'a ()> as &'static dyn Trait<T, &'static ()>)
.say_hello(&0);
}

generic::<&'static ()>();

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm. Breaking MIRI does not bode well for the fallout here.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

proving dyn Trait<&'x (), &'y ()>: Supertrait<&'z ()> is ambiguous as it either requires 'z = 'x or 'z = 'y. The reason this previously compiled with -Znext-solver is that.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your last sentence cut off I think.

Comment on lines 15 to +16
(&() as &dyn D<&(), &()>).f()
//[next]~^ ERROR: type annotations needed: cannot satisfy `dyn D<&(), &()>: B<&()>`

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So...this on first glance this really doesn't seem to me like it should fail. I guess from a technical perspective, I can probably see why it does (lack of OR constraints) but even that I'm unsure about, because I would expect that D<C, E>: B<C> and D<C, E>: B<E> to be able to be solved separately without region constraints.

Given that I would expect that this test be marked as known-bug under the next-solver.

@lcnr lcnr Nov 2, 2026 •

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one is odd because it should also just be ambiguous during HIR typeck already.

For dyn D<&'a (), &'b ()> HIR typeck explicitly proves B<&'a ()> and B<&'b ()>, both of which work as one of the candidates has no region constraints. The MIR body has the function item <dyn D<&'a (), &'b ()> as D<&'c (), &'d ()>>::f, proving dyn D<&'a (), &'b ()>: D<&'c (), &'d ()> for that one is ambiguous.


fn bar<'x, 'y>() {
impls_trait::<'y, _>(foo::<'x, 'y>());
//[next]~^ ERROR: type annotations needed: cannot satisfy `impl Trait<'_> + Trait<'_>: Trait<'_>`

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similar point to above.

// Need the ambiguous `T: Sup<'a, (), Assoc = &'static str>` bound to only be
// used inside of the trait impl, as otherwise we also encounter ambiguity
// during normalization, which ICEs instead of ignoring it.
impl<'a, T: Sup<'a, (), Assoc = &'static str> + ?Sized> HideMe for T {

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, this one clearly should not pass.

trait D<'a, 'b>: Tr<'a> + Tr<'b> {}
//[current]~^ ERROR: type annotations needed: cannot satisfy `Self: Tr<'a>`

impl<'t> Tr<'t> for &'t str { fn get(&self) -> &'t str { *self } }

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one I can see failing, because this does register a region constraint.

@lcnr
lcnr force-pushed the next-solver-soundness-bug branch from d5ef0a9 to 7100d2a Compare November 2, 2026 07:51
@lcnr
lcnr force-pushed the next-solver-soundness-bug branch from 7100d2a to 1dd5fc5 Compare November 2, 2026 07:55
@rustbot

rustbot commented Nov 2, 2026

Copy link
Copy Markdown
Collaborator

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.

@lcnr

lcnr commented Nov 2, 2026

Copy link
Copy Markdown
Contributor Author

so in general, we tend to have dyn Trait<'a, 'b>: Sup<'a> or dyn Trait<'a, 'a>: Sup<'b> during HIR typeck, where the two trait Trait<'a, 'b>: Sup<'a> + Sup<'b> candidates have the same constraints, and then in MIR borrowck we then have to prove dyn Trait<'x, 'y>: Sup<'z>, where the two candidates have different constraints.

Seems like the (undesired, probably) fallback is basically all around dyn Trait? We don't get similar fallout from non-dyn multiple super traits?

This is effectively only a problem for the builtin dyn Trait candidates if there are two equal-modulo regions super trait bounds, or similarly, you could have the same issue with item bounds for <T as Trait>::Assoc<'a, 'a> with type Assoc<'a, 'b>: Tr<'a> + Tr<'b>

Have we done crater with these changes yet? The breakage to the MIRI test has me worried about whether we may see this pop up often.

This PR reverts the behavior back to the "correct" behavior pre #160982. We tested that behavior as part of full next-solver crater runs in #133502. Most notably the crater run in #133502 (comment). We didn't encounter any meaningful breakage in that crater run because of this.

This affects cases which previously ICEd and were tracked in rust-lang/trait-system-refactor-initiative#27. Even back when the cases which now error resulted in ICE, this was something we didn't really encounter.

I would personally just merge this.

@lcnr

lcnr commented Nov 2, 2026

Copy link
Copy Markdown
Contributor Author

If there is undesired breakage here, I think we should mark those tests as known-bug.

This breakage does feel... fairly desired to me. Or well, it is intended - but undesirable - breakage and for this correctly work, we do need OR region constraints.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-trait-system-refactor The Rustc Trait System Refactor Initiative (-Znext-solver)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

MIR borrowck ignores ambiguity in ProvePredicate

6 participants