[red-knot] simplify gradually-equivalent types out of unions and intersections (#17467)

## Summary

If two types are gradually-equivalent, that means they share the same
set of possible materializations. There's no need to keep two such types
in the same union or intersection; we should simplify them.

Fixes https://github.com/astral-sh/ruff/issues/17465

The one downside here is that now we will simplify e.g. `Unknown |
Todo(...)` to just `Unknown`, if `Unknown` was added to the union first.
This is correct from a type perspective (they are equivalent types), but
it can mean we lose visibility into part of the cause for the type
inferring as unknown. I think this is OK, but if we think it's important
to avoid this, I can add a special case to try to preserve `Todo` over
`Unknown`, if we see them both in the same union or intersection.

## Test Plan

Added and updated mdtests.
This commit is contained in:
Carl Meyer 2025-04-18 15:08:57 -07:00 committed by GitHub
parent 8fe2dd5e03
commit 2a478ce1b2
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 35 additions and 31 deletions

View File

@ -302,7 +302,7 @@ class C:
c_instance = C() c_instance = C()
reveal_type(c_instance.a) # revealed: Unknown | Literal[1] reveal_type(c_instance.a) # revealed: Unknown | Literal[1]
reveal_type(c_instance.b) # revealed: Unknown | @Todo(starred unpacking) reveal_type(c_instance.b) # revealed: Unknown
``` ```
#### Attributes defined in for-loop (unpacking) #### Attributes defined in for-loop (unpacking)
@ -1892,6 +1892,17 @@ reveal_type(B().x) # revealed: Unknown | Literal[1]
reveal_type(A().x) # revealed: Unknown | Literal[1] reveal_type(A().x) # revealed: Unknown | Literal[1]
``` ```
This case additionally tests our union/intersection simplification logic:
```py
class H:
def __init__(self):
self.x = 1
def copy(self, other: "H"):
self.x = other.x or self.x
```
### Builtin types attributes ### Builtin types attributes
This test can probably be removed eventually, but we currently include it because we do not yet This test can probably be removed eventually, but we currently include it because we do not yet

View File

@ -201,3 +201,15 @@ def _(literals_2: Literal[0, 1], b: bool, flag: bool):
# Now union the two: # Now union the two:
reveal_type(bool_and_literals_128 if flag else literals_128_shifted) # revealed: int reveal_type(bool_and_literals_128 if flag else literals_128_shifted) # revealed: int
``` ```
## Simplifying gradually-equivalent types
If two types are gradually equivalent, we can keep just one of them in a union:
```py
from typing import Any, Union
from knot_extensions import Intersection, Not
def _(x: Union[Intersection[Any, Not[int]], Intersection[Any, Not[int]]]):
reveal_type(x) # revealed: Any & ~int
```

View File

@ -842,7 +842,7 @@ def unknown(
### Mixed dynamic types ### Mixed dynamic types
We currently do not simplify mixed dynamic types, but might consider doing so in the future: Gradually-equivalent types can be simplified out of intersections:
```py ```py
from typing import Any from typing import Any
@ -854,10 +854,10 @@ def mixed(
i3: Intersection[Not[Any], Unknown], i3: Intersection[Not[Any], Unknown],
i4: Intersection[Not[Any], Not[Unknown]], i4: Intersection[Not[Any], Not[Unknown]],
) -> None: ) -> None:
reveal_type(i1) # revealed: Any & Unknown reveal_type(i1) # revealed: Any
reveal_type(i2) # revealed: Any & Unknown reveal_type(i2) # revealed: Any
reveal_type(i3) # revealed: Any & Unknown reveal_type(i3) # revealed: Any
reveal_type(i4) # revealed: Any & Unknown reveal_type(i4) # revealed: Any
``` ```
## Invalid ## Invalid

View File

@ -12,7 +12,7 @@ x = [1, 2, 3]
reveal_type(x) # revealed: list reveal_type(x) # revealed: list
# TODO reveal int # TODO reveal int
reveal_type(x[0]) # revealed: Unknown | @Todo(Support for `typing.TypeVar` instances in type expressions) reveal_type(x[0]) # revealed: Unknown
# TODO reveal list # TODO reveal list
reveal_type(x[0:1]) # revealed: @Todo(specialized non-generic class) reveal_type(x[0:1]) # revealed: @Todo(specialized non-generic class)

View File

@ -47,10 +47,7 @@ static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]],
static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes)) static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes))
static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict)) static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict))
# TODO: No errors
# error: [static-assert-error]
static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any)) static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any))
# error: [static-assert-error]
static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any])) static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any]))
``` ```

View File

@ -1441,24 +1441,6 @@ impl<'db> Type<'db> {
} }
} }
/// Returns true if both `self` and `other` are the same gradual form
/// (limited to `Any`, `Unknown`, or `Todo`).
pub(crate) fn is_same_gradual_form(self, other: Type<'db>) -> bool {
matches!(
(self, other),
(
Type::Dynamic(DynamicType::Any),
Type::Dynamic(DynamicType::Any)
) | (
Type::Dynamic(DynamicType::Unknown),
Type::Dynamic(DynamicType::Unknown)
) | (
Type::Dynamic(DynamicType::Todo(_)),
Type::Dynamic(DynamicType::Todo(_))
)
)
}
/// Returns true if this type and `other` are gradual equivalent. /// Returns true if this type and `other` are gradual equivalent.
/// ///
/// > Two gradual types `A` and `B` are equivalent /// > Two gradual types `A` and `B` are equivalent

View File

@ -278,7 +278,7 @@ impl<'db> UnionBuilder<'db> {
break; break;
} }
if ty.is_same_gradual_form(element_type) if ty.is_gradual_equivalent_to(self.db, element_type)
|| ty.is_subtype_of(self.db, element_type) || ty.is_subtype_of(self.db, element_type)
|| element_type.is_object(self.db) || element_type.is_object(self.db)
{ {
@ -560,7 +560,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
for (index, existing_positive) in self.positive.iter().enumerate() { for (index, existing_positive) in self.positive.iter().enumerate() {
// S & T = S if S <: T // S & T = S if S <: T
if existing_positive.is_subtype_of(db, new_positive) if existing_positive.is_subtype_of(db, new_positive)
|| existing_positive.is_same_gradual_form(new_positive) || existing_positive.is_gradual_equivalent_to(db, new_positive)
{ {
return; return;
} }
@ -656,7 +656,9 @@ impl<'db> InnerIntersectionBuilder<'db> {
let mut to_remove = SmallVec::<[usize; 1]>::new(); let mut to_remove = SmallVec::<[usize; 1]>::new();
for (index, existing_negative) in self.negative.iter().enumerate() { for (index, existing_negative) in self.negative.iter().enumerate() {
// ~S & ~T = ~T if S <: T // ~S & ~T = ~T if S <: T
if existing_negative.is_subtype_of(db, new_negative) { if existing_negative.is_subtype_of(db, new_negative)
|| existing_negative.is_gradual_equivalent_to(db, new_negative)
{
to_remove.push(index); to_remove.push(index);
} }
// same rule, reverse order // same rule, reverse order