Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 6 commits into from
Jan 16, 2025
Merged

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

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1c77b78
Add a failing test
AlexWaygood Jan 16, 2025
099e3f7
[red-knot] Implement disjointness for `Instance` types where the unde…
AlexWaygood Jan 16, 2025
7765965
fix subtle edge cases to do with `type[T]` types where `T` has a cust…
AlexWaygood Jan 16, 2025
1d78b74
run pre-commit
AlexWaygood Jan 16, 2025
dac2982
Update crates/red_knot_python_semantic/resources/mdtest/type_properti…
AlexWaygood Jan 16, 2025
d6c4521
Update is_disjoint_from.md
AlexWaygood Jan 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 4 additions & 8 deletions crates/red_knot_python_semantic/resources/mdtest/narrow/isinstance.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
39 changes: 39 additions & 0 deletions ...s/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
associated class of the instance type is not a subclass of `T`'s metaclass.
AlexWaygood marked this conversation as resolved.
Show resolved Hide resolved

```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]))
```
57 changes: 20 additions & 37 deletions crates/red_knot_python_semantic/src/types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Comment on lines +1283 to +1291
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! I like that we can delegate to instance-vs-instance, rather than checking finality here also.

It seems right that T actually disappears from this check, apart from its metaclass. There's no difference between type[object] and type[OtherClass] as regards disjointness from an instance type, as long as the metaclass of OtherClass is just type.

}
Comment on lines +1281 to 1292
Copy link
Member Author

@AlexWaygood AlexWaygood Jan 16, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@carljm I realised almost as soon as our pairing session here that we were missing some subtle edge cases where a type[T] type could still be disjoint from an instance type even if the instance type was a subtype of type. So this logic is a little fiddlier than what we initially implemented. See the mdtest I've added for examples!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did a property test reveal this, or you just realized it looking at the code/tests?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just me reading the diff on github prior to filing the PR!


(
Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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)) => {
Expand All @@ -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
Expand All @@ -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))
}
}
}
Expand Down
Loading