[red knot] add Type::is_disjoint_from and intersection simplifications

[sharkdp]

Summary

• Add Type::is_disjoint_from as a way to test whether two types overlap
• Add a first set of simplification rules for intersection types
  • S & T = S for S <: T
  • S & ~T = Never for S <: T
  • ~S & ~T = ~T for S <: T
  • A & ~B = A for A disjoint from B
  • A & B = Never for A disjoint from B
  • bool & ~Literal[bool] = Literal[!bool]

resolves one item in #12694

Open questions:

• Can we somehow leverage the (anti) symmetry between positive and negative contributions? I could imagine that there would be a way if we had Type::Not(type)/Type::Negative(type), but with the positive/negative architecture, I'm not sure. Note that there is a certain duplication in the add_positive/add_negative functions (e.g. S & ~T = Never is implemented twice), but other rules are actually not perfectly symmetric: S & T = S vs ~S & ~T = ~T.
• I'm not particularly proud of the way add_positive/add_negative turned out. They are long imperative-style functions with some mutability mixed in (to_remove). I'm happy to look into ways to improve this code if we decide to go with this approach of implementing a set of ad-hoc rules for simplification.
• Is it useful to perform simplifications eagerly in add_positive/add_negative? (@carljm) This is what I did for now.

Test Plan

• Unit tests for Type::is_disjoint_from
• Observe changes in Markdown-based tests
• Unit tests for IntersectionBuilder::build()

[github-actions]

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

[carljm]

Can we somehow leverage the (anti) symmetry between positive and negative contributions? I could imagine that there would be a way if we had Type::Not(type)/Type::Negative(type), but with the positive/negative architecture, I'm not sure.

FWIW, I'm quite open to the idea that we discard the positive/negative approach in favor of a Type::Not, if it makes intersection simplification easier.

The downside is we then have to add handling for Type::Not throughout the type system, but I suspect that may actually not be too difficult, since in many places we can just treat it as object, which is less precise but never unsound.

[carljm]

This is great! I suspect that this approach will carry us a long way; I'm not feeling any particular need to explore more radical approaches. (I'm not 100% sure, but I suspect that the lazy-BDD approach I linked you to may just not be workable anyway for the complexity of Python's type system; particularly inheritance and multiple inheritance.)

[carljm]

Looks like this is still in-process, so didn't do a full re-review of the code, just a few responses to inline comments.

[carljm]

It just occurred to me now on second read-through that this case is incorrect if it comes before the union case, because the union of two Type::Function is not disjoint from one of those same Type::Function.

I think this case is really the same as the None and Literal types case below, and could probably just be merged with it?

Would be good to add a test case that would have caught this (to create a union of function or class types, define them in if/else branches.)

[sharkdp]

It just occurred to me now on second read-through that this case is incorrect if it comes before the union case, because the union of two Type::Function is not disjoint from one of those same Type::Function.

Ah, you're right.

I think this case is really the same as the None and Literal types case below, and could probably just be merged with it?

👍

Would be good to add a test case that would have caught this (to create a union of function or class types, define them in if/else branches.)

Yes. I added a test that failed with the previous version.

[carljm]

Because bool is a subtype of int in Python (sadly), we must also include KnownClass::Int here.

There was already a test for this case, but it asserted wrongly that int and a BooleanLiteral were disjoint; I switched it to assert the opposite.

There was also an IntersectionBuilder test relying on this assumption of bool/int disjointness; I fixed it by using a StringLiteral instead of a BooleanLiteral.

[carljm]

This is excellent work, thank you!!