[red-knot] type[T] is disjoint from type[S] if the metaclass of T is disjoint from the metaclass of S (#15547)

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

@@ -246,3 +246,31 @@ def _(x: type, y: type[int]):
     if issubclass(x, y):
         reveal_type(x)  # revealed: type[int]
 ```
+
+### Disjoint `type[]` types are narrowed to `Never`
+
+Here, `type[UsesMeta1]` and `type[UsesMeta2]` are disjoint because a common subclass of `UsesMeta1`
+and `UsesMeta2` could only exist if a common subclass of their metaclasses could exist. This is
+known to be impossible due to the fact that `Meta1` is marked as `@final`.
+
+```py
+from typing import final
+
+@final
+class Meta1(type): ...
+
+class Meta2(type): ...
+class UsesMeta1(metaclass=Meta1): ...
+class UsesMeta2(metaclass=Meta2): ...
+
+def _(x: type[UsesMeta1], y: type[UsesMeta2]):
+    if issubclass(x, y):
+        reveal_type(x)  # revealed: Never
+    else:
+        reveal_type(x)  # revealed: type[UsesMeta1]
+
+    if issubclass(y, x):
+        reveal_type(y)  # revealed: Never
+    else:
+        reveal_type(y)  # revealed: type[UsesMeta2]
+```

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

@@ -37,3 +37,22 @@ class UsesMeta2(metaclass=Meta2): ...
 static_assert(not is_disjoint_from(Meta2, type[UsesMeta2]))
 static_assert(is_disjoint_from(Meta1, type[UsesMeta2]))
 ```
+
+## `type[T]` versus `type[S]`
+
+By the same token, `type[T]` is disjoint from `type[S]` if the metaclass of `T` is disjoint from the
+metaclass of `S`.
+
+```py
+from typing import final
+from knot_extensions import static_assert, is_disjoint_from
+
+@final
+class Meta1(type): ...
+
+class Meta2(type): ...
+class UsesMeta1(metaclass=Meta1): ...
+class UsesMeta2(metaclass=Meta2): ...
+
+static_assert(is_disjoint_from(type[UsesMeta1], type[UsesMeta2]))
+```