diff --git a/crates/red_knot_python_semantic/resources/mdtest/annotations/tuple.md b/crates/red_knot_python_semantic/resources/mdtest/annotations/tuple.md new file mode 100644 index 0000000000..1903c01f82 --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/annotations/tuple.md @@ -0,0 +1,15 @@ +# Tuple + +## `Never` + +If a tuple type contains a `Never` element, then it is eagerly simplified to `Never` which means +that a tuple type containing `Never` is disjoint from any other tuple type. + +```py +from typing_extensions import Never + +def _(x: tuple[Never], y: tuple[int, Never], z: tuple[Never, int]): + reveal_type(x) # revealed: Never + reveal_type(y) # revealed: Never + reveal_type(z) # revealed: Never +``` diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md index 3d2296807d..479bf0efb2 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -61,7 +61,7 @@ static_assert(is_disjoint_from(B2, FinalSubclass)) ## Tuple types ```py -from typing_extensions import Literal +from typing_extensions import Literal, Never from knot_extensions import TypeOf, is_disjoint_from, static_assert static_assert(is_disjoint_from(tuple[()], TypeOf[object])) @@ -353,3 +353,29 @@ class UsesMeta2(metaclass=Meta2): ... static_assert(is_disjoint_from(type[UsesMeta1], type[UsesMeta2])) ``` + +## Callables + +No two callable types are disjoint because there exists a non-empty callable type +`(*args: object, **kwargs: object) -> Never` that is a subtype of all fully static callable types. +As such, for any two callable types, it is possible to conceive of a runtime callable object that +would inhabit both types simultaneously. + +```py +from knot_extensions import CallableTypeOf, is_disjoint_from, static_assert +from typing_extensions import Callable, Literal, Never + +def mixed(a: int, /, b: str, *args: int, c: int = 2, **kwargs: int) -> None: ... + +static_assert(not is_disjoint_from(Callable[[], Never], CallableTypeOf[mixed])) +static_assert(not is_disjoint_from(Callable[[int, str], float], CallableTypeOf[mixed])) + +# Using gradual form +static_assert(not is_disjoint_from(Callable[..., None], Callable[[], None])) +static_assert(not is_disjoint_from(Callable[..., None], Callable[..., None])) +static_assert(not is_disjoint_from(Callable[..., None], Callable[[Literal[1]], None])) + +# Using `Never` +static_assert(not is_disjoint_from(Callable[[], Never], Callable[[], Never])) +static_assert(not is_disjoint_from(Callable[[Never], str], Callable[[Never], int])) +``` diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index f81d92a6e6..7cd2a9ebc7 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -1343,6 +1343,19 @@ impl<'db> Type<'db> { .to_instance(db) .is_disjoint_from(db, other), + (Type::Callable(_) | Type::FunctionLiteral(_), Type::Callable(_)) + | (Type::Callable(_), Type::FunctionLiteral(_)) => { + // No two callable types are ever disjoint because + // `(*args: object, **kwargs: object) -> Never` is a subtype of all fully static + // callable types. + false + } + + (Type::Callable(_), _) | (_, Type::Callable(_)) => { + // TODO: Implement disjointness for general callable type with other types + false + } + (Type::ModuleLiteral(..), other @ Type::Instance(..)) | (other @ Type::Instance(..), Type::ModuleLiteral(..)) => { // Modules *can* actually be instances of `ModuleType` subclasses @@ -1379,11 +1392,6 @@ impl<'db> Type<'db> { // TODO: add checks for the above cases once we support them instance.is_disjoint_from(db, KnownClass::Tuple.to_instance(db)) } - - (Type::Callable(_), _) | (_, Type::Callable(_)) => { - // TODO: Implement disjointedness for callable types - false - } } }