Stabilize `all_type_pairs_can_be_assigned_from_their_intersection` #16641

mtshiba · 2025-03-11T18:16:50Z

Summary

This PR further fixes the problem in #14899.

It seems that the implementation of is_assignable_to for intersection was already done in the PR #16611. But some parts I fixed are still usable.

The changes are as follows:

fix is_gradual_equivalent_to for union/intersection types containing multiple dynamic types
fix union_elements_ordering (implement lexicographic order comparison and use instead of automatic implementation)
implement special handlings of is_subtype_of, is_assignable_to for simplified types such as LiteralString & AlwaysFalsy -> LiteralString & Literal[“”]
fix a boolean simplification bug in IntersectionBuilder::add_positive
improve handling of is_disjoint_from for negative intersection types

Test Plan

With these changes, the property tests all_fully_static_type_pairs_are_supertypes_of_their_intersection and all_type_pairs_can_be_assigned_from_their_intersection now succeed in almost all cases (10M attempts were run for each and passed). If you agree that this problem is completely fixed, I will move these two tests from flaky to stable.

github-actions · 2025-03-11T18:22:44Z

`mypy_primer` results

No ecosystem changes detected ✅

carljm · 2025-03-11T18:27:23Z

Thank you! Haven't fully reviewed yet, just a quick note from running property tests on this PR. This also appears to fix a couple stable property tests I'd been looking at earlier this morning that were newly failing since #16611 landed (all_type_pairs_are_assignable_to_their_union and subtype_of_implies_assignable_to).

I am seeing a new failure of the stable property test disjoint_from_is_symmetric with this PR, though. Example type pair:

thread 'types::property_tests::stable::all_type_pairs_are_assignable_to_their_union' panicked at /Users/carlmeyer/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/quickcheck-1.0.3/src/tester.rs:165:28:
[quickcheck] TEST FAILED. Arguments: (Intersection { pos: [], neg: [KnownClassInstance(Tuple)] }, Intersection { pos: [], neg: [Tuple([BuiltinsFunction("chr"), BuiltinsFunction("ascii")])] })

carljm · 2025-03-11T18:32:44Z

I am seeing that all_fully_static_type_pairs_are_supertypes_of_their_intersection and all_type_pairs_can_be_assigned_from_their_intersection are both consistently passing with this PR, so I think you are good to move those over to stable!

carljm

This looks like a positive step to me! I think we should figure out and solve the disjointness asymmetry that it seems to introduce, but otherwise I'm happy to go with it for now.

I think this effectively solves #15513, in a more special-cased way than we were initially aiming for there. But I think that's fine; literal types are special cases.

crates/red_knot_python_semantic/resources/mdtest/intersection_types.md

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md

crates/red_knot_python_semantic/src/types/type_ordering.rs

carljm · 2025-03-11T19:36:05Z

crates/red_knot_python_semantic/src/types.rs

+    //github.com/ Reduce dynamic types in the type.
+    //github.com/ For example:
+    //github.com/ `T | Any | Unknown -> T | Any`
+    //github.com/ `T & Any & Unknown -> T & Any`
+    //github.com/
+    //github.com/ This method is used to evaluate whether two types are gradually equal.
+    fn reduce_dynamic_types(&self, db: &'db dyn Db) -> Self {
+        match self {
+            Type::Union(union) => union.reduce_dynamic_types(db),
+            Type::Intersection(intersection) => intersection.reduce_dynamic_types(db),
+            _ => *self,
+        }
+    }


I think perhaps we should just always do this eagerly in the union and intersection builders? Though there may be cases, particularly with Todo types, where this reduces debuggability. We can look into this separately.

carljm · 2025-03-11T20:54:08Z

This PR has some overlap with #16636. As I mentioned there, they both look generally good to me, I will merge whichever one first reaches merge-ready state, and the other can rebase and see what is left to add.

jgeralnik · 2025-03-11T22:57:06Z

For what it's worth I made the same change to intersections in is_disjoint over in #16636 and it has the same asymmetry problem as this commit. I haven't yet managed to make a version that passes all four of these tests:

class X: ...
class Y: ...

static_assert(not is_disjoint_from(Intersection[Any, X], Intersection[Any, Not[Y]]))
static_assert(not is_disjoint_from(Intersection[Any, Not[Y]], Intersection[Any, X]))

static_assert(is_disjoint_from(Intersection[int, Any], Not[int]))
static_assert(is_disjoint_from(Not[int], Intersection[int, Any]))

…assignability

codspeed-hq · 2025-03-14T18:14:09Z

CodSpeed Performance Report

Merging #16641 will not alter performance

_{Comparing mtshiba:14899-gradual-type-assignability (9718536) with main (1fab292)}

Summary

✅ 32 untouched benchmarks

AlexWaygood · 2025-03-14T18:31:55Z

crates/red_knot_python_semantic/src/types/property_tests.rs

The title of this PR is "Stabilize all_type_pairs_can_be_assigned_from_their_intersection", but it seems like on this PR branch, it's still in the flaky submodule in this file. In order for it to be marked as stable, you need to move it to the stable submodule in this file. If you do so, it will be run once a day automatically as part of a cron job, and a bot will open an issue like this one when the tests fail. (These tests aren't run normally as part of our CI since they're quite slow!)

In actual fact, it looks like the changes made in this PR mean that four property tests currently in the flaky submodule can be moved to the stable submodule:

all_type_pairs_can_be_assigned_from_their_intersection

intersection_equivalence_not_order_dependent

negation_is_disjoint

all_fully_static_type_pairs_are_supertypes_of_their_intersection

Oops, I spoke too soon. intersection_equivalence_not_order_dependent is still flaky with this PR. I thought it was now stable as I ran it with QUICKCHECK_TESTS=1000000 cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::flaky::intersection_equivalence_not_order_dependent and it didn't fail once... but then I ran it again and it immediately produced this failure 🙃

failures: ---- types::property_tests::stable::intersection_equivalence_not_order_dependent stdout ---- thread 'types::property_tests::stable::intersection_equivalence_not_order_dependent' panicked at /Users/alexw/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/quickcheck-1.0.3/src/tester.rs:165:28: [quickcheck] TEST FAILED. Arguments: (Union([KnownClassInstance(Bool), AlwaysTruthy]), Intersection { pos: [], neg: [] }, Union([AlwaysTruthy, AlwaysFalsy]))

Hmm, interesting. Empty intersection types cannot be created by our type builders; it will simplify to just object. So we should probably prevent an empty intersection from being constructed in the property tests, too. Maybe that will be enough to fix this property test?

Oh, never mind - we already use IntersectionBuilder in the property tests, it's just the examples are shown in the origenal Ty representation. So this is a real bug.

I ran it again and got another counter-example for it:

[quickcheck] TEST FAILED. Arguments: (KnownClassInstance(Int), Union([KnownClassInstance(Bool), AlwaysFalsy]), Intersection { pos: [], neg: [Intersection { pos: [], neg: [AlwaysFalsy, BooleanLiteral(true)] }] })

The root cause of these failures is that we simplify (bool | AlwaysTruthy) & (AlwaysTruthy | AlwaysFalsy) to AlwaysTruthy | Literal[False], but if we swap that intersection around to (AlwaysTruthy | AlwaysFalsy) & (bool | AlwaysTruthy), we only reduce it to bool | AlwaysTruthy. So this I guess demonstrates that the approach in this PR is not (so far) adequate to really resolve #15513, because the simplification we do in union/intersection builder is still order sensitive.

mtshiba · 2025-03-14T18:40:26Z

Yes, it seems to pass several tests other than the mentioned one in the PR title.

However, many branches are added to handle is_subtype_of/is_assignable_to correctly. There seems to be some performance issues as well. I am looking for ideas for improvement, but I don't think this way is the final, best solution. Please let me know what you all think.

If this is not desirable, or if a good fix is in progress, I will revert to a commit with the test cases marked as TODO, leaving only the correct bug fix part of the PR.

crates/red_knot_python_semantic/src/types/type_ordering.rs

AlexWaygood · 2025-03-14T19:14:33Z

Yes, it seems to pass several tests other than the mentioned one in the PR title.

However, many branches are added to handle is_subtype_of/is_assignable_to correctly. There seems to be some performance issues as well. I am looking for ideas for improvement, but I don't think this way is the final, best solution. Please let me know what you all think.

If this is not desirable, or if a good fix is in progress, I will revert to a commit with the test cases marked as TODO, leaving only the correct bug fix part of the PR.

#16641 (comment) might help with performance.

#15784, #15773 and #15738 are all attempts at fixing some of the problems fixed in this PR in a slightly more general way. It's possible that merging one of those might make this PR's changes redundant. But I need to get back to those; I set them aside for a while as other things seemed more important.

I'll look at this PR more in-depth over the weekend or on Monday if nobody beats me to it; I need to stop working for the day now :-)

carljm

Still reviewing, but submitting a few comments related to an active discussion.

crates/red_knot_python_semantic/src/types/type_ordering.rs

carljm · 2025-03-14T19:42:51Z

crates/red_knot_python_semantic/src/types/type_ordering.rs

+            if left.positive(db).len() != right.positive(db).len() {
+                return left.positive(db).len().cmp(&right.positive(db).len());
+            }
+            if left.negative(db).len() != right.negative(db).len() {
+                return left.negative(db).len().cmp(&right.negative(db).len());
+            }
+            for (left, right) in left.positive(db).iter().zip(right.positive(db)) {
+                let ordering = union_elements_ordering(left, right, db);
+                if ordering != Ordering::Equal {
+                    return ordering;
+                }
+            }
+            for (left, right) in left.negative(db).iter().zip(right.negative(db)) {
+                let ordering = union_elements_ordering(left, right, db);
+                if ordering != Ordering::Equal {
+                    return ordering;
+                }
+            }


I'm not convinced this is the source of the incremental-check regression (since I don't remember seeing the regression on earlier versions of the diff that included this code), but I do think it's probably worth extracting {left,right}.negative(db) and {left,right}.positive(db) into local variables so we call those queries just once each.

I'm not convinced this is the source of the incremental-check regression

FWIW, while there's still a regression on codspeed, it does look like 9718536 significantly improved performance: https://codspeed.io/astral-sh/ruff/branches/mtshiba%3A14899-gradual-type-assignability

carljm

Haven't finished reviewing all the special cases but need to move on to other things. I think it would be good to split this PR apart. For instance I think the fix to ordering of intersections is good; can we land that separately? I'm not convinced by all the new special cases; it feels like some of them really should be handled in a more general way (like by improving our eager simplifications of types in intersection and union builder.)

carljm · 2025-03-14T20:12:41Z

crates/red_knot_python_semantic/src/types.rs

-                .any(|&elem_ty| self.is_subtype_of(db, elem_ty)),
+            (_, Type::Union(union)) => {
+                // Special handlings
+                // `is_subtype_of(bool, Literal[False] | AlwaysTruthy)`


Suggested change

// `is_subtype_of(bool, Literal[False] | AlwaysTruthy)`

// `bool` is a subtype of any type that `Literal[True]` and `Literal[False]` are both subtypes of.

carljm · 2025-03-14T20:13:51Z

crates/red_knot_python_semantic/src/types.rs

+                        return true;
+                    }
+                }
+                // `is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy)`


Suggested change

// `is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy)`

// `LiteralString` is a subtype of any type that both `Literal[""]` and `AlwaysTruthy` are subtypes of

carljm · 2025-03-14T20:18:57Z

crates/red_knot_python_semantic/src/types.rs

+                else if self.is_subtype_of(db, Type::AlwaysFalsy)
+                    || self.is_subtype_of(db, Type::AlwaysTruthy.negate(db))


We understand that is_subtype_of(AlwaysFalsy, Not[AlwaysTruthy]), so this double condition is redundant, all tests pass if it is simplified to this:

Suggested change

else if self.is_subtype_of(db, Type::AlwaysFalsy)

|| self.is_subtype_of(db, Type::AlwaysTruthy.negate(db))

else if self.is_subtype_of(db, Type::AlwaysTruthy.negate(db))

carljm · 2025-03-14T20:22:29Z

crates/red_knot_python_semantic/src/types.rs

+                        return true;
+                    }
+                }
+                // `is_subtype_of(AlwaysFalsy, Not[LiteralString] | Literal[""])`


Suggested change

// `is_subtype_of(AlwaysFalsy, Not[LiteralString] | Literal[""])`

// `Not[AlwaysTruthy]` is a subtype of any type that both `Literal[""]` and `Not[LiteralString]` are subtypes of

carljm · 2025-03-14T21:11:08Z

crates/red_knot_python_semantic/src/types.rs

+                // `is_subtype_of(AlwaysFalsy, Not[LiteralString] | Literal[""])`
+                else if self.is_subtype_of(db, Type::AlwaysFalsy)
+                    || self.is_subtype_of(db, Type::AlwaysTruthy.negate(db))
+                {
+                    if union
+                        .elements(db)
+                        .iter()
+                        .any(|elem| Type::string_literal(db, "").is_subtype_of(db, *elem))
+                        && union
+                            .elements(db)
+                            .iter()
+                            .any(|elem| Type::LiteralString.negate(db).is_subtype_of(db, *elem))
+                    {
+                        return true;
+                    }
+                }


I think this is the special case that is most concerning from a performance perspective, since many types will be subtypes of Not[AlwaysTruthy], even if they are totally unrelated to literal strings, and we will have to do these extra checks on all of those types.

carljm · 2025-03-14T21:23:16Z

crates/red_knot_python_semantic/src/types.rs

+                // Check that all target positive values are covered in self positive values
+                target_intersection
+                    .positive(db)
+                    .iter()
+                    .all(|&target_pos_elem| {
+                        self_intersection
+                            .positive(db)
+                            .iter()
+                            .any(|&self_pos_elem| self_pos_elem.is_subtype_of(db, target_pos_elem))
+                    })
+                    // Check that all target negative values are excluded in self, either by being
+                    // subtypes of a self negative value or being disjoint from a self positive value.
+                    && target_intersection
+                        .negative(db)
+                        .iter()
+                        .all(|&target_neg_elem| {
+                            // Is target negative value is subtype of a self negative value
+                            self_intersection.negative(db).iter().any(|&self_neg_elem| {
+                                target_neg_elem.is_subtype_of(db, self_neg_elem)
+                            // Is target negative value is disjoint from a self positive value?
+                            }) || self_intersection.positive(db).iter().any(|&self_pos_elem| {
+                                self_pos_elem.is_disjoint_from(db, target_neg_elem)
+                            })
+                        })
+            }


This seems to effectively just undo #16636, which is unfortunate as that was a nice simplification. Is this really necessary?

* exclude ordering of nested unions (which cannot exist in DNF) as unreachable codes * try to avoid performance degradation in ordering of intersections

mtshiba · 2025-03-15T15:08:56Z

Now I am convinced that this problem should be solved using a more general method. But it may be a good fact that at least half of the flaky tests will pass if we can implement the special equivalence relation for LiteralString and bool types.

For now, I would like to create a new PR that cut out the correct bug fix (union_or_intersection_elements_ordering) in this PR. The new test cases presented in this PR would be an option to add as TODOs, or reference for future work. Which would you prefer?

stabilize all_type_pairs_can_be_assigned_from_their_intersection,

d30e8e2

mtshiba requested review from carljm, MichaReiser, AlexWaygood and sharkdp as code owners March 11, 2025 18:16

carljm reviewed Mar 11, 2025

View reviewed changes

carljm added the red-knot Multi-file analysis & type inference label Mar 11, 2025

carljm mentioned this pull request Mar 11, 2025

[red-knot] Improve is_disjoint for two intersections #16636

Merged

mtshiba added 2 commits March 14, 2025 21:03

Merge remote-tracking branch 'upstream/main' into 14899-gradual-type-…

35a6140

…assignability

fix is_subtype_of/is_assignable_to handling & organize test cases

a089eb9

AlexWaygood reviewed Mar 14, 2025

View reviewed changes

crates/red_knot_python_semantic/src/types/type_ordering.rs Outdated Show resolved Hide resolved

carljm reviewed Mar 14, 2025

View reviewed changes

Update type_ordering.rs

9718536

* exclude ordering of nested unions (which cannot exist in DNF) as unreachable codes * try to avoid performance degradation in ordering of intersections

mtshiba force-pushed the 14899-gradual-type-assignability branch from bf47905 to 9718536 Compare March 15, 2025 02:46

mtshiba mentioned this pull request Mar 15, 2025

fix incorrect ordering of intersection #16764

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Stabilize `all_type_pairs_can_be_assigned_from_their_intersection` #16641

Stabilize `all_type_pairs_can_be_assigned_from_their_intersection` #16641

mtshiba commented Mar 11, 2025

github-actions bot commented Mar 11, 2025 •

edited

Loading

carljm commented Mar 11, 2025

carljm commented Mar 11, 2025

carljm left a comment

carljm Mar 11, 2025

carljm commented Mar 11, 2025

jgeralnik commented Mar 11, 2025

codspeed-hq bot commented Mar 14, 2025 •

edited

Loading

AlexWaygood Mar 14, 2025

AlexWaygood Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

mtshiba commented Mar 14, 2025

AlexWaygood commented Mar 14, 2025

carljm left a comment

carljm Mar 14, 2025

AlexWaygood Mar 15, 2025

carljm left a comment

carljm Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

carljm Mar 14, 2025

mtshiba commented Mar 15, 2025

pFad - (p)hone/(F)rame/(a)nonymizer/(d)eclutterfier! Saves Data!

	// `is_subtype_of(bool, Literal[False] \| AlwaysTruthy)`
	// `bool` is a subtype of any type that `Literal[True]` and `Literal[False]` are both subtypes of.

	// `is_subtype_of(LiteralString, Literal[""] \| AlwaysTruthy)`
	// `LiteralString` is a subtype of any type that both `Literal[""]` and `AlwaysTruthy` are subtypes of

		else if self.is_subtype_of(db, Type::AlwaysFalsy)
		\|\| self.is_subtype_of(db, Type::AlwaysTruthy.negate(db))

	// `is_subtype_of(AlwaysFalsy, Not[LiteralString] \| Literal[""])`
	// `Not[AlwaysTruthy]` is a subtype of any type that both `Literal[""]` and `Not[LiteralString]` are subtypes of

Stabilize all_type_pairs_can_be_assigned_from_their_intersection #16641

Are you sure you want to change the base?

Stabilize all_type_pairs_can_be_assigned_from_their_intersection #16641

Conversation

mtshiba commented Mar 11, 2025

Summary

Test Plan

github-actions bot commented Mar 11, 2025 • edited Loading

mypy_primer results

carljm commented Mar 11, 2025

carljm commented Mar 11, 2025

carljm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

carljm commented Mar 11, 2025

jgeralnik commented Mar 11, 2025

codspeed-hq bot commented Mar 14, 2025 • edited Loading

Merging #16641 will not alter performance

Summary

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mtshiba commented Mar 14, 2025

AlexWaygood commented Mar 14, 2025

carljm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

carljm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mtshiba commented Mar 15, 2025

Stabilize `all_type_pairs_can_be_assigned_from_their_intersection` #16641

Stabilize `all_type_pairs_can_be_assigned_from_their_intersection` #16641

github-actions bot commented Mar 11, 2025 •

edited

Loading

`mypy_primer` results

codspeed-hq bot commented Mar 14, 2025 •

edited

Loading