[red-knot] (Gradual) intersection types are not handled in assignability

[sharkdp]

The is_assignable_to-is-reflexive property test, which makes sure that we can assign any type to itself, is currently failing with counter-examples like Any & T, where T is an arbitrary type (that doesn't let the intersection collapse).

The reason for this is that we can't rely on equivalence for assignability of gradual types anymore ever since #14758. We do have some special casing for gradual types like Any and Unknown, as well as for unions and tuples of these, but we do lack handling of intersections.

This is not completely trivial. We can patch this with some superficial handling like

--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -748,6 +748,14 @@ impl<'db> Type<'db> {
                 .elements(db)
                 .iter()
                 .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)),
+            (Type::Intersection(intersection), ty) => intersection
+                .positive(db)
+                .iter()
+                .any(|&elem_ty| elem_ty.is_assignable_to(db, ty)),
+            (ty, Type::Intersection(intersection)) => intersection
+                .positive(db)
+                .iter()
+                .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)),
             (Type::Tuple(self_tuple), Type::Tuple(target_tuple)) => {
                 let self_elements = self_tuple.elements(db);
                 let target_elements = target_tuple.elements(db);

which also works for things like T & ~Any, because we always add Any/Unknown as positive contributions to intersections.

But then quickcheck finds types like ~tuple[Any, T], for which the simple handling above breaks.

[carljm]

Moving this out of Backlog and into Ready, and also marking help-wanted in case a contributor is interested in it, because I think having the quickcheck tests stable and green on main is quite valuable. Just now I was making another change to type relations, ran the quickcheck tests, and hit this failure, which diverted me for a while until I realized it was failing also on main and found this issue.

[rtpg]

which also works for things like T & ~Any, because we always add Any/Unknown as positive contributions to intersections.

Regarding this, is Ty meant to mirror exactly the sort of structures that we'd end up with using Type<'db>? Like we would never have T & ~Any with Type, and we wouldn't have an intersection of unions (since we normalize to unions of intersections).

I think the arbitrary generator currently in the property tests will gladly generate non-normalized intersections in particular, which might be generating false positives in these tests.

[rtpg]

After poking at this a bit more, I now feel like the main problem with the existing Ty generation is mainly that a test failure shows the Ty intead of a representation of the actual Type used. So you don't see the shape of the actual type tested, just the pre-transformed Ty smart constructor.

[AlexWaygood]

After poking at this a bit more, I now feel like the main problem with the existing Ty generation is mainly that a test failure shows the Ty intead of a representation of the actual Type used. So you don't see the shape of the actual type tested, just the pre-transformed Ty smart constructor.

Yeah, agreed that this would be a big usability improvement!

[rtpg]

The idle thought I had here is that it would be cool if quickcheck ran shrunk failures one last time after finding minimal repros, and had a "verbose log" mechanism that would let me put in "expensive" logs or TestResult error message generation, without actually causing slowdowns most of the time. Or really any sort of way to run something on the minimum repro right before stopping.

For now I might try to just add something into the test harness and see how much slower it is. Computers still are fast after all.

[sharkdp]

This issue is actually a bit more general than the title/description make it sound like.

We currently don't have any logic for handling intersection types in the is_assignable_to relation. We do have special handling in is_equivalent_to and is_subtype_of, so for fully-static types, we're probably good(?). But for gradual types, it looks like we need some special handling. For example, we currently don't allow Unknown & int to be assigned to int, so something like this fails:

def f(x) -> None:
    if isinstance(x, int):
        reveal_type(x)  # Unknown & int
        y: int = x  # currently fails with invalid-assignment

We could probably write a property test like forall T, S. is_assignable_to(T & S, T) that would catch this?

[sharkdp]

This bug now has some failing unit tests here:

ruff/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md

Lines 267 to 276 in beb8e2d

	# TODO: The following assertions should not fail (see https://github.com/astral-sh/ruff/issues/14899)
	# error: [static-assert-error]
	static_assert(is_assignable_to(Intersection[Any, int], int))
	# error: [static-assert-error]
	static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Any]))
	# error: [static-assert-error]
	static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]]))
	# error: [static-assert-error]
	static_assert(is_assignable_to(Intersection[Unrelated, Any], Not[tuple[Unrelated, Any]]))