diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md index 3da4221cfaf73..fd14139baeb18 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md +++ b/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 ``` 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 new file mode 100644 index 0000000000000..b6d85cf5bff17 --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md @@ -0,0 +1,39 @@ +# 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 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])) +``` diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 4e0c7a2e36bf8..089c1f6a86a00 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/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)) } } }