[red-knot] Distribute intersections on negation #13962

rtpg · 2024-10-28T10:59:06Z

Summary

This does two things:

distribute negated intersections when building up intersections (i.e. going from A & ~(B & C) to (A & ~B) | (A & ~C)) (fixing [red-knot] fix adding intersection to negative side of an intersection #13931)
add some classes from typing to KnownClass

The second point was to enable writing a test for the first case using protocols defined in typing (here, Sized and Hashable). Was a bit worried about another test that could be susceptible to simplifications, and it was straightforward to pull in

Test Plan

cargo test

rtpg · 2024-10-28T11:54:40Z

Sorry, in my rush to send this in with the test I added passing I had intro'd a regression on another test. Please ignore this PR until I get this green (unless you know what's actually wrong here of course)

MichaReiser · 2024-10-28T11:57:05Z

@rtpg no worries. I'll convert the PR to a draft and you can mark it as ready when it's ready :)

crates/red_knot_python_semantic/src/types/builder.rs

github-actions · 2024-10-28T23:43:00Z

`ruff-ecosystem` results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

rtpg · 2024-10-29T00:12:50Z

Alright this one is ready for review, all green etc.

rtpg · 2024-10-29T00:25:06Z

crates/red_knot_python_semantic/src/types/builder.rs

+                IntersectionBuilder::new(&db)
+                    .add_positive(it)
+                    .add_negative(st)
+                    .build(),


a part of me wants something like Type::intersection(elts: Vec<Type<'db>>) for testing but I got pretty used to writing out the intersection builder at this point 😆

Ha, you aren't the first to say this after working on IntersectionBuilder, cc @sharkdp 😆 It's not a problem at all to add test helpers to make tests less verbose, someone just needs to feel the pain sufficiently to actually do it!

rtpg · 2024-10-29T00:45:11Z

crates/red_knot_python_semantic/src/types.rs

@@ -1232,6 +1244,9 @@ impl<'db> KnownClass {
            | Self::Set
            | Self::Dict => module.name() == "builtins",
            Self::GenericAlias | Self::ModuleType | Self::FunctionType => module.name() == "types",
+            Self::Sized | Self::Hashable => {


basically all of the "interesting" protocols in typing are deprecated aliases at this point to members of collections.abc.

carljm

Looks great, thank you! Just a few suggested changes, main one being to remove Sized and Hashable from KnownClass

carljm · 2024-10-29T02:05:18Z

crates/red_knot_python_semantic/src/stdlib.rs

@@ -63,6 +65,13 @@ pub(crate) fn types_symbol_ty<'db>(db: &'db dyn Db, symbol: &str) -> Type<'db> {
    core_module_symbol_ty(db, CoreStdlibModule::Types, symbol)
 }

+/// Lookup the type of `symbol` in the `typing` module namespace.
+///
+/// Returns `Unbound` if the `types` module isn't available for some reason.


Suggested change

/// Returns `Unbound` if the `types` module isn't available for some reason.

/// Returns `Unbound` if the `typing` module isn't available for some reason.

carljm · 2024-10-29T02:10:29Z

crates/red_knot_python_semantic/src/types.rs

+    // Typing
+    Sized,
+    Hashable,


Sorry to catch this only after you'd done the work, but I don't see any reason for these to be known classes? We should only use KnownClass when either a) the type has special-cased behavior that is not reflected in its typeshed definition, or b) we will commonly need to conjure this type "from thin air" within the type inference code itself, usually because the type is builtin and sometimes created "from thin air" by the runtime (e.g. bool) or because it is closely related to other special-cased types (e.g. KnownClass::Int and Type::IntLiteral, etc.)

I don't think Sized or Hashable meet either of those criteria.

If you want to use these types (or any other typeshed type) in tests, you don't need it to be a KnownClass; that's just a minor convenience. You can just use typing_symbol_ty (added in this PR, and something we'll definitely want) directly in the test.

I hadn't quite internalized that I only actually really need typing_symbol_ty, thanks for pointing that out. Will remove theKnownClass entries

carljm · 2024-10-29T02:14:23Z

crates/red_knot_python_semantic/src/types/builder.rs

        let i0 = IntersectionBuilder::new(&db)
            .add_positive(ta)
            .add_negative(t1)
            .build();
+        // intersection = int & ~(Any & ~Literal[1])
+        // -> int & (~Any  | Literal[1])
+        // (~Any is treated as Any for adding purposes)


Suggested change

// (~Any is treated as Any for adding purposes)

// (~Any is equivalent to Any)

carljm · 2024-10-29T02:15:49Z

crates/red_knot_python_semantic/src/types/builder.rs

+        // -> int & (~Any  | Literal[1])
+        // (~Any is treated as Any for adding purposes)
+        // -> (int & Any) | (int & Literal[1])
+        // -> (int & Any) | Literal[1]
        let intersection = IntersectionBuilder::new(&db)


Confusing to name this intersection when it is actually a union :)

Suggested change

let intersection = IntersectionBuilder::new(&db)

let union = IntersectionBuilder::new(&db)

FWIW another option here is to just assert on the displayed form of the type, build_negative_union_de_morgan does that

At first wasn't a fan because of the display issues, but given it's DNF (I belive) it's unambiguous... will do that

carljm · 2024-10-29T02:16:10Z

crates/red_knot_python_semantic/src/types/builder.rs

+            .add_positive(ta)
+            .build();
+
+        assert_eq!(intersection.elements(&db), &[i_and_a, t1,]);


Suggested change

assert_eq!(intersection.elements(&db), &[i_and_a, t1,]);

assert_eq!(union.elements(&db), &[i_and_a, t1,]);

carljm · 2024-10-29T02:18:00Z

crates/red_knot_python_semantic/src/types/builder.rs

+        let it = KnownClass::Int.to_instance(&db);
+        let st = KnownClass::Sized.to_instance(&db);
+        let ht = KnownClass::Hashable.to_instance(&db);
+        // sh_t: Sized & ~Hashable


Suggested change

// sh_t: Sized & ~Hashable

// s_not_h_t: Sized & ~Hashable

also clean up some other details

carljm

Looks good, thank you!!

rtpg added 2 commits October 28, 2024 20:57

Add some typing classes to KnownClass

a324834

Distribute negated intersections when building intersections

8c608c2

rtpg requested review from carljm, MichaReiser and AlexWaygood as code owners October 28, 2024 10:59

MichaReiser marked this pull request as draft October 28, 2024 11:56

TomerBin reviewed Oct 28, 2024

View reviewed changes

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

Rewrite test for non-Any-folding behavior

e01da82

rtpg marked this pull request as ready for review October 29, 2024 00:12

Add an extra test for more complex negation

e7e432b

rtpg commented Oct 29, 2024

View reviewed changes

carljm requested changes Oct 29, 2024

View reviewed changes

remove Sizable and Hashable from known classes

338692b

also clean up some other details

carljm approved these changes Oct 29, 2024

View reviewed changes

carljm enabled auto-merge (squash) October 29, 2024 02:55

carljm merged commit 2fe2032 into astral-sh:main Oct 29, 2024
18 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[red-knot] Distribute intersections on negation #13962

[red-knot] Distribute intersections on negation #13962

rtpg commented Oct 28, 2024 •

edited by carljm

Loading

rtpg commented Oct 28, 2024

MichaReiser commented Oct 28, 2024

github-actions bot commented Oct 28, 2024 •

edited

Loading

rtpg commented Oct 29, 2024

rtpg Oct 29, 2024

carljm Oct 29, 2024

rtpg Oct 29, 2024

carljm left a comment

carljm Oct 29, 2024

carljm Oct 29, 2024

rtpg Oct 29, 2024

carljm Oct 29, 2024

carljm Oct 29, 2024

carljm Oct 29, 2024

rtpg Oct 29, 2024

carljm Oct 29, 2024

carljm Oct 29, 2024

carljm left a comment

	/// Returns `Unbound` if the `types` module isn't available for some reason.
	/// Returns `Unbound` if the `typing` module isn't available for some reason.

	// (~Any is treated as Any for adding purposes)
	// (~Any is equivalent to Any)

	let intersection = IntersectionBuilder::new(&db)
	let union = IntersectionBuilder::new(&db)

	assert_eq!(intersection.elements(&db), &[i_and_a, t1,]);
	assert_eq!(union.elements(&db), &[i_and_a, t1,]);

[red-knot] Distribute intersections on negation #13962

[red-knot] Distribute intersections on negation #13962

Conversation

rtpg commented Oct 28, 2024 • edited by carljm Loading

Summary

Test Plan

rtpg commented Oct 28, 2024

MichaReiser commented Oct 28, 2024

github-actions bot commented Oct 28, 2024 • edited Loading

ruff-ecosystem results

Linter (stable)

Linter (preview)

rtpg commented Oct 29, 2024

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

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

rtpg commented Oct 28, 2024 •

edited by carljm

Loading

github-actions bot commented Oct 28, 2024 •

edited

Loading

`ruff-ecosystem` results