Support parametric recursive alias relations
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 2909af5..13373a1 100644
--- a/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
+++ b/crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
@@ -306,6 +306,13 @@
     values: list[Selector] = []
     accept_selector(config.selector)
 
+type RecursiveSentinel = tuple[RecursiveSentinel]
+type EitherOrRecursiveSentinel = RecursiveSentinel | A | B
+
+def accept_either_or_recursive_sentinel(value: EitherOrRecursiveSentinel) -> None: ...
+def _(choice: Choice) -> None:
+    accept_either_or_recursive_sentinel(choice)
+
 class ExtendedChoice(Enum):
     A = "A"
     B = "B"
@@ -641,6 +648,192 @@
     y = x
 ```
 
+### Subtyping of recursive generic aliases
+
+Type relation for recursive aliases is checked structurally.
+
+```py
+from typing import Callable
+from ty_extensions import static_assert
+from ty_extensions._internal import is_assignable_to, is_subtype_of
+
+type DirectCovariantA[T] = T | tuple[DirectCovariantA[T], ...]
+type DirectCovariantB[T] = T | tuple[DirectCovariantB[T], ...]
+
+static_assert(is_subtype_of(DirectCovariantA[int], DirectCovariantB[object]))
+static_assert(is_subtype_of(DirectCovariantB[int], DirectCovariantA[object]))
+static_assert(not is_subtype_of(DirectCovariantA[object], DirectCovariantB[int]))
+static_assert(is_subtype_of(DirectCovariantA[DirectCovariantA[int]], DirectCovariantB[DirectCovariantB[object]]))
+static_assert(not is_subtype_of(DirectCovariantA[DirectCovariantA[object]], DirectCovariantB[DirectCovariantB[int]]))
+
+type DirectCovariantA2[T] = T | tuple[DirectCovariantA2[T | DirectCovariantA2[T]], ...]
+type DirectCovariantB2[T] = T | tuple[DirectCovariantB2[T | DirectCovariantB2[T]], ...]
+
+static_assert(is_subtype_of(DirectCovariantA2[int], DirectCovariantB2[int]))
+static_assert(not is_subtype_of(DirectCovariantB2[int], DirectCovariantA2[str]))
+static_assert(is_subtype_of(DirectCovariantA2[int], DirectCovariantB2[object]))
+static_assert(is_subtype_of(DirectCovariantA2[DirectCovariantA2[int]], DirectCovariantB2[DirectCovariantB2[object]]))
+static_assert(not is_subtype_of(DirectCovariantA2[DirectCovariantA2[object]], DirectCovariantB2[DirectCovariantB2[int]]))
+
+type DirectContravariantA[T] = Callable[[T], DirectContravariantA[T] | None]
+type DirectContravariantB[T] = Callable[[T], DirectContravariantB[T] | None]
+
+static_assert(is_subtype_of(DirectContravariantA[object], DirectContravariantB[int]))
+static_assert(is_subtype_of(DirectContravariantB[object], DirectContravariantA[int]))
+static_assert(not is_subtype_of(DirectContravariantA[int], DirectContravariantB[object]))
+static_assert(is_subtype_of(DirectContravariantA[DirectContravariantA[int]], DirectContravariantB[DirectContravariantB[object]]))
+static_assert(
+    not is_subtype_of(DirectContravariantA[DirectContravariantA[object]], DirectContravariantB[DirectContravariantB[int]])
+)
+
+type DirectInvariantA[T] = list[T | DirectInvariantA[T]]
+type DirectInvariantB[T] = list[T | DirectInvariantB[T]]
+
+static_assert(is_subtype_of(DirectInvariantA[int], DirectInvariantB[int]))
+static_assert(is_subtype_of(DirectInvariantB[int], DirectInvariantA[int]))
+static_assert(not is_subtype_of(DirectInvariantA[int], DirectInvariantB[str]))
+static_assert(not is_subtype_of(DirectInvariantB[str], DirectInvariantA[int]))
+static_assert(not is_subtype_of(DirectInvariantA[int], DirectInvariantB[object]))
+static_assert(not is_assignable_to(DirectInvariantA[int], DirectInvariantB[str]))
+static_assert(is_subtype_of(DirectInvariantA[DirectInvariantA[int]], DirectInvariantB[DirectInvariantB[int]]))
+static_assert(not is_subtype_of(DirectInvariantA[DirectInvariantA[int]], DirectInvariantB[DirectInvariantB[str]]))
+```
+
+### Subtyping of mutually recursive generic aliases
+
+Mutually recursive aliases can be structurally equivalent even when they have different definitions,
+but their type arguments still have to satisfy the alias variance.
+
+```py
+from typing import Callable, Never
+from ty_extensions import static_assert
+from ty_extensions._internal import is_assignable_to, is_subtype_of
+
+type CovariantA[T] = T | tuple[CovariantB[T], ...]
+type CovariantB[T] = T | tuple[CovariantA[T], ...]
+
+static_assert(is_subtype_of(CovariantA[int], CovariantB[object]))
+static_assert(is_subtype_of(CovariantB[int], CovariantA[object]))
+static_assert(not is_subtype_of(CovariantA[object], CovariantB[int]))
+static_assert(is_subtype_of(CovariantA[CovariantA[int]], CovariantB[CovariantB[object]]))
+static_assert(not is_subtype_of(CovariantA[CovariantA[object]], CovariantB[CovariantB[int]]))
+
+type CovariantA2[T] = T | tuple[CovariantB2[T | CovariantA2[T]], ...]
+type CovariantB2[T] = T | tuple[CovariantA2[T | CovariantB2[T]], ...]
+
+static_assert(is_subtype_of(CovariantA2[int], CovariantB2[int]))
+static_assert(not is_subtype_of(CovariantB2[int], CovariantA2[str]))
+static_assert(is_subtype_of(CovariantA2[int], CovariantB2[object]))
+static_assert(is_subtype_of(CovariantA2[CovariantA2[int]], CovariantB2[CovariantB2[object]]))
+static_assert(not is_subtype_of(CovariantA2[CovariantA2[object]], CovariantB2[CovariantB2[int]]))
+static_assert(is_subtype_of(CovariantA2[int], CovariantA2[object] | CovariantB2[object]))
+
+type AliasOfCovariantA2[T] = CovariantA2[T]
+type AliasOfCovariantB2[T] = CovariantB2[T]
+
+static_assert(is_subtype_of(AliasOfCovariantA2[int], AliasOfCovariantB2[object]))
+static_assert(is_subtype_of(AliasOfCovariantA2[AliasOfCovariantA2[int]], AliasOfCovariantB2[AliasOfCovariantB2[object]]))
+static_assert(not is_subtype_of(AliasOfCovariantA2[object], AliasOfCovariantB2[int]))
+
+type ContravariantA[T] = Callable[[T], ContravariantB[T] | None]
+type ContravariantB[T] = Callable[[T], ContravariantA[T] | None]
+
+static_assert(is_subtype_of(ContravariantA[object], ContravariantB[int]))
+static_assert(is_subtype_of(ContravariantB[object], ContravariantA[int]))
+static_assert(not is_subtype_of(ContravariantA[int], ContravariantB[object]))
+static_assert(is_subtype_of(ContravariantA[ContravariantA[int]], ContravariantB[ContravariantB[object]]))
+static_assert(not is_subtype_of(ContravariantA[ContravariantA[object]], ContravariantB[ContravariantB[int]]))
+
+type InvariantA[T] = list[T | InvariantB[T]]
+type InvariantB[T] = list[T | InvariantA[T]]
+
+static_assert(is_subtype_of(InvariantA[int], InvariantB[int]))
+static_assert(is_subtype_of(InvariantB[int], InvariantA[int]))
+static_assert(not is_subtype_of(InvariantA[int], InvariantB[str]))
+static_assert(not is_subtype_of(InvariantB[str], InvariantA[int]))
+static_assert(not is_subtype_of(InvariantA[int], InvariantB[object]))
+static_assert(not is_assignable_to(InvariantA[int], InvariantB[str]))
+static_assert(is_subtype_of(InvariantA[InvariantA[int]], InvariantB[InvariantB[int]]))
+static_assert(not is_subtype_of(InvariantA[InvariantA[int]], InvariantB[InvariantB[str]]))
+
+type SwapA[T, U] = tuple[SwapB[U, T], T, U]
+type SwapB[T, U] = tuple[SwapA[U, T], U, T]
+
+static_assert(is_subtype_of(SwapA[int, str], SwapB[str, int]))
+static_assert(is_subtype_of(SwapB[int, str], SwapA[str, int]))
+static_assert(not is_subtype_of(SwapA[int, str], SwapB[int, str]))
+
+type SwapGrowA[T, U] = T | tuple[SwapGrowB[U | SwapGrowA[T, U], T]]
+type SwapGrowB[T, U] = U | tuple[SwapGrowA[U | SwapGrowB[T, U], T]]
+
+static_assert(is_subtype_of(SwapGrowA[int, str], SwapGrowB[str, int]))
+
+type DuplicateGrowA[T, U] = T | tuple[DuplicateGrowA[T | DuplicateGrowA[T, U], U | DuplicateGrowA[T, U]]]
+type DuplicateGrowB[T, U] = T | tuple[DuplicateGrowB[T | DuplicateGrowB[T, U], U | DuplicateGrowB[T, U]]]
+
+static_assert(is_subtype_of(DuplicateGrowA[int, int], DuplicateGrowB[int, int]))
+
+type ArityGrowA[T] = T | tuple[ArityGrowB[T | ArityGrowA[T], T]]
+type ArityGrowB[T, U] = T | U | tuple[ArityGrowA[T]]
+
+static_assert(is_subtype_of(ArityGrowA[int], ArityGrowB[int, int]))
+static_assert(not is_subtype_of(ArityGrowA[int], ArityGrowB[int, str]))
+
+type SourceConstraintA[T] = T | list[T] | tuple[SourceConstraintA[str]]
+type SourceConstraintB[T] = T | list[int] | tuple[SourceConstraintB[str]]
+
+static_assert(not is_subtype_of(SourceConstraintA[int], SourceConstraintB[int]))
+
+# TODO: These decidable growing relations are outside the current finite parametric-rule fragment,
+# but a more precise recursive-alias solver should eventually classify them.
+
+type DifferentGrowA[T] = T | tuple[DifferentGrowA[list[T]]]
+type DifferentGrowB[T] = T | tuple[DifferentGrowB[set[T]]]
+
+static_assert(not is_subtype_of(DifferentGrowA[int], DifferentGrowB[int]))
+
+type NeverGrowA[T] = T | tuple[NeverGrowA[Never | NeverGrowA[T]]]
+type NeverGrowB[T] = T | tuple[NeverGrowB[Never]]
+
+static_assert(not is_subtype_of(NeverGrowA[int], NeverGrowB[int]))
+
+type OneSidedGrowA[T] = T | tuple[OneSidedGrowA[T | OneSidedGrowA[str]]]
+type OneSidedGrowB[T] = T | tuple[OneSidedGrowB[T]]
+
+static_assert(not is_subtype_of(OneSidedGrowA[int], OneSidedGrowB[int]))
+
+type BadA[T] = T | tuple[BadA[BadA[str]]]
+type BadB[T] = T | tuple[BadB[BadA[int]]]
+
+static_assert(not is_subtype_of(BadA[int], BadB[int]))
+```
+
+### Recursive generic alias relations that encode context-free grammar inclusion
+
+Recursive generic aliases can encode context-free grammars by threading a continuation type through
+the alias type arguments. For arbitrary aliases of this shape, deciding
+`GrammarA[End] <: GrammarB[End]` would decide context-free language inclusion, which is undecidable.
+This section documents the encoding shape rather than a future TODO for ty to prove every relation
+in the fragment.
+
+```py
+from typing import Literal
+from ty_extensions import static_assert
+from ty_extensions._internal import is_subtype_of
+
+type End = None
+type A[Rest] = tuple[Literal["a"], Rest]
+type B[Rest] = tuple[Literal["b"], Rest]
+
+# `AnyWord[Rest]` recognizes any word over `a | b`, followed by `Rest`.
+type AnyWord[Rest] = Rest | A[AnyWord[Rest]] | B[AnyWord[Rest]]
+
+# `Balanced[Rest]` recognizes `a^n b^n`, followed by `Rest`.
+type Balanced[Rest] = Rest | A[Balanced[B[Rest]]]
+
+static_assert(not is_subtype_of(B[End], Balanced[End]))
+```
+
 ### Non-recursive nested generic aliases
 
 A repeated use of the same generic alias can be a finite alias application instead of recursion.
diff --git a/crates/ty_python_semantic/src/types/cyclic.rs b/crates/ty_python_semantic/src/types/cyclic.rs
index 977fe67..cbdbfa9 100644
--- a/crates/ty_python_semantic/src/types/cyclic.rs
+++ b/crates/ty_python_semantic/src/types/cyclic.rs
@@ -85,18 +85,18 @@
         true
     }
 
-    /// Return `true` if `self` should use the recursive fallback for an active item.
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool
+    /// Return the active item that should provide the recursive fallback for `self`.
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self>
     where
         Self: Sized,
     {
         if !self.needs_recursive_identity() {
-            return false;
+            return None;
         }
 
         let identity = self.to_identity(db);
         seen.iter()
-            .any(|active| active.needs_recursive_identity() && active.to_identity(db) == identity)
+            .find(|active| active.needs_recursive_identity() && active.to_identity(db) == identity)
     }
 }
 
@@ -111,8 +111,8 @@
         Type::needs_recursive_identity(*self)
     }
 
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool {
-        type_has_recursive_identity_cycle(db, *self, seen, |active| *active, |_| true)
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self> {
+        type_recursive_identity_cycle(db, *self, seen, |active| *active, |_| true)
     }
 }
 
@@ -129,11 +129,11 @@
         self.0.needs_recursive_identity() || self.1.needs_recursive_identity()
     }
 
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool {
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self> {
         let identity = self.to_identity(db);
         let active_matches = |active: &Self| active.to_identity(db) == identity;
 
-        type_pair_has_recursive_identity_cycle(
+        type_pair_recursive_identity_cycle(
             db,
             self.0,
             self.1,
@@ -145,15 +145,15 @@
     }
 }
 
-/// Return `true` if a type should use the recursive fallback for an active type identity.
-pub(crate) fn type_has_recursive_identity_cycle<'db, S>(
+/// Return the active item that should provide the recursive fallback for a type.
+pub(crate) fn type_recursive_identity_cycle<'a, 'db, S>(
     db: &'db dyn Db,
     ty: Type<'db>,
-    seen: &[S],
+    seen: &'a [S],
     active_type: impl Fn(&S) -> Type<'db> + Copy,
     active_matches: impl Fn(&S) -> bool + Copy,
-) -> bool {
-    type_has_recursive_identity_cycle_impl(
+) -> Option<&'a S> {
+    type_recursive_identity_cycle_impl(
         db,
         ty,
         seen,
@@ -163,18 +163,18 @@
     )
 }
 
-/// Return `true` if either type should use the recursive fallback for an active item.
-pub(crate) fn type_pair_has_recursive_identity_cycle<'db, S>(
+/// Return the active item that should provide the recursive fallback for either type.
+pub(crate) fn type_pair_recursive_identity_cycle<'a, 'db, S>(
     db: &'db dyn Db,
     left: Type<'db>,
     right: Type<'db>,
-    seen: &[S],
+    seen: &'a [S],
     active_left: impl Fn(&S) -> Type<'db> + Copy,
     active_right: impl Fn(&S) -> Type<'db> + Copy,
     active_matches: impl Fn(&S) -> bool + Copy,
-) -> bool {
-    type_has_recursive_identity_cycle(db, left, seen, active_left, active_matches)
-        || type_has_recursive_identity_cycle(db, right, seen, active_right, active_matches)
+) -> Option<&'a S> {
+    type_recursive_identity_cycle(db, left, seen, active_left, active_matches)
+        .or_else(|| type_recursive_identity_cycle(db, right, seen, active_right, active_matches))
 }
 
 #[derive(Debug, Clone, Copy, Eq, PartialEq)]
@@ -183,29 +183,25 @@
     AfterSecondUnfold,
 }
 
-fn type_has_recursive_identity_cycle_impl<'db, S>(
+fn type_recursive_identity_cycle_impl<'a, 'db, S>(
     db: &'db dyn Db,
     ty: Type<'db>,
-    seen: &[S],
+    seen: &'a [S],
     active_type: impl Fn(&S) -> Type<'db> + Copy,
     active_matches: impl Fn(&S) -> bool + Copy,
     non_nested_alias_cycle_policy: NonNestedAliasCyclePolicy,
-) -> bool {
+) -> Option<&'a S> {
     let Type::TypeAlias(alias) = ty else {
-        let Some(identity) = ty.recursive_identity(db) else {
-            return false;
-        };
-        return seen.iter().any(|active| {
+        let identity = ty.recursive_identity(db)?;
+        return seen.iter().find(|active| {
             active_matches(active) && active_type(active).recursive_identity(db) == Some(identity)
         });
     };
 
     let identity = TypeIdentity::TypeAlias(alias.definition(db));
-    if !seen.iter().any(|active| {
+    let first_matching_active = seen.iter().find(|active| {
         active_matches(active) && active_type(active).recursive_identity(db) == Some(identity)
-    }) {
-        return false;
-    }
+    })?;
 
     let active_alias_count = seen
         .iter()
@@ -215,13 +211,13 @@
         .count();
 
     let Some(generic_context) = alias.generic_context(db) else {
-        return true;
+        return Some(first_matching_active);
     };
     if generic_context
         .variables(db)
         .any(|typevar| typevar.is_paramspec(db))
     {
-        return true;
+        return Some(first_matching_active);
     }
 
     let specialization = alias
@@ -231,7 +227,7 @@
         is_nested_alias_application(db, ty, seen, active_type, active_matches);
 
     if nested_alias_application {
-        return false;
+        return None;
     }
 
     if specialization.types(db).iter().copied().any(|argument| {
@@ -244,12 +240,17 @@
             })
         })
     }) {
-        return true;
+        return Some(first_matching_active);
     }
 
-    match non_nested_alias_cycle_policy {
+    let has_cycle = match non_nested_alias_cycle_policy {
         NonNestedAliasCyclePolicy::Immediate => true,
         NonNestedAliasCyclePolicy::AfterSecondUnfold => active_alias_count > 1,
+    };
+    if has_cycle {
+        Some(first_matching_active)
+    } else {
+        None
     }
 }
 
@@ -329,7 +330,7 @@
     pub fn visit(&self, db: &'db dyn Db, item: T, compute: impl FnOnce() -> R) -> R {
         match self.begin_visit(db, item) {
             CycleDetectorVisit::Ready(result) => result,
-            CycleDetectorVisit::Cycle(_) => self.fallback.clone(),
+            CycleDetectorVisit::Cycle { .. } => self.fallback.clone(),
             CycleDetectorVisit::Pending(item) => {
                 let result = compute();
                 self.finish_visit(item, result)
@@ -349,8 +350,11 @@
             return CycleDetectorVisit::Ready(self.fallback.clone());
         }
 
-        if item.has_recursive_identity_cycle(db, &seen) {
-            return CycleDetectorVisit::Cycle(item);
+        if let Some(active) = item.recursive_identity_cycle(db, &seen) {
+            return CycleDetectorVisit::Cycle {
+                active: active.clone(),
+                current: item,
+            };
         }
         drop(seen);
 
@@ -374,8 +378,8 @@
     /// The item already has a completed result or hit an exact recursive edge.
     Ready(R),
     /// A different item with the same abstract identity is already pending.
-    /// The item is the input that hit the active obligation.
-    Cycle(T),
+    /// The active item is the pending obligation; the current item is the input that hit it.
+    Cycle { active: T, current: T },
     /// The caller should compute the result and pass it to [`CycleDetector::finish_visit`].
     Pending(T),
 }
@@ -450,7 +454,7 @@
     ty: Type<'db>,
     seen: &[Type<'db>],
 ) -> bool {
-    type_has_recursive_identity_cycle_impl(
+    type_recursive_identity_cycle_impl(
         db,
         ty,
         seen,
@@ -458,6 +462,7 @@
         |_| true,
         NonNestedAliasCyclePolicy::AfterSecondUnfold,
     )
+    .is_some()
 }
 
 enum TypeTransformerVisit<'db> {
@@ -740,7 +745,7 @@
     }
 
     #[test]
-    fn identity_cycle_reports_current_item() {
+    fn identity_cycle_reports_active_and_current_items() {
         let db = setup_db();
         let detector = IdentityDetector::new(0);
         let first = TestItem {
@@ -756,9 +761,11 @@
             panic!("first visit should be pending");
         };
 
-        let CycleDetectorVisit::Cycle(current) = detector.begin_visit(&db, second) else {
+        let CycleDetectorVisit::Cycle { active, current } = detector.begin_visit(&db, second)
+        else {
             panic!("second visit should detect an identity cycle");
         };
+        assert_eq!(active, first);
         assert_eq!(current, second);
 
         detector.finish_visit(active_item, 10);
diff --git a/crates/ty_python_semantic/src/types/infer/builder/binary_expressions.rs b/crates/ty_python_semantic/src/types/infer/builder/binary_expressions.rs
index 92b77df..9c79ed6 100644
--- a/crates/ty_python_semantic/src/types/infer/builder/binary_expressions.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder/binary_expressions.rs
@@ -6,7 +6,7 @@
 use crate::types::call::CallArguments;
 use crate::types::constraints::ConstraintSetBuilder;
 use crate::types::cyclic::{
-    CycleDetector, HasIdentity, TypeIdentity, type_pair_has_recursive_identity_cycle,
+    CycleDetector, HasIdentity, TypeIdentity, type_pair_recursive_identity_cycle,
 };
 use crate::types::diagnostic::{
     DIVISION_BY_ZERO, report_unsupported_augmented_assignment, report_unsupported_binary_operation,
@@ -34,11 +34,11 @@
         (self.0.to_identity(db), self.1, self.2.to_identity(db))
     }
 
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool {
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self> {
         let identity = self.to_identity(db);
         let active_matches = |active: &Self| active.to_identity(db) == identity;
 
-        type_pair_has_recursive_identity_cycle(
+        type_pair_recursive_identity_cycle(
             db,
             self.0,
             self.2,
diff --git a/crates/ty_python_semantic/src/types/infer/comparisons.rs b/crates/ty_python_semantic/src/types/infer/comparisons.rs
index 0755fac..48eeef0 100644
--- a/crates/ty_python_semantic/src/types/infer/comparisons.rs
+++ b/crates/ty_python_semantic/src/types/infer/comparisons.rs
@@ -7,7 +7,7 @@
 use crate::types::constraints::ConstraintSetBuilder;
 use crate::types::context::InferContext;
 use crate::types::cyclic::{
-    CycleDetector, HasIdentity, TypeIdentity, type_pair_has_recursive_identity_cycle,
+    CycleDetector, HasIdentity, TypeIdentity, type_pair_recursive_identity_cycle,
 };
 use crate::types::equality::{equality_truthiness, inequality_truthiness};
 use crate::types::tuple::TupleSpec;
@@ -41,11 +41,11 @@
         (self.0.to_identity(db), self.1, self.2.to_identity(db))
     }
 
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool {
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self> {
         let identity = self.to_identity(db);
         let active_matches = |active: &Self| active.to_identity(db) == identity;
 
-        type_pair_has_recursive_identity_cycle(
+        type_pair_recursive_identity_cycle(
             db,
             self.0,
             self.2,
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index efdd158..aaff2c2 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -11,8 +11,7 @@
     OwnedConstraintSet,
 };
 use crate::types::cyclic::{
-    CycleDetectorVisit, HasIdentity, PairVisitor, TypeIdentity,
-    type_pair_has_recursive_identity_cycle,
+    CycleDetectorVisit, HasIdentity, PairVisitor, TypeIdentity, type_pair_recursive_identity_cycle,
 };
 use crate::types::enums::is_single_member_enum;
 use crate::types::function::FunctionDecorators;
@@ -22,13 +21,15 @@
     ApplyTypeMappingVisitor, CallableType, ClassBase, ClassLiteral, ClassType, CycleDetector,
     IntersectionType, KnownBoundMethodType, KnownClass, KnownInstanceType, LiteralValueTypeKind,
     MemberLookupPolicy, PropertyInstanceType, ProtocolInstanceType, SubclassOfInner,
-    SubclassOfType, TypeVarBoundOrConstraints, UnionType, UpcastPolicy,
+    SubclassOfType, TypeAliasType, TypeVarBoundOrConstraints, UnionBuilder, UnionType,
+    UpcastPolicy,
 };
 use crate::{
     Db,
     types::{
-        ErrorContext, ErrorContextTree, Type, constraints::ConstraintSet,
-        generics::InferableTypeVars,
+        ErrorContext, ErrorContextTree, Type,
+        constraints::ConstraintSet,
+        generics::{InferableTypeVars, Specialization},
     },
 };
 
@@ -742,11 +743,11 @@
         self.0.needs_recursive_identity() || self.1.needs_recursive_identity()
     }
 
-    fn has_recursive_identity_cycle(&self, db: &'db dyn Db, seen: &[Self]) -> bool {
+    fn recursive_identity_cycle<'a>(&self, db: &'db dyn Db, seen: &'a [Self]) -> Option<&'a Self> {
         let identity = self.to_identity(db);
         let active_matches = |active: &Self| active.to_identity(db) == identity;
 
-        type_pair_has_recursive_identity_cycle(
+        type_pair_recursive_identity_cycle(
             db,
             self.0,
             self.1,
@@ -797,6 +798,289 @@
     pub(super) materialization_visitor: &'a ApplyTypeMappingVisitor<'db>,
 }
 
+#[derive(Clone, Debug, Eq, PartialEq)]
+enum ParametricTerm<'db> {
+    SourceConstructor(Box<[Self]>),
+    TargetConstructor(Box<[Self]>),
+    Concrete(Type<'db>),
+    Union(Box<[Self]>),
+}
+
+#[derive(Clone, Copy, Eq, PartialEq)]
+enum ParametricConstructorSide {
+    Source,
+    Target,
+}
+
+impl<'db> ParametricTerm<'db> {
+    fn from_type(
+        db: &'db dyn Db,
+        ty: Type<'db>,
+        active_source: TypeAliasType<'db>,
+        active_target: TypeAliasType<'db>,
+    ) -> Self {
+        match ty {
+            Type::TypeAlias(alias) if alias.definition(db) == active_source.definition(db) => {
+                Self::SourceConstructor(Self::alias_arguments(
+                    db,
+                    alias,
+                    active_source,
+                    active_target,
+                ))
+            }
+            Type::TypeAlias(alias) if alias.definition(db) == active_target.definition(db) => {
+                Self::TargetConstructor(Self::alias_arguments(
+                    db,
+                    alias,
+                    active_source,
+                    active_target,
+                ))
+            }
+            Type::Union(union) => Self::union(
+                union
+                    .elements(db)
+                    .iter()
+                    .map(|element| Self::from_type(db, *element, active_source, active_target)),
+            ),
+            _ => Self::Concrete(ty),
+        }
+    }
+
+    fn alias_arguments(
+        db: &'db dyn Db,
+        alias: TypeAliasType<'db>,
+        active_source: TypeAliasType<'db>,
+        active_target: TypeAliasType<'db>,
+    ) -> Box<[Self]> {
+        let Some(specialization) =
+            TypeRelationChecker::type_alias_specialization_or_default(db, alias)
+        else {
+            return Box::new([]);
+        };
+
+        specialization
+            .types(db)
+            .iter()
+            .map(|ty| Self::from_type(db, *ty, active_source, active_target))
+            .collect()
+    }
+
+    fn union(elements: impl IntoIterator<Item = Self>) -> Self {
+        let mut elements: Vec<_> = elements.into_iter().collect();
+        if elements.is_empty() {
+            Self::Concrete(Type::Never)
+        } else if elements.len() == 1 {
+            elements.remove(0)
+        } else {
+            Self::Union(elements.into_boxed_slice())
+        }
+    }
+}
+
+struct ParametricSubtypingRule<'db> {
+    source: Box<[ParametricTerm<'db>]>,
+    target: Box<[ParametricTerm<'db>]>,
+}
+
+impl<'db> ParametricSubtypingRule<'db> {
+    fn from_specializations(
+        db: &'db dyn Db,
+        source: Specialization<'db>,
+        target: Specialization<'db>,
+        active_source: TypeAliasType<'db>,
+        active_target: TypeAliasType<'db>,
+    ) -> Self {
+        Self {
+            source: Self::arguments_from_specialization(db, source, active_source, active_target),
+            target: Self::arguments_from_specialization(db, target, active_source, active_target),
+        }
+    }
+
+    fn arguments_from_specialization(
+        db: &'db dyn Db,
+        specialization: Specialization<'db>,
+        active_source: TypeAliasType<'db>,
+        active_target: TypeAliasType<'db>,
+    ) -> Box<[ParametricTerm<'db>]> {
+        specialization
+            .types(db)
+            .iter()
+            .map(|ty| ParametricTerm::from_type(db, *ty, active_source, active_target))
+            .collect()
+    }
+
+    fn has_same_constructor_arities_as(&self, current: &Self) -> bool {
+        self.source.len() == current.source.len() && self.target.len() == current.target.len()
+    }
+}
+
+#[derive(Clone, Copy)]
+struct ParametricRuleApplication<'rule, 'db> {
+    rule: &'rule ParametricSubtypingRule<'db>,
+}
+
+impl<'rule, 'db> ParametricRuleApplication<'rule, 'db> {
+    const fn new(rule: &'rule ParametricSubtypingRule<'db>) -> Self {
+        Self { rule }
+    }
+
+    fn accepts(self, current: &ParametricSubtypingRule<'db>) -> bool {
+        self.rule.has_same_constructor_arities_as(current)
+            && self.current_is_parametric_instance(current)
+    }
+
+    fn current_is_parametric_instance(self, current: &ParametricSubtypingRule<'db>) -> bool {
+        self.arguments_are_parametric_instances(&current.source, &self.rule.source)
+            && self.arguments_are_parametric_instances(&current.target, &self.rule.target)
+    }
+
+    fn equivalent(self, left: &ParametricTerm<'db>, right: &ParametricTerm<'db>) -> bool {
+        use ParametricTerm::{Concrete, SourceConstructor, TargetConstructor, Union};
+
+        match (left, right) {
+            (SourceConstructor(left), SourceConstructor(right)) => {
+                self.arguments_are_equivalent(left, right)
+                    || self.arguments_match_same_rule_constructor(
+                        left,
+                        right,
+                        ParametricConstructorSide::Source,
+                    )
+            }
+            (TargetConstructor(left), TargetConstructor(right)) => {
+                self.arguments_are_equivalent(left, right)
+                    || self.arguments_match_same_rule_constructor(
+                        left,
+                        right,
+                        ParametricConstructorSide::Target,
+                    )
+            }
+            (Concrete(left), Concrete(right)) => left == right,
+            (Union(left), Union(right)) => {
+                left.len() == right.len()
+                    && left.iter().all(|left_element| {
+                        right
+                            .iter()
+                            .any(|right_element| self.equivalent(left_element, right_element))
+                    })
+            }
+            _ => false,
+        }
+    }
+
+    fn arguments_are_equivalent(
+        self,
+        left: &[ParametricTerm<'db>],
+        right: &[ParametricTerm<'db>],
+    ) -> bool {
+        left.len() == right.len()
+            && left
+                .iter()
+                .zip(right)
+                .all(|(left, right)| self.equivalent(left, right))
+    }
+
+    fn arguments_match_same_rule_constructor(
+        self,
+        left: &[ParametricTerm<'db>],
+        right: &[ParametricTerm<'db>],
+        side: ParametricConstructorSide,
+    ) -> bool {
+        self.any_rule_constructor_arguments(side, |rule_arguments| {
+            self.arguments_are_parametric_instances(left, rule_arguments)
+                && self.arguments_are_parametric_instances(right, rule_arguments)
+        })
+    }
+
+    fn arguments_match_rule_constructor(
+        self,
+        arguments: &[ParametricTerm<'db>],
+        side: ParametricConstructorSide,
+    ) -> bool {
+        self.any_rule_constructor_arguments(side, |rule_arguments| {
+            self.arguments_are_parametric_instances(arguments, rule_arguments)
+        })
+    }
+
+    fn any_rule_constructor_arguments(
+        self,
+        side: ParametricConstructorSide,
+        predicate: impl Fn(&[ParametricTerm<'db>]) -> bool,
+    ) -> bool {
+        let rule_arguments = match side {
+            ParametricConstructorSide::Source => &self.rule.source,
+            ParametricConstructorSide::Target => &self.rule.target,
+        };
+
+        predicate(rule_arguments)
+    }
+
+    fn arguments_are_parametric_instances(
+        self,
+        arguments: &[ParametricTerm<'db>],
+        rule_arguments: &[ParametricTerm<'db>],
+    ) -> bool {
+        arguments.len() == rule_arguments.len()
+            && arguments
+                .iter()
+                .zip(rule_arguments)
+                .all(|(argument, rule_argument)| {
+                    self.is_parametric_instance_of(argument, rule_argument)
+                })
+    }
+
+    fn is_parametric_instance_of(
+        self,
+        argument: &ParametricTerm<'db>,
+        rule_argument: &ParametricTerm<'db>,
+    ) -> bool {
+        if self.equivalent(argument, rule_argument) {
+            return true;
+        }
+
+        let ParametricTerm::Union(elements) = argument else {
+            return false;
+        };
+
+        match rule_argument {
+            ParametricTerm::Union(rule_elements) => {
+                self.union_is_parametric_instance(elements, rule_elements)
+            }
+            rule_argument => {
+                self.union_is_parametric_instance(elements, std::slice::from_ref(rule_argument))
+            }
+        }
+    }
+
+    fn union_is_parametric_instance(
+        self,
+        elements: &[ParametricTerm<'db>],
+        rule_elements: &[ParametricTerm<'db>],
+    ) -> bool {
+        rule_elements.iter().all(|rule_element| {
+            elements
+                .iter()
+                .any(|element| self.equivalent(element, rule_element))
+        }) && elements.iter().all(|element| {
+            rule_elements
+                .iter()
+                .any(|rule_element| self.equivalent(element, rule_element))
+                || self.is_recursive_constructor_application(element)
+        })
+    }
+
+    fn is_recursive_constructor_application(self, argument: &ParametricTerm<'db>) -> bool {
+        match argument {
+            ParametricTerm::SourceConstructor(arguments) => {
+                self.arguments_match_rule_constructor(arguments, ParametricConstructorSide::Source)
+            }
+            ParametricTerm::TargetConstructor(arguments) => {
+                self.arguments_match_rule_constructor(arguments, ParametricConstructorSide::Target)
+            }
+            ParametricTerm::Concrete(_) | ParametricTerm::Union(_) => false,
+        }
+    }
+}
+
 impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
     pub(super) fn subtyping(
         constraints: &'c ConstraintSetBuilder<'db>,
@@ -977,8 +1261,8 @@
             .begin_visit(db, (source, target, self.relation, self.typevar_evaluation))
         {
             CycleDetectorVisit::Ready(result) => result,
-            CycleDetectorVisit::Cycle(current) => {
-                self.recursive_type_pair_fallback(db, current.0, current.1)
+            CycleDetectorVisit::Cycle { active, current } => {
+                self.recursive_type_pair_fallback(db, active.0, active.1, current.0, current.1)
             }
             CycleDetectorVisit::Pending(item) => {
                 let result = work();
@@ -989,20 +1273,99 @@
 
     fn recursive_type_pair_fallback(
         &self,
-        _db: &'db dyn Db,
+        db: &'db dyn Db,
+        active_source: Type<'db>,
+        active_target: Type<'db>,
         source: Type<'db>,
         target: Type<'db>,
     ) -> ConstraintSet<'db, 'c> {
-        if matches!((source, target), (Type::TypeAlias(_), Type::TypeAlias(_))) {
+        if let (
+            Type::TypeAlias(active_source_alias),
+            Type::TypeAlias(active_target_alias),
+            Type::TypeAlias(source_alias),
+            Type::TypeAlias(target_alias),
+        ) = (active_source, active_target, source, target)
+        {
+            if Self::recursive_type_alias_pair_has_parametric_rule(
+                db,
+                active_source_alias,
+                active_target_alias,
+                source_alias,
+                target_alias,
+            ) {
+                return self.always();
+            }
             return self.never();
         }
 
         // Mixed recursive cycles (for example, alias vs. protocol) keep the existing
-        // coinductive fallback. Alias pairs are rejected above instead of generating another
-        // recursive obligation.
+        // coinductive fallback. The parametric rule check above is only sound for alias pairs,
+        // where both recursive constructors expose comparable specialization arguments.
         self.always()
     }
 
+    fn recursive_type_alias_pair_has_parametric_rule(
+        db: &'db dyn Db,
+        active_source: TypeAliasType<'db>,
+        active_target: TypeAliasType<'db>,
+        current_source: TypeAliasType<'db>,
+        current_target: TypeAliasType<'db>,
+    ) -> bool {
+        if active_source.definition(db) != current_source.definition(db)
+            || active_target.definition(db) != current_target.definition(db)
+        {
+            return false;
+        }
+
+        let (
+            Some(active_source_specialization),
+            Some(active_target_specialization),
+            Some(current_source_specialization),
+            Some(current_target_specialization),
+        ) = (
+            Self::type_alias_specialization_or_default(db, active_source),
+            Self::type_alias_specialization_or_default(db, active_target),
+            Self::type_alias_specialization_or_default(db, current_source),
+            Self::type_alias_specialization_or_default(db, current_target),
+        )
+        else {
+            return false;
+        };
+
+        let rule = ParametricSubtypingRule::from_specializations(
+            db,
+            active_source_specialization,
+            active_target_specialization,
+            active_source,
+            active_target,
+        );
+        let current_application = ParametricSubtypingRule::from_specializations(
+            db,
+            current_source_specialization,
+            current_target_specialization,
+            active_source,
+            active_target,
+        );
+
+        // Growing aliases can revisit the same constructor pair with larger specialization
+        // arguments. Close the cycle only when the current constructor application is an instance
+        // of the finite parametric rule induced by the active obligation. Everything else is
+        // outside this finite fragment and is rejected instead of generating another recursive
+        // obligation.
+        ParametricRuleApplication::new(&rule).accepts(&current_application)
+    }
+
+    fn type_alias_specialization_or_default(
+        db: &'db dyn Db,
+        alias: TypeAliasType<'db>,
+    ) -> Option<Specialization<'db>> {
+        alias.specialization(db).or_else(|| {
+            alias
+                .generic_context(db)
+                .map(|generic_context| generic_context.default_specialization(db, None))
+        })
+    }
+
     /// Is `target` a metaclass instance (a nominal instance of a subclass of `builtins.type`)?
     ///
     /// This does not include all types that are subtypes of `builtins.type`! The semantic
@@ -1219,7 +1582,18 @@
             // that depend on multiple elements, such as all members of an enum, are visible.
             (_, Type::Union(union)) if union.has_aliases(db) => {
                 self.with_recursion_guard(db, source, target, || {
-                    self.check_type_pair(db, source, union.expand_aliases(db))
+                    let expanded = union
+                        .elements(db)
+                        .iter()
+                        .copied()
+                        .fold(
+                            UnionBuilder::new(db)
+                                .no_cyclic_query(true)
+                                .recursively_defined(union.recursively_defined(db)),
+                            UnionBuilder::add,
+                        )
+                        .build();
+                    self.check_type_pair(db, source, expanded)
                 })
             }
 
diff --git a/crates/ty_python_semantic/src/types/set_theoretic.rs b/crates/ty_python_semantic/src/types/set_theoretic.rs
index 10bcd59..5ab42b3 100644
--- a/crates/ty_python_semantic/src/types/set_theoretic.rs
+++ b/crates/ty_python_semantic/src/types/set_theoretic.rs
@@ -116,7 +116,9 @@
         elements
             .into_iter()
             .fold(
-                UnionBuilder::new(db).cycle_recovery(true),
+                UnionBuilder::new(db)
+                    .unpack_aliases(false)
+                    .no_cyclic_query(true),
                 |builder, element| builder.add(element.into()),
             )
             .build()
@@ -386,7 +388,7 @@
     ) -> Option<Type<'db>> {
         let mut builder = UnionBuilder::new(db)
             .unpack_aliases(false)
-            .cycle_recovery(true)
+            .no_cyclic_query(true)
             .recursively_defined(self.recursively_defined(db));
         let mut empty = true;
         for ty in self.elements(db) {
diff --git a/crates/ty_python_semantic/src/types/set_theoretic/builder.rs b/crates/ty_python_semantic/src/types/set_theoretic/builder.rs
index 970cb69..0156a37 100644
--- a/crates/ty_python_semantic/src/types/set_theoretic/builder.rs
+++ b/crates/ty_python_semantic/src/types/set_theoretic/builder.rs
@@ -378,11 +378,11 @@
         &mut self,
         db: &'db dyn Db,
         other_type: Type<'db>,
-        cycle_recovery: bool,
+        no_cyclic_query: bool,
     ) -> ReduceResult<'db> {
-        if cycle_recovery {
-            // A widened literal group must absorb matching literals from later iterations for
-            // recovery to converge. Preserve that exact fallback reduction without relation queries.
+        if no_cyclic_query {
+            // Keep exact literal-fallback reductions even when relation-based reductions are
+            // disabled.
             return match self {
                 UnionElement::Type(existing) => ReduceResult::Type(*existing),
                 UnionElement::IntLiterals(_) => {
@@ -533,9 +533,11 @@
     elements: Vec<UnionElement<'db>>,
     db: &'db dyn Db,
     unpack_aliases: bool,
-    /// This is enabled when joining types in a `cycle_recovery` function. Because recovery cannot
-    /// introduce a new cycle, relation-based union simplifications are skipped in this mode.
-    cycle_recovery: bool,
+    /// Disable union simplifications that would issue relation queries.
+    ///
+    /// This is used while handling recursive queries or cycle recovery,
+    /// where issuing another relation query from union construction can re-enter the same recursion.
+    no_cyclic_query: bool,
     recursively_defined: RecursivelyDefined,
 }
 
@@ -601,7 +603,7 @@
             db,
             elements: vec![],
             unpack_aliases: true,
-            cycle_recovery: false,
+            no_cyclic_query: false,
             recursively_defined: RecursivelyDefined::No,
         }
     }
@@ -611,11 +613,9 @@
         self
     }
 
-    pub(crate) fn cycle_recovery(mut self, val: bool) -> Self {
-        self.cycle_recovery = val;
-        if self.cycle_recovery {
-            self.unpack_aliases = false;
-        }
+    /// Disable union simplifications that would issue relation queries.
+    pub(crate) fn no_cyclic_query(mut self, val: bool) -> Self {
+        self.no_cyclic_query = val;
         self
     }
 
@@ -671,9 +671,9 @@
     }
 
     pub(crate) fn add_in_place_impl(&mut self, ty: Type<'db>, seen_aliases: &mut Vec<Type<'db>>) {
-        let cycle_recovery = self.cycle_recovery;
+        let no_cyclic_query = self.no_cyclic_query;
         let should_widen = |literals, recursively_defined: RecursivelyDefined| {
-            if recursively_defined.is_yes() && cycle_recovery {
+            if recursively_defined.is_yes() && no_cyclic_query {
                 literals >= MAX_RECURSIVE_UNION_LITERALS
             } else {
                 literals >= MAX_NON_RECURSIVE_UNION_LITERALS
@@ -693,7 +693,7 @@
                 self.recursively_defined = self
                     .recursively_defined
                     .or(union.recursively_defined(self.db));
-                if self.cycle_recovery && self.recursively_defined.is_yes() {
+                if self.no_cyclic_query && self.recursively_defined.is_yes() {
                     let literals = self.elements.iter().fold(0, |acc, elem| match elem {
                         UnionElement::IntLiterals(literals) => acc + literals.len(),
                         UnionElement::StringLiterals(literals) => acc + literals.len(),
@@ -709,9 +709,23 @@
             // Adding `Never` to a union is a no-op.
             Type::Never => {}
             Type::TypeAlias(alias) if self.unpack_aliases => {
-                if seen_aliases.contains(&ty) {
-                    // Union contains itself recursively via a type alias. This is an error, just
-                    // leave out the recursive alias. TODO surface this error.
+                let seen_alias = if self.no_cyclic_query {
+                    ty.recursive_identity(self.db).is_some_and(|identity| {
+                        seen_aliases
+                            .iter()
+                            .any(|seen| seen.recursive_identity(self.db) == Some(identity))
+                    })
+                } else {
+                    seen_aliases.contains(&ty)
+                };
+
+                if seen_alias {
+                    if self.no_cyclic_query {
+                        self.push_type(ty, seen_aliases);
+                    } else {
+                        // Union contains itself recursively via a type alias. This is an error,
+                        // just leave out the recursive alias. TODO surface this error.
+                    }
                 } else {
                     seen_aliases.push(ty);
                     self.add_in_place_impl(alias.value_type(self.db), seen_aliases);
@@ -740,12 +754,12 @@
                                     continue;
                                 }
                                 UnionElement::Type(existing)
-                                    if cycle_recovery
+                                    if no_cyclic_query
                                         && literal.fallback_instance(self.db) == *existing =>
                                 {
                                     return;
                                 }
-                                UnionElement::Type(existing) if !cycle_recovery => {
+                                UnionElement::Type(existing) if !no_cyclic_query => {
                                     // e.g. `existing` could be `Literal[""] & Any`,
                                     // and `ty` could be `Literal[""]`
                                     if ty.is_redundant_with(self.db, *existing) {
@@ -793,12 +807,12 @@
                                     continue;
                                 }
                                 UnionElement::Type(existing)
-                                    if cycle_recovery
+                                    if no_cyclic_query
                                         && literal.fallback_instance(self.db) == *existing =>
                                 {
                                     return;
                                 }
-                                UnionElement::Type(existing) if !cycle_recovery => {
+                                UnionElement::Type(existing) if !no_cyclic_query => {
                                     if ty.is_redundant_with(self.db, *existing) {
                                         return;
                                     }
@@ -848,12 +862,12 @@
                                     continue;
                                 }
                                 UnionElement::Type(existing)
-                                    if cycle_recovery
+                                    if no_cyclic_query
                                         && literal.fallback_instance(self.db) == *existing =>
                                 {
                                     return;
                                 }
-                                UnionElement::Type(existing) if !cycle_recovery => {
+                                UnionElement::Type(existing) if !no_cyclic_query => {
                                     if ty.is_redundant_with(self.db, *existing) {
                                         return;
                                     }
@@ -924,12 +938,12 @@
                                     continue;
                                 }
                                 UnionElement::Type(existing)
-                                    if cycle_recovery
+                                    if no_cyclic_query
                                         && literal.fallback_instance(self.db) == *existing =>
                                 {
                                     return;
                                 }
-                                UnionElement::Type(existing) if !cycle_recovery => {
+                                UnionElement::Type(existing) if !no_cyclic_query => {
                                     if ty.is_redundant_with(self.db, *existing) {
                                         return;
                                     }
@@ -983,7 +997,7 @@
                 }
             }
             // Adding `object` to a union results in `object`.
-            ty if ty.is_object() && !cycle_recovery => self.collapse_to_object(),
+            ty if ty.is_object() => self.collapse_to_object(),
             _ => self.push_type(ty, seen_aliases),
         }
     }
@@ -1001,13 +1015,13 @@
         // If an alias gets here, it means we aren't unpacking aliases, and we also
         // shouldn't try to simplify aliases out of the union, because that will require
         // unpacking them.
-        let should_simplify_full = !matches!(ty, Type::TypeAlias(_)) && !self.cycle_recovery;
+        let should_simplify_full = !matches!(ty, Type::TypeAlias(_)) && !self.no_cyclic_query;
 
         let mut ty_negated: Option<Type> = None;
         let mut to_remove = SmallVec::<[usize; 2]>::new();
 
         for (i, element) in self.elements.iter_mut().enumerate() {
-            let element_type = match element.try_reduce(self.db, ty, self.cycle_recovery) {
+            let element_type = match element.try_reduce(self.db, ty, self.no_cyclic_query) {
                 ReduceResult::KeepIf(keep) => {
                     if !keep {
                         to_remove.push(i);
@@ -1029,11 +1043,26 @@
             }
 
             // `object` already contains every possible union element.
-            if !self.cycle_recovery && element_type == Type::object() {
+            if element_type == Type::object() {
                 return;
             }
 
-            if !self.cycle_recovery && should_preserve_hashable_union(self.db, ty, element_type) {
+            if self.no_cyclic_query
+                && let Type::LiteralValue(literal) = ty
+                && literal.fallback_instance(self.db) == element_type
+            {
+                return;
+            }
+
+            if self.no_cyclic_query
+                && let Type::LiteralValue(literal) = element_type
+                && literal.fallback_instance(self.db) == ty
+            {
+                to_remove.push(i);
+                continue;
+            }
+
+            if !self.no_cyclic_query && should_preserve_hashable_union(self.db, ty, element_type) {
                 continue;
             }
 
@@ -1053,7 +1082,7 @@
             }
 
             // Fold `(T & ~AlwaysTruthy) | (T & ~AlwaysFalsy)` to `T`.
-            if !self.cycle_recovery
+            if !self.no_cyclic_query
                 && let Some(merged_type) = merge_truthiness_guarded_pair(self.db, ty, element_type)
             {
                 to_remove.push(i);
@@ -1061,7 +1090,7 @@
                 continue;
             }
 
-            if !self.cycle_recovery
+            if !self.no_cyclic_query
                 && element_type
                     .as_literal_value_kind()
                     .zip(bool_pair(ty))
@@ -1124,7 +1153,7 @@
     pub(crate) fn try_build(self) -> Option<Type<'db>> {
         let db = self.db;
         let unpack_aliases = self.unpack_aliases;
-        let cycle_recovery = self.cycle_recovery;
+        let no_cyclic_query = self.no_cyclic_query;
         let recursively_defined = self.recursively_defined;
 
         let type_count = self.elements.iter().map(UnionElement::type_count).sum();
@@ -1167,10 +1196,10 @@
             }
         }
 
-        if normalize_enum_complement_unions(db, &mut types) {
+        if !no_cyclic_query && normalize_enum_complement_unions(db, &mut types) {
             let builder = UnionBuilder::new(db)
                 .unpack_aliases(unpack_aliases)
-                .cycle_recovery(cycle_recovery)
+                .no_cyclic_query(no_cyclic_query)
                 .recursively_defined(recursively_defined);
             return types
                 .into_iter()
@@ -1978,14 +2007,14 @@
     }
 
     #[test]
-    fn cycle_recovery_widens_recursive_literal_union() {
+    fn no_cyclic_query_widens_recursive_literal_union() {
         let db = setup_db();
         let literal_limit =
             i64::try_from(MAX_RECURSIVE_UNION_LITERALS).expect("literal limit fits in i64");
 
         let union = (0..=literal_limit).map(Type::int_literal).fold(
             UnionBuilder::new(&db)
-                .cycle_recovery(true)
+                .no_cyclic_query(true)
                 .recursively_defined(RecursivelyDefined::Yes),
             UnionBuilder::add,
         );
@@ -1995,7 +2024,7 @@
         let assert_widens = |literal, instance| {
             for (first, second) in [(literal, instance), (instance, literal)] {
                 let union = UnionBuilder::new(&db)
-                    .cycle_recovery(true)
+                    .no_cyclic_query(true)
                     .add(first)
                     .add(second)
                     .build();
@@ -2028,26 +2057,25 @@
     }
 
     #[test]
-    fn cycle_recovery_skips_other_redundancy_simplification() {
+    fn no_cyclic_query_preserves_relation_free_reductions() {
         let db = setup_db();
 
-        for (left, right) in [
-            (Type::string_literal(&db, "literal"), Type::literal_string()),
-            (Type::bool_literal(true), KnownClass::Bool.to_instance(&db)),
-            (Type::int_literal(1), Type::object()),
-            (Type::bool_literal(true), Type::bool_literal(false)),
-        ] {
-            for (first, second) in [(left, right), (right, left)] {
-                let union = UnionBuilder::new(&db)
-                    .cycle_recovery(true)
-                    .add(first)
-                    .add(second)
-                    .build()
-                    .expect_union();
-                assert!(union.elements(&db).contains(&left));
-                assert!(union.elements(&db).contains(&right));
-            }
-        }
+        assert_eq!(
+            UnionBuilder::new(&db)
+                .no_cyclic_query(true)
+                .add(Type::bool_literal(true))
+                .add(KnownClass::Bool.to_instance(&db))
+                .build(),
+            KnownClass::Bool.to_instance(&db)
+        );
+        assert_eq!(
+            UnionBuilder::new(&db)
+                .no_cyclic_query(true)
+                .add(Type::int_literal(1))
+                .add(Type::object())
+                .build(),
+            Type::object()
+        );
     }
 
     #[test]