fix disjointness checks with type-of @final classes

ibraheemdev · ibraheemdev · commit b7a9f44965db · 2025-12-03T05:07:48.000-05:00
diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/type.md b/crates/ty_python_semantic/resources/mdtest/narrow/type.md
@@ -92,8 +92,7 @@ def f(x: A[int] | B):
         reveal_type(x)  # revealed: A[int] | B
 
     if type(x) is A:
-        # TODO: this should be `A[int]`, but `A[int] | B` would be better than `Never`
-        reveal_type(x)  # revealed: Never
+        reveal_type(x)  # revealed: A[int]
     else:
         reveal_type(x)  # revealed: A[int] | B
 
@@ -111,8 +110,7 @@ def f(x: A[int] | B):
     if type(x) is not A:
         reveal_type(x)  # revealed: A[int] | B
     else:
-        # TODO: this should be `A[int]`, but `A[int] | B` would be better than `Never`
-        reveal_type(x)  # revealed: Never
+        reveal_type(x)  # revealed: A[int]
 
     if type(x) is not B:
         reveal_type(x)  # revealed: A[int] | B
@@ -217,8 +215,7 @@ class B: ...
 
 def _[T](x: A | B):
     if type(x) is A[str]:
-        # TODO: `type()` never returns a generic alias, so `type(x)` cannot be `A[str]`
-        reveal_type(x)  # revealed: A[int] | B
+        reveal_type(x)  # revealed: Never
     else:
         reveal_type(x)  # revealed: A[int] | B
 ```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_of/basic.md b/crates/ty_python_semantic/resources/mdtest/type_of/basic.md
@@ -215,7 +215,7 @@ same also applies to enum classes with members, which are implicitly final:
 
 ```toml
 [environment]
-python-version = "3.10"
+python-version = "3.12"
 ```
 
 ```py
@@ -235,3 +235,170 @@ def _(x: type[Foo], y: type[EllipsisType], z: type[Answer]):
     reveal_type(y)  # revealed: <class 'EllipsisType'>
     reveal_type(z)  # revealed: <class 'Answer'>
 ```
+
+## Subtyping `@final` classes
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from typing import final, Any
+from ty_extensions import is_assignable_to, is_subtype_of, is_disjoint_from, static_assert
+
+class Biv[T]: ...
+
+class Cov[T]:
+    def pop(self) -> T:
+        raise NotImplementedError
+
+class Contra[T]:
+    def push(self, value: T) -> None:
+        pass
+
+class Inv[T]:
+    x: T
+
+@final
+class BivSub[T](Biv[T]): ...
+
+@final
+class CovSub[T](Cov[T]): ...
+
+@final
+class ContraSub[T](Contra[T]): ...
+
+@final
+class InvSub[T](Inv[T]): ...
+
+def _[T, U]():
+    static_assert(is_subtype_of(type[BivSub[T]], type[BivSub[U]]))
+    static_assert(not is_disjoint_from(type[BivSub[U]], type[BivSub[T]]))
+
+    static_assert(not is_subtype_of(type[CovSub[T]], type[CovSub[U]]))
+    static_assert(not is_disjoint_from(type[CovSub[U]], type[CovSub[T]]))
+
+    static_assert(not is_subtype_of(type[ContraSub[T]], type[ContraSub[U]]))
+    static_assert(not is_disjoint_from(type[ContraSub[U]], type[ContraSub[T]]))
+
+    static_assert(not is_subtype_of(type[InvSub[T]], type[InvSub[U]]))
+    static_assert(not is_disjoint_from(type[InvSub[U]], type[InvSub[T]]))
+
+def _():
+    static_assert(is_subtype_of(type[BivSub[bool]], type[BivSub[int]]))
+    static_assert(is_subtype_of(type[BivSub[int]], type[BivSub[bool]]))
+    static_assert(is_disjoint_from(type[BivSub[int]], type[BivSub[str]]))
+    static_assert(not is_disjoint_from(type[BivSub[bool]], type[BivSub[int]]))
+
+    static_assert(is_subtype_of(type[CovSub[bool]], type[CovSub[int]]))
+    static_assert(not is_subtype_of(type[CovSub[int]], type[CovSub[bool]]))
+    static_assert(is_disjoint_from(type[CovSub[int]], type[CovSub[str]]))
+    static_assert(not is_disjoint_from(type[CovSub[bool]], type[CovSub[int]]))
+
+    static_assert(not is_subtype_of(type[ContraSub[bool]], type[ContraSub[int]]))
+    static_assert(is_subtype_of(type[ContraSub[int]], type[ContraSub[bool]]))
+    static_assert(is_disjoint_from(type[ContraSub[int]], type[ContraSub[str]]))
+    static_assert(not is_disjoint_from(type[ContraSub[bool]], type[ContraSub[int]]))
+
+    static_assert(not is_subtype_of(type[InvSub[bool]], type[InvSub[int]]))
+    static_assert(not is_subtype_of(type[InvSub[int]], type[InvSub[bool]]))
+    static_assert(is_disjoint_from(type[InvSub[int]], type[InvSub[str]]))
+    static_assert(not is_disjoint_from(type[InvSub[bool]], type[InvSub[int]]))
+
+def _[T]():
+    static_assert(is_subtype_of(type[BivSub[T]], type[BivSub[Any]]))
+    static_assert(is_subtype_of(type[BivSub[Any]], type[BivSub[T]]))
+    static_assert(is_assignable_to(type[BivSub[T]], type[BivSub[Any]]))
+    static_assert(is_assignable_to(type[BivSub[Any]], type[BivSub[T]]))
+    static_assert(not is_disjoint_from(type[BivSub[T]], type[BivSub[Any]]))
+
+    static_assert(not is_subtype_of(type[CovSub[T]], type[CovSub[Any]]))
+    static_assert(not is_subtype_of(type[CovSub[Any]], type[CovSub[T]]))
+    static_assert(is_assignable_to(type[CovSub[T]], type[CovSub[Any]]))
+    static_assert(is_assignable_to(type[CovSub[Any]], type[CovSub[T]]))
+    static_assert(not is_disjoint_from(type[CovSub[T]], type[CovSub[Any]]))
+
+    static_assert(not is_subtype_of(type[ContraSub[T]], type[ContraSub[Any]]))
+    static_assert(not is_subtype_of(type[ContraSub[Any]], type[ContraSub[T]]))
+    static_assert(is_assignable_to(type[ContraSub[T]], type[ContraSub[Any]]))
+    static_assert(is_assignable_to(type[ContraSub[Any]], type[ContraSub[T]]))
+    static_assert(not is_disjoint_from(type[ContraSub[T]], type[ContraSub[Any]]))
+
+    static_assert(not is_subtype_of(type[InvSub[T]], type[InvSub[Any]]))
+    static_assert(not is_subtype_of(type[InvSub[Any]], type[InvSub[T]]))
+    static_assert(is_assignable_to(type[InvSub[T]], type[InvSub[Any]]))
+    static_assert(is_assignable_to(type[InvSub[Any]], type[InvSub[T]]))
+    static_assert(not is_disjoint_from(type[InvSub[T]], type[InvSub[Any]]))
+
+def _[T, U]():
+    static_assert(is_subtype_of(type[BivSub[T]], type[Biv[T]]))
+    static_assert(not is_subtype_of(type[Biv[T]], type[BivSub[T]]))
+    static_assert(not is_disjoint_from(type[BivSub[T]], type[Biv[T]]))
+    static_assert(not is_disjoint_from(type[BivSub[U]], type[Biv[T]]))
+    static_assert(not is_disjoint_from(type[BivSub[U]], type[Biv[U]]))
+
+    static_assert(is_subtype_of(type[CovSub[T]], type[Cov[T]]))
+    static_assert(not is_subtype_of(type[Cov[T]], type[CovSub[T]]))
+    static_assert(not is_disjoint_from(type[CovSub[T]], type[Cov[T]]))
+    static_assert(not is_disjoint_from(type[CovSub[U]], type[Cov[T]]))
+    static_assert(not is_disjoint_from(type[CovSub[U]], type[Cov[U]]))
+
+    static_assert(is_subtype_of(type[ContraSub[T]], type[Contra[T]]))
+    static_assert(not is_subtype_of(type[Contra[T]], type[ContraSub[T]]))
+    static_assert(not is_disjoint_from(type[ContraSub[T]], type[Contra[T]]))
+    static_assert(not is_disjoint_from(type[ContraSub[U]], type[Contra[T]]))
+    static_assert(not is_disjoint_from(type[ContraSub[U]], type[Contra[U]]))
+
+    static_assert(is_subtype_of(type[InvSub[T]], type[Inv[T]]))
+    static_assert(not is_subtype_of(type[Inv[T]], type[InvSub[T]]))
+    static_assert(not is_disjoint_from(type[InvSub[T]], type[Inv[T]]))
+    static_assert(not is_disjoint_from(type[InvSub[U]], type[Inv[T]]))
+    static_assert(not is_disjoint_from(type[InvSub[U]], type[Inv[U]]))
+
+def _():
+    static_assert(is_subtype_of(type[BivSub[bool]], type[Biv[int]]))
+    static_assert(is_subtype_of(type[BivSub[int]], type[Biv[bool]]))
+    static_assert(not is_disjoint_from(type[BivSub[bool]], type[Biv[int]]))
+    static_assert(not is_disjoint_from(type[BivSub[int]], type[Biv[bool]]))
+
+    static_assert(is_subtype_of(type[CovSub[bool]], type[Cov[int]]))
+    static_assert(not is_subtype_of(type[CovSub[int]], type[Cov[bool]]))
+    static_assert(not is_disjoint_from(type[CovSub[bool]], type[Cov[int]]))
+    static_assert(not is_disjoint_from(type[CovSub[int]], type[Cov[bool]]))
+
+    static_assert(not is_subtype_of(type[ContraSub[bool]], type[Contra[int]]))
+    static_assert(is_subtype_of(type[ContraSub[int]], type[Contra[bool]]))
+    static_assert(not is_disjoint_from(type[ContraSub[int]], type[Contra[bool]]))
+    static_assert(not is_disjoint_from(type[ContraSub[bool]], type[Contra[int]]))
+
+    static_assert(not is_subtype_of(type[InvSub[bool]], type[Inv[int]]))
+    static_assert(not is_subtype_of(type[InvSub[int]], type[Inv[bool]]))
+    static_assert(not is_disjoint_from(type[InvSub[bool]], type[Inv[int]]))
+    static_assert(not is_disjoint_from(type[InvSub[int]], type[Inv[bool]]))
+
+def _[T]():
+    static_assert(is_subtype_of(type[BivSub[T]], type[Biv[Any]]))
+    static_assert(is_subtype_of(type[BivSub[Any]], type[Biv[T]]))
+    static_assert(is_assignable_to(type[BivSub[T]], type[Biv[Any]]))
+    static_assert(is_assignable_to(type[BivSub[Any]], type[Biv[T]]))
+    static_assert(not is_disjoint_from(type[BivSub[T]], type[Biv[Any]]))
+
+    static_assert(not is_subtype_of(type[CovSub[T]], type[Cov[Any]]))
+    static_assert(not is_subtype_of(type[CovSub[Any]], type[Cov[T]]))
+    static_assert(is_assignable_to(type[CovSub[T]], type[Cov[Any]]))
+    static_assert(is_assignable_to(type[CovSub[Any]], type[Cov[T]]))
+    static_assert(not is_disjoint_from(type[CovSub[T]], type[Cov[Any]]))
+
+    static_assert(not is_subtype_of(type[ContraSub[T]], type[Contra[Any]]))
+    static_assert(not is_subtype_of(type[ContraSub[Any]], type[Contra[T]]))
+    static_assert(is_assignable_to(type[ContraSub[T]], type[Contra[Any]]))
+    static_assert(is_assignable_to(type[ContraSub[Any]], type[Contra[T]]))
+    static_assert(not is_disjoint_from(type[ContraSub[T]], type[Contra[Any]]))
+
+    static_assert(not is_subtype_of(type[InvSub[T]], type[Inv[Any]]))
+    static_assert(not is_subtype_of(type[InvSub[Any]], type[Inv[T]]))
+    static_assert(is_assignable_to(type[InvSub[T]], type[Inv[Any]]))
+    static_assert(is_assignable_to(type[InvSub[Any]], type[Inv[T]]))
+    static_assert(not is_disjoint_from(type[InvSub[T]], type[Inv[Any]]))
+```
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
@@ -2724,6 +2724,17 @@ impl<'db> Type<'db> {
                 )
             }
 
+            (Type::GenericAlias(self_alias), Type::GenericAlias(target_alias)) => {
+                ClassType::from(self_alias).has_relation_to_impl(
+                    db,
+                    ClassType::from(target_alias),
+                    inferable,
+                    relation,
+                    relation_visitor,
+                    disjointness_visitor,
+                )
+            }
+
             // `Literal[str]` is a subtype of `type` because the `str` class object is an instance of its metaclass `type`.
             // `Literal[abc.ABC]` is a subtype of `abc.ABCMeta` because the `abc.ABC` class object
             // is an instance of its metaclass `abc.ABCMeta`.
@@ -3307,7 +3318,6 @@ impl<'db> Type<'db> {
                 | Type::WrapperDescriptor(..)
                 | Type::ModuleLiteral(..)
                 | Type::ClassLiteral(..)
-                | Type::GenericAlias(..)
                 | Type::SpecialForm(..)
                 | Type::KnownInstance(..)),
                 right @ (Type::BooleanLiteral(..)
@@ -3321,7 +3331,6 @@ impl<'db> Type<'db> {
                 | Type::WrapperDescriptor(..)
                 | Type::ModuleLiteral(..)
                 | Type::ClassLiteral(..)
-                | Type::GenericAlias(..)
                 | Type::SpecialForm(..)
                 | Type::KnownInstance(..)),
             ) => ConstraintSet::from(left != right),
@@ -3504,13 +3513,25 @@ impl<'db> Type<'db> {
                 ConstraintSet::from(true)
             }
 
+            (Type::GenericAlias(left_alias), Type::GenericAlias(right_alias)) => {
+                ConstraintSet::from(left_alias.origin(db) != right_alias.origin(db)).or(db, || {
+                    left_alias.specialization(db).is_disjoint_from_impl(
+                        db,
+                        right_alias.specialization(db),
+                        inferable,
+                        disjointness_visitor,
+                        relation_visitor,
+                    )
+                })
+            }
+
             (Type::SubclassOf(subclass_of_ty), Type::ClassLiteral(class_b))
             | (Type::ClassLiteral(class_b), Type::SubclassOf(subclass_of_ty)) => {
                 match subclass_of_ty.subclass_of() {
                     SubclassOfInner::Dynamic(_) => ConstraintSet::from(false),
-                    SubclassOfInner::Class(class_a) => {
-                        class_b.when_subclass_of(db, None, class_a).negate(db)
-                    }
+                    SubclassOfInner::Class(class_a) => ConstraintSet::from(
+                        !class_a.could_exist_in_mro_of(db, ClassType::NonGeneric(class_b)),
+                    ),
                     SubclassOfInner::TypeVar(_) => unreachable!(),
                 }
             }
@@ -3519,9 +3540,9 @@ impl<'db> Type<'db> {
             | (Type::GenericAlias(alias_b), Type::SubclassOf(subclass_of_ty)) => {
                 match subclass_of_ty.subclass_of() {
                     SubclassOfInner::Dynamic(_) => ConstraintSet::from(false),
-                    SubclassOfInner::Class(class_a) => ClassType::from(alias_b)
-                        .when_subclass_of(db, class_a, inferable)
-                        .negate(db),
+                    SubclassOfInner::Class(class_a) => ConstraintSet::from(
+                        !class_a.could_exist_in_mro_of(db, ClassType::Generic(alias_b)),
+                    ),
                     SubclassOfInner::TypeVar(_) => unreachable!(),
                 }
             }
@@ -3815,6 +3836,8 @@ impl<'db> Type<'db> {
                     relation_visitor,
                 )
             }
+
+            (Type::GenericAlias(_), _) | (_, Type::GenericAlias(_)) => ConstraintSet::from(true),
         }
     }
 
diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
@@ -706,6 +706,30 @@ impl<'db> ClassType<'db> {
             .find_map(|base| base.as_disjoint_base(db))
     }
 
+    /// Return `true` if this class could exist in the MRO of `other`.
+    pub(super) fn could_exist_in_mro_of(self, db: &'db dyn Db, other: Self) -> bool {
+        other.iter_mro(db)
+            .filter_map(ClassBase::into_class)
+            .any(|class| match (self, class) {
+                (ClassType::NonGeneric(this_class), ClassType::NonGeneric(other_class)) => {
+                    this_class == other_class
+                }
+                (ClassType::Generic(this_alias), ClassType::Generic(other_alias)) => {
+                    this_alias.origin(db) == other_alias.origin(db)
+                        && this_alias
+                            .specialization(db)
+                            .is_disjoint_from(
+                                db,
+                                other_alias.specialization(db),
+                                InferableTypeVars::None,
+                            )
+                            .is_never_satisfied(db)
+                }
+                (ClassType::NonGeneric(_), ClassType::Generic(_))
+                | (ClassType::Generic(_), ClassType::NonGeneric(_)) => false,
+            })
+    }
+
     /// Return `true` if this class could coexist in an MRO with `other`.
     ///
     /// For two given classes `A` and `B`, it is often possible to say for sure
@@ -716,34 +740,12 @@ impl<'db> ClassType<'db> {
             return true;
         }
 
-        if self.is_final(db) || other.is_final(db) {
-            let (this, other) = if self.is_final(db) {
-                (self, other)
-            } else {
-                (other, self)
-            };
+        if self.is_final(db) {
+            return other.could_exist_in_mro_of(db, self);
+        }
 
-            return this
-                .iter_mro(db)
-                .filter_map(ClassBase::into_class)
-                .any(|class| match (class, other) {
-                    (ClassType::NonGeneric(this_class), ClassType::NonGeneric(other_class)) => {
-                        this_class == other_class
-                    }
-                    (ClassType::Generic(this_alias), ClassType::Generic(other_alias)) => {
-                        this_alias.origin(db) == other_alias.origin(db)
-                            && this_alias
-                                .specialization(db)
-                                .is_disjoint_from(
-                                    db,
-                                    other_alias.specialization(db),
-                                    InferableTypeVars::None,
-                                )
-                                .is_never_satisfied(db)
-                    }
-                    (ClassType::NonGeneric(_), ClassType::Generic(_))
-                    | (ClassType::Generic(_), ClassType::NonGeneric(_)) => false,
-                });
+        if other.is_final(db) {
+            return self.could_exist_in_mro_of(db, other);
         }
 
         // Two disjoint bases can only coexist in an MRO if one is a subclass of the other.
@@ -1859,15 +1861,6 @@ impl<'db> ClassLiteral<'db> {
             .contains(&ClassBase::Class(other))
     }
 
-    pub(super) fn when_subclass_of(
-        self,
-        db: &'db dyn Db,
-        specialization: Option<Specialization<'db>>,
-        other: ClassType<'db>,
-    ) -> ConstraintSet<'db> {
-        ConstraintSet::from(self.is_subclass_of(db, specialization, other))
-    }
-
     /// Return `true` if this class constitutes a typed dict specification (inherits from
     /// `typing.TypedDict`, either directly or indirectly).
     #[salsa::tracked(cycle_initial=is_typed_dict_cycle_initial,
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
