[ty] Better implementation of assignability for intersections with negated gradual elements (#20773)

crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md

@@ -721,6 +721,75 @@ static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], No
 static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
 ```
 
+## Intersections with non-fully-static negated elements
+
+A type can be _assignable_ to an intersection containing negated elements only if the _bottom_
+materialization of that type is disjoint from the _bottom_ materialization of all negated elements
+in the intersection. This differs from subtyping, which should do the disjointness check against the
+_top_ materialization of the negated elements.
+
+```py
+from typing_extensions import Any, Never, Sequence
+from ty_extensions import Not, is_assignable_to, static_assert
+
+# The bottom materialization of `tuple[Any]` is `tuple[Never]`,
+# which simplifies to `Never`, so `tuple[int]` and `tuple[()]` are
+# both assignable to `~tuple[Any]`
+static_assert(is_assignable_to(tuple[int], Not[tuple[Any]]))
+static_assert(is_assignable_to(tuple[()], Not[tuple[Any]]))
+
+# But the bottom materialization of `tuple[Any, ...]` is `tuple[Never, ...]`,
+# which simplifies to `tuple[()]`, so `tuple[int]` is still assignable to
+# `~tuple[Any, ...]`, but `tuple[()]` is not
+static_assert(is_assignable_to(tuple[int], Not[tuple[Any, ...]]))
+static_assert(not is_assignable_to(tuple[()], Not[tuple[Any, ...]]))
+
+# Similarly, the bottom materialization of `Sequence[Any]` is `Sequence[Never]`,
+# so `tuple[()]` is not assignable to `~Sequence[Any]`, and nor is `list[Never]`,
+# since both `tuple[()]` and `list[Never]` are subtypes of `Sequence[Never]`.
+# `tuple[int, ...]` is also not assignable to `~Sequence[Any]`, as although it is
+# not a subtype of `Sequence[Never]` it is also not disjoint from `Sequence[Never]`:
+# `tuple[()]` is a subtype of both `Sequence[Never]` and `tuple[int, ...]`, so
+# `tuple[int, ...]` and `Sequence[Never]` cannot be considered disjoint.
+#
+# Other `list` and `tuple` specializations *are* assignable to `~Sequence[Any]`,
+# however, since there are many fully static materializations of `Sequence[Any]`
+# that would be disjoint from a given `list` or `tuple` specialization.
+static_assert(not is_assignable_to(tuple[()], Not[Sequence[Any]]))
+static_assert(not is_assignable_to(list[Never], Not[Sequence[Any]]))
+static_assert(not is_assignable_to(tuple[int, ...], Not[Sequence[Any]]))
+
+# TODO: should pass (`tuple[int]` should be considered disjoint from `Sequence[Never]`)
+static_assert(is_assignable_to(tuple[int], Not[Sequence[Any]]))  # error: [static-assert-error]
+
+# TODO: should pass (`list[int]` should be considered disjoint from `Sequence[Never]`)
+static_assert(is_assignable_to(list[int], Not[Sequence[Any]]))  # error: [static-assert-error]
+
+# If the left-hand side is also not fully static,
+# the left-hand side will be assignable to the right if the bottom materialization
+# of the left-hand side is disjoint from the bottom materialization of all negated
+# elements on the right-hand side
+
+# `tuple[Any, ...]` cannot be assignable to `~tuple[Any, ...]`,
+# because the bottom materialization of `tuple[Any, ...]` is
+# `tuple[()]`, and `tuple[()]` is not disjoint from itself
+static_assert(not is_assignable_to(tuple[Any, ...], Not[tuple[Any, ...]]))
+
+# but `tuple[Any]` is assignable to `~tuple[Any]`,
+# as the bottom materialization of `tuple[Any]` is `Never`,
+# and `Never` *is* disjoint from itself
+static_assert(is_assignable_to(tuple[Any], Not[tuple[Any]]))
+
+# The same principle applies for non-fully-static `list` specializations.
+# TODO: this should pass (`Bottom[list[Any]]` should simplify to `Never`)
+static_assert(is_assignable_to(list[Any], Not[list[Any]]))  # error: [static-assert-error]
+
+# `Bottom[list[Any]]` is `Never`, which is disjoint from `Bottom[Sequence[Any]]`
+# (which is `Sequence[Never]`).
+# TODO: this should pass (`Bottom[list[Any]]` should simplify to `Never`)
+static_assert(is_assignable_to(list[Any], Not[Sequence[Any]]))  # error: [static-assert-error]
+```
+
 ## General properties
 
 See also: our property tests in `property_tests.rs`.

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

@@ -533,6 +533,45 @@ static_assert(not is_subtype_of(int, Not[Literal[3]]))
 static_assert(not is_subtype_of(Literal[1], Intersection[int, Not[Literal[1]]]))
 ```
 
+## Intersections with non-fully-static negated elements
+
+A type can be a _subtype_ of an intersection containing negated elements only if the _top_
+materialization of that type is disjoint from the _top_ materialization of all negated elements in
+the intersection. This differs from assignability, which should do the disjointness check against
+the _bottom_ materialization of the negated elements.
+
+```py
+from typing_extensions import Any, Never, Sequence
+from ty_extensions import Not, is_subtype_of, static_assert
+
+# The top materialization of `tuple[Any]` is `tuple[object]`,
+# which is disjoint from `tuple[()]` but not `tuple[int]`,
+# so `tuple[()]` is a subtype of `~tuple[Any]` but `tuple[int]`
+# is not.
+static_assert(is_subtype_of(tuple[()], Not[tuple[Any]]))
+static_assert(not is_subtype_of(tuple[int], Not[tuple[Any]]))
+static_assert(not is_subtype_of(tuple[Any], Not[tuple[Any]]))
+
+# The top materialization of `tuple[Any, ...]` is `tuple[object, ...]`,
+# so no tuple type can be considered a subtype of `~tuple[Any, ...]`
+static_assert(not is_subtype_of(tuple[()], Not[tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[int], Not[tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[int, ...], Not[tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[object, ...], Not[tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[Any, ...], Not[tuple[Any, ...]]))
+
+# Similarly, the top materialization of `Sequence[Any]` is `Sequence[object]`,
+# so no sequence type can be considered a subtype of `~Sequence[Any]`.
+static_assert(not is_subtype_of(tuple[()], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(tuple[int], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(tuple[int, ...], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(tuple[object, ...], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(tuple[Any, ...], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(list[Never], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(list[Any], Not[Sequence[Any]]))
+static_assert(not is_subtype_of(list[int], Not[Sequence[Any]]))
+```
+
 ## Special types
 
 ### `Never`

crates/ty_python_semantic/src/types.rs

@@ -1757,8 +1757,29 @@ impl<'db> Type<'db> {
                     )
                 })
                 .and(db, || {
+                    // For subtyping, we would want to check whether the *top materialization* of `self`
+                    // is disjoint from the *top materialization* of `neg_ty`. As an optimization, however,
+                    // we can avoid this explicit transformation here, since our `Type::is_disjoint_from`
+                    // implementation already only returns true for `T.is_disjoint_from(U)` if the *top
+                    // materialization* of `T` is disjoint from the *top materialization* of `U`.
+                    //
+                    // Note that the implementation of redundancy here may be too strict from a
+                    // theoretical perspective: under redundancy, `T <: ~U` if `Bottom[T]` is disjoint
+                    // from `Top[U]` and `Bottom[U]` is disjoint from `Top[T]`. It's possible that this
+                    // could be improved. For now, however, we err on the side of strictness for our
+                    // redundancy implementation: a fully complete implementation of redundancy may lead
+                    // to non-transitivity (highly undesirable); and pragmatically, a full implementation
+                    // of redundancy may not generally lead to simpler types in many situations.
+                    let self_ty = match relation {
+                        TypeRelation::Subtyping | TypeRelation::Redundancy => self,
+                        TypeRelation::Assignability => self.bottom_materialization(db),
+                    };
                     intersection.negative(db).iter().when_all(db, |&neg_ty| {
-                        self.is_disjoint_from_impl(
+                        let neg_ty = match relation {
+                            TypeRelation::Subtyping | TypeRelation::Redundancy => neg_ty,
+                            TypeRelation::Assignability => neg_ty.bottom_materialization(db),
+                        };
+                        self_ty.is_disjoint_from_impl(
                             db,
                             neg_ty,
                             disjointness_visitor,
@@ -2284,10 +2305,21 @@ impl<'db> Type<'db> {
         }
     }
 
-    /// Return true if this type and `other` have no common elements.
+    /// Return true if `self & other` should simplify to `Never`:
+    /// if the intersection of the two types could never be inhabited by any
+    /// possible runtime value.
     ///
-    /// Note: This function aims to have no false positives, but might return
+    /// Our implementation of disjointness for non-fully-static types only
-    /// wrong `false` answers in some cases.
+    /// returns true if the *top materialization* of `self` has no overlap with
+    /// the *top materialization* of `other`.
+    ///
+    /// For example, `list[int]` is disjoint from `list[str]`: the two types have
+    /// no overlap. But `list[Any]` is not disjoint from `list[str]`: there exists
+    /// a fully static materialization of `list[Any]` (`list[str]`) that is a
+    /// subtype of `list[str]`
+    ///
+    /// This function aims to have no false positives, but might return wrong
+    /// `false` answers in some cases.
     pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool {
         self.when_disjoint_from(db, other).is_always_satisfied()
     }