Skip to content

Commit 2a478ce

Browse files
authored
[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 #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.
1 parent 8fe2dd5 commit 2a478ce

File tree

7 files changed

+35
-31
lines changed

7 files changed

+35
-31
lines changed

crates/red_knot_python_semantic/resources/mdtest/attributes.md

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -302,7 +302,7 @@ class C:
302302

303303
c_instance = C()
304304
reveal_type(c_instance.a) # revealed: Unknown | Literal[1]
305-
reveal_type(c_instance.b) # revealed: Unknown | @Todo(starred unpacking)
305+
reveal_type(c_instance.b) # revealed: Unknown
306306
```
307307

308308
#### Attributes defined in for-loop (unpacking)
@@ -1892,6 +1892,17 @@ reveal_type(B().x) # revealed: Unknown | Literal[1]
18921892
reveal_type(A().x) # revealed: Unknown | Literal[1]
18931893
```
18941894

1895+
This case additionally tests our union/intersection simplification logic:
1896+
1897+
```py
1898+
class H:
1899+
def __init__(self):
1900+
self.x = 1
1901+
1902+
def copy(self, other: "H"):
1903+
self.x = other.x or self.x
1904+
```
1905+
18951906
### Builtin types attributes
18961907

18971908
This test can probably be removed eventually, but we currently include it because we do not yet

crates/red_knot_python_semantic/resources/mdtest/call/union.md

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,3 +201,15 @@ def _(literals_2: Literal[0, 1], b: bool, flag: bool):
201201
# Now union the two:
202202
reveal_type(bool_and_literals_128 if flag else literals_128_shifted) # revealed: int
203203
```
204+
205+
## Simplifying gradually-equivalent types
206+
207+
If two types are gradually equivalent, we can keep just one of them in a union:
208+
209+
```py
210+
from typing import Any, Union
211+
from knot_extensions import Intersection, Not
212+
213+
def _(x: Union[Intersection[Any, Not[int]], Intersection[Any, Not[int]]]):
214+
reveal_type(x) # revealed: Any & ~int
215+
```

crates/red_knot_python_semantic/resources/mdtest/intersection_types.md

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -842,7 +842,7 @@ def unknown(
842842

843843
### Mixed dynamic types
844844

845-
We currently do not simplify mixed dynamic types, but might consider doing so in the future:
845+
Gradually-equivalent types can be simplified out of intersections:
846846

847847
```py
848848
from typing import Any
@@ -854,10 +854,10 @@ def mixed(
854854
i3: Intersection[Not[Any], Unknown],
855855
i4: Intersection[Not[Any], Not[Unknown]],
856856
) -> None:
857-
reveal_type(i1) # revealed: Any & Unknown
858-
reveal_type(i2) # revealed: Any & Unknown
859-
reveal_type(i3) # revealed: Any & Unknown
860-
reveal_type(i4) # revealed: Any & Unknown
857+
reveal_type(i1) # revealed: Any
858+
reveal_type(i2) # revealed: Any
859+
reveal_type(i3) # revealed: Any
860+
reveal_type(i4) # revealed: Any
861861
```
862862

863863
## Invalid

crates/red_knot_python_semantic/resources/mdtest/subscript/lists.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ x = [1, 2, 3]
1212
reveal_type(x) # revealed: list
1313

1414
# TODO reveal int
15-
reveal_type(x[0]) # revealed: Unknown | @Todo(Support for `typing.TypeVar` instances in type expressions)
15+
reveal_type(x[0]) # revealed: Unknown
1616

1717
# TODO reveal list
1818
reveal_type(x[0:1]) # revealed: @Todo(specialized non-generic class)

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,10 +47,7 @@ static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]],
4747
static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes))
4848
static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict))
4949

50-
# TODO: No errors
51-
# error: [static-assert-error]
5250
static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any))
53-
# error: [static-assert-error]
5451
static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any]))
5552
```
5653

crates/red_knot_python_semantic/src/types.rs

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1441,24 +1441,6 @@ impl<'db> Type<'db> {
14411441
}
14421442
}
14431443

1444-
/// Returns true if both `self` and `other` are the same gradual form
1445-
/// (limited to `Any`, `Unknown`, or `Todo`).
1446-
pub(crate) fn is_same_gradual_form(self, other: Type<'db>) -> bool {
1447-
matches!(
1448-
(self, other),
1449-
(
1450-
Type::Dynamic(DynamicType::Any),
1451-
Type::Dynamic(DynamicType::Any)
1452-
) | (
1453-
Type::Dynamic(DynamicType::Unknown),
1454-
Type::Dynamic(DynamicType::Unknown)
1455-
) | (
1456-
Type::Dynamic(DynamicType::Todo(_)),
1457-
Type::Dynamic(DynamicType::Todo(_))
1458-
)
1459-
)
1460-
}
1461-
14621444
/// Returns true if this type and `other` are gradual equivalent.
14631445
///
14641446
/// > Two gradual types `A` and `B` are equivalent

crates/red_knot_python_semantic/src/types/builder.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ impl<'db> UnionBuilder<'db> {
278278
break;
279279
}
280280

281-
if ty.is_same_gradual_form(element_type)
281+
if ty.is_gradual_equivalent_to(self.db, element_type)
282282
|| ty.is_subtype_of(self.db, element_type)
283283
|| element_type.is_object(self.db)
284284
{
@@ -560,7 +560,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
560560
for (index, existing_positive) in self.positive.iter().enumerate() {
561561
// S & T = S if S <: T
562562
if existing_positive.is_subtype_of(db, new_positive)
563-
|| existing_positive.is_same_gradual_form(new_positive)
563+
|| existing_positive.is_gradual_equivalent_to(db, new_positive)
564564
{
565565
return;
566566
}
@@ -656,7 +656,9 @@ impl<'db> InnerIntersectionBuilder<'db> {
656656
let mut to_remove = SmallVec::<[usize; 1]>::new();
657657
for (index, existing_negative) in self.negative.iter().enumerate() {
658658
// ~S & ~T = ~T if S <: T
659-
if existing_negative.is_subtype_of(db, new_negative) {
659+
if existing_negative.is_subtype_of(db, new_negative)
660+
|| existing_negative.is_gradual_equivalent_to(db, new_negative)
661+
{
660662
to_remove.push(index);
661663
}
662664
// same rule, reverse order

0 commit comments

Comments
 (0)