[ty] Better implementation of assignability for intersections with negated gradual elements

[AlexWaygood]

Our implementation of assignability between a type T and another type ~U is currently too strict. We currently only consider T assignable to ~U if Top[T] is disjoint from Top[U]. That's correct for subtyping and redundancy, but not for assignability: for assignability, we should be more permissive, and allow T to be considered assignable to ~U if Bottom[T] is disjoint from Bottom[U].

As part of this PR, I also improved the docstring of Type::is_disjoint_from to make it clear what it actually does (it tests for disjointness between the top materializations of the pair of types).

Fixes astral-sh/ty#767

Test plan

• Added mdtests that fail on main
• Ran QUICKCHECK_TESTS=1000000 cargo test --release -p ty_python_semantic -- --ignored types::property_tests::stable locally

[github-actions]

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

[github-actions]

mypy_primer results

Changes were detected when running on open source projects

arviz (https://github.com/arviz-devs/arviz)
- arviz/tests/base_tests/test_stats_utils.py:226:29: error[invalid-argument-type] Argument to bound method `__init__` is incorrect: Expected `Unknown & ~str`, found `Unknown & ~Literal["any"]`
- arviz/tests/base_tests/test_stats_utils.py:228:82: error[invalid-argument-type] Argument to bound method `__init__` is incorrect: Expected `Unknown & ~str`, found `Unknown & ~Literal["any"]`
- Found 733 diagnostics
+ Found 731 diagnostics

No memory usage changes detected ✅

[sharkdp]

It's true that it is enough to test disjointness by checking if the intersection between the two top-materializations is empty, but I think I would prefer a definition that is a bit clearer / more intuitive.

Two gradual types A and B are disjoint if their intersection is empty: A & B = Never.

From this definition, you can arrive at your property:

• A & B = Never is true if and only if the bottom and the top materialization of the two types are the same, i.e. if Top[A & B] = Never and Bottom[A & B] = Never.
• Top[X] = Never always implies Bottom[X] = Never, because Bottom[X] <: Top[X].
• This means that it is enough to test Top[A & B] = Never.
• Since Top[…] distributes over intersections, we can also write this as Top[A] & Top[B] = Never, which is equivalent to saying that the two fully-static types Top[A] and Top[B] must be disjoint.

[AlexWaygood]

Two gradual types A and B are disjoint if their intersection is empty: A & B = Never.

Riiight, but with our current implementation, this is surely circular -- we call is_disjoint_from from our intersection simplification infrastructure to determine whether A & B should simplify to Never!

[sharkdp]

Ok, I thought you wanted to clarify what the semantics of this function are, not how it's implemented (it's not implemented by comparing top-materializations either, as far as I can tell).

[AlexWaygood]

it's not implemented by comparing top-materializations either

yes, fair point. I'll try to reword it 👍

[sharkdp]

I'm happy to review the rest of the PR as well, but that will have to wait until tomorrow 😄

[sharkdp]

Our implementation of assignability between a type T and another type ~U is currently too strict. We currently only consider T assignable to ~U if Top[T] is disjoint from Top[U]. That's correct for subtyping and redundancy, but not for assignability: for assignability, we should be more permissive, and allow T to be considered assignable to ~U if Bottom[T] is disjoint from Bottom[U].

Let me see if I understand this:

• T is a subtype of ~U if Top[T] <: Bottom[~U]. We have Bottom[~U] = ~Top[U], so this is equivalent to Top[T] <: ~Top[U], which is equivalent to saying that Top[T] needs to be disjoint from Top[U] ✔️
• T is assignable to ~U if Bottom[T] <: Top[~U], i.e. Bottom[T] <: ~Bottom[U], which is equivalent to Bottom[T] being disjoint from Bottom[U] ✔️
• T is redundant with ~U if Bottom[T] <: Bottom[~U] (i.e. Bottom[T] <: ~Top[U]) and Top[T] <: Top[~U] (i.e. Top[T] <: ~Bottom[T]), which would mean that Bottom[T] needs to be disjoint from Top[U] and Top[T] needs to be disjoint from Bottom[U] ❌

The check for redundancy implemented here is too strict. This is not too surprising, because we know that redundancy is a weaker relation than subtyping. A counterexample would be T = Any and U = Any. T = Any is not a subtype of ~U = ~Any = Any, but the two types are redundant. And indeed, Bottom[T] = Never is disjoint from Top[U] = object, and Top[T] = object is disjoint from Bottom[U] = Never (the rules for redundancy above), but Top[T] = object is not disjoint from Top[U] = object (the rule for subtyping above).

I don't know what this means for this PR. I think there is still the bigger question as to whether or not we can actually use the true redundancy relation for union simplification (given that it breaks transitivity), or if we actually need something that sits between redundancy and subtyping, the sorts of ad-hoc rules that we currently implement in order to simplify things like Any | Any to Any.

[AlexWaygood]

• T is redundant with ~U if Bottom[T] <: Bottom[~U] (i.e. Bottom[T] <: ~Top[U]) and Top[T] <: Top[~U] (i.e. Top[T] <: ~Bottom[T]), which would mean that Bottom[T] needs to be disjoint from Top[U] and Top[T] needs to be disjoint from Bottom[U] ❌

The check for redundancy implemented here is too strict. This is not too surprising, because we know that redundancy is a weaker relation than subtyping.

That all seems correct to me. It's also unchanged from the redundancy implementation on main, however. This PR only touches the assignability relation for intersections with negated elements; it doesn't touch the subtyping or redundancy relations. So I would argue that this PR is a strict improvement on the semantics implemented on main, even if there are still further improvements that we might be able to make to the redundancy implementation (which would require more tests, and would require us to double-check that there aren't examples we can think of where implementing the redundancy relation more fully in this way would break transitivity).

I could add a comment linking to this discussion, and noting that this is probably not a complete implementation of the redundancy relation, but that we always err on the side of strictness for redundancy?

A counterexample would be T = Any and U = Any. T = Any is not a subtype of ~U = ~Any = Any, but the two types are redundant. And indeed, Bottom[T] = Never is disjoint from Top[U] = object, and Top[T] = object is disjoint from Bottom[U] = Never (the rules for redundancy above), but Top[T] = object is not disjoint from Top[U] = object (the rule for subtyping above).

Indeed. But pragmatically, we already recognise Any as being redundant from ~Any, because of the fact that we eagerly simplify ~Any to Any in our intersection builder: https://play.ty.dev/882fb732-dc66-4571-9898-ca51f0816cc0

[carljm]

I think it is a "known issue" that our implementation of redundancy is "too strict" compared to what it theoretically could/should be, but it must be too strict in order to avoid breaking transitivity (and transitivity is critical to the correct functioning of union simplification.)

I think there is still the bigger question as to whether or not we can actually use the true redundancy relation for union simplification (given that it breaks transitivity), or if we actually need something that sits between redundancy and subtyping

I think this is basically right, but I would frame it slightly differently. The reason we named the redundancy relation "redundancy" is in order to communicate "this is the relation we use for determining redundancy in unions." So we don't "need something that sits between redundancy and subtyping." We already have exactly that: we call it "redundancy". It sits between "S+ <: T+ && S- <: T- subtyping" (what you are I think here calling "true redundancy", but we could also call "true subtyping") and "S+ <: T- subtyping" (which we currently call "subtyping", but could also be called "too-strict subtyping.") Our redundancy relation is "too-strict subtyping", but with some ad-hoc elements of "true subtyping", (hopefully) carefully chosen to avoid breaking transitivity.

I don't think there is an open question about whether we can use a relation that breaks transitivity for union simplification. We definitely cannot, or else the result of union simplification depends on the order elements are added; this is not tenable.

[AlexWaygood]

I think this is basically right, but I would frame it slightly differently. The reason we named the redundancy relation "redundancy" is in order to communicate "this is the relation we use for determining redundancy in unions." So we don't "need something that sits between redundancy and subtyping." We already have exactly that: we call it "redundancy". It sits between "S+ <: T+ && S- <: T- subtyping" (what you are I think here calling "true redundancy", but we could also call "true subtyping") and "S+ <: T- subtyping" (which we currently call "subtyping", but could also be called "too-strict subtyping.") Our redundancy relation is "too-strict subtyping", but with some ad-hoc elements of "true subtyping", (hopefully) carefully chosen to avoid breaking transitivity.

Yes, I think the disconnect is that the ("pure"? But nontransitive?) version of the redundancy relation described in the doc-comment above the TypeRelation::Redundancy variant currently is not the version that we've actually implemented, because, as you say, the version that we've actually implemented deliberately errs on the side of strictness to avoid non-transitivity

[carljm]

I think the disconnect is that the ("pure"? But nontransitive?) version of the redundancy relation described in the doc-comment above the TypeRelation::Redundancy variant currently is not the version that we've actually implemented, because, as you say, the version that we've actually implemented deliberately errs on the side of strictness to avoid non-transitivity

Then we should reflect some of this discussion into that doc comment, to help us avoid continuing to have this same conversation on every PR related to redundancy 😆

[sharkdp]

I was genuinely confused by this, because there was an effort to formalize the new relation called redundancy in #20602, but then we ended up with a doc comment that essentially just describes "S+ <: T+ && S- <: T-" subtyping in a different way, as pointed out here. So I thought we actually aim to implement the "S+ <: T+ && S- <: T-" subtyping relation under the name of "redundancy". But this discussion here clarifies the situation: the doc comment is wrong, and what we call "redundancy" is "too-strict subtyping, but with some ad-hoc elements of true subtyping".

In that case, I'm just worried that we won't be able to succinctly define what that relation actually is. Basically what Doug said here (with what looks like a wrong definition of assignability 😉).