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.

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

Conversation

AlexWaygood
Copy link
Member

Summary

Closes #15508

For any two instance types T and S, we know they are disjoint if either T is final and T is not a subclass of S or S is final and S is not a subclass of T.

Correspondingly, for any two types type[T] and S where S is an instance type, type[T] can be said to be disjoint from S if S is disjoint from U, where U is the type that represents all instances of T's metaclass.

And a heterogeneous tuple type can be said to be disjoint from an instance type if the instance type is disjoint from tuple (a type representing all instances of the tuple class at runtime).

Test Plan

  • A new mdtest added. Most of our is_disjoint_from() tests are not written as mdtests just yet, but it's pretty hard to test some of these edge cases from a Rust unit test!
  • Ran QUICKCHECK_TESTS=1000000 cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::stable

Co-authored-by: Carl Meyer carl@astral.sh

@AlexWaygood AlexWaygood added the red-knot Multi-file analysis & type inference label Jan 16, 2025
Comment on lines +1281 to 1292
(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)
}
Copy link
Member Author

@AlexWaygood AlexWaygood Jan 16, 2025

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!

Copy link
Contributor

github-actions bot commented Jan 16, 2025

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

Copy link
Contributor

@carljm carljm left a comment

Choose a reason for hiding this comment

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

Net reduction in lines of code (excluding tests), and improves correctness! Love to see it.

Comment on lines +1281 to 1292
(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)
}
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?

Comment on lines +1283 to +1291
// `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)
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.

…es/is_disjoint_from.md

Co-authored-by: Carl Meyer <carl@astral.sh>
@AlexWaygood AlexWaygood enabled auto-merge (squash) January 16, 2025 23:42
@AlexWaygood AlexWaygood merged commit 3950b00 into main Jan 16, 2025
20 checks passed
@AlexWaygood AlexWaygood deleted the alex/final-instances branch January 16, 2025 23:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
red-knot Multi-file analysis & type inference
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[red-knot] type & ~Literal[True] & bool should simplify to Never
2 participants