From 0252ee65318b409d52b40919c78b31a69174363c Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Thu, 5 Jun 2025 15:48:09 +0200
Subject: [PATCH] Equivalence

---
 .../resources/mdtest/pep695_type_aliases.md   | 92 +++++++++++++++++++
 crates/ty_python_semantic/src/types.rs        | 24 +++++
 2 files changed, 116 insertions(+)

diff --git a/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md b/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
index daa538db39..6d5e131c11 100644
--- a/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
+++ b/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
@@ -23,6 +23,98 @@ def f() -> None:
     reveal_type(x)  # revealed: IntOrStr
 ```
 
+## Type properties
+
+### Equivalence
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+
+type IntOrStr = int | str
+type StrOrInt = str | int
+
+static_assert(is_equivalent_to(IntOrStr, IntOrStr))
+static_assert(is_equivalent_to(IntOrStr, StrOrInt))
+
+type Rec1 = tuple[Rec1, int]
+type Rec2 = tuple[Rec2, int]
+
+type Other = tuple[Other, str]
+
+static_assert(is_equivalent_to(Rec1, Rec2))
+static_assert(not is_equivalent_to(Rec1, Other))
+
+type Cycle1A = tuple[Cycle1B, int]
+type Cycle1B = tuple[Cycle1A, str]
+
+type Cycle2A = tuple[Cycle2B, int]
+type Cycle2B = tuple[Cycle2A, str]
+
+static_assert(is_equivalent_to(Cycle1A, Cycle2A))
+static_assert(is_equivalent_to(Cycle1B, Cycle2B))
+static_assert(not is_equivalent_to(Cycle1A, Cycle1B))
+static_assert(not is_equivalent_to(Cycle1A, Cycle2B))
+
+# type Cycle3A = tuple[Cycle3B] | None
+# type Cycle3B = tuple[Cycle3A] | None
+
+# static_assert(is_equivalent_to(Cycle3A, Cycle3A))
+# static_assert(is_equivalent_to(Cycle3A, Cycle3B))
+```
+
+### Assignability
+
+```py
+type IntOrStr = int | str
+
+x1: IntOrStr = 1
+x2: IntOrStr = "1"
+x3: IntOrStr | None = None
+
+def _(int_or_str: IntOrStr) -> None:
+    # TODO: those should not be errors
+    x3: int | str = int_or_str  # error: [invalid-assignment]
+    x4: int | str | None = int_or_str  # error: [invalid-assignment]
+    x5: int | str | None = int_or_str or None  # error: [invalid-assignment]
+```
+
+### Narrowing (intersections)
+
+```py
+class P: ...
+class Q: ...
+
+type EitherOr = P | Q
+
+def _(x: EitherOr) -> None:
+    if isinstance(x, P):
+        reveal_type(x)  # revealed: P
+    elif isinstance(x, Q):
+        reveal_type(x)  # revealed: Q & ~P
+    else:
+        # TODO: This should be Never
+        reveal_type(x)  # revealed: EitherOr & ~P & ~Q
+```
+
+### Fully static
+
+```py
+from typing import Any
+from ty_extensions import static_assert, is_fully_static
+
+type IntOrStr = int | str
+type RecFullyStatic = int | tuple[RecFullyStatic]
+
+static_assert(is_fully_static(IntOrStr))
+static_assert(is_fully_static(RecFullyStatic))
+
+type IntOrAny = int | Any
+type RecNotFullyStatic = Any | tuple[RecNotFullyStatic]
+
+static_assert(not is_fully_static(IntOrAny))
+static_assert(not is_fully_static(RecNotFullyStatic))
+```
+
 ## `__value__` attribute
 
 ```py
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index fd100d93ad..3bd4852ed9 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -275,6 +275,25 @@ fn is_fully_static_cycle_initial<'db>(_db: &'db dyn Db, _self: Type<'db>, _dummy
     true
 }
 
+#[expect(clippy::trivially_copy_pass_by_ref)]
+fn is_equivalent_to_cycle_recover<'db>(
+    _db: &'db dyn Db,
+    _value: &bool,
+    _count: u32,
+    _self: Type<'db>,
+    _other: Type<'db>,
+) -> salsa::CycleRecoveryAction<bool> {
+    salsa::CycleRecoveryAction::Iterate
+}
+
+fn is_equivalent_to_cycle_initial<'db>(
+    _db: &'db dyn Db,
+    _self: Type<'db>,
+    _other: Type<'db>,
+) -> bool {
+    true
+}
+
 /// Meta data for `Type::Todo`, which represents a known limitation in ty.
 #[cfg(debug_assertions)]
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
@@ -1706,6 +1725,8 @@ impl<'db> Type<'db> {
     /// This method returns `false` if either `self` or `other` is not fully static.
     ///
     /// [equivalent to]: https://typing.python.org/en/latest/spec/glossary.html#term-equivalent
+
+    #[salsa::tracked(cycle_fn=is_equivalent_to_cycle_recover, cycle_initial=is_equivalent_to_cycle_initial)]
     pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool {
         // TODO equivalent but not identical types: TypedDicts, Protocols, type aliases, etc.
 
@@ -1735,6 +1756,9 @@ impl<'db> Type<'db> {
             | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol)) => {
                 n.class.is_object(db) && protocol.normalized(db) == nominal
             }
+            (Type::TypeAliasRef(left), right) => left.value_type(db).is_equivalent_to(db, right),
+            (left, Type::TypeAliasRef(right)) => left.is_equivalent_to(db, right.value_type(db)),
+
             _ => self == other && self.is_fully_static(db) && other.is_fully_static(db),
         }
     }