[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!