Refactor `ty_is_int` #200

tiif · 2025-08-12T08:40:52Z

Ignore the first commit, it is just UPDATE_EXPECT=1 for the change in main branch

Fixed #198

lcnr · 2025-08-12T08:53:24Z

crates/formality-check/src/mini_rust_check.rs

-                if !ty_is_int(value_ty) {
-                    bail!("The value used for switch must be an int.");
-                }
+                self.prove_goal(&typeck_env.env, Wcs::default(), value_ty.is_int())?;


I personally don't like introducing a new judgement for this. I think if we want this check to be a proper judgement maybe add a builtin trait and prove value_ty: BuiltinInteger here 🤔

Even if it's a proper judegement:tm: but instead be just something else you can prove. Predicates feel core to the type system in a way in which "is this an integer" does not. That's just my personal vibe here though

What's the reasoning behind changing an assertion to an actual goal?

The reason of changing this to a goal is I feel we should have a way to say "this type is an int" somewhere instead of having this function https://github.com/rust-lang/a-mir-formality/pull/200/files#diff-b58482e54c5aa3c63282fc2a3a0aa88194e826004773bd7bc9e385f29b5c3e0d

But I do agree that adding a predicate for this might be an overkill.

could we instead just use a "non-predicate" judgement here. Same as we do for trait_ref_is_knowable or however it's called?

Oh, I forgot to mention that I was using a Relation instead of Predicate.

From my understanding, we can only use a judgment_fn! through prove_wc, and when we call prove_wc, we need to pick one of the below as the Wc type:

pub enum WcData { /// Means the built-in relation holds. #[cast] Relation(Relation), /// Means the predicate holds. #[cast] Predicate(Predicate), // Equivalent to `for<'a>` except that it can also express `for<ty T>` and so forth: // means `$v0` is true for any value of the bound variables (e.g., `'a` or `T`). #[grammar(for $v0)] ForAll(Binder<Wc>), #[grammar(if $v0 $v1)] Implies(Wcs, Wc), }

Relation looks the most reasonable to me among all of them.

lcnr · 2025-08-12T08:54:09Z

crates/formality-prove/src/prove/prove_wc.rs

+        (
+            (is_int(decl, env, assumptions, ty) => c)
+            ----------------------------- ("ty is int")
+            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)


how does a-mir-formality handle normalization when proving predicates/relations?

Because right now <u32 as Id>::This fails to satisfy IsInt

Yeah that's true, I did an experiment in 331c737#diff-2ca1246445028c80247cd13d93fd973d22ca55cfb7a76c0903a04c09055d706c and it indeed failed.

The place where normalization is done should be here

a-mir-formality/crates/formality-prove/src/prove/prove_normalize.rs

Line 17 in 8b130f7

pub fn prove_normalize(

It is possible to use prove_normalize when proving a goal, for example:

a-mir-formality/crates/formality-prove/src/prove/is_local.rs

Lines 288 to 295 in 8b130f7

(

(prove_normalize(&decls, env, &assumptions, goal) => (c1, p))

(let assumptions = c1.substitution().apply(&assumptions))

(is_local_parameter(&decls, c1.env(), assumptions, p) => c2)

--- ("local parameter")

(is_local_parameter(decls, env, assumptions, goal) => c1.seq(c2))

)

But with the change in c0fbd8b, it is possible to make IsInt work with normalization.

lcnr · 2025-08-12T13:39:48Z

crates/formality-prove/src/prove/prove_wc.rs

+            (let assumptions = c1.substitution().apply(&assumptions))
+            (is_int(&decl, &env, assumptions, p) => c2)
+            ----------------------------- ("ty is int")
+            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c2)


hmm, maybe also as a question for @nikomatsakis

This currently means there are 2 leaf judegements for proving is_int, one with normalization and one without.

What does prove_normalize actually do 😅 is it "normalize until rigid [but at least 1 step]" or "normalize 1 step"?

I think regardless, I personally prefer the setup of prove_wc(Relation::IsInt(ty)) -> normalize(ty) -> prove_wc(Relation::IsInt(normalized_ty)) so that there's only one "leaf" judgement here

I write two judgements because prove_normalize will fail if we pass an int type to it. I slightly changed the rule for ty_is_int in 1f601cf so it always normalize the type to rigid if possible, and if it can't be normalize to rigid, it should just fail.

Answer: prove_normalize does a single step. I think this logic is good, because the base mir-formality infra should handle cycles -- we should add a test for fun, though.

The idea is that judgment functions correspond to "Random Rust Code" in the compiler and Predicates/Relations are limited to things that can appear in where-clauses (explicitly or implicitly). The `formality_prove` module then roughly corresponds to the trait system + type inference logic in rustc.

nikomatsakis · 2025-08-15T13:05:48Z

@lcnr -- @tiif and I discussed it and did a bit of refactoring. Now there is no Relation::TyIsInt and instead we are writing judgments in the mini-rust-check, which I think corresponds a bit more to the compiler (judgment fn is basically "Random Rust Code" and predicates/relations are reserved for things you will find in where-clause lists, implicitly or explicitly).

lcnr · 2025-08-15T14:44:39Z

crates/formality-check/src/mini_rust_check.rs

+        // For the rest of the case, it should fail.
+
+        (
+            (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))


Suggested change

(prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))

(prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))!

I'd guess we don't care about this candidate if stuff is unnormalizeable? or well, we currently use this judegement even for non alias types 🤔 I feel like maybe limiting prove_normalize to require an AliasTerm (or whatever we've got in a-mir-formality) would make avoid this?

Yes, I debated about that. I think this is a good addition, the only downside would be if you expect it to be normalizable and it's not... you won't readily know why... might be that we can do better with these annotations.

I feel like maybe limiting prove_normalize to require an AliasTerm (or whatever we've got in a-mir-formality) would make avoid this?

Thinking about this, this seems generally desirable esp if it's literally shallow one-step normalization, using it for non-alias types seems weird imo

clearly not something that has to happen in this PR 😁

lcnr

the impl seems nice now 😊 👍

Co-authored-by: lcnr <[email protected]>

tiif added 5 commits August 12, 2025 10:39

UPDATE_EXPECT=1 for the failing test in main

a889ecd

Write down the rules

992f4c2

Use prove_goal to check if the type is int

9980d0e

Update tests

6ee4489

fmt

4379ad6

lcnr reviewed Aug 12, 2025

View reviewed changes

tiif added 7 commits August 12, 2025 10:55

remove spurious change

652dba9

Experiment with projection

331c737

fmt

e237c2d

Remove spurious change

df0fe30

Make is_int work with normalization

c0fbd8b

Add an extra rule for rigidty

c7f3363

Slightly tweak the logic

582560e

lcnr reviewed Aug 12, 2025

View reviewed changes

tiif and others added 3 commits August 15, 2025 13:33

Refactor ty_is_int

1f601cf

remove fn is_alias

33d8a48

lcnr reviewed Aug 15, 2025

View reviewed changes

Update crates/formality-check/src/mini_rust_check.rs

130f628

Co-authored-by: lcnr <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Refactor `ty_is_int` #200

Refactor `ty_is_int` #200

Uh oh!

tiif commented Aug 12, 2025

Uh oh!

lcnr Aug 12, 2025

Uh oh!

tiif Aug 12, 2025

Uh oh!

lcnr Aug 12, 2025

Uh oh!

tiif Aug 15, 2025 •

edited

Loading

Uh oh!

lcnr Aug 12, 2025

Uh oh!

tiif Aug 12, 2025

Uh oh!

tiif Aug 12, 2025

Uh oh!

lcnr Aug 12, 2025 •

edited

Loading

Uh oh!

tiif Aug 15, 2025 •

edited

Loading

Uh oh!

nikomatsakis Aug 15, 2025

Uh oh!

nikomatsakis commented Aug 15, 2025

Uh oh!

lcnr Aug 15, 2025

Uh oh!

nikomatsakis Aug 15, 2025

Uh oh!

lcnr Aug 18, 2025

Uh oh!

lcnr left a comment

Uh oh!

Uh oh!

	(
	(prove_normalize(&decls, env, &assumptions, goal) => (c1, p))
	(let assumptions = c1.substitution().apply(&assumptions))
	(is_local_parameter(&decls, c1.env(), assumptions, p) => c2)
	--- ("local parameter")
	(is_local_parameter(decls, env, assumptions, goal) => c1.seq(c2))
	)

	(prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
	(prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))!

Refactor ty_is_int #200

Are you sure you want to change the base?

Refactor ty_is_int #200

Uh oh!

Conversation

tiif commented Aug 12, 2025

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!

tiif Aug 15, 2025 • 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!

lcnr Aug 12, 2025 • 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!

tiif Aug 15, 2025 • 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!

nikomatsakis commented Aug 15, 2025

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!

lcnr left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Refactor `ty_is_int` #200

Refactor `ty_is_int` #200

tiif Aug 15, 2025 •

edited

Loading

lcnr Aug 12, 2025 •

edited

Loading

tiif Aug 15, 2025 •

edited

Loading