[red-knot] Implement disjointness for Instance types where the underlying class is @final

crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md

@@ -199,24 +199,20 @@ def f(
     if isinstance(a, bool):
         reveal_type(a)  # revealed: Never
     else:
-        # TODO: `bool` is final, so `& ~bool` is redundant here
-        reveal_type(a)  # revealed: P & AlwaysTruthy & ~bool
+        reveal_type(a)  # revealed: P & AlwaysTruthy
 
     if isinstance(b, bool):
         reveal_type(b)  # revealed: Never
     else:
-        # TODO: `bool` is final, so `& ~bool` is redundant here
-        reveal_type(b)  # revealed: P & AlwaysFalsy & ~bool
+        reveal_type(b)  # revealed: P & AlwaysFalsy
 
     if isinstance(c, bool):
         reveal_type(c)  # revealed: Never
     else:
-        # TODO: `bool` is final, so `& ~bool` is redundant here
-        reveal_type(c)  # revealed: P & ~AlwaysTruthy & ~bool
+        reveal_type(c)  # revealed: P & ~AlwaysTruthy
 
     if isinstance(d, bool):
         reveal_type(d)  # revealed: Never
     else:
-        # TODO: `bool` is final, so `& ~bool` is redundant here
-        reveal_type(d)  # revealed: P & ~AlwaysFalsy & ~bool
+        reveal_type(d)  # revealed: P & ~AlwaysFalsy
 ```

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

@@ -0,0 +1,36 @@
+# Tests for disjointness
+
+If two types can be disjoint, it means that it is known that no possible runtime object could ever inhabit both types simultaneously.
+
+TODO: Most of our disjointness tests are still Rust tests; they should be moved to this file.
+
+## Instance types versus `type[T]` types
+
+An instance type is disjoint from a `type[T]` type if the instance type is `@final`
+and the associated class of the instance type is not a subclass of `T`'s metaclass.
+
+```py
+from typing import final
+from knot_extensions import is_disjoint_from, static_assert
+
+@final
+class Foo: ...
+
+static_assert(is_disjoint_from(Foo, type[int]))
+static_assert(is_disjoint_from(type[object], Foo))
+static_assert(is_disjoint_from(type[dict], Foo))
+
+# Instance types can be disjoint from `type[]` types
+# even if the instance type is a subtype of `type`
+
+@final
+class Meta1(type): ...
+class UsesMeta1(metaclass=Meta1): ...
+
+static_assert(not is_disjoint_from(Meta1, type[UsesMeta1]))
+
+class Meta2(type): ...
+class UsesMeta2(metaclass=Meta2): ...
+static_assert(not is_disjoint_from(Meta2, type[UsesMeta2]))
+static_assert(is_disjoint_from(Meta1, type[UsesMeta2]))
+```

crates/red_knot_python_semantic/src/types.rs

@@ -1278,14 +1278,17 @@ impl<'db> Type<'db> {
 
             (Type::SubclassOf(_), Type::SubclassOf(_)) => false,
 
-            (Type::SubclassOf(_), Type::Instance(instance))
-            | (Type::Instance(instance), Type::SubclassOf(_)) => {
-                // TODO this should be `true` if the instance is of a final type which is not a
-                // subclass of type. (With non-final types, we never know whether a subclass might
-                // multiply-inherit `type` or a subclass of it, and thus not be disjoint with
-                // `type[...]`.) Until we support finality, hardcode None, which is known to be
-                // final.
-                instance.class.is_known(db, KnownClass::NoneType)
+            (Type::SubclassOf(subclass_of_ty), instance @ Type::Instance(_))
+            | (instance @ Type::Instance(_), Type::SubclassOf(subclass_of_ty)) => {
+                // `type[T]` is disjoint from `S`, where `S` is an instance type,
+                // if `U` is disjoint from `S`,
+                // where `U` represents all instances of `T`'s metaclass
+                let metaclass_instance = subclass_of_ty
+                    .subclass_of()
+                    .into_class()
+                    .map(|class| class.metaclass(db).to_instance(db))
+                    .unwrap_or_else(|| KnownClass::Type.to_instance(db));
+                instance.is_disjoint_from(db, metaclass_instance)
             }
 
             (
@@ -1339,24 +1342,6 @@ impl<'db> Type<'db> {
                 known_instance_ty.is_disjoint_from(db, KnownClass::Tuple.to_instance(db))
             }
 
-            (
-                Type::Instance(InstanceType { class: class_none }),
-                Type::Instance(InstanceType { class: class_other }),
-            )
-            | (
-                Type::Instance(InstanceType { class: class_other }),
-                Type::Instance(InstanceType { class: class_none }),
-            ) if class_none.is_known(db, KnownClass::NoneType) => {
-                !class_none.is_subclass_of(db, class_other)
-            }
-
-            (Type::Instance(InstanceType { class: class_none }), _)
-            | (_, Type::Instance(InstanceType { class: class_none }))
-                if class_none.is_known(db, KnownClass::NoneType) =>
-            {
-                true
-            }
-
             (Type::BooleanLiteral(..), Type::Instance(InstanceType { class }))
             | (Type::Instance(InstanceType { class }), Type::BooleanLiteral(..)) => {
                 // A `Type::BooleanLiteral()` must be an instance of exactly `bool`
@@ -1430,15 +1415,12 @@ impl<'db> Type<'db> {
                 other.is_disjoint_from(db, KnownClass::ModuleType.to_instance(db))
             }
 
-            (Type::Instance(..), Type::Instance(..)) => {
-                // TODO: once we have support for `final`, there might be some cases where
-                // we can determine that two types are disjoint. Once we do this, some cases
-                // above (e.g. NoneType) can be removed. For non-final classes, we return
-                // false (multiple inheritance).
-
-                // TODO: is there anything specific to do for instances of KnownClass::Type?
-
-                false
+            (
+                Type::Instance(InstanceType { class: left_class }),
+                Type::Instance(InstanceType { class: right_class }),
+            ) => {
+                (left_class.is_final(db) && !left_class.is_subclass_of(db, right_class))
+                    || (right_class.is_final(db) && !right_class.is_subclass_of(db, left_class))
             }
 
             (Type::Tuple(tuple), Type::Tuple(other_tuple)) => {
@@ -1451,7 +1433,8 @@ impl<'db> Type<'db> {
                         .any(|(e1, e2)| e1.is_disjoint_from(db, *e2))
             }
 
-            (Type::Tuple(..), Type::Instance(..)) | (Type::Instance(..), Type::Tuple(..)) => {
+            (Type::Tuple(..), instance @ Type::Instance(_))
+            | (instance @ Type::Instance(_), Type::Tuple(..)) => {
                 // We cannot be sure if the tuple is disjoint from the instance because:
                 //   - 'other' might be the homogeneous arbitrary-length tuple type
                 //     tuple[T, ...] (which we don't have support for yet); if all of
@@ -1460,7 +1443,7 @@ impl<'db> Type<'db> {
                 //     over the same or compatible *Ts, would overlap with tuple.
                 //
                 // TODO: add checks for the above cases once we support them
-                false
+                instance.is_disjoint_from(db, KnownClass::Tuple.to_instance(db))
             }
         }
     }