remove last vestiges of the old check by nikomatsakis · Pull Request #244 · rust-lang/a-mir-formality

nikomatsakis · 2026-02-25T14:27:19Z

No description provided.

nikomatsakis · 2026-02-25T14:27:57Z

I have to rebase this and drop the first two commits I think

nikomatsakis · 2026-02-26T14:50:17Z

OK, this has been rebased and is ready to go! cc @lqd @tiif

Also cc @BoxyUwU, this modifies slightly the const syntax, but not the new fancy stuff we were talking about.

tiif

I like the new function argument syntax :) Other than the nit, everything looks good.

Also, the final commit message is different from the diff, did you forget to add the change?

View changes since this review

tiif · 2026-02-27T08:41:51Z

-        expect_test::expect![[r#"
-            the rule "borrow of disjoint places" at (nll.rs) failed because
-              condition evaluted to false: `place_disjoint_from_place(&loan.place.to_place_expression(), &access.place)`
-                &loan.place.to_place_expression() = *(local(m))
-                &access.place = *(local(m))
-
-            the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
-              condition evaluted to false: `outlived_by_loan.iter().all(|p| match p
-              {
-                  Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.data()
-                  {
-                      LtData::Static => false, LtData::Variable(Variable::UniversalVar(_))
-                      => false, LtData::Variable(Variable::ExistentialVar(_)) => true,
-                      LtData::Variable(Variable::BoundVar(_)) =>
-                      panic!("cannot outlive a bound var"),
-                  }, Parameter::Const(_) => panic!("cannot outlive a constant"),
-              })`
-
-            the rule "write-indirect" at (nll.rs) failed because
-              pattern `TypedPlaceExpressionKind::Deref(place_loaned_ref)` did not match value `local(m)`
-
-            the rule "write-indirect" at (nll.rs) failed because
-              condition evaluted to false: `place_accessed.is_prefix_of(&place_loaned_ref.to_place_expression())`
-                place_accessed = *(local(m))
-                &place_loaned_ref.to_place_expression() = local(m)"#]]


It's interesting that this problem case 3 test passed. I suppose it is related to the change where we move verify_universal_outlives to prove_judgment, but I don't really understand why.

same, I don't understand why this changed either, nor why checking for universal subset errors more or at a different place would change anything here.

The reason that problem case number 3 passes now is because we are no longer collecting all the outlives relations in a pre-pass and then using them everywhere along the graph, but rather accumulating them as we go. This is the heart of polonius, basically, and so it fixes this behavior.

tiif · 2026-02-27T09:22:27Z

We should be able to remove this function, it is no longer used.

lqd

+1 on tiif's comments
the new syntax is way better
the last 2 commits also likely need to be dropped
It'd be cool to discuss the change we don't understand at the next meeting

View changes since this review

lqd · 2026-02-28T17:27:05Z

@@ -134,19 +135,9 @@ enum AccessKind {
 /// Given the `TypeckEnv`, and a (populated) list of `pending_outlives`


we can also remove this mention of pending_outlives since it's removed in this commit

lqd · 2026-02-28T17:31:17Z

-    $*params
-
+#[term(minirust {
    // then declare the body


"the body" instead?

lqd · 2026-02-28T17:38:01Z

-        expect_test::expect![[r#"
-            the rule "borrow of disjoint places" at (nll.rs) failed because
-              condition evaluted to false: `place_disjoint_from_place(&loan.place.to_place_expression(), &access.place)`
-                &loan.place.to_place_expression() = *(local(m))
-                &access.place = *(local(m))
-
-            the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
-              condition evaluted to false: `outlived_by_loan.iter().all(|p| match p
-              {
-                  Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.data()
-                  {
-                      LtData::Static => false, LtData::Variable(Variable::UniversalVar(_))
-                      => false, LtData::Variable(Variable::ExistentialVar(_)) => true,
-                      LtData::Variable(Variable::BoundVar(_)) =>
-                      panic!("cannot outlive a bound var"),
-                  }, Parameter::Const(_) => panic!("cannot outlive a constant"),
-              })`
-
-            the rule "write-indirect" at (nll.rs) failed because
-              pattern `TypedPlaceExpressionKind::Deref(place_loaned_ref)` did not match value `local(m)`
-
-            the rule "write-indirect" at (nll.rs) failed because
-              condition evaluted to false: `place_accessed.is_prefix_of(&place_loaned_ref.to_place_expression())`
-                place_accessed = *(local(m))
-                &place_loaned_ref.to_place_expression() = local(m)"#]]


same, I don't understand why this changed either, nor why checking for universal subset errors more or at a different place would change anything here.

lqd · 2026-02-28T17:41:37Z

        LivePlaces,
    },
-    mini_rust_check::{ty_is_adt, ty_is_ref, Location, PendingOutlives, TypeckEnv},
+    mini_rust_check::{ty_is_adt, ty_is_int, ty_is_ref, Location, PendingOutlives, TypeckEnv},


did retcon fail in this commit? the message looks more about the previous commit than this one

lqd · 2026-02-28T17:43:46Z

        LivePlaces,
    },
-    mini_rust_check::{ty_is_adt, ty_is_int, ty_is_ref, Location, PendingOutlives, TypeckEnv},
+    mini_rust_check::{ty_is_adt, ty_is_ref, Location, PendingOutlives, TypeckEnv},


this is the inverse of the previous commit? "fix: check switch discriminant is an integer type in NLL"? :/

… signatures

Move verify_universal_outlives check from the return terminator into prove_judgment, so it runs every time outlives constraints accumulate. This catches unsound universal region relationships even in code that never returns (e.g., infinite loops). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

rustbot · 2026-03-09T13:03:40Z

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.

- Remove dead `check_blocks` function - Update stale `pending_outlives` doc comment - Fix "then declare the body" → "the body" comment Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nikomatsakis · 2026-03-11T13:12:08Z

We discussed this in detail. We decided to merge the code but to open a FIXME about adding back in the outlives constraints needed to accurately model NLL-as-it-is-today.

lqd · 2026-03-13T12:01:09Z

I was surprised this wasn't merged yet, especially because I mistakenly said it was in our call yesterday, apologies.

So I've made CI green and took care of

but to open a FIXME about adding back in the outlives constraints needed to accurately model NLL-as-it-is-today.

Done in #253

nikomatsakis force-pushed the living-large branch from 7e62c1c to f3f57e9 Compare February 26, 2026 14:48

This comment has been minimized.

Sign in to view

nikomatsakis requested a review from lqd February 26, 2026 14:49

tiif reviewed Feb 27, 2026

View reviewed changes

lqd reviewed Feb 28, 2026

View reviewed changes

nikomatsakis and others added 5 commits March 8, 2026 17:20

refactor: add InputArg to pair parameter names with types in function…

a0a56b8

… signatures

refactor: simplify MiniRust body syntax and add MiniRustConst

a18dc50

fix: check switch discriminant is an integer type in NLL

14e041d

fixup: fix rebase artifacts from all-refs and tick-syntax merges

60b1620

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nikomatsakis force-pushed the living-large branch from f3f57e9 to 60b1620 Compare March 9, 2026 13:03

chore: address PR review nits

4eb8947

- Remove dead `check_blocks` function - Update stale `pending_outlives` doc comment - Fix "then declare the body" → "the body" comment Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

pacify rustfmt

0ff1b44

lqd mentioned this pull request Mar 13, 2026

Add back limitations to more accurately model NLLs #253

Open

nikomatsakis merged commit 1448023 into rust-lang:main Mar 13, 2026
3 checks passed

rustbot mentioned this pull request Mar 13, 2026

Add covering set impl for generic version of trait when all values of a const are covered by impls #132

Closed

		@@ -134,19 +135,9 @@ enum AccessKind {
		/// Given the `TypeckEnv`, and a (populated) list of `pending_outlives`

Conversation

nikomatsakis commented Feb 25, 2026

Uh oh!

nikomatsakis commented Feb 25, 2026

Uh oh!

This comment has been minimized.

nikomatsakis commented Feb 26, 2026

Uh oh!

tiif left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lqd left a comment • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rustbot commented Mar 9, 2026

Uh oh!

nikomatsakis commented Mar 11, 2026

Uh oh!

lqd commented Mar 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tiif left a comment •

edited

Loading

lqd left a comment •

edited by rustbot

Loading