From eb436b05df1d2655f980eee80c71c6940b546ad4 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 19 Feb 2026 20:21:23 +0100
Subject: [PATCH 1/6] Node definitions (Block A)

---
 lib/elixir/lib/module/types/descr.ex | 35 +++++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 6 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 17d17cbbbed..ffda89dc5a4 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -110,6 +110,22 @@ defmodule Module.Types.Descr do
   @boolset :sets.from_list([true, false], version: 2)
   def boolean(), do: %{atom: {:union, @boolset}}
 
+  ## Nodes
+
+  # @spec descr() :: map() | :term
+  # @spec state() :: map()
+  # @spec node() :: {id :: reference(), state :: map(), generator :: (state() -> node())}
+  def make_node(state, generator), do: {make_ref(), state, generator}
+
+  # @spec to_node(descr :: descr() | node()) :: node()
+  def to_node(:term), do: make_node(:term, fn _state -> :term end)
+  def to_node(descr = %{}), do: make_node(%{}, fn _state -> descr end)
+  def to_node(node) when is_tuple(node), do: node
+
+  def to_descr(:term), do: :term
+  def to_descr(descr = %{}), do: descr
+  def to_descr({_id, state, generator}), do: generator.(state)
+
   @doc """
   Gets the upper bound of a gradual type.
 
@@ -1942,8 +1958,11 @@ defmodule Module.Types.Descr do
   #
   # none() types can be given and, while stored, it means the list type is empty.
   defp list_descr(list_type, last_type, empty?) do
-    {list_dynamic?, list_type} = list_pop_dynamic(list_type)
-    {last_dynamic?, last_type} = list_pop_dynamic(last_type)
+    list_type_descr = to_descr(list_type)
+    last_type_descr = to_descr(last_type)
+
+    {list_dynamic?, list_type} = list_pop_dynamic(list_type_descr)
+    {last_dynamic?, last_type} = list_pop_dynamic(last_type_descr)
 
     list_part =
       if last_type == :term do
@@ -2612,8 +2631,10 @@ defmodule Module.Types.Descr do
   end
 
   defp map_descr_pairs([{key, value} | rest], fields, domain, dynamic?) do
+    value_descr = to_descr(value)
+
     {value, dynamic?} =
-      case :maps.take(:dynamic, value) do
+      case :maps.take(:dynamic, value_descr) do
         :error -> {value, dynamic?}
         {dynamic, _static} -> {dynamic, true}
       end
@@ -4311,18 +4332,20 @@ defmodule Module.Types.Descr do
   end
 
   defp tuple_descr([value | rest], acc, dynamic?) do
+    value_descr = to_descr(value)
+
     # Check if the static part is empty
     static_empty? =
-      case value do
+      case value_descr do
         # Has dynamic component, check static separately
         %{dynamic: _} -> false
-        _ -> empty?(value)
+        _ -> empty?(value_descr)
       end
 
     if static_empty? do
       :empty
     else
-      case :maps.take(:dynamic, value) do
+      case :maps.take(:dynamic, value_descr) do
         :error ->
           tuple_descr(rest, [value | acc], dynamic?)
 

From 8ecaf0052edebee85b603eb04af512f448c7f8c9 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 19 Feb 2026 20:29:37 +0100
Subject: [PATCH 2/6] Add md file

---
 recursive_types.md | 441 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 441 insertions(+)
 create mode 100644 recursive_types.md

diff --git a/recursive_types.md b/recursive_types.md
new file mode 100644
index 00000000000..1555f0c3d5e
--- /dev/null
+++ b/recursive_types.md
@@ -0,0 +1,441 @@
+# Recursive Types via Type Nodes in Elixir
+
+### A coinductive representation using closures and maps
+
+---
+
+**Abstract.**
+We describe a technique for representing recursive types in Elixir by introducing a *type node* structure. A type node pairs a *state*—a map recording one stepping step for every recursion variable—with a *generator function* that, given a state, produces a type descriptor (*descr*). This coinductive encoding naturally extends to mutually recursive definitions, keeps each node self-contained, and integrates smoothly with set-theoretic operations such as union.
+
+---
+
+## Table of Contents
+
+1. [Background: Type Descriptors](#1-background-type-descriptors)
+2. [Type Nodes](#2-type-nodes)
+3. [The Role of Nodes and Descriptors](#3-the-role-of-nodes-and-descriptors)
+4. [Constructing Recursive Types](#4-constructing-recursive-types)
+5. [Example: Simple Recursive List](#5-example-simple-recursive-list)
+6. [Example: Mutually Recursive Types](#6-example-mutually-recursive-types)
+7. [Using Nodes in Set Operations](#7-using-nodes-in-set-operations)
+8. [Node Identity and Memoization](#8-node-identity-and-memoization)
+9. [Summary](#9-summary)
+10. [Implementation Plan](#10-implementation-plan)
+
+---
+
+## 1. Background: Type Descriptors
+
+A *type descriptor* (or simply *descr*) is an Elixir map whose keys are type-kind tags and whose values describe the inhabitants of that kind:
+
+```
+descr = %{atom => atom_kind, tuple => tuple_kind, ...}
+```
+
+For example, the type "integer or `nil`" is represented as:
+
+```
+%{integer => true, atom => [:nil]}
+```
+
+Here `integer => true` means "integers are present" (as a whole) and `atom => [:nil]` means "the atoms present are the set {`nil`}".
+
+Descriptors support set-theoretic operations (union, intersection, negation) defined pointwise on each kind. We assume these operations are already implemented and focus on the extension to *recursive* types.
+
+## 2. Type Nodes
+
+**Definition 2.1 (Type node).** A *type node* is a triple
+
+```
+node = (id, state, f : state → descr)
+```
+
+where:
+
+- **id** is a unique identity (an Elixir `reference()`, see [Section 8](#8-node-identity-and-memoization));
+- **state** is a map `%{X => f_X, Y => f_Y, ...}` that records, for every recursion variable, its *generator function*; and
+- **f** is one such generator function, producing a `descr` when applied to a state.
+
+In Elixir syntax a node is simply a three-element tuple:
+
+```elixir
+{id, state, f}
+```
+
+**Definition 2.2 (stepping).** To *step* a node n_X = (id_X, state, f_X), we apply the generator to the state:
+
+```
+step(n_X) = f_X(state)
+```
+
+This yields a descriptor in which every occurrence of a recursion variable Y has been replaced by a fresh, self-contained node (id_Y, state, f_Y). stepping can therefore be iterated as many times as needed.
+
+## 3. The Role of Nodes and Descriptors
+
+It is important to distinguish two layers and the operations that belong to each.
+
+**Descriptors are types.** A `descr` is the canonical representation of a type. All set-theoretic operations—union, intersection, negation, difference—are defined on descriptors and return descriptors:
+
+```
+union : descr × descr → descr
+inter : descr × descr → descr
+etc.
+```
+
+**Nodes are used by type constructors.** Type constructors—`tuple`, `map`, `list`, etc.—build composite types and take *nodes* as their arguments. For instance:
+
+- `tuple([n_1, ..., n_k])` builds the tuple type {n_1, ..., n_k};
+- `list(n)` builds the list type whose elements have type n;
+- `map([{k_1, n_1}, ...])` builds a map type with the given key–value associations.
+
+By accepting nodes rather than descriptors, constructors can refer to types that have not yet been fully expanded—which is exactly what is needed for recursive definitions.
+
+**Descriptors pass as nodes.** Since a descriptor d can always be lifted to a node via `fresh_node(d) = (make_ref(), %{}, fn _ -> d end)`, descriptors can be used wherever a node is expected. In practice the implementation can accept both representations transparently.
+
+**Constructors ≠ set operations.** Constructors and set operations live at different levels:
+
+|                                              | **Inputs**        | **Output** |
+|----------------------------------------------|-------------------|------------|
+| Type constructors (`tuple`, `list`, ...)     | node, ..., node   | descr      |
+| Set operations (`union`, `inter`, ...)       | descr, descr      | descr      |
+
+Constructors consume nodes because they need to embed possibly-recursive sub-types into a descriptor. Set operations, on the other hand, combine already-formed descriptors pointwise by kind.
+
+## 4. Constructing Recursive Types
+
+The construction proceeds in four steps.
+
+### Step 1 — Read the equations and build generator functions
+
+For each recursive equation X = τ_X, we build a function f_X = `fn state -> d_X` where d_X is the body of the equation, translated into a descriptor, with every reference to a recursion variable Y replaced by the node expression `(make_ref(), state, state.Y)`.
+
+### Step 2 — Collect all generators
+
+This yields a family of generator functions f_X, f_Y, ..., one per equation.
+
+### Step 3 — Build the state
+
+Assemble the state map:
+
+```
+state = %{X => f_X, Y => f_Y, ...}
+```
+
+The state captures *all the ways to perform one stepping step* for each variable.
+
+### Step 4 — Build the type nodes
+
+Each recursive type is now represented as a node (with a fresh id):
+
+```
+n_X = (id_X, state, f_X)
+n_Y = (id_Y, state, f_Y)
+...
+```
+
+## 5. Example: Simple Recursive List
+
+Consider the recursive type "list of integers":
+
+```
+X = {int, X} | nil
+```
+
+**Generator.**
+
+```
+f_X = fn state ->
+  %{tuple => [:int, (make_ref(), state, state.X)],
+    atom  => [:nil]}
+end
+```
+
+**State.**
+
+```
+state = %{X => f_X}
+```
+
+**Node.**
+
+```
+n_X = (id_X, state, f_X)
+```
+
+In Elixir:
+
+```elixir
+fX = fn state ->
+  %{tuple: [:int, {make_ref(), state, state[:X]}],
+    atom: [:nil]}
+end
+
+state = %{X: fX}
+nX = {make_ref(), state, fX}
+```
+
+stepping once:
+
+```elixir
+step(nX)
+```
+
+returns the descriptor:
+
+```
+%{tuple => [:int, (id', state, f_X)],
+  atom  => [:nil]}
+```
+
+The inner `(id', state, f_X)` is itself a self-contained node that can be steped again at will.
+
+## 6. Example: Mutually Recursive Types
+
+```
+Y = {bool, X} | nil
+X = {int,  Y} | nil
+```
+
+**Step 1 — Generators.**
+
+```
+f_Y = fn state ->
+  %{tuple => [:bool, (make_ref(), state, state.X)],
+    atom  => [:nil]}
+end
+
+f_X = fn state ->
+  %{tuple => [:int, (make_ref(), state, state.Y)],
+    atom  => [:nil]}
+end
+```
+
+**Step 3 — State.**
+
+```
+state = %{Y => f_Y, X => f_X}
+```
+
+**Step 4 — Nodes.**
+
+```
+n_Y = (id_Y, state, f_Y)
+n_X = (id_X, state, f_X)
+```
+
+In Elixir:
+
+```elixir
+fY = fn st ->
+  %{tuple: [:bool, {make_ref(), st, st[:X]}],
+    atom: [:nil]}
+end
+
+fX = fn st ->
+  %{tuple: [:int, {make_ref(), st, st[:Y]}],
+    atom: [:nil]}
+end
+
+state = %{Y: fY, X: fX}
+
+nY = {make_ref(), state, fY}
+nX = {make_ref(), state, fX}
+```
+
+## 7. Using Nodes in Set Operations
+
+Set-theoretic operations on descriptors (union, intersection, ...) are extended to nodes by first stepping each operand to obtain a descriptor and then computing the operation on descriptors.
+
+### 7.1 Union of Two Nodes
+
+Given two nodes n_1 = (id_1, state_1, f_1) and n_2 = (id_2, state_2, f_2), the union is computed as follows:
+
+1. **step** both nodes: d_1 = f_1(state_1), d_2 = f_2(state_2).
+2. **Compute** the pointwise union of the two descriptors: d = union_descr(d_1, d_2).
+3. **Wrap** the result into a self-contained node using `fresh_node`: union_node(n_1, n_2) = fresh_node(union_descr(d_1, d_2)).
+
+> **Remark (Self-containedness).** Each node produced by stepping is *self-contained*: the triple (id, state, f_Y) already carries enough information to be steped further without any external context. An alternative design would thread the state through every set operation, but self-containedness simplifies the interface: a node is a black box that can be steped on demand.
+
+### 7.2 Conversion Functions
+
+Two functions convert between nodes and descriptors:
+
+```elixir
+# node → descr
+def step({_id, state, f}), do: f.(state)
+
+# descr → node
+def fresh_node(d) do
+  {make_ref(), %{}, fn _state -> d end}
+end
+```
+
+`step` takes a node and produces a descriptor by applying the generator to its state. `fresh_node` takes a descriptor and wraps it into a trivial node with a fresh id, an empty state, and a constant generator.
+
+### 7.3 Elixir Sketch
+
+```elixir
+def union_node(n1, n2) do
+  d1 = step(n1)
+  d2 = step(n2)
+  fresh_node(union_descr(d1, d2))
+end
+```
+
+## 8. Node Identity and Memoization
+
+So far a node is a pair (state, f). In practice we augment it with a unique *identity* tag, making a node a triple:
+
+```
+node = (id, state, f : state → descr)
+```
+
+In Elixir the identity is a fresh `reference()` obtained by calling `make_ref()`:
+
+```elixir
+def make_node(state, f) do
+  {make_ref(), state, f}
+end
+```
+
+References are unique values that support constant-time equality comparison. Two nodes created at different call sites will always have distinct identities, even if they happen to carry the same state and generator.
+
+**Why an identity?** The emptiness decision algorithm for set-theoretic types [1] works by exploring nodes and memoizing which ones have already been visited. Without an identity, the algorithm would need structural comparison of closures—which is impossible in general. With a reference-based identity, the algorithm can record visited nodes in a `MapSet` keyed by their id, guaranteeing termination of the recursive exploration in the presence of cyclic types.
+
+```elixir
+def empty?(node, seen \\ MapSet.new())
+def empty?({id, _state, _f} = node, seen) do
+  if MapSet.member?(seen, id) do
+    true
+  else
+    seen = MapSet.put(seen, id)
+    descr = step(node)
+    empty_descr?(descr, seen)
+  end
+end
+```
+
+The `seen` set acts as the memoization table: when a node is encountered a second time (detected via its id), the algorithm can conclude without re-exploring it—following the coinductive interpretation that a type variable encountered again is not empty (it contributes no new inhabitants but does not block either).
+
+**Updated conversion functions.** With the triple representation, the conversion functions become:
+
+```elixir
+# node → descr
+def step({_id, state, f}), do: f.(state)
+
+# descr → node
+def fresh_node(d) do
+  {make_ref(), %{}, fn _state -> d end}
+end
+```
+
+## 9. Summary
+
+| **Concept**              | **Elixir representation**         |
+|--------------------------|-----------------------------------|
+| Type descriptor (descr)  | `%{atom: ..., tuple: ..., ...}`   |
+| Generator function (f_X) | `fn state -> descr end`           |
+| State (state)            | `%{X: fX, Y: fY, ...}`           |
+| Type node (node)         | `{id, state, fX}`                 |
+| Node identity            | `make_ref()`                      |
+| stepping                | `fX.(state)`                      |
+
+The key insight is that every recursive type is encoded as a pair of (i) a shared state recording one stepping step per variable and (ii) the particular generator for the variable of interest. This representation is *coinductive*: we never build an infinite object; instead, we lazily produce one layer of the type on demand by calling `f(state)`.
+
+---
+
+## 10. Implementation Plan
+
+The following is an ordered list of implementation blocks. Within each block, all items must be implemented together (they are mutually dependent). Blocks themselves are listed in dependency order: a block can only be started once all blocks it depends on are complete.
+
+### Block A — Core node module *(no dependencies)*
+
+This block introduces the node data structure and the basic conversion functions. It touches no existing code.
+
+- **A.1** Define the node triple `{id, state, f}`.
+- **A.2** Implement `make_node(state, f)` which calls `make_ref()` to produce a fresh id.
+- **A.3** Implement step : node → descr, i.e. `step({_id, state, f}) = f.(state)`.
+- **A.4** Implement fresh_node : descr → node, i.e. `fresh_node(d) = {make_ref(), %{}, fn _ -> d end}`.
+- **A.5** Implement a coercion helper `to_node(x)` that returns `x` unchanged if it is already a node, or calls `fresh_node(x)` if it is a descr. This allows callers to pass either representation transparently.
+
+### Block B — Kind internals: descr → node *(depends on A)*
+
+This is the largest and most invasive block. Every type kind (`tuple_kind`, `list_kind`, `map_kind`, ...) currently stores nested *descrs* for its sub-types. These must all change to store *nodes* instead.
+
+- **B.1** Change the internal representation of each kind so that sub-type positions hold nodes rather than descrs. For example, `tuple_kind` for arity k stores k nodes instead of k descrs.
+- **B.2** Update every type constructor (`tuple/1`, `list/1`, `map/1`, ...) to accept nodes as arguments (using `to_node` for backward compatibility).
+- **B.3** Update all kind-level set operations (union, intersection, negation *per kind*) to handle nodes in sub-type positions. Where these operations need to combine sub-types, they must use the node-level operations from Block C (or operate structurally on nodes without stepping, depending on the algorithm).
+- **B.4** Update every pattern match and traversal of kind internals across the codebase to expect nodes where descrs were before.
+
+> **Remark.** Items B.1–B.4 are tightly coupled: changing the internal representation (B.1) immediately breaks all constructors (B.2), kind-level operations (B.3), and traversals (B.4). They must all be updated in a single atomic change.
+
+### Block C — Set operations on nodes *(depends on A)*
+
+These are thin wrappers: step both operands, apply the descr-level operation, wrap the result.
+
+- **C.1** Implement `union_node(n1, n2)`.
+- **C.2** Implement `inter_node(n1, n2)`.
+- **C.3** Implement `negate_node(n)`.
+- **C.4** Implement `diff_node(n1, n2)`.
+
+Block C can be implemented in parallel with Block B (both depend only on A), but Block B.3 may call into Block C functions.
+
+### Block D — Recursive type builder *(depends on A + B)*
+
+The four-step construction algorithm from [Section 4](#4-constructing-recursive-types).
+
+- **D.1** Read recursive type equations and produce generator functions f_X = `fn state -> d_X`.
+- **D.2** Collect all generators into the state map state = `%{X => f_X, ...}`.
+
+  %{X => f_X}
+  f_X = fn state -> tuple([integer(), {state, state.X}]) |> union(atom(:nil)) end
+
+- **D.3** Build each type node via `make_node(state, fX)`.
+- **D.4** Integrate with the module/function that translates user-facing type syntax into the internal representation.
+
+### Block E — Emptiness with memoization *(depends on A + B)*
+
+- **E.1** Update `empty?/1` to accept nodes (not just descrs).
+- **E.2** Add a `seen` parameter (`MapSet` of node ids) threaded through the recursion.
+- **E.3** When a node id is already in `seen`, return `true` (coinductive base case).
+- **E.4** Update `empty_descr?` so that when it recurses into kind sub-types (which are now nodes), it calls the node-level `empty?` with the `seen` set.
+
+### Block F — Remaining recursive algorithms *(depends on A + B + E)*
+
+Every algorithm that recurses into the sub-types of a descriptor must be updated in the same spirit as emptiness.
+
+- **F.1** Subtyping: thread a memoization set; handle nodes in sub-type positions.
+- **F.2** Pretty-printing / `to_string`: step nodes on demand and track visited ids to avoid infinite output.
+- **F.3** Any other traversal (e.g. type normalization, materialization) that inspects kind internals.
+
+### Dependency Graph
+
+```
+         ┌─────────────┐
+         │ A: Core nodes│
+         └──────┬──────┘
+           ┌────┴────┐
+           ▼         ▼
+  ┌──────────────┐ ┌─────────────────┐
+  │B: Kind       │ │C: Set ops on    │
+  │   internals  │◄┤   nodes         │
+  └──┬───┬───┬──┘ │ (B.3 may call C)│
+     │   │   │    └─────────────────┘
+     ▼   │   ▼
+┌────────┐│┌──────────┐
+│D: Rec. │││E:        │
+│ builder│││ Emptiness│
+└────────┘│└────┬─────┘
+          │     │
+          ▼     ▼
+      ┌────────────┐
+      │F: Other    │
+      │  algorithms│
+      └────────────┘
+```
+
+---
+
+### References
+
+[1] Mickaël Laurent and Kim Nguyen. *Implementing Set-Theoretic Types.* Proceedings of the ACM on Programming Languages, 8(POPL), 2024.
\ No newline at end of file

From 1cdf86d34ef4011e21ccc7e1e8db004d1e8cba02 Mon Sep 17 00:00:00 2001
From: Graham Preston <graham.preston@gmail.com>
Date: Thu, 26 Feb 2026 22:27:13 +0100
Subject: [PATCH 3/6] Graham: Add some notes from investigating Block B work

---
 lib/elixir/block_b_notes.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 lib/elixir/block_b_notes.md

diff --git a/lib/elixir/block_b_notes.md b/lib/elixir/block_b_notes.md
new file mode 100644
index 00000000000..6808b7232a7
--- /dev/null
+++ b/lib/elixir/block_b_notes.md
@@ -0,0 +1,14 @@
+## Notes for Block B - Graham 26/02/2026
+
+- B.1 - Update internal representations to hold nodes rather than descrs: I'm actually not sure if anything has to be done here. In an object-oriented language, we would be changing field types, however here where we simply process structures as given, it should only matter whether the functions doing such processing can handle such field shapes. This describes exactly the next task.
+- B.2 - Update type constructors to accept nodes as arguments: This was already done as part of Block A. For example, in tuple_descr/3, the first line is `value_descr = to_descr(value)`, to handle the case where `value` is a node, rather than a descr as it previously would have been.
+- B.3 - Update kind-level set operations to handle nodes in sub-type positions:
+    * **Question:** Looking at the implemention of `union` for example, we see `union/3` which calls code such as `tuple_union/2`. I don't think I understand how, for example, a union between a tuple and an atom is created.
+    * Maybe answer: the key isn't necessarily saying "this is a union between two maps" for example; it is rather saying "the first things is a map, give me the union between that and whatever the second value is on the BDD level"
+    * Hint for myself to properly interpret code: a descr is a collection of disjoint BDDs. So each value of a key in a descr is a BDD in itself.
+
+- Overall, it appears what needs to be ensured **is that BDDs can contain nodes, and not just descrs**.
+    * Doing a quick skim of the set operations, it doesn't seem like any of them explicitly assume sub-components of a BDD to be a descr rather than a node. They end up returning sub-components directly, or re-passing sub-components to other BDD operations with the same characteristics. I believe that overall this is a good sign.
+    * I think the easiest way to see what actually has to be changed is to create some test cases. Or at least, create some literal creation/literal operation cases that can be run in the REPL to demonstrate whatever the behavior at the time (during incremental code changes) is.
+    * With all that being said, it feels like right now, normal operations *should* more or less work with stateless (non-recursive) nodes. And if they don't, it's jsut a matter of tracking down trivial signature changes. I'm really not sure Block B has that much work as long as functions are dynamic. It seems to me like the next real work is Block C where nodes will have to be unrolled one level before having the Block B set operations applied to them.
+    * I might hypothesize that the LLM is imagining the evaluation of set operations in a recursive expression manner because that's what it looks like for a programming language implementation for example, but for better or worse, within this set-theoretic types framework we somehow end up doing fewer "unwrap"-recursive calls than expected. That, or I'm just totally missing them.

From 3d012898217c537f19e22dea03dd85fef9c10e39 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 23 Mar 2026 07:13:19 +0100
Subject: [PATCH 4/6] Implement Block D: recursive type builder with tuple node
 passthrough

Add recursive/1 to build self-contained type nodes from mutually
recursive equations. Fix tuple_descr to store node elements without
eagerly stepping them, preventing infinite recursion in generators.
---
 lib/elixir/lib/module/types/descr.ex          |  65 +++-
 .../test/elixir/module/types/descr_test.exs   | 354 ++++++++++++++++++
 2 files changed, 416 insertions(+), 3 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index ffda89dc5a4..8bf5b52732b 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -126,6 +126,50 @@ defmodule Module.Types.Descr do
   def to_descr(descr = %{}), do: descr
   def to_descr({_id, state, generator}), do: generator.(state)
 
+  @doc """
+  Builds recursive type nodes from a set of mutually recursive equations.
+
+  Takes a map `%{name => generator}` where each generator is a function
+  `fn state -> descr` that may refer to recursion variables by building
+  nodes from the state: `{make_ref(), state, state[name]}`.
+
+  Returns a map `%{name => node}` with one self-contained node per variable.
+
+  ## Example
+
+  The recursive type `X = {integer(), X} | nil` is defined as:
+
+      %{X: node_x} = recursive(%{
+        X: fn state ->
+          tuple([integer(), {make_ref(), state, state[:X]}])
+          |> union(atom([:nil]))
+        end
+      })
+
+  For mutually recursive types `X = {int, Y} | nil` and `Y = {bool, X} | nil`:
+
+      %{X: node_x, Y: node_y} = recursive(%{
+        X: fn state ->
+          tuple([integer(), {make_ref(), state, state[:Y]}])
+          |> union(atom([:nil]))
+        end,
+        Y: fn state ->
+          tuple([boolean(), {make_ref(), state, state[:X]}])
+          |> union(atom([:nil]))
+        end
+      })
+  """
+  def recursive(equations) when is_map(equations) do
+    # The generators ARE the state — each variable maps to its generator function.
+    # This is the state map from Section 4, Step 3.
+    state = equations
+
+    # Step 4: build one node per variable with the shared state.
+    Map.new(equations, fn {name, generator} ->
+      {name, make_node(state, generator)}
+    end)
+  end
+
   @doc """
   Gets the upper bound of a gradual type.
 
@@ -413,7 +457,7 @@ defmodule Module.Types.Descr do
   def union(none, other) when none == @none, do: other
   def union(other, none) when none == @none, do: other
 
-  def union(left, right) do
+  def union(%{} = left, %{} = right) do
     is_gradual_left = gradual?(left)
     is_gradual_right = gradual?(right)
 
@@ -431,6 +475,8 @@ defmodule Module.Types.Descr do
     end
   end
 
+  def union(left, right), do: union(to_descr(left), to_descr(right))
+
   @compile {:inline, union_static: 2}
   defp union_static(left, right) do
     symmetrical_merge(left, right, &union/3)
@@ -453,7 +499,7 @@ defmodule Module.Types.Descr do
   def intersection(%{dynamic: :term}, other), do: dynamic(remove_optional(other))
   def intersection(other, %{dynamic: :term}), do: dynamic(remove_optional(other))
 
-  def intersection(left, right) do
+  def intersection(%{} = left, %{} = right) do
     is_gradual_left = gradual?(left)
     is_gradual_right = gradual?(right)
 
@@ -471,6 +517,8 @@ defmodule Module.Types.Descr do
     end
   end
 
+  def intersection(left, right), do: intersection(to_descr(left), to_descr(right))
+
   @compile {:inline, intersection_static: 2}
   defp intersection_static(left, right) do
     symmetrical_intersection(left, right, &intersection/3)
@@ -496,7 +544,9 @@ defmodule Module.Types.Descr do
   def difference(left, :term), do: keep_optional(left)
   def difference(left, none) when none == @none, do: left
 
-  def difference(left, right) do
+  def difference(left, %{} = right) do
+    left = to_descr(left)
+
     if gradual?(left) or gradual?(right) do
       {left_dynamic, left_static} = pop_dynamic(left)
       {right_dynamic, right_static} = pop_dynamic(right)
@@ -508,6 +558,8 @@ defmodule Module.Types.Descr do
     end
   end
 
+  def difference(left, right), do: difference(to_descr(left), to_descr(right))
+
   # For static types, the difference is component-wise
   defp difference_static(left, descr) when descr == %{}, do: left
   defp difference_static(left, :term), do: keep_optional(left)
@@ -579,6 +631,7 @@ defmodule Module.Types.Descr do
   """
   def negation(:term), do: none()
   def negation(%{} = descr), do: difference(term(), descr)
+  def negation(node), do: negation(to_descr(node))
 
   @doc """
   Check if a type is empty.
@@ -4331,6 +4384,12 @@ defmodule Module.Types.Descr do
     tuple_descr(rest, [:term | acc], dynamic?)
   end
 
+  # Nodes (3-tuples with a reference id) are stored as-is without stepping.
+  # This avoids infinite recursion for recursive type nodes.
+  defp tuple_descr([{id, _state, _gen} = node | rest], acc, dynamic?) when is_reference(id) do
+    tuple_descr(rest, [node | acc], dynamic?)
+  end
+
   defp tuple_descr([value | rest], acc, dynamic?) do
     value_descr = to_descr(value)
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 6e3099f94db..158f032005f 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -3265,4 +3265,358 @@ defmodule Module.Types.DescrTest do
       assert subtype?(range, Enum.reduce(entries, &union/2))
     end
   end
+
+  ## Block A — Node infrastructure
+
+  describe "make_node (A.1 / A.2)" do
+    test "returns a triple {id, state, generator}" do
+      state = %{x: 1}
+      gen = fn s -> s end
+      node = make_node(state, gen)
+
+      assert {id, ^state, ^gen} = node
+      assert is_reference(id)
+    end
+
+    test "each call produces a fresh id" do
+      gen = fn _ -> :ok end
+      {id1, _, _} = make_node(%{}, gen)
+      {id2, _, _} = make_node(%{}, gen)
+      assert id1 != id2
+    end
+  end
+
+  describe "to_descr / step (A.3)" do
+    test "stepping a node applies the generator to the state" do
+      descr = integer()
+      node = make_node(%{}, fn _state -> descr end)
+      assert to_descr(node) == descr
+    end
+
+    test "stepping a node with non-trivial state" do
+      node = make_node(%{val: float()}, fn state -> state.val end)
+      assert to_descr(node) == float()
+    end
+
+    test "to_descr is identity on :term" do
+      assert to_descr(:term) == :term
+    end
+
+    test "to_descr is identity on a descr map" do
+      d = union(integer(), atom())
+      assert to_descr(d) == d
+    end
+  end
+
+  describe "to_node / fresh_node (A.4 / A.5)" do
+    test "wrapping a descr map produces a node whose step returns the original" do
+      d = integer()
+      node = to_node(d)
+      assert {id, %{}, _gen} = node
+      assert is_reference(id)
+      assert to_descr(node) == d
+    end
+
+    test "wrapping :term produces a node whose step returns :term" do
+      node = to_node(:term)
+      assert {id, :term, _gen} = node
+      assert is_reference(id)
+      assert to_descr(node) == :term
+    end
+
+    test "to_node on an existing node returns it unchanged" do
+      node = make_node(%{}, fn _ -> integer() end)
+      assert to_node(node) === node
+    end
+
+    test "wrapping and stepping round-trips for complex descrs" do
+      d = union(tuple([integer(), atom()]), list(float()))
+      assert to_descr(to_node(d)) == d
+    end
+  end
+
+  ## Block B — Kind internals accept nodes
+
+  describe "tuple constructor accepts nodes (B.1 / B.2)" do
+    test "tuple/1 accepts nodes and produces a non-empty tuple descr" do
+      n1 = to_node(integer())
+      n2 = to_node(atom())
+
+      result = tuple([n1, n2])
+      assert is_map_key(result, :tuple)
+      assert map_size(result) > 0
+    end
+
+    test "tuple/1 accepts a mix of nodes and descrs" do
+      n = to_node(integer())
+      result = tuple([n, float()])
+      assert is_map_key(result, :tuple)
+      assert map_size(result) > 0
+    end
+  end
+
+  describe "list constructor accepts nodes (B.1 / B.2)" do
+    test "list/1 accepts a node element type" do
+      n = to_node(integer())
+      from_node = list(n)
+      from_descr = list(integer())
+      assert equal?(from_node, from_descr)
+    end
+
+    test "non_empty_list/2 accepts nodes for both element and tail" do
+      elem_node = to_node(integer())
+      tail_node = to_node(empty_list())
+
+      from_nodes = non_empty_list(elem_node, tail_node)
+      from_descrs = non_empty_list(integer(), empty_list())
+      assert equal?(from_nodes, from_descrs)
+    end
+  end
+
+  describe "map constructor accepts nodes (B.1 / B.2)" do
+    test "closed_map accepts node values" do
+      n = to_node(integer())
+      result = closed_map(a: n)
+      assert is_map_key(result, :map)
+      assert map_size(result) > 0
+    end
+
+    test "open_map accepts node values" do
+      n = to_node(atom())
+      result = open_map(b: n)
+      assert is_map_key(result, :map)
+      assert map_size(result) > 0
+    end
+
+    test "map stores nodes in value positions" do
+      n = to_node(float())
+      %{map: bdd} = closed_map(x: n)
+      # Extract the leaf fields from the BDD
+      {_tag, fields} = bdd
+      node_val = Map.get(fields, :x)
+      assert {id, _state, _gen} = node_val
+      assert is_reference(id)
+      assert to_descr(node_val) == float()
+    end
+
+    test "map with mixed node and descr values" do
+      n = to_node(float())
+      result = closed_map(x: n, y: integer())
+      assert is_map_key(result, :map)
+      assert map_size(result) > 0
+    end
+  end
+
+  ## Block C — Set operations accept nodes polymorphically
+
+  describe "union on nodes (C.1)" do
+    test "union of two nodes returns the union descr" do
+      n1 = to_node(integer())
+      n2 = to_node(float())
+      assert equal?(union(n1, n2), union(integer(), float()))
+    end
+
+    test "union of a node and a descr" do
+      n = to_node(integer())
+      assert equal?(union(n, float()), union(integer(), float()))
+      assert equal?(union(atom(), n), union(atom(), integer()))
+    end
+
+    test "union with none() node is identity" do
+      n = to_node(atom())
+      n_none = to_node(none())
+      assert equal?(union(n, n_none), atom())
+    end
+
+    test "union with term() node is term" do
+      n = to_node(integer())
+      n_term = to_node(:term)
+      assert union(n, n_term) == :term
+    end
+  end
+
+  describe "intersection on nodes (C.2)" do
+    test "intersection of two nodes returns the intersection descr" do
+      n1 = to_node(union(integer(), atom()))
+      n2 = to_node(integer())
+      assert equal?(intersection(n1, n2), integer())
+    end
+
+    test "intersection of a node and a descr" do
+      n = to_node(union(integer(), atom()))
+      assert equal?(intersection(n, integer()), integer())
+      assert equal?(intersection(atom(), n), atom())
+    end
+
+    test "intersection of disjoint nodes is none" do
+      n1 = to_node(integer())
+      n2 = to_node(atom())
+      assert equal?(intersection(n1, n2), none())
+    end
+
+    test "intersection with term() node is identity" do
+      n = to_node(float())
+      n_term = to_node(:term)
+      assert equal?(intersection(n, n_term), float())
+    end
+  end
+
+  describe "negation on nodes (C.3)" do
+    test "negation of a node returns the negation descr" do
+      n = to_node(integer())
+      assert equal?(negation(n), negation(integer()))
+    end
+
+    test "double negation round-trips" do
+      n = to_node(atom())
+      assert equal?(negation(negation(n)), atom())
+    end
+  end
+
+  describe "difference on nodes (C.4)" do
+    test "difference of two nodes returns the difference descr" do
+      n1 = to_node(union(integer(), atom()))
+      n2 = to_node(atom())
+      assert equal?(difference(n1, n2), integer())
+    end
+
+    test "difference of a node and a descr" do
+      n = to_node(union(integer(), float()))
+      assert equal?(difference(n, float()), integer())
+      assert equal?(difference(union(integer(), float()), to_node(float())), integer())
+    end
+
+    test "difference from itself is none" do
+      n = to_node(float())
+      assert equal?(difference(n, n), none())
+    end
+
+    test "difference from none() is identity" do
+      n = to_node(integer())
+      n_none = to_node(none())
+      assert equal?(difference(n, n_none), integer())
+    end
+  end
+
+  ## Block D — Recursive type builder
+
+  describe "recursive/1 (D.1 / D.2 / D.3)" do
+    test "simple recursive list: X = {integer(), X} | nil" do
+      %{X: node_x} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), {make_ref(), state, state[:X]}])
+            |> union(atom([:nil]))
+          end
+        })
+
+      # node_x is a proper node triple
+      assert {id, state, gen} = node_x
+      assert is_reference(id)
+      assert is_map_key(state, :X)
+      assert is_function(gen, 1)
+
+      # stepping once produces a descr with :tuple and :atom keys
+      d = to_descr(node_x)
+      assert is_map_key(d, :tuple)
+      assert is_map_key(d, :atom)
+    end
+
+    test "stepping a recursive node yields a descr containing a nested node" do
+      %{X: node_x} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), {make_ref(), state, state[:X]}])
+            |> union(atom([:nil]))
+          end
+        })
+
+      # Step once to get the descriptor
+      d1 = to_descr(node_x)
+
+      # The tuple kind should exist and the descriptor should be non-empty
+      assert is_map(d1)
+      refute d1 == %{}
+    end
+
+    test "mutually recursive types: X = {int, Y} | nil, Y = {bool, X} | nil" do
+      %{X: node_x, Y: node_y} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), {make_ref(), state, state[:Y]}])
+            |> union(atom([:nil]))
+          end,
+          Y: fn state ->
+            tuple([boolean(), {make_ref(), state, state[:X]}])
+            |> union(atom([:nil]))
+          end
+        })
+
+      # Both are valid node triples sharing the same state
+      assert {id_x, state_x, _} = node_x
+      assert {id_y, state_y, _} = node_y
+      assert is_reference(id_x)
+      assert is_reference(id_y)
+      assert id_x != id_y
+
+      # They share the same state
+      assert state_x === state_y
+
+      # Both variables are present in the shared state
+      assert is_map_key(state_x, :X)
+      assert is_map_key(state_x, :Y)
+    end
+
+    test "stepping mutually recursive nodes produces valid descriptors" do
+      %{X: node_x, Y: node_y} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), {make_ref(), state, state[:Y]}])
+            |> union(atom([:nil]))
+          end,
+          Y: fn state ->
+            tuple([boolean(), {make_ref(), state, state[:X]}])
+            |> union(atom([:nil]))
+          end
+        })
+
+      dx = to_descr(node_x)
+      dy = to_descr(node_y)
+
+      # Both produce non-empty descriptors with tuple and atom parts
+      assert is_map_key(dx, :tuple)
+      assert is_map_key(dx, :atom)
+      assert is_map_key(dy, :tuple)
+      assert is_map_key(dy, :atom)
+    end
+
+    test "iterated stepping of a recursive node" do
+      %{X: node_x} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), {make_ref(), state, state[:X]}])
+            |> union(atom([:nil]))
+          end
+        })
+
+      # Step multiple times without crashing (coinductive stepping is lazy)
+      d1 = to_descr(node_x)
+      assert is_map(d1)
+
+      # The node can be stepped again (it regenerates a fresh node inside)
+      d2 = to_descr(node_x)
+      assert is_map(d2)
+    end
+
+    test "single non-recursive equation degenerates to a plain node" do
+      %{X: node_x} =
+        recursive(%{
+          X: fn _state -> integer() end
+        })
+
+      assert {id, _state, _gen} = node_x
+      assert is_reference(id)
+      assert equal?(to_descr(node_x), integer())
+    end
+  end
 end

From 7fe9589c8045167d1e825965ada9f5c4ee12c024 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 26 Mar 2026 13:26:33 +0100
Subject: [PATCH 5/6] Continue recursive types work

---
 lib/elixir/lib/module/types/descr.ex          |  758 ++++++--
 .../test/elixir/module/types/descr_test.exs   | 1562 +++++++++++++++--
 2 files changed, 1995 insertions(+), 325 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 8bf5b52732b..355132785e5 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -83,6 +83,7 @@ defmodule Module.Types.Descr do
 
   @compile {:inline, unfold: 1}
   defp unfold(:term), do: unfolded_term()
+  defp unfold({_id, state, generator}), do: generator.(state) |> unfold()
   defp unfold(other), do: other
   defp unfolded_term, do: @term
 
@@ -126,6 +127,103 @@ defmodule Module.Types.Descr do
   def to_descr(descr = %{}), do: descr
   def to_descr({_id, state, generator}), do: generator.(state)
 
+  # Collect generator functions embedded in a type (node, descr, or :term).
+  # Walks BDD leaves without unfolding any nodes. Returns a list of generators.
+  defp collect_generators({ref, _state, gen}) when is_reference(ref), do: [gen]
+  defp collect_generators(:term), do: []
+
+  defp collect_generators(%{} = descr) do
+    # Use direct key lookups instead of Enum.flat_map to avoid dispatching
+    # the Enumerable protocol on maps with __struct__ (e.g. struct types).
+    tuple_gens =
+      case descr do
+        %{tuple: bdd} -> collect_generators_from_bdd(bdd, &collect_generators_tuple_leaf/1)
+        _ -> []
+      end
+
+    list_gens =
+      case descr do
+        %{list: bdd} -> collect_generators_from_bdd(bdd, &collect_generators_list_leaf/1)
+        _ -> []
+      end
+
+    map_gens =
+      case descr do
+        %{map: bdd} -> collect_generators_from_bdd(bdd, &collect_generators_map_leaf/1)
+        _ -> []
+      end
+
+    tuple_gens ++ list_gens ++ map_gens
+  end
+
+  defp collect_generators(_), do: []
+
+  defp collect_generators_from_bdd(:bdd_top, _leaf_fn), do: []
+  defp collect_generators_from_bdd(:bdd_bot, _leaf_fn), do: []
+  defp collect_generators_from_bdd({_, _} = leaf, leaf_fn), do: leaf_fn.(leaf)
+
+  defp collect_generators_from_bdd({_lit, c, u, d}, leaf_fn) do
+    collect_generators_from_bdd(c, leaf_fn) ++
+      collect_generators_from_bdd(u, leaf_fn) ++
+      collect_generators_from_bdd(d, leaf_fn)
+  end
+
+  # Tuple leaf: {tag, [element, ...]}
+  defp collect_generators_tuple_leaf({_tag, elements}) do
+    Enum.flat_map(elements, &collect_generators/1)
+  end
+
+  # List leaf: {list_type, last_type}
+  defp collect_generators_list_leaf({list_type, last_type}) do
+    collect_generators(list_type) ++ collect_generators(last_type)
+  end
+
+  # Map leaf: {tag, %{key => value, ...}} or {%{domains}, %{fields}}
+  defp collect_generators_map_leaf({_tag, fields}) when is_map(fields) do
+    :maps.fold(fn _k, v, acc -> collect_generators(v) ++ acc end, [], fields)
+  end
+
+  defp collect_generators_map_leaf(_), do: []
+
+  defp empty_memo_key(descr), do: {:empty_seen, empty_memo_normalize(descr)}
+
+  # Normalize recursive obligations to stable unary memo keys by erasing
+  # fresh node references and retaining generator identity only.
+  defp empty_memo_normalize({ref, _state, generator}) when is_reference(ref) do
+    {:node, generator}
+  end
+
+  # Compiler-internal struct-like maps such as %{__struct__: :term} should not
+  # be traversed as regular maps for this prototype key.
+  defp empty_memo_normalize(%{__struct__: struct}) when is_atom(struct) do
+    {:struct, struct}
+  end
+
+  defp empty_memo_normalize(%{} = map) do
+    map
+    |> :maps.to_list()
+    |> then(fn entries ->
+      :lists.map(
+        fn {key, value} -> {empty_memo_normalize(key), empty_memo_normalize(value)} end,
+        entries
+      )
+    end)
+    |> :lists.sort()
+  end
+
+  defp empty_memo_normalize(list) when is_list(list) do
+    :lists.map(&empty_memo_normalize/1, list)
+  end
+
+  defp empty_memo_normalize(tuple) when is_tuple(tuple) do
+    tuple
+    |> Tuple.to_list()
+    |> then(fn elements -> :lists.map(&empty_memo_normalize/1, elements) end)
+    |> List.to_tuple()
+  end
+
+  defp empty_memo_normalize(other), do: other
+
   @doc """
   Builds recursive type nodes from a set of mutually recursive equations.
 
@@ -135,6 +233,26 @@ defmodule Module.Types.Descr do
 
   Returns a map `%{name => node}` with one self-contained node per variable.
 
+  ## Important constraint
+
+  Inside a generator, recursion variables (nodes built from the state) may
+  only appear as arguments to **type constructors** (`tuple/1`, `list/1`,
+  `non_empty_list/2`, `closed_map/1`, `open_map/1`, etc.).
+
+  They must **never** be passed to **set-theoretic operations** (`union/2`,
+  `intersection/2`, `difference/2`, `negation/1`) inside the generator.
+  These operations eagerly unfold their arguments via `to_descr/1`, which
+  triggers the generator again, causing infinite recursion.
+
+  Correct: node inside a constructor, set operations on the result:
+
+      tuple([integer(), {make_ref(), state, state[:X]}])
+      |> union(atom([:nil]))
+
+  Wrong: node passed directly to a set operation:
+
+      union({make_ref(), state, state[:X]}, atom([:nil]))
+
   ## Example
 
   The recursive type `X = {integer(), X} | nil` is defined as:
@@ -160,7 +278,7 @@ defmodule Module.Types.Descr do
       })
   """
   def recursive(equations) when is_map(equations) do
-    # The generators ARE the state — each variable maps to its generator function.
+    # The generators ARE the state: each variable maps to its generator function.
     # This is the state map from Section 4, Step 3.
     state = equations
 
@@ -420,6 +538,7 @@ defmodule Module.Types.Descr do
   Returns true if the type has a gradual part.
   """
   def gradual?(:term), do: false
+  def gradual?({_id, state, generator}), do: gradual?(generator.(state))
   def gradual?(descr), do: is_map_key(descr, :dynamic)
 
   @doc """
@@ -589,37 +708,15 @@ defmodule Module.Types.Descr do
 
   defp iterator_difference_static(:none, map), do: map
 
-  # This function is designed to compute the difference during subtyping efficiently.
-  # Do not use it for anything else.
-  defp empty_difference_subtype?(%{dynamic: dyn_left} = left, %{dynamic: dyn_right} = right) do
-    # Dynamic will either exist on both sides or on none
-    empty_difference_subtype?(dyn_left, dyn_right) and
-      empty_difference_subtype?(Map.delete(left, :dynamic), Map.delete(right, :dynamic))
-  end
-
-  defp empty_difference_subtype?(left, :term), do: keep_optional(left) == @none
-
-  defp empty_difference_subtype?(left, right) do
-    iterator_empty_difference_subtype?(:maps.next(:maps.iterator(unfold(left))), unfold(right))
-  end
-
-  defp iterator_empty_difference_subtype?({key, v1, iterator}, map) do
-    case map do
-      %{^key => v2} ->
-        value = difference(key, v1, v2)
-        value in @empty_difference or empty_key?(key, value)
-
-      %{} ->
-        empty_key?(key, v1)
-    end and
-      iterator_empty_difference_subtype?(:maps.next(iterator), map)
-  end
-
-  defp iterator_empty_difference_subtype?(:none, _map), do: true
-
   # Returning 0 from the callback is taken as none() for that subtype.
   defp difference(:atom, v1, v2), do: atom_difference(v1, v2)
   defp difference(:bitmap, v1, v2), do: v1 - (v1 &&& v2)
+
+  defp difference(:dynamic, v1, v2) do
+    descr = difference_static(v1, v2)
+    if descr == @none, do: 0, else: descr
+  end
+
   defp difference(:list, v1, v2), do: list_difference(v1, v2)
   defp difference(:map, v1, v2), do: map_difference(v1, v2)
   defp difference(:optional, 1, 1), do: 0
@@ -642,23 +739,52 @@ defmodule Module.Types.Descr do
   the type is non-empty as we normalize then during construction.
   """
   def empty?(:term), do: false
+  def empty?(%{} = descr), do: empty_seen?(descr, %{})
+  def empty?({_id, _state, _gen} = node), do: empty_seen?(node, %{})
 
-  def empty?(%{} = descr) do
-    case :maps.get(:dynamic, descr, descr) do
-      :term ->
-        false
+  # This is Algorithm 1 (non-optimized version) from
+  # "Implement Set-Theoretic Types" (https://hal.science/hal-05369012v1/document).
+  # TODO: implement Algorithm 2 (optimized).
+  #
+  # Internal emptiness check with coinductive memoization.
+  # The `seen` map stores both raw node generators and normalized unary
+  # emptiness obligations so recursive calls can terminate structurally.
+  defp empty_seen?(:term, _seen), do: false
 
-      value when value == @none ->
-        true
+  defp empty_seen?(%{} = descr, seen) do
+    key = empty_memo_key(descr)
+
+    if :erlang.is_map_key(key, seen) do
+      true
+    else
+      seen = Map.put(seen, key, true)
+
+      case :maps.get(:dynamic, descr, descr) do
+        :term ->
+          false
+
+        value when value == @none ->
+          true
+
+        descr ->
+          not Map.has_key?(descr, :atom) and
+            not Map.has_key?(descr, :bitmap) and
+            not Map.has_key?(descr, :optional) and
+            (not Map.has_key?(descr, :tuple) or tuple_empty?(descr.tuple, seen)) and
+            (not Map.has_key?(descr, :map) or map_empty?(descr.map, seen)) and
+            (not Map.has_key?(descr, :list) or list_empty?(descr.list, seen)) and
+            (not Map.has_key?(descr, :fun) or fun_empty?(descr.fun, seen))
+      end
+    end
+  end
 
-      descr ->
-        not Map.has_key?(descr, :atom) and
-          not Map.has_key?(descr, :bitmap) and
-          not Map.has_key?(descr, :optional) and
-          (not Map.has_key?(descr, :tuple) or tuple_empty?(descr.tuple)) and
-          (not Map.has_key?(descr, :map) or map_empty?(descr.map)) and
-          (not Map.has_key?(descr, :list) or list_empty?(descr.list)) and
-          (not Map.has_key?(descr, :fun) or fun_empty?(descr.fun))
+  # Node: check for cycle via generator identity, then unfold
+  defp empty_seen?({_id, state, generator}, seen) do
+    if :erlang.is_map_key(generator, seen) do
+      true
+    else
+      seen = Map.put(seen, generator, true)
+      empty_seen?(generator.(state), seen)
     end
   end
 
@@ -666,11 +792,11 @@ defmodule Module.Types.Descr do
 
   # For atom, bitmap, tuple, and optional, if the key is present,
   # then they are not empty,
-  defp empty_key?(:fun, value), do: fun_empty?(value)
-  defp empty_key?(:map, value), do: map_empty?(value)
-  defp empty_key?(:list, value), do: list_empty?(value)
-  defp empty_key?(:tuple, value), do: tuple_empty?(value)
-  defp empty_key?(_, _value), do: false
+  defp empty_key?(:fun, value, seen), do: fun_empty?(value, seen)
+  defp empty_key?(:map, value, seen), do: map_empty?(value, seen)
+  defp empty_key?(:list, value, seen), do: list_empty?(value, seen)
+  defp empty_key?(:tuple, value, seen), do: tuple_empty?(value, seen)
+  defp empty_key?(_, _value, _seen), do: false
 
   @doc """
   Converts all floats or integers into numbers.
@@ -886,6 +1012,11 @@ defmodule Module.Types.Descr do
         right_static = Map.delete(right, :dynamic)
         subtype_static?(left, right_static)
 
+      is_grad_left ->
+        # Both gradual: check dynamic and static parts separately
+        subtype_static?(Map.get(left, :dynamic), Map.get(right, :dynamic)) and
+          subtype_static?(Map.delete(left, :dynamic), Map.delete(right, :dynamic))
+
       true ->
         subtype_static?(left, right)
     end
@@ -894,6 +1025,93 @@ defmodule Module.Types.Descr do
   defp subtype_static?(same, same), do: true
   defp subtype_static?(left, right), do: empty_difference_subtype?(left, right)
 
+  # Fused difference + emptiness check that short-circuits per-key.
+  # This is Algorithm 1 from Laurent & Nguyen, fused with subtyping.
+  defp empty_difference_subtype?(%{dynamic: dyn_left} = left, %{dynamic: dyn_right} = right) do
+    empty_difference_subtype?(dyn_left, dyn_right) and
+      empty_difference_subtype?(Map.delete(left, :dynamic), Map.delete(right, :dynamic))
+  end
+
+  defp empty_difference_subtype?(left, :term), do: keep_optional(left) == @none
+
+  defp empty_difference_subtype?(left, right) do
+    iterator_empty_difference_subtype?(
+      :maps.next(:maps.iterator(unfold(left))),
+      unfold(right),
+      %{}
+    )
+  end
+
+  defp iterator_empty_difference_subtype?({key, v1, iterator}, map, seen) do
+    case map do
+      %{^key => v2} ->
+        value = difference(key, v1, v2)
+        value in @empty_difference or empty_key?(key, value, seen)
+
+      %{} ->
+        empty_key?(key, v1, seen)
+    end and
+      iterator_empty_difference_subtype?(:maps.next(iterator), map, seen)
+  end
+
+  defp iterator_empty_difference_subtype?(:none, _map, _seen), do: true
+
+  # Recursive subtype check that reuses the unary emptiness memo by reducing
+  # subtyping to emptiness of the set difference under the current `seen` map.
+  defp subtype_seen?(left, right, seen) do
+    do_subtype_seen?(unfold(left), unfold(right), seen)
+  end
+
+  defp do_subtype_seen?(left, right, seen) do
+    is_grad_left = gradual?(left)
+    is_grad_right = gradual?(right)
+
+    cond do
+      is_grad_left and not is_grad_right ->
+        left_dynamic = Map.get(left, :dynamic)
+        subtype_static_seen?(left_dynamic, right, seen)
+
+      is_grad_right and not is_grad_left ->
+        right_static = Map.delete(right, :dynamic)
+        subtype_static_seen?(left, right_static, seen)
+
+      is_grad_left ->
+        subtype_static_seen?(Map.get(left, :dynamic), Map.get(right, :dynamic), seen) and
+          subtype_static_seen?(Map.delete(left, :dynamic), Map.delete(right, :dynamic), seen)
+
+      true ->
+        subtype_static_seen?(left, right, seen)
+    end
+  end
+
+  defp subtype_static_seen?(same, same, _seen), do: true
+
+  defp subtype_static_seen?(left, right, seen),
+    do: empty_difference_subtype_seen?(left, right, seen)
+
+  # Fused difference + emptiness with the caller's coinductive context.
+  # Mirrors empty_difference_subtype? but passes `seen` for memoization.
+  # We must register a memo key for the overall difference before iterating,
+  # so that recursive encounters with the same subtype obligation short-circuit.
+  defp empty_difference_subtype_seen?(left, :term, _seen), do: keep_optional(left) == @none
+
+  defp empty_difference_subtype_seen?(left, right, seen) do
+    diff = difference_static(left, right)
+    key = empty_memo_key(diff)
+
+    if :erlang.is_map_key(key, seen) do
+      true
+    else
+      seen = Map.put(seen, key, true)
+
+      iterator_empty_difference_subtype?(
+        :maps.next(:maps.iterator(unfold(left))),
+        unfold(right),
+        seen
+      )
+    end
+  end
+
   @doc """
   Check if a type is equal to another.
 
@@ -915,6 +1133,8 @@ defmodule Module.Types.Descr do
 
   # Two gradual types are disjoint if their upper bounds are disjoint.
   def disjoint?(left, right) do
+    left = to_descr(left)
+    right = to_descr(right)
     left_upper = unfold(left) |> Map.get(:dynamic, left)
     right_upper = unfold(right) |> Map.get(:dynamic, right)
 
@@ -1595,14 +1815,14 @@ defmodule Module.Types.Descr do
   # and compile into tuples of positive and negative nodes. Positive nodes are
   # those followed by a left path, negative nodes are those followed by a right path.
   defp fun_bdd_to_dnf(bdd),
-    do: bdd_to_dnf(bdd) |> Enum.filter(fn {pos, neg} -> not fun_line_empty?(pos, neg) end)
+    do: bdd_to_dnf(bdd) |> Enum.filter(fn {pos, neg} -> not fun_line_empty?(pos, neg, %{}) end)
 
   # Check if all functions types for all arities are empty.
-  defp fun_empty?({:negation, _}), do: false
+  defp fun_empty?({:negation, _}, _seen), do: false
 
-  defp fun_empty?({:union, repr}) do
+  defp fun_empty?({:union, repr}, seen) do
     Enum.all?(repr, fn {_ar, bdd} ->
-      Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg) end)
+      Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg, seen) end)
     end)
   end
 
@@ -1613,9 +1833,9 @@ defmodule Module.Types.Descr do
   #
   # - `{[fun(1)], []}` is not empty
   # - `{[fun(integer() -> atom())], [fun(none() -> term())]}` is empty
-  defp fun_line_empty?([], _), do: false
+  defp fun_line_empty?([], _, _seen), do: false
 
-  defp fun_line_empty?(positives, negatives) do
+  defp fun_line_empty?(positives, negatives, seen) do
     # Check if any negative function negates the whole positive intersection
     # e.g. (integer() -> atom()) is negated by:
     #
@@ -1627,7 +1847,7 @@ defmodule Module.Types.Descr do
       # Check if the negative function's domain is a supertype of the positive
       # domain and if the phi function determines emptiness.
       subtype?(args_to_domain(neg_arguments), fetch_domain(positives)) and
-        phi_starter(neg_arguments, neg_return, positives)
+        phi_starter(neg_arguments, neg_return, positives, seen)
     end)
   end
 
@@ -1651,12 +1871,12 @@ defmodule Module.Types.Descr do
   # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
   #
   # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
-  defp phi_starter(arguments, return, positives) do
+  defp phi_starter(arguments, return, positives, seen) do
     # Optimization: When all positive functions have non-empty domains,
     # we can simplify the phi function check to a direct subtyping test.
     # This avoids the expensive recursive phi computation by checking only that applying the
     # input to the positive intersection yields a subtype of the return
-    case disjoint_non_empty_domains?({arguments, return}, positives) do
+    case disjoint_non_empty_domains?({arguments, return}, positives, seen) do
       :disjoint_non_empty ->
         apply_disjoint(arguments, positives) |> subtype?(return)
 
@@ -1666,17 +1886,20 @@ defmodule Module.Types.Descr do
       _ ->
         # Initialize memoization cache for the recursive phi computation
         arguments = Enum.map(arguments, &{false, &1})
-        {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{})
+        {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{}, seen)
         result
     end
   end
 
-  defp phi(args, {b, t}, [], cache) do
-    result = Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
+  defp phi(args, {b, t}, [], cache, seen) do
+    result =
+      Enum.any?(args, fn {bool, typ} -> bool and empty_seen?(typ, seen) end) or
+        (b and empty_seen?(t, seen))
+
     {result, Map.put(cache, {args, {b, t}, []}, result)}
   end
 
-  defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do
+  defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache, seen) do
     # Create cache key from function arguments
     cache_key = {args, {b, ret}, [{arguments, return} | rest_positive]}
 
@@ -1686,7 +1909,8 @@ defmodule Module.Types.Descr do
 
       %{} ->
         # Compute result and cache it
-        {result1, cache} = phi(args, {true, intersection(ret, return)}, rest_positive, cache)
+        {result1, cache} =
+          phi(args, {true, intersection(ret, return)}, rest_positive, cache, seen)
 
         if not result1 do
           cache = Map.put(cache, cache_key, false)
@@ -1698,7 +1922,7 @@ defmodule Module.Types.Descr do
                 {new_result, new_cache} =
                   args
                   |> List.update_at(index, fn {_, arg} -> {true, difference(arg, type)} end)
-                  |> phi({b, ret}, rest_positive, acc_cache)
+                  |> phi({b, ret}, rest_positive, acc_cache, seen)
 
                 if new_result do
                   {:cont, {index + 1, acc_result and new_result, new_cache}}
@@ -1714,9 +1938,9 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp disjoint_non_empty_domains?({arguments, return}, positives) do
+  defp disjoint_non_empty_domains?({arguments, return}, positives, seen) do
     b1 = all_disjoint_arguments?(positives)
-    b2 = all_non_empty_arguments?([{arguments, return} | positives])
+    b2 = all_non_empty_arguments?([{arguments, return} | positives], seen)
 
     cond do
       b1 and b2 -> :disjoint_non_empty
@@ -1725,9 +1949,9 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp all_non_empty_arguments?(positives) do
+  defp all_non_empty_arguments?(positives, seen) do
     Enum.all?(positives, fn {args, _ret} ->
-      Enum.all?(args, fn arg -> not empty?(arg) end)
+      Enum.all?(args, fn arg -> not empty_seen?(arg, seen) end)
     end)
   end
 
@@ -2011,57 +2235,83 @@ defmodule Module.Types.Descr do
   #
   # none() types can be given and, while stored, it means the list type is empty.
   defp list_descr(list_type, last_type, empty?) do
-    list_type_descr = to_descr(list_type)
-    last_type_descr = to_descr(last_type)
+    # Detect recursive nodes (from recursive/1, with non-empty state) in
+    # either position. These must be stored as-is without unfolding to
+    # prevent infinite recursion during construction.
+    list_is_rec_node = match?({id, state, _} when is_reference(id) and state != %{}, list_type)
+    last_is_rec_node = match?({id, state, _} when is_reference(id) and state != %{}, last_type)
 
-    {list_dynamic?, list_type} = list_pop_dynamic(list_type_descr)
-    {last_dynamic?, last_type} = list_pop_dynamic(last_type_descr)
+    if list_is_rec_node or last_is_rec_node do
+      # For non-node positions, resolve normally; for node positions, store as-is
+      {list_dynamic?, resolved_list} =
+        if list_is_rec_node, do: {false, list_type}, else: list_pop_dynamic(to_descr(list_type))
 
-    list_part =
-      if last_type == :term do
-        list_new(:term, :term)
-      else
-        case :maps.take(:list, last_type) do
-          :error ->
-            list_new(list_type, last_type)
+      {last_dynamic?, resolved_last} =
+        if last_is_rec_node, do: {false, last_type}, else: list_pop_dynamic(to_descr(last_type))
 
-          {bdd, last_type_no_list} ->
-            # `last_type` may itself represent one or more list types.
-            # Our goal is to fold those list types into `list_type` while retaining the
-            # possible type of the final element (which can be `[]` or any non-list value).
-            #
-            # The list types inside `last_type` are stored in a BDD that includes possible
-            # negations, so we must evaluate each node with its sign taken into account.
-            #
-            # A negation only matters when the negated list type is a supertype of the
-            # corresponding positive list type; in that case we subtract the negated
-            # variant from the positive one. This is done in list_bdd_to_pos_dnf/1.
-            {list_type, last_type} =
-              list_bdd_to_pos_dnf(bdd)
-              |> Enum.reduce({list_type, last_type_no_list}, fn
-                {list, last, _negs}, {acc_list, acc_last} ->
-                  {union(list, acc_list), union(last, acc_last)}
-              end)
+      list_part = list_new(resolved_list, resolved_last)
 
-            list_new(list_type, last_type)
-        end
+      list_descr =
+        if empty?, do: %{list: list_part, bitmap: @bit_empty_list}, else: %{list: list_part}
+
+      case list_dynamic? or last_dynamic? do
+        true -> %{dynamic: list_descr}
+        false -> list_descr
       end
+    else
+      list_type_descr = to_descr(list_type)
+      last_type_descr = to_descr(last_type)
 
-    list_descr =
-      if empty?, do: %{list: list_part, bitmap: @bit_empty_list}, else: %{list: list_part}
+      {list_dynamic?, list_type} = list_pop_dynamic(list_type_descr)
+      {last_dynamic?, last_type} = list_pop_dynamic(last_type_descr)
 
-    case list_dynamic? or last_dynamic? do
-      true -> %{dynamic: list_descr}
-      false -> list_descr
+      list_part =
+        if last_type == :term do
+          list_new(:term, :term)
+        else
+          case :maps.take(:list, last_type) do
+            :error ->
+              list_new(list_type, last_type)
+
+            {bdd, last_type_no_list} ->
+              # `last_type` may itself represent one or more list types.
+              # Our goal is to fold those list types into `list_type` while retaining the
+              # possible type of the final element (which can be `[]` or any non-list value).
+              #
+              # The list types inside `last_type` are stored in a BDD that includes possible
+              # negations, so we must evaluate each node with its sign taken into account.
+              #
+              # A negation only matters when the negated list type is a supertype of the
+              # corresponding positive list type; in that case we subtract the negated
+              # variant from the positive one. This is done in list_bdd_to_pos_dnf/1.
+              {list_type, last_type} =
+                list_bdd_to_pos_dnf(bdd)
+                |> Enum.reduce({list_type, last_type_no_list}, fn
+                  {list, last, _negs}, {acc_list, acc_last} ->
+                    {union(list, acc_list), union(last, acc_last)}
+                end)
+
+              list_new(list_type, last_type)
+          end
+        end
+
+      list_descr =
+        if empty?, do: %{list: list_part, bitmap: @bit_empty_list}, else: %{list: list_part}
+
+      case list_dynamic? or last_dynamic? do
+        true -> %{dynamic: list_descr}
+        false -> list_descr
+      end
     end
   end
 
   defp list_new(list_type, last_type), do: bdd_leaf(list_type, last_type)
 
-  defp non_empty_list_literals_intersection(list_literals) do
+  defp non_empty_list_literals_intersection(list_literals, seen) do
     try do
       Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} ->
-        {non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)}
+        {non_empty_intersection!(list, next_list, seen),
+         non_empty_intersection!(last, next_last, seen)}
       end)
     catch
       :empty -> :empty
@@ -2079,7 +2329,7 @@ defmodule Module.Types.Descr do
   defp list_bdd_to_pos_dnf(bdd) do
     bdd_to_dnf(bdd)
     |> Enum.reduce([], fn {pos_list, negs}, acc ->
-      case non_empty_list_literals_intersection(pos_list) do
+      case non_empty_list_literals_intersection(pos_list, %{}) do
         :empty ->
           acc
 
@@ -2110,6 +2360,10 @@ defmodule Module.Types.Descr do
   end
 
   defp list_tail_unfold(:term), do: @not_non_empty_list
+
+  defp list_tail_unfold({id, state, gen}) when is_reference(id),
+    do: Map.delete(gen.(state), :list)
+
   defp list_tail_unfold(other), do: Map.delete(other, :list)
 
   @compile {:inline, list_union: 2}
@@ -2235,12 +2489,22 @@ defmodule Module.Types.Descr do
   end
 
   defp list_leaf_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
-    try do
-      list = non_empty_intersection!(list1, list2)
-      last = non_empty_intersection!(last1, last2)
-      bdd_leaf(list, last)
-    catch
-      :empty -> :bdd_bot
+    has_node =
+      collect_generators(list1) != [] or
+        collect_generators(list2) != [] or
+        collect_generators(last1) != [] or
+        collect_generators(last2) != []
+
+    if has_node do
+      bdd_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2))
+    else
+      try do
+        list = non_empty_intersection!(list1, list2)
+        last = non_empty_intersection!(last1, last2)
+        bdd_leaf(list, last)
+      catch
+        :empty -> :bdd_bot
+      end
     end
   end
 
@@ -2254,7 +2518,19 @@ defmodule Module.Types.Descr do
   # 3. Base case: adds bdd2 type to negations of bdd1 type
   # The result may be larger than the initial bdd1, which is maintained in the accumulator.
   defp list_difference(bdd_leaf(list1, last1) = bdd1, bdd_leaf(list2, last2) = bdd2) do
+    # When element or tail types contain recursive nodes, skip subtype/disjoint
+    # optimizations to avoid infinite unfolding. Fall through to bdd_difference
+    # which preserves nodes as-is for later cycle-aware emptiness checking.
+    has_node =
+      collect_generators(list1) != [] or
+        collect_generators(list2) != [] or
+        collect_generators(last1) != [] or
+        collect_generators(last2) != []
+
     cond do
+      has_node ->
+        bdd_difference(bdd1, bdd2)
+
       disjoint?(list1, list2) or disjoint?(last1, last2) ->
         bdd_leaf(list1, last1)
 
@@ -2271,30 +2547,31 @@ defmodule Module.Types.Descr do
   defp list_difference(bdd1, bdd2),
     do: bdd_difference(bdd1, bdd2)
 
-  defp list_empty?(@non_empty_list_top), do: false
+  defp list_empty?(@non_empty_list_top, _seen), do: false
 
-  defp list_empty?(bdd) do
+  defp list_empty?(bdd, seen) do
     bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, negs} ->
-      case non_empty_list_literals_intersection(pos) do
+      case non_empty_list_literals_intersection(pos, seen) do
         :empty -> true
-        {list, last} -> list_line_empty?(list, last, negs)
+        {list, last} -> list_line_empty?(list, last, negs, seen)
       end
     end)
   end
 
-  defp list_line_empty?(list_type, last_type, negs) do
+  defp list_line_empty?(list_type, last_type, negs, seen) do
     last_type = list_tail_unfold(last_type)
     # To make a list {list, last} empty with some negative lists:
     # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one.
     # 2. Each of the list supertypes:
     #     a. either completely covers the type, if its last type is a supertype of the positive one,
     #     b. or it removes part of the last type.
-    empty?(list_type) or empty?(last_type) or
+    empty_seen?(list_type, seen) or empty_seen?(last_type, seen) or
       Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type ->
-        if subtype?(list_type, neg_type) do
+        if subtype_seen?(list_type, neg_type, seen) do
+          neg_last = list_tail_unfold(neg_last)
           d = difference(acc_last_type, neg_last)
-          if empty?(d), do: {:halt, nil}, else: {:cont, d}
+          if empty_seen?(d, seen), do: {:halt, nil}, else: {:cont, d}
         else
           {:cont, acc_last_type}
         end
@@ -2683,6 +2960,14 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # Recursive type nodes are stored as-is without stepping (same as tuple_descr).
+  # Stepping would call the generator, which would call closed_map/open_map again,
+  # producing fresh nodes ad infinitum.
+  defp map_descr_pairs([{key, {id, _state, _gen} = node} | rest], fields, domain, dynamic?)
+       when is_reference(id) and is_atom(key) do
+    map_descr_pairs(rest, [{key, node} | fields], domain, dynamic?)
+  end
+
   defp map_descr_pairs([{key, value} | rest], fields, domain, dynamic?) do
     value_descr = to_descr(value)
 
@@ -2734,7 +3019,7 @@ defmodule Module.Types.Descr do
   defp non_empty_map_only?(descr) do
     case :maps.take(:map, descr) do
       :error -> false
-      {map_bdd, rest} -> empty?(rest) and not map_empty?(map_bdd)
+      {map_bdd, rest} -> empty?(rest) and not map_empty?(map_bdd, %{})
     end
   end
 
@@ -2805,12 +3090,24 @@ defmodule Module.Types.Descr do
 
   defp do_map_union_optimization_strategy(:none, _, status), do: status
 
+  # Bail out when either value is a recursive node — calling union/subtype?
+  # on nodes during BDD construction would unfold the generator and loop.
+  defp do_map_union_optimization_strategy({_key, {id, _, _}, _iterator}, _pos2, _status)
+       when is_reference(id),
+       do: nil
+
   defp do_map_union_optimization_strategy({key, v1, iterator}, pos2, status) do
-    with %{^key => v2} <- pos2,
-         next_status when next_status != nil <- map_union_next_strategy(key, v1, v2, status) do
-      do_map_union_optimization_strategy(:maps.next(iterator), pos2, next_status)
-    else
-      _ -> nil
+    case pos2 do
+      %{^key => {id, _, _}} when is_reference(id) ->
+        nil
+
+      _ ->
+        with %{^key => v2} <- pos2,
+             next_status when next_status != nil <- map_union_next_strategy(key, v1, v2, status) do
+          do_map_union_optimization_strategy(:maps.next(iterator), pos2, next_status)
+        else
+          _ -> nil
+        end
     end
   end
 
@@ -3054,6 +3351,11 @@ defmodule Module.Types.Descr do
     if empty?(type), do: throw(:empty), else: type
   end
 
+  defp non_empty_intersection!(type1, type2, seen) do
+    type = intersection(type1, type2)
+    if empty_seen?(type, seen), do: throw(:empty), else: type
+  end
+
   # Takes all the lines from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Positive nodes are
   # those followed by a left path, negative nodes are those followed by a right path.
@@ -3065,7 +3367,7 @@ defmodule Module.Types.Descr do
           acc
 
         {tag, fields} ->
-          if init_map_line_empty?(tag, fields, negs) do
+          if init_map_line_empty?(tag, fields, negs, %{}) do
             acc
           else
             [{tag, fields, negs} | acc]
@@ -3981,7 +4283,7 @@ defmodule Module.Types.Descr do
   # Short-circuits if it finds a non-empty map literal in the union.
   # Since the algorithm is recursive, we implement the short-circuiting
   # as throw/catch.
-  defp map_empty?(bdd) do
+  defp map_empty?(bdd, seen) do
     bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, negs} ->
       case non_empty_map_literals_intersection(pos) do
@@ -3992,24 +4294,28 @@ defmodule Module.Types.Descr do
           # We check the emptiness of the fields because non_empty_map_literal_intersection
           # will not return :empty on fields that are set to none() and that exist
           # just in one map, but not the other.
-          init_map_line_empty?(tag, fields, negs)
+          init_map_line_empty?(tag, fields, negs, seen)
       end
     end)
   end
 
-  defp init_map_line_empty?(tag, fields, negs) do
-    Enum.any?(Map.to_list(fields), fn {_key, type} -> empty?(type) end) or
-      map_line_empty?(tag, fields, negs)
+  defp init_map_line_empty?(tag, fields, negs, seen) do
+    Enum.any?(Map.to_list(fields), fn {_key, type} -> empty_seen?(type, seen) end) or
+      map_line_empty?(tag, fields, negs, seen)
   end
 
   # These positives get checked once when calling init_map_line_empty?, and then every time
   # an intersection or difference is computed, its emptiness is checked again.
   # So they are all necessarily non-empty.
-  defp map_line_empty?(_, _pos, []), do: false
-  defp map_line_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true
-  defp map_line_empty?(:open, fs, [{:closed, _} | negs]), do: map_line_empty?(:open, fs, negs)
+  defp map_line_empty?(_, _pos, [], _seen), do: false
+  defp map_line_empty?(_, _, [{:open, neg_fields} | _], _seen) when neg_fields == %{}, do: true
+
+  defp map_line_empty?(:open, fs, [{:closed, _} | negs], seen),
+    do: map_line_empty?(:open, fs, negs, seen)
+
+  defp map_line_empty?(tag, fields, all_negs, seen) when all_negs != [] do
+    [{neg_tag, neg_fields} | negs] = all_negs
 
-  defp map_line_empty?(tag, fields, [{neg_tag, neg_fields} | negs]) do
     if map_check_domain_keys(tag, neg_tag) do
       atom_default = map_key_tag_to_type(tag)
       neg_atom_default = map_key_tag_to_type(neg_tag)
@@ -4029,18 +4335,24 @@ defmodule Module.Types.Descr do
           # There may be value in common
           tag == :open ->
             diff = difference(term_or_optional(), neg_type)
-            empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs)
+
+            empty_seen?(diff, seen) or
+              map_line_empty?(tag, Map.put(fields, neg_key, diff), negs, seen)
 
           true ->
             diff = difference(atom_default, neg_type)
-            empty?(diff) or map_line_empty?(tag, Map.put(fields, neg_key, diff), negs)
+
+            empty_seen?(diff, seen) or
+              map_line_empty?(tag, Map.put(fields, neg_key, diff), negs, seen)
         end
       end) and
         Enum.all?(Map.to_list(fields), fn {key, type} ->
           case neg_fields do
             %{^key => neg_type} ->
               diff = difference(type, neg_type)
-              empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs)
+
+              empty_seen?(diff, seen) or
+                map_line_empty?(tag, Map.put(fields, key, diff), negs, seen)
 
             %{} ->
               cond do
@@ -4055,15 +4367,17 @@ defmodule Module.Types.Descr do
                 true ->
                   # an absent key in a open negative map can be ignored
                   diff = difference(type, neg_atom_default)
-                  empty?(diff) or map_line_empty?(tag, Map.put(fields, key, diff), negs)
+
+                  empty_seen?(diff, seen) or
+                    map_line_empty?(tag, Map.put(fields, key, diff), negs, seen)
               end
           end
         end)
     else
-      map_line_empty?(tag, fields, negs)
+      map_line_empty?(tag, fields, tl(all_negs), seen)
     end
   catch
-    :closed -> map_line_empty?(tag, fields, negs)
+    :closed -> map_line_empty?(tag, fields, tl(all_negs), seen)
   end
 
   # Verify the domain condition from equation (22) in paper ICFP'23 https://www.irif.fr/~gc/papers/icfp23.pdf
@@ -4384,8 +4698,12 @@ defmodule Module.Types.Descr do
     tuple_descr(rest, [:term | acc], dynamic?)
   end
 
-  # Nodes (3-tuples with a reference id) are stored as-is without stepping.
-  # This avoids infinite recursion for recursive type nodes.
+  # Recursive type nodes (3-tuples with a reference id) are stored as-is
+  # without stepping. Stepping would call the generator, which calls tuple()
+  # again, producing fresh nodes ad infinitum. This is safe because dynamic()
+  # never appears inside recursive type definitions, so skipping dynamic
+  # detection here loses nothing. Emptiness of nodes is handled lazily by
+  # the memoized empty?/2 algorithm when the node is eventually unfolded.
   defp tuple_descr([{id, _state, _gen} = node | rest], acc, dynamic?) when is_reference(id) do
     tuple_descr(rest, [node | acc], dynamic?)
   end
@@ -4393,28 +4711,37 @@ defmodule Module.Types.Descr do
   defp tuple_descr([value | rest], acc, dynamic?) do
     value_descr = to_descr(value)
 
-    # Check if the static part is empty
-    static_empty? =
-      case value_descr do
-        # Has dynamic component, check static separately
-        %{dynamic: _} -> false
-        _ -> empty?(value_descr)
-      end
-
-    if static_empty? do
-      :empty
+    # Skip emptiness check for values containing recursive nodes to avoid
+    # infinite unfolding during construction. Like the bare node clause above,
+    # dynamic() never appears inside recursive type definitions, so skipping
+    # dynamic detection loses nothing. Node emptiness is handled lazily by
+    # the memoized empty_seen? algorithm.
+    if collect_generators(value_descr) != [] do
+      tuple_descr(rest, [value | acc], dynamic?)
     else
-      case :maps.take(:dynamic, value_descr) do
-        :error ->
-          tuple_descr(rest, [value | acc], dynamic?)
+      # Check if the static part is empty
+      static_empty? =
+        case value_descr do
+          # Has dynamic component, check static separately
+          %{dynamic: _} -> false
+          _ -> empty?(value_descr)
+        end
 
-        {dynamic, _static} ->
-          # Check if dynamic component is empty
-          if empty?(dynamic) do
-            :empty
-          else
-            tuple_descr(rest, [dynamic | acc], true)
-          end
+      if static_empty? do
+        :empty
+      else
+        case :maps.take(:dynamic, value_descr) do
+          :error ->
+            tuple_descr(rest, [value | acc], dynamic?)
+
+          {dynamic, _static} ->
+            # Check if dynamic component is empty
+            if empty?(dynamic) do
+              :empty
+            else
+              tuple_descr(rest, [dynamic | acc], true)
+            end
+        end
       end
     end
   end
@@ -4425,14 +4752,24 @@ defmodule Module.Types.Descr do
 
   defp tuple_new(tag, elements), do: bdd_leaf(tag, elements)
 
+  # defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2)
+
   defp tuple_intersection(bdd1, bdd2) do
     bdd_intersection(bdd1, bdd2, &tuple_leaf_intersection/2)
   end
 
-  defp tuple_leaf_intersection(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
-    case tuple_literal_intersection(tag1, elements1, tag2, elements2) do
-      {tag, elements} -> bdd_leaf(tag, elements)
-      :empty -> :bdd_bot
+  defp tuple_leaf_intersection(bdd_leaf(tag1, elems1) = l1, bdd_leaf(tag2, elems2) = l2) do
+    has_node =
+      Enum.any?(elems1, &(collect_generators(&1) != [])) or
+        Enum.any?(elems2, &(collect_generators(&1) != []))
+
+    if has_node do
+      bdd_intersection(l1, l2)
+    else
+      case tuple_literal_intersection(tag1, elems1, tag2, elems2) do
+        {tag, elements} -> bdd_leaf(tag, elements)
+        :empty -> :bdd_bot
+      end
     end
   end
 
@@ -4487,8 +4824,16 @@ defmodule Module.Types.Descr do
     do: bdd_difference(bdd1, bdd2, &tuple_leaf_disjoint?/2)
 
   defp tuple_leaf_disjoint?(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
-    mismatched_tuple_sizes?(tag1, elements1, tag2, elements2) or
-      disjoint_tagged_tuples?(elements1, elements2)
+    has_node =
+      Enum.any?(elements1, &(collect_generators(&1) != [])) or
+        Enum.any?(elements2, &(collect_generators(&1) != []))
+
+    if has_node do
+      false
+    else
+      mismatched_tuple_sizes?(tag1, elements1, tag2, elements2) or
+        disjoint_tagged_tuples?(elements1, elements2)
+    end
   end
 
   # A very cheap check for tagged tuples
@@ -4517,27 +4862,29 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp tuple_empty?(bdd) do
+  defp tuple_empty?(bdd, seen) do
     bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, negs} ->
       case non_empty_tuple_literals_intersection(pos) do
         :empty -> true
-        {tag, fields} -> tuple_line_empty?(tag, fields, negs)
+        {tag, fields} -> tuple_line_empty?(tag, fields, negs, seen)
       end
     end)
   end
 
-  # No negations, so not empty unless there's an empty type
-  # Note: since the extraction from the BDD is done in a way that guarantees that
-  # the elements are non-empty, we can avoid checking for empty types there.
-  # Otherwise, tuple_empty?(_, elements, []) would be Enum.any?(elements, &empty?/1)
-  defp tuple_line_empty?(_, _, []), do: false
+  # No negations: elements may contain nodes (from single positive leaf),
+  # so we must check if any element is empty using cycle-aware emptiness.
+  # This handles recursive types like X = {X} correctly.
+  defp tuple_line_empty?(_, elements, [], seen),
+    do: Enum.any?(elements, &empty_seen?(&1, seen))
+
   # Open empty negation makes it empty
-  defp tuple_line_empty?(_, _, [{:open, []} | _]), do: true
+  defp tuple_line_empty?(_, _, [{:open, []} | _], _seen), do: true
   # Open positive can't be emptied by a single closed negative
-  defp tuple_line_empty?(:open, _pos, [{:closed, _}]), do: false
+  defp tuple_line_empty?(:open, _pos, [{:closed, _}], _seen), do: false
 
-  defp tuple_line_empty?(tag, elements, [{neg_tag, neg_elements} | negs]) do
+  defp tuple_line_empty?(tag, elements, negs, seen) do
+    [{neg_tag, neg_elements} | negs] = negs
     n = length(elements)
     m = length(neg_elements)
 
@@ -4545,37 +4892,40 @@ defmodule Module.Types.Descr do
     # 1. When removing larger tuples from a fixed-size positive tuple
     # 2. When removing smaller tuples from larger tuples
     if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do
-      tuple_line_empty?(tag, elements, negs)
+      tuple_line_empty?(tag, elements, negs, seen)
     else
-      tuple_elements_empty?([], tag, elements, neg_elements, negs) and
-        tuple_empty_arity?(n, m, tag, elements, neg_tag, negs)
+      tuple_elements_empty?([], tag, elements, neg_elements, negs, seen) and
+        tuple_empty_arity?(n, m, tag, elements, neg_tag, negs, seen)
     end
   end
 
   # Recursively check elements for emptiness
-  defp tuple_elements_empty?(_, _, _, [], _), do: true
+  defp tuple_elements_empty?(_, _, _, [], _, _seen), do: true
 
-  defp tuple_elements_empty?(acc_meet, tag, elements, [neg_type | neg_elements], negs) do
+  defp tuple_elements_empty?(acc_meet, tag, elements, [neg_type | neg_elements], negs, seen) do
     # Handles the case where {tag, elements} is an open tuple, like {:open, []}
     {ty, elements} = List.pop_at(elements, 0, term())
+
     diff = difference(ty, neg_type)
     meet = intersection(ty, neg_type)
 
     # In this case, there is no intersection between the positive and this negative.
     # So we should just "go next"
-    (empty?(diff) or tuple_line_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and
-      (empty?(meet) or tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs))
+    (empty_seen?(diff, seen) or
+       tuple_line_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs, seen)) and
+      (empty_seen?(meet, seen) or
+         tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs, seen))
   end
 
   # Determines if the set difference is empty when:
   # - Positive tuple: {tag, elements} of size n
   # - Negative tuple: open or closed tuples of size m
-  defp tuple_empty_arity?(n, m, tag, elements, neg_tag, negs) do
+  defp tuple_empty_arity?(n, m, tag, elements, neg_tag, negs, seen) do
     # The tuples to consider are all those of size n to m - 1, and if the negative tuple is
     # closed, we also need to consider tuples of size greater than m + 1.
     tag == :closed or
-      (Enum.all?(n..(m - 1)//1, &tuple_line_empty?(:closed, tuple_fill(elements, &1), negs)) and
-         (neg_tag == :open or tuple_line_empty?(:open, tuple_fill(elements, m + 1), negs)))
+      (Enum.all?(n..(m - 1)//1, &tuple_line_empty?(:closed, tuple_fill(elements, &1), negs, seen)) and
+         (neg_tag == :open or tuple_line_empty?(:open, tuple_fill(elements, m + 1), negs, seen)))
   end
 
   defp tuple_eliminate_negations(tag, elements, negs) do
@@ -4700,9 +5050,17 @@ defmodule Module.Types.Descr do
          bdd_leaf(tag1, elements1) = tuple1,
          bdd_leaf(tag2, elements2) = tuple2
        ) do
-    case maybe_optimize_tuple_union({tag1, elements1}, {tag2, elements2}) do
-      {tag, elements} -> bdd_leaf(tag, elements)
-      nil -> bdd_union(tuple1, tuple2)
+    has_node =
+      Enum.any?(elements1, &(collect_generators(&1) != [])) or
+        Enum.any?(elements2, &(collect_generators(&1) != []))
+
+    if has_node do
+      bdd_union(tuple1, tuple2)
+    else
+      case maybe_optimize_tuple_union({tag1, elements1}, {tag2, elements2}) do
+        {tag, elements} -> bdd_leaf(tag, elements)
+        nil -> bdd_union(tuple1, tuple2)
+      end
     end
   end
 
@@ -4760,6 +5118,16 @@ defmodule Module.Types.Descr do
        when status in [:all_equal, :left_subtype_of_right],
        do: :left_subtype_of_right
 
+  # Bail out when either element is a recursive node — calling union/subtype?
+  # on nodes during BDD construction would unfold the generator and loop.
+  defp do_tuple_union_optimization_strategy(_tag1, [{id, _, _} | _], _tag2, _pos2, _i, _status)
+       when is_reference(id),
+       do: nil
+
+  defp do_tuple_union_optimization_strategy(_tag1, _pos1, _tag2, [{id, _, _} | _], _i, _status)
+       when is_reference(id),
+       do: nil
+
   defp do_tuple_union_optimization_strategy(tag1, [v1 | pos1], tag2, [v2 | pos2], i, status) do
     if next_status = tuple_union_next_strategy(i, v1, v2, status) do
       do_tuple_union_optimization_strategy(tag1, pos1, tag2, pos2, i + 1, next_status)
@@ -4811,7 +5179,7 @@ defmodule Module.Types.Descr do
           acc
 
         {tag, elements} ->
-          if tuple_line_empty?(tag, elements, negative_tuples) do
+          if tuple_line_empty?(tag, elements, negative_tuples, %{}) do
             acc
           else
             tuple_eliminate_negations(tag, elements, negative_tuples) |> tuple_dnf_union(acc)
@@ -4950,7 +5318,7 @@ defmodule Module.Types.Descr do
   defp non_empty_tuple_only?(descr) do
     case :maps.take(:tuple, descr) do
       :error -> false
-      {tuple_bdd, rest} -> empty?(rest) and not tuple_empty?(tuple_bdd)
+      {tuple_bdd, rest} -> empty?(rest) and not tuple_empty?(tuple_bdd, %{})
     end
   end
 
@@ -5784,7 +6152,7 @@ defmodule Module.Types.Descr do
   defp iterator_non_disjoint_intersection?({key, v1, iterator}, map) do
     with %{^key => v2} <- map,
          value when value not in @empty_intersection <- intersection(key, v1, v2),
-         false <- empty_key?(key, value) do
+         false <- empty_key?(key, value, %{}) do
       true
     else
       _ -> iterator_non_disjoint_intersection?(:maps.next(iterator), map)
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 158f032005f..eb804650afb 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -3266,247 +3266,208 @@ defmodule Module.Types.DescrTest do
     end
   end
 
-  ## Block A — Node infrastructure
+  ## Node infrastructure
 
-  describe "make_node (A.1 / A.2)" do
-    test "returns a triple {id, state, generator}" do
+  describe "recursive types" do
+    test "building a node" do
+      # "a node is a triple {id, state, generator}
       state = %{x: 1}
       gen = fn s -> s end
       node = make_node(state, gen)
 
       assert {id, ^state, ^gen} = node
       assert is_reference(id)
-    end
 
-    test "each call produces a fresh id" do
+      # each call produces a fresh id
       gen = fn _ -> :ok end
       {id1, _, _} = make_node(%{}, gen)
       {id2, _, _} = make_node(%{}, gen)
       assert id1 != id2
     end
-  end
 
-  describe "to_descr / step (A.3)" do
-    test "stepping a node applies the generator to the state" do
+    test "to_descr (from node)" do
+      # stepping a node applies the generator to the state
       descr = integer()
       node = make_node(%{}, fn _state -> descr end)
       assert to_descr(node) == descr
-    end
 
-    test "stepping a node with non-trivial state" do
+      # stepping a node with non-trivial state
       node = make_node(%{val: float()}, fn state -> state.val end)
       assert to_descr(node) == float()
-    end
 
-    test "to_descr is identity on :term" do
+      # to_descr is identity on :term
       assert to_descr(:term) == :term
-    end
 
-    test "to_descr is identity on a descr map" do
+      # to_descr is identity on a descr map
       d = union(integer(), atom())
       assert to_descr(d) == d
     end
-  end
 
-  describe "to_node / fresh_node (A.4 / A.5)" do
-    test "wrapping a descr map produces a node whose step returns the original" do
+    test "to_node (from descr) / fresh_node" do
+      # wrapping a descr map produces a node whose step returns the original
       d = integer()
       node = to_node(d)
       assert {id, %{}, _gen} = node
       assert is_reference(id)
       assert to_descr(node) == d
-    end
 
-    test "wrapping :term produces a node whose step returns :term" do
+      # wrapping :term produces a node whose step returns :term
       node = to_node(:term)
       assert {id, :term, _gen} = node
       assert is_reference(id)
       assert to_descr(node) == :term
-    end
 
-    test "to_node on an existing node returns it unchanged" do
+      # to_node on an existing node returns it unchanged
       node = make_node(%{}, fn _ -> integer() end)
       assert to_node(node) === node
-    end
 
-    test "wrapping and stepping round-trips for complex descrs" do
+      # wrapping and stepping round-trips for complex descrs
       d = union(tuple([integer(), atom()]), list(float()))
       assert to_descr(to_node(d)) == d
     end
-  end
 
-  ## Block B — Kind internals accept nodes
+    ## Kind internals accept nodes
 
-  describe "tuple constructor accepts nodes (B.1 / B.2)" do
-    test "tuple/1 accepts nodes and produces a non-empty tuple descr" do
+    test "tuple constructor accepts nodes and descrs" do
+      # tuple/1 accepts nodes and produces a non-empty tuple descr
       n1 = to_node(integer())
       n2 = to_node(atom())
 
       result = tuple([n1, n2])
-      assert is_map_key(result, :tuple)
-      assert map_size(result) > 0
-    end
+      refute empty?(result)
 
-    test "tuple/1 accepts a mix of nodes and descrs" do
+      # tuple/1 accepts a mix of nodes and descrs
       n = to_node(integer())
       result = tuple([n, float()])
-      assert is_map_key(result, :tuple)
-      assert map_size(result) > 0
+      assert equal?(result, tuple([integer(), float()]))
+
+      # todo: test tuple operations (index access) on recursive tuples
     end
-  end
 
-  describe "list constructor accepts nodes (B.1 / B.2)" do
-    test "list/1 accepts a node element type" do
+    test "list constructor accepts nodes" do
+      # list/1 accepts a node element type
       n = to_node(integer())
       from_node = list(n)
       from_descr = list(integer())
       assert equal?(from_node, from_descr)
-    end
 
-    test "non_empty_list/2 accepts nodes for both element and tail" do
+      # non_empty_list/2 accepts nodes for both element and tail
       elem_node = to_node(integer())
       tail_node = to_node(empty_list())
 
       from_nodes = non_empty_list(elem_node, tail_node)
       from_descrs = non_empty_list(integer(), empty_list())
       assert equal?(from_nodes, from_descrs)
+
+      # todo: test list operations (head, tail, cons) on recursive lists
     end
-  end
 
-  describe "map constructor accepts nodes (B.1 / B.2)" do
-    test "closed_map accepts node values" do
+    test "map constructor accepts nodes" do
+      # closed_map accepts node values
       n = to_node(integer())
       result = closed_map(a: n)
-      assert is_map_key(result, :map)
-      assert map_size(result) > 0
-    end
+      refute empty?(result)
 
-    test "open_map accepts node values" do
+      # open_map accepts node values
       n = to_node(atom())
       result = open_map(b: n)
-      assert is_map_key(result, :map)
-      assert map_size(result) > 0
-    end
-
-    test "map stores nodes in value positions" do
-      n = to_node(float())
-      %{map: bdd} = closed_map(x: n)
-      # Extract the leaf fields from the BDD
-      {_tag, fields} = bdd
-      node_val = Map.get(fields, :x)
-      assert {id, _state, _gen} = node_val
-      assert is_reference(id)
-      assert to_descr(node_val) == float()
-    end
+      refute empty?(result)
 
-    test "map with mixed node and descr values" do
+      # map with mixed node and descr values" do
       n = to_node(float())
       result = closed_map(x: n, y: integer())
       assert is_map_key(result, :map)
       assert map_size(result) > 0
+
+      # todo: test map operations (fetch, update, ...) on recursive maps
     end
-  end
 
-  ## Block C — Set operations accept nodes polymorphically
+    ## Set operations accept nodes polymorphically
 
-  describe "union on nodes (C.1)" do
-    test "union of two nodes returns the union descr" do
+    test "union on nodes" do
+      # union works on nodes
       n1 = to_node(integer())
       n2 = to_node(float())
       assert equal?(union(n1, n2), union(integer(), float()))
-    end
 
-    test "union of a node and a descr" do
+      # union of a node and a descr
       n = to_node(integer())
       assert equal?(union(n, float()), union(integer(), float()))
       assert equal?(union(atom(), n), union(atom(), integer()))
-    end
 
-    test "union with none() node is identity" do
+      # union with none() node is identity
       n = to_node(atom())
       n_none = to_node(none())
       assert equal?(union(n, n_none), atom())
-    end
 
-    test "union with term() node is term" do
+      # union with term() node is term
       n = to_node(integer())
       n_term = to_node(:term)
       assert union(n, n_term) == :term
     end
-  end
 
-  describe "intersection on nodes (C.2)" do
-    test "intersection of two nodes returns the intersection descr" do
+    test "intersection on nodes" do
+      # intersection of two nodes is equivalent to the intersection descr
       n1 = to_node(union(integer(), atom()))
       n2 = to_node(integer())
       assert equal?(intersection(n1, n2), integer())
-    end
 
-    test "intersection of a node and a descr" do
+      # intersection of a node and a descr
       n = to_node(union(integer(), atom()))
       assert equal?(intersection(n, integer()), integer())
       assert equal?(intersection(atom(), n), atom())
-    end
 
-    test "intersection of disjoint nodes is none" do
+      # intersection of disjoint nodes is none
       n1 = to_node(integer())
       n2 = to_node(atom())
       assert equal?(intersection(n1, n2), none())
-    end
 
-    test "intersection with term() node is identity" do
+      # intersection with term() node is identity
       n = to_node(float())
       n_term = to_node(:term)
       assert equal?(intersection(n, n_term), float())
     end
-  end
 
-  describe "negation on nodes (C.3)" do
-    test "negation of a node returns the negation descr" do
+    test "negation on nodes" do
+      # negation of a node is equivalent to the negation descr
       n = to_node(integer())
       assert equal?(negation(n), negation(integer()))
-    end
 
-    test "double negation round-trips" do
+      # double negation round-trips
       n = to_node(atom())
       assert equal?(negation(negation(n)), atom())
     end
-  end
 
-  describe "difference on nodes (C.4)" do
-    test "difference of two nodes returns the difference descr" do
+    test "difference on nodes" do
+      # difference of two nodes returns the difference descr
       n1 = to_node(union(integer(), atom()))
       n2 = to_node(atom())
       assert equal?(difference(n1, n2), integer())
-    end
 
-    test "difference of a node and a descr" do
+      # difference of a node and a descr
       n = to_node(union(integer(), float()))
       assert equal?(difference(n, float()), integer())
       assert equal?(difference(union(integer(), float()), to_node(float())), integer())
-    end
 
-    test "difference from itself is none" do
+      # difference from itself is none
       n = to_node(float())
       assert equal?(difference(n, n), none())
-    end
 
-    test "difference from none() is identity" do
+      # difference from none() is identity
       n = to_node(integer())
       n_none = to_node(none())
       assert equal?(difference(n, n_none), integer())
     end
-  end
 
-  ## Block D — Recursive type builder
+    ## Recursive type builder
 
-  describe "recursive/1 (D.1 / D.2 / D.3)" do
-    test "simple recursive list: X = {integer(), X} | nil" do
+    test "recursive builder" do
+      ## simple recursive list: X = {integer(), X} | nil
       %{X: node_x} =
         recursive(%{
           X: fn state ->
-            tuple([integer(), {make_ref(), state, state[:X]}])
-            |> union(atom([:nil]))
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
           end
         })
 
@@ -3520,63 +3481,57 @@ defmodule Module.Types.DescrTest do
       d = to_descr(node_x)
       assert is_map_key(d, :tuple)
       assert is_map_key(d, :atom)
-    end
-
-    test "stepping a recursive node yields a descr containing a nested node" do
-      %{X: node_x} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), {make_ref(), state, state[:X]}])
-            |> union(atom([:nil]))
-          end
-        })
-
-      # Step once to get the descriptor
-      d1 = to_descr(node_x)
 
-      # The tuple kind should exist and the descriptor should be non-empty
-      assert is_map(d1)
-      refute d1 == %{}
+      # some subtypes
+      # {integer(), nil} <: X
+      assert subtype?(tuple([integer(), atom([nil])]), node_x)
+      # nil <: X
+      assert subtype?(atom([nil]), node_x)
+      # {integer(), {integer(), nil}} <: X
+      assert subtype?(tuple([integer(), tuple([integer(), atom([nil])])]), node_x)
+      # {integer(), integer()} </: X
+      refute subtype?(tuple([integer(), integer()]), node_x)
     end
 
-    test "mutually recursive types: X = {int, Y} | nil, Y = {bool, X} | nil" do
+    test "mutually recursive nodes" do
+      # X = {int, Y} | nil, Y = {bool, X} | nil
       %{X: node_x, Y: node_y} =
         recursive(%{
           X: fn state ->
-            tuple([integer(), {make_ref(), state, state[:Y]}])
-            |> union(atom([:nil]))
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
           end,
           Y: fn state ->
-            tuple([boolean(), {make_ref(), state, state[:X]}])
-            |> union(atom([:nil]))
+            tuple([boolean(), make_node(state, state[:X])])
+            |> union(atom([nil]))
           end
         })
 
-      # Both are valid node triples sharing the same state
+      # both are valid node triples sharing the same state
       assert {id_x, state_x, _} = node_x
       assert {id_y, state_y, _} = node_y
       assert is_reference(id_x)
       assert is_reference(id_y)
       assert id_x != id_y
 
-      # They share the same state
+      # they share the same state
       assert state_x === state_y
 
-      # Both variables are present in the shared state
+      # both variables are present in the shared state
       assert is_map_key(state_x, :X)
       assert is_map_key(state_x, :Y)
     end
 
-    test "stepping mutually recursive nodes produces valid descriptors" do
+    test "stepping mutually recursive nodes" do
       %{X: node_x, Y: node_y} =
         recursive(%{
           X: fn state ->
-            tuple([integer(), {make_ref(), state, state[:Y]}])
-            |> union(atom([:nil]))
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
           end,
           Y: fn state ->
-            tuple([boolean(), {make_ref(), state, state[:X]}])
-            |> union(atom([:nil]))
+            tuple([boolean(), make_node(state, state[:X])])
+            |> union(atom([nil]))
           end
         })
 
@@ -3594,8 +3549,8 @@ defmodule Module.Types.DescrTest do
       %{X: node_x} =
         recursive(%{
           X: fn state ->
-            tuple([integer(), {make_ref(), state, state[:X]}])
-            |> union(atom([:nil]))
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
           end
         })
 
@@ -3619,4 +3574,1351 @@ defmodule Module.Types.DescrTest do
       assert equal?(to_descr(node_x), integer())
     end
   end
+
+  ## Emptiness on recursive types
+
+  describe "emptiness of recursive types" do
+    test "non-recursive nodes" do
+      # a node wrapping integer() is not empty
+      node = make_node(%{}, fn _state -> integer() end)
+      refute empty?(node)
+
+      # a node wrapping none() is empty
+      node_none = make_node(%{}, fn _state -> none() end)
+      assert empty?(node_none)
+    end
+
+    test "simple recursive types" do
+      # X = {integer(), X} | nil is not empty (inhabited by nil, {1,nil}, ...)
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+
+      # X = {X} is empty (no base case)
+      %{X: nx} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+
+      # X = {X, X} is empty (no base case)
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:X]), make_node(state, state[:X])])
+          end
+        })
+
+      assert empty?(nx)
+
+      # X = {integer()} | {X, X} has base case, not empty
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            union(
+              tuple([integer()]),
+              tuple([make_node(state, state[:X]), make_node(state, state[:X])])
+            )
+          end
+        })
+
+      refute empty?(nx)
+    end
+
+    test "mutual recursion" do
+      # X = {int,Y}|nil, Y = {bool,X}|nil: both not empty
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([boolean(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+      refute empty?(ny)
+
+      # X = {Y}, Y = {X}: both empty (no base case)
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:Y])]) end,
+          Y: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+      assert empty?(ny)
+
+      # X = {Y}|nil, Y = {X}: X not empty, Y not empty (Y can hold {nil})
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([make_node(state, state[:X])])
+          end
+        })
+
+      refute empty?(nx)
+      refute empty?(ny)
+    end
+
+    test "cycle detection" do
+      # direct self-reference: X = {X} is empty
+      %{X: nx} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+
+      # 2-cycle: X = {Y}, Y = {X}, both empty
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:Y])]) end,
+          Y: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+      assert empty?(ny)
+
+      # 3-cycle: X→Y→Z→X, no base case, all empty
+      %{X: nx, Y: ny, Z: nz} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:Y])]) end,
+          Y: fn state -> tuple([make_node(state, state[:Z])]) end,
+          Z: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+      assert empty?(ny)
+      assert empty?(nz)
+
+      # 3-cycle with nil base case on Z: none empty
+      %{X: nx, Y: ny, Z: nz} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:Y])]) end,
+          Y: fn state -> tuple([make_node(state, state[:Z])]) end,
+          Z: fn state ->
+            tuple([make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+      refute empty?(ny)
+      refute empty?(nz)
+
+      # 4-cycle: A→B→C→D→A, no base case, all empty
+      %{A: na, B: nb, C: nc, D: nd} =
+        recursive(%{
+          A: fn state -> tuple([make_node(state, state[:B])]) end,
+          B: fn state -> tuple([make_node(state, state[:C])]) end,
+          C: fn state -> tuple([make_node(state, state[:D])]) end,
+          D: fn state -> tuple([make_node(state, state[:A])]) end
+        })
+
+      assert empty?(na)
+      assert empty?(nb)
+      assert empty?(nc)
+      assert empty?(nd)
+
+      # 4-cycle with nil base case on D: none empty
+      %{A: na, B: nb, C: nc, D: nd} =
+        recursive(%{
+          A: fn state -> tuple([make_node(state, state[:B])]) end,
+          B: fn state -> tuple([make_node(state, state[:C])]) end,
+          C: fn state -> tuple([make_node(state, state[:D])]) end,
+          D: fn state ->
+            tuple([make_node(state, state[:A])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(na)
+      refute empty?(nb)
+      refute empty?(nc)
+      refute empty?(nd)
+    end
+
+    test "diamond patterns" do
+      # X->{Y,Z}, Y->{W}, Z->{W}, W->{X}
+      # the dependency graph has a diamond shape:
+      #
+      #       X
+      #      / \
+      #     Y   Z
+      #      \ /
+      #       W
+      #       |
+      #       X  (cycle)
+      #
+      # no base case: all empty
+      %{X: nx, Y: ny, Z: nz, W: nw} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:Y]), make_node(state, state[:Z])])
+          end,
+          Y: fn state -> tuple([make_node(state, state[:W])]) end,
+          Z: fn state -> tuple([make_node(state, state[:W])]) end,
+          W: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+      assert empty?(ny)
+      assert empty?(nz)
+      assert empty?(nw)
+
+      # same with base case on W: none empty
+      %{X: nx, Y: ny, Z: nz, W: nw} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:Y]), make_node(state, state[:Z])])
+          end,
+          Y: fn state -> tuple([make_node(state, state[:W])]) end,
+          Z: fn state -> tuple([make_node(state, state[:W])]) end,
+          W: fn state ->
+            tuple([make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+      refute empty?(ny)
+      refute empty?(nz)
+      refute empty?(nw)
+    end
+
+    test "recursive lists" do
+      # X = non_empty_list(integer(), X) | []: not empty
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(integer(), make_node(state, state[:X]))
+            |> union(empty_list())
+          end
+        })
+
+      refute empty?(nx)
+
+      # X = non_empty_list(X, []): empty (no scalar base)
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(make_node(state, state[:X]), empty_list())
+          end
+        })
+
+      assert empty?(nx)
+
+      # workaround encoding with union of constructors: not empty
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            union(
+              non_empty_list(integer(), make_node(state, state[:X])),
+              union(non_empty_list(integer(), empty_list()), empty_list())
+            )
+          end
+        })
+
+      refute empty?(nx)
+
+      # X = non_empty_list(X, []) | []
+      # Y = non_empty_list(Y, []) | non_empty_list(integer(), []) | []
+      nodes =
+        recursive(%{
+          x: fn state ->
+            union(
+              non_empty_list({make_ref(), state, state[:x]}, empty_list()),
+              empty_list()
+            )
+          end,
+          y: fn state ->
+            union(
+              union(
+                non_empty_list({make_ref(), state, state[:y]}, empty_list()),
+                non_empty_list(integer(), empty_list())
+              ),
+              empty_list()
+            )
+          end
+        })
+
+      nx = nodes[:x]
+      ny = nodes[:y]
+
+      # Just check if the difference is computable (without emptiness check)
+      d = difference(nx, ny)
+      assert empty?(d)
+      assert subtype?(nx, ny)
+    end
+
+    test "binary trees" do
+      # Tree = {atom, Tree, Tree} | nil: not empty
+      %{T: nt} =
+        recursive(%{
+          T: fn state ->
+            tuple([
+              atom(),
+              make_node(state, state[:T]),
+              make_node(state, state[:T])
+            ])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nt)
+    end
+
+    test "regular expressions (on lists)" do
+      # int_then_bool_list = {integer(), int_list} or bool_list
+      # bool_list = {boolean(), bool_list} or []
+      # int_or_bool_list = {integer() or boolean(), int_or_bool_list} or []
+      %{IntThenBoolList: int_then_bool_list, BoolList: bool_list, IntOrBoolList: int_or_bool_list} =
+        recursive(%{
+          IntThenBoolList: fn state ->
+            union(
+              tuple([integer(), make_node(state, state[:IntThenBoolList])]),
+              make_node(state, state[:BoolList])
+            )
+          end,
+          BoolList: fn state ->
+            union(
+              tuple([boolean(), make_node(state, state[:BoolList])]),
+              empty_list()
+            )
+          end,
+          IntOrBoolList: fn state ->
+            union(
+              tuple([union(integer(), boolean()), make_node(state, state[:IntOrBoolList])]),
+              empty_list()
+            )
+          end
+        })
+
+      refute empty?(int_then_bool_list)
+      refute empty?(bool_list)
+      refute empty?(int_or_bool_list)
+      assert subtype?(bool_list, int_or_bool_list)
+      assert subtype?(int_then_bool_list, int_or_bool_list)
+    end
+
+    test "regular expressions (on maps)" do
+      # bool_chain = %{val: boolean(), next: bool_chain} | %{}
+      # int_or_bool_chain = %{val: integer() | boolean(), next: int_or_bool_chain} | %{}
+      # int_then_bool_chain = %{val: integer(), next: int_then_bool_chain} | bool_chain
+      %{
+        IntThenBoolChain: int_then_bool_chain,
+        BoolChain: bool_chain,
+        IntOrBoolChain: int_or_bool_chain
+      } =
+        recursive(%{
+          IntThenBoolChain: fn state ->
+            union(
+              closed_map(val: integer(), next: make_node(state, state[:IntThenBoolChain])),
+              make_node(state, state[:BoolChain])
+            )
+          end,
+          BoolChain: fn state ->
+            union(
+              closed_map(val: boolean(), next: make_node(state, state[:BoolChain])),
+              empty_map()
+            )
+          end,
+          IntOrBoolChain: fn state ->
+            union(
+              closed_map(
+                val: union(integer(), boolean()),
+                next: make_node(state, state[:IntOrBoolChain])
+              ),
+              empty_map()
+            )
+          end
+        })
+
+      refute empty?(int_then_bool_chain)
+      refute empty?(bool_chain)
+      refute empty?(int_or_bool_chain)
+      assert subtype?(bool_chain, int_or_bool_chain)
+      assert subtype?(int_then_bool_chain, int_or_bool_chain)
+    end
+
+    test "regular expressions (on non-empty lists)" do
+      # bool_list = non_empty_list(boolean(), bool_list) | []
+      # int_or_bool_list = non_empty_list(integer() | boolean(), int_or_bool_list) | []
+      # int_then_bool_list = non_empty_list(integer(), int_then_bool_list) | bool_list
+      %{IntThenBoolList: int_then_bool_list, BoolList: bool_list, IntOrBoolList: int_or_bool_list} =
+        recursive(%{
+          IntThenBoolList: fn state ->
+            union(
+              non_empty_list(integer(), make_node(state, state[:IntThenBoolList])),
+              make_node(state, state[:BoolList])
+            )
+          end,
+          BoolList: fn state ->
+            union(
+              non_empty_list(boolean(), make_node(state, state[:BoolList])),
+              empty_list()
+            )
+          end,
+          IntOrBoolList: fn state ->
+            union(
+              non_empty_list(
+                union(integer(), boolean()),
+                make_node(state, state[:IntOrBoolList])
+              ),
+              empty_list()
+            )
+          end
+        })
+
+      refute empty?(int_then_bool_list)
+      refute empty?(bool_list)
+      refute empty?(int_or_bool_list)
+      assert subtype?(bool_list, int_or_bool_list)
+      assert subtype?(int_then_bool_list, int_or_bool_list)
+    end
+
+    test "mixed constructors" do
+      # X = {integer(), X} | non_empty_list(X, []) | nil: not empty
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            union(
+              tuple([integer(), make_node(state, state[:X])]),
+              union(
+                non_empty_list(make_node(state, state[:X]), empty_list()),
+                atom([nil])
+              )
+            )
+          end
+        })
+
+      refute empty?(nx)
+      assert subtype?(atom([nil]), nx)
+      assert subtype?(tuple([integer(), atom([nil])]), nx)
+    end
+
+    test "non-recursive equations" do
+      # X = integer(): not empty
+      %{X: nx} = recursive(%{X: fn _state -> integer() end})
+      refute empty?(nx)
+
+      # X = none(): empty
+      %{X: nx} = recursive(%{X: fn _state -> none() end})
+      assert empty?(nx)
+
+      # X = term(): not empty
+      %{X: nx} = recursive(%{X: fn _state -> :term end})
+      refute empty?(nx)
+
+      # empty equation map
+      result = recursive(%{})
+      assert result == %{}
+    end
+
+    test "difference of node with itself" do
+      # difference(node, node) is empty for non-recursive node
+      node = to_node(union(integer(), atom([nil])))
+      assert empty?(difference(node, node))
+    end
+  end
+
+  ## Subtyping on recursive types
+
+  describe "subtyping on recursive types" do
+    test "simple recursive list" do
+      # X = {integer(), X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # nil <: X
+      assert subtype?(atom([nil]), nx)
+
+      # {integer(), nil} <: X
+      assert subtype?(tuple([integer(), atom([nil])]), nx)
+
+      # {integer(), {integer(), nil}} <: X
+      inner = tuple([integer(), atom([nil])])
+      assert subtype?(tuple([integer(), inner]), nx)
+
+      # depth 3: {int, {int, {int, nil}}} <: X
+      d2 = tuple([integer(), inner])
+      assert subtype?(tuple([integer(), d2]), nx)
+
+      # depth 4
+      d3 = tuple([integer(), d2])
+      assert subtype?(tuple([integer(), d3]), nx)
+
+      # atom(:foo) is not a subtype
+      refute subtype?(atom([:foo]), nx)
+
+      # a plain integer is not a subtype
+      refute subtype?(integer(), nx)
+
+      # wrong element type: {float(), nil}
+      refute subtype?(tuple([float(), atom([nil])]), nx)
+
+      # {integer(), atom(:foo)}: :foo is not X
+      refute subtype?(tuple([integer(), atom([:foo])]), nx)
+
+      # union of finite unfoldings is a subtype
+      d1 = tuple([integer(), atom([nil])])
+      d2 = tuple([integer(), d1])
+      assert subtype?(union(atom([nil]), union(d1, d2)), nx)
+
+      # X <: term()
+      assert subtype?(nx, :term)
+
+      # none() <: X
+      assert subtype?(none(), nx)
+    end
+
+    test "mutual recursion" do
+      # X = {int, Y} | nil, Y = {bool, X} | nil
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([boolean(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # nil <: X, nil <: Y
+      assert subtype?(atom([nil]), nx)
+      assert subtype?(atom([nil]), ny)
+
+      # {integer(), nil} <: X
+      assert subtype?(tuple([integer(), atom([nil])]), nx)
+
+      # {boolean(), nil} <: Y
+      assert subtype?(tuple([boolean(), atom([nil])]), ny)
+
+      # {int, {bool, nil}} <: X
+      inner_y = tuple([boolean(), atom([nil])])
+      assert subtype?(tuple([integer(), inner_y]), nx)
+
+      # {bool, {int, nil}} <: Y
+      inner_x = tuple([integer(), atom([nil])])
+      assert subtype?(tuple([boolean(), inner_x]), ny)
+
+      # {int, {bool, {int, nil}}} <: X
+      level3 = tuple([integer(), atom([nil])])
+      level2 = tuple([boolean(), level3])
+      assert subtype?(tuple([integer(), level2]), nx)
+
+      # both X and Y <: term()
+      assert subtype?(nx, :term)
+      assert subtype?(ny, :term)
+    end
+
+    test "recursive lists" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(integer(), make_node(state, state[:X]))
+            |> union(empty_list())
+          end
+        })
+
+      # [] <: X
+      assert subtype?(empty_list(), nx)
+
+      # non_empty_list(integer()) <: X (terminates with [])
+      assert subtype?(non_empty_list(integer()), nx)
+    end
+
+    test "binary trees" do
+      %{T: nt} =
+        recursive(%{
+          T: fn state ->
+            tuple([
+              integer(),
+              make_node(state, state[:T]),
+              make_node(state, state[:T])
+            ])
+            |> union(atom([nil]))
+          end
+        })
+
+      # nil is a valid tree
+      assert subtype?(atom([nil]), nt)
+
+      # {42, nil, nil} is a valid tree
+      assert subtype?(tuple([integer(), atom([nil]), atom([nil])]), nt)
+
+      # {1, {2, nil, nil}, {3, nil, nil}} is a valid tree
+      leaf = tuple([integer(), atom([nil]), atom([nil])])
+      assert subtype?(tuple([integer(), leaf, leaf]), nt)
+
+      # wrong arity: {1, nil} not a subtype
+      refute subtype?(tuple([integer(), atom([nil])]), nt)
+
+      # wrong tag type: {float, nil, nil} not a subtype
+      refute subtype?(tuple([float(), atom([nil]), atom([nil])]), nt)
+    end
+
+    test "expression trees" do
+      # Expr = integer() | {atom, Expr, Expr}, Binop = {atom, Expr, Expr}
+      %{Expr: nexpr, Binop: nbinop} =
+        recursive(%{
+          Expr: fn state ->
+            union(
+              integer(),
+              tuple([
+                atom(),
+                make_node(state, state[:Expr]),
+                make_node(state, state[:Expr])
+              ])
+            )
+          end,
+          Binop: fn state ->
+            tuple([atom(), make_node(state, state[:Expr]), make_node(state, state[:Expr])])
+          end
+        })
+
+      refute empty?(nexpr)
+      refute empty?(nbinop)
+
+      # 42 is an Expr
+      assert subtype?(integer(), nexpr)
+
+      # {:+, 1, 2} is an Expr and a Binop
+      assert subtype?(tuple([atom(), integer(), integer()]), nexpr)
+      assert subtype?(tuple([atom(), integer(), integer()]), nbinop)
+
+      # {:*, {:+, 1, 2}, 3} is an Expr
+      inner = tuple([atom(), integer(), integer()])
+      assert subtype?(tuple([atom(), inner, integer()]), nexpr)
+    end
+
+    test "disjoint?" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # recursive type is disjoint from unrelated scalars
+      assert disjoint?(nx, float())
+      assert disjoint?(nx, binary())
+      assert disjoint?(nx, pid())
+
+      # not disjoint from base case
+      refute disjoint?(nx, atom([nil]))
+
+      # not disjoint from tuple()
+      refute disjoint?(nx, tuple())
+    end
+  end
+
+  ## Set operations on recursive types
+
+  describe "set operations on recursive types" do
+    test "union" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # union with none() is identity
+      assert equal?(union(nx, none()), nx)
+
+      # union of two distinct recursive types is not empty
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            tuple([float(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(union(nx, ny))
+
+      # union of stepped recursive type with another type
+      dx = to_descr(nx)
+      refute empty?(union(dx, float()))
+    end
+
+    test "intersection" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # intersection with term() is identity
+      assert equal?(intersection(nx, :term), nx)
+
+      # intersection with disjoint type is empty
+      assert empty?(intersection(nx, float()))
+
+      # intersection of two recursive types sharing base case is not empty
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            tuple([float(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(intersection(nx, ny))
+
+      # intersection of stepped type with its base case
+      dx = to_descr(nx)
+      assert equal?(intersection(dx, atom()), atom([nil]))
+    end
+
+    test "difference" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # difference of stepped type minus base case: only tuple part remains
+      dx = to_descr(nx)
+      result = difference(dx, atom([nil]))
+      assert is_map_key(result, :tuple)
+      refute is_map_key(result, :atom)
+    end
+  end
+
+  ## Recursive type edge cases
+
+  describe "recursive type edge cases" do
+    test "non-recursive equations" do
+      # X = integer()
+      %{X: nx} = recursive(%{X: fn _state -> integer() end})
+      assert equal?(to_descr(nx), integer())
+
+      # X = none()
+      %{X: nx} = recursive(%{X: fn _state -> none() end})
+      assert empty?(nx)
+
+      # X = term()
+      %{X: nx} = recursive(%{X: fn _state -> :term end})
+      assert equal?(to_descr(nx), :term)
+
+      # two independent non-recursive equations
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn _state -> integer() end,
+          Y: fn _state -> atom() end
+        })
+
+      assert equal?(to_descr(nx), integer())
+      assert equal?(to_descr(ny), atom())
+
+      # compound type
+      %{X: nx} =
+        recursive(%{
+          X: fn _state -> union(integer(), tuple([atom(), float()])) end
+        })
+
+      assert equal?(to_descr(nx), union(integer(), tuple([atom(), float()])))
+    end
+
+    test "multiple base cases" do
+      # X = {int, X} | nil | :done | :error
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil, :done, :error]))
+          end
+        })
+
+      refute empty?(nx)
+      assert subtype?(atom([nil]), nx)
+      assert subtype?(atom([:done]), nx)
+      assert subtype?(atom([:error]), nx)
+    end
+
+    test "broad tuple elements" do
+      # X = {term(), X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([:term, make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+      assert subtype?(tuple([:term, atom([nil])]), nx)
+    end
+
+    test "parallel independent recursion" do
+      # X = {int, X}|nil, Y = {float, Y}|nil (independent)
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([float(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end
+        })
+
+      refute empty?(nx)
+      refute empty?(ny)
+
+      # they share a state but are independent types
+      assert subtype?(tuple([integer(), atom([nil])]), nx)
+      assert subtype?(tuple([float(), atom([nil])]), ny)
+      refute subtype?(tuple([float(), atom([nil])]), nx)
+      refute subtype?(tuple([integer(), atom([nil])]), ny)
+    end
+
+    test "empty equation map" do
+      result = recursive(%{})
+      assert result == %{}
+    end
+
+    test "node identity" do
+      # each node from recursive/1 gets a unique id
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([boolean(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      {id_x, _, _} = nx
+      {id_y, _, _} = ny
+      assert id_x != id_y
+
+      # make_ref ensures distinct ids even for same generator
+      gen = fn _state -> integer() end
+      {id1, _, _} = make_node(%{}, gen)
+      {id2, _, _} = make_node(%{}, gen)
+      assert id1 != id2
+
+      # memoization prevents infinite loop on cyclic X = {X}
+      %{X: nx} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+
+      # memoization prevents infinite loop on mutual cycle X = {Y}, Y = {X}
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn state -> tuple([make_node(state, state[:Y])]) end,
+          Y: fn state -> tuple([make_node(state, state[:X])]) end
+        })
+
+      assert empty?(nx)
+      assert empty?(ny)
+    end
+
+    test "stepping recursive nodes" do
+      # stepping produces a descr with :tuple and :atom keys
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      d = to_descr(nx)
+      assert is_map_key(d, :tuple)
+      assert is_map_key(d, :atom)
+
+      # stepping twice does not crash (coinductive laziness)
+      d1 = to_descr(nx)
+      assert is_map(d1)
+      d2 = to_descr(nx)
+      assert is_map(d2)
+    end
+  end
+
+  ## Cross-recursive subtyping (two-node blind spots)
+
+  describe "cross-recursive subtyping" do
+    test "list tail recursion: X <: Y where both recurse in tail position" do
+      # X = non_empty_list(integer(), X) | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(integer(), make_node(state, state[:X]))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = non_empty_list(integer(), Y) | non_empty_list(integer(), nil) | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            non_empty_list(integer(), make_node(state, state[:Y]))
+            |> union(non_empty_list(integer(), atom([nil])))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "list element recursion: X <: Y where both recurse in element type" do
+      # X = [X] | nil  (list whose elements are themselves X)
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(make_node(state, state[:X]))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = [Y] | [integer()] | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            non_empty_list(make_node(state, state[:Y]))
+            |> union(non_empty_list(integer()))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "list negative case: recursive list is NOT subtype of unrelated type" do
+      # X = non_empty_list(integer(), X) | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(integer(), make_node(state, state[:X]))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = non_empty_list(float()) | nil (different element type)
+      ny = union(non_empty_list(float()), atom([nil]))
+
+      refute subtype?(nx, ny)
+    end
+
+    test "tuple element recursion: X <: Y where both recurse in element" do
+      # X = {X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = {Y} | {integer()} | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            tuple([make_node(state, state[:Y])])
+            |> union(tuple([integer()]))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "map value recursion: X <: Y where both recurse in field value" do
+      # X = %{a: X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            closed_map(a: make_node(state, state[:X]))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = %{a: Y} | %{a: integer()} | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            closed_map(a: make_node(state, state[:Y]))
+            |> union(closed_map(a: integer()))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "mutual recursion across systems" do
+      # X = {Y} | nil, Y = {X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            tuple([make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # A = {B} | nil, B = {A} | {integer()} | nil
+      %{A: na} =
+        recursive(%{
+          A: fn state ->
+            tuple([make_node(state, state[:B])])
+            |> union(atom([nil]))
+          end,
+          B: fn state ->
+            tuple([make_node(state, state[:A])])
+            |> union(tuple([integer()]))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, na)
+    end
+
+    test "tuple negative: recursive tuple NOT subtype of finite tuple" do
+      # X = {X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      ny = union(tuple([integer()]), atom([nil]))
+      refute subtype?(nx, ny)
+    end
+
+    test "tuple 2-element, recursive in 2nd position" do
+      # X = {int, X} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([integer(), make_node(state, state[:X])])
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = {int, Y} | {int, nil} | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            tuple([integer(), make_node(state, state[:Y])])
+            |> union(tuple([integer(), atom([nil])]))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "map negative: recursive map NOT subtype when base cases differ" do
+      # X = %{a: X} | %{a: atom()}
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            closed_map(a: make_node(state, state[:X]))
+            |> union(closed_map(a: atom()))
+          end
+        })
+
+      # Y = %{a: Y} | %{a: integer()}
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            closed_map(a: make_node(state, state[:Y]))
+            |> union(closed_map(a: integer()))
+          end
+        })
+
+      refute subtype?(nx, ny)
+    end
+
+    test "list element negative: recursive list NOT subtype when base cases differ" do
+      # X = [X] | [atom()] | []
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(make_node(state, state[:X]))
+            |> union(non_empty_list(atom()))
+            |> union(empty_list())
+          end
+        })
+
+      # Y = [Y] | [integer()] | []
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            non_empty_list(make_node(state, state[:Y]))
+            |> union(non_empty_list(integer()))
+            |> union(empty_list())
+          end
+        })
+
+      refute subtype?(nx, ny)
+    end
+
+    test "same-shape recursive list: BoolList <: IntOrBoolList" do
+      # BoolList = non_empty_list(boolean(), BoolList) | []
+      # IntOrBoolList = non_empty_list(integer() | boolean(), IntOrBoolList) | []
+      %{BoolList: bl, IntOrBoolList: iobl} =
+        recursive(%{
+          BoolList: fn state ->
+            non_empty_list(boolean(), make_node(state, state[:BoolList]))
+            |> union(empty_list())
+          end,
+          IntOrBoolList: fn state ->
+            non_empty_list(union(integer(), boolean()), make_node(state, state[:IntOrBoolList]))
+            |> union(empty_list())
+          end
+        })
+
+      assert subtype?(bl, iobl)
+    end
+
+    test "recursive list with different tail: IntThenBoolList <: IntOrBoolList" do
+      # IntThenBoolList = non_empty_list(integer(), IntThenBoolList) | BoolList
+      # BoolList = non_empty_list(boolean(), BoolList) | []
+      # IntOrBoolList = non_empty_list(integer() | boolean(), IntOrBoolList) | []
+      %{IntThenBoolList: itbl, IntOrBoolList: iobl} =
+        recursive(%{
+          IntThenBoolList: fn state ->
+            non_empty_list(integer(), make_node(state, state[:IntThenBoolList]))
+            |> union(make_node(state, state[:BoolList]))
+          end,
+          BoolList: fn state ->
+            non_empty_list(boolean(), make_node(state, state[:BoolList]))
+            |> union(empty_list())
+          end,
+          IntOrBoolList: fn state ->
+            non_empty_list(union(integer(), boolean()), make_node(state, state[:IntOrBoolList]))
+            |> union(empty_list())
+          end
+        })
+
+      assert subtype?(itbl, iobl)
+    end
+
+    test "map linked list: BoolChain <: IntOrBoolChain" do
+      # BoolChain = %{val: boolean(), next: BoolChain} | %{}
+      # IntOrBoolChain = %{val: integer() | boolean(), next: IntOrBoolChain} | %{}
+      %{BoolChain: bc, IntOrBoolChain: iobc} =
+        recursive(%{
+          BoolChain: fn state ->
+            closed_map(val: boolean(), next: make_node(state, state[:BoolChain]))
+            |> union(empty_map())
+          end,
+          IntOrBoolChain: fn state ->
+            closed_map(
+              val: union(integer(), boolean()),
+              next: make_node(state, state[:IntOrBoolChain])
+            )
+            |> union(empty_map())
+          end
+        })
+
+      assert subtype?(bc, iobc)
+    end
+
+    test "cross-container mutual recursion: tuple + list" do
+      # X = {Y} | nil, Y = [X]
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([make_node(state, state[:Y])])
+            |> union(atom([nil]))
+          end,
+          Y: fn state ->
+            non_empty_list(make_node(state, state[:X]), empty_list())
+            |> union(empty_list())
+          end
+        })
+
+      # A = {B} | {[integer()]} | nil, B = [A] | [integer()]
+      %{A: na} =
+        recursive(%{
+          A: fn state ->
+            tuple([make_node(state, state[:B])])
+            |> union(tuple([non_empty_list(integer(), empty_list())]))
+            |> union(atom([nil]))
+          end,
+          B: fn state ->
+            non_empty_list(make_node(state, state[:A]), empty_list())
+            |> union(non_empty_list(integer(), empty_list()))
+            |> union(empty_list())
+          end
+        })
+
+      assert subtype?(nx, na)
+    end
+
+    # TODO: nested container recursion — node is inside a tuple inside a tuple.
+    # X = {{X}} | nil, Y = {{Y}} | {{integer()}} | nil
+    # @tag :skip
+    test "nested tuple wrapping tuple with recursive element" do
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            tuple([tuple([make_node(state, state[:X])])])
+            |> union(atom([nil]))
+          end
+        })
+
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            tuple([tuple([make_node(state, state[:Y])])])
+            |> union(tuple([tuple([integer()])]))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "nested map wrapping map with recursive field" do
+      # X = %{outer: %{inner: X}} | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            closed_map(outer: closed_map(inner: make_node(state, state[:X])))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = %{outer: %{inner: Y}} | %{outer: %{inner: integer()}} | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            closed_map(outer: closed_map(inner: make_node(state, state[:Y])))
+            |> union(closed_map(outer: closed_map(inner: integer())))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "nested map negative with recursive field" do
+      # X = %{outer: %{inner: X}} | %{outer: %{inner: atom()}}
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            closed_map(outer: closed_map(inner: make_node(state, state[:X])))
+            |> union(closed_map(outer: closed_map(inner: atom())))
+          end
+        })
+
+      # Y = %{outer: %{inner: Y}} | %{outer: %{inner: integer()}}
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            closed_map(outer: closed_map(inner: make_node(state, state[:Y])))
+            |> union(closed_map(outer: closed_map(inner: integer())))
+          end
+        })
+
+      refute subtype?(nx, ny)
+    end
+
+    test "nested list wrapping list with recursive element" do
+      # X = [[X]] | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(
+              non_empty_list(make_node(state, state[:X]), empty_list()),
+              empty_list()
+            )
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = [[Y]] | [[integer()]] | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            non_empty_list(
+              non_empty_list(make_node(state, state[:Y]), empty_list()),
+              empty_list()
+            )
+            |> union(non_empty_list(non_empty_list(integer(), empty_list()), empty_list()))
+            |> union(atom([nil]))
+          end
+        })
+
+      assert subtype?(nx, ny)
+    end
+
+    test "nested list negative with recursive element" do
+      # X = [[X]] | [[atom()]] | nil
+      %{X: nx} =
+        recursive(%{
+          X: fn state ->
+            non_empty_list(
+              non_empty_list(make_node(state, state[:X]), empty_list()),
+              empty_list()
+            )
+            |> union(non_empty_list(non_empty_list(atom(), empty_list()), empty_list()))
+            |> union(atom([nil]))
+          end
+        })
+
+      # Y = [[Y]] | [[integer()]] | nil
+      %{Y: ny} =
+        recursive(%{
+          Y: fn state ->
+            non_empty_list(
+              non_empty_list(make_node(state, state[:Y]), empty_list()),
+              empty_list()
+            )
+            |> union(non_empty_list(non_empty_list(integer(), empty_list()), empty_list()))
+            |> union(atom([nil]))
+          end
+        })
+
+      refute subtype?(nx, ny)
+    end
+  end
 end

From e0beb905d06f0ec0916077e245956cbf5e0dfc2b Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 31 Mar 2026 00:00:54 +0200
Subject: [PATCH 6/6] Clean up tests and change 'fn state' to 'fn recur'

---
 lib/elixir/lib/module/types/descr.ex          |  446 ++--
 .../test/elixir/module/types/descr_test.exs   | 1967 +++++------------
 2 files changed, 818 insertions(+), 1595 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 355132785e5..8bd08de2511 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -83,7 +83,7 @@ defmodule Module.Types.Descr do
 
   @compile {:inline, unfold: 1}
   defp unfold(:term), do: unfolded_term()
-  defp unfold({_id, state, generator}), do: generator.(state) |> unfold()
+  defp unfold({_id, _state, _generator} = node), do: to_descr(node) |> unfold()
   defp unfold(other), do: other
   defp unfolded_term, do: @term
 
@@ -115,7 +115,7 @@ defmodule Module.Types.Descr do
 
   # @spec descr() :: map() | :term
   # @spec state() :: map()
-  # @spec node() :: {id :: reference(), state :: map(), generator :: (state() -> node())}
+  # @spec node() :: {id :: reference(), state :: map(), generator :: ((atom() -> node()) -> node())}
   def make_node(state, generator), do: {make_ref(), state, generator}
 
   # @spec to_node(descr :: descr() | node()) :: node()
@@ -125,7 +125,11 @@ defmodule Module.Types.Descr do
 
   def to_descr(:term), do: :term
   def to_descr(descr = %{}), do: descr
-  def to_descr({_id, state, generator}), do: generator.(state)
+
+  def to_descr({_id, state, generator}) do
+    recur = fn name -> make_node(state, state[name]) end
+    generator.(recur)
+  end
 
   # Collect generator functions embedded in a type (node, descr, or :term).
   # Walks BDD leaves without unfolding any nodes. Returns a list of generators.
@@ -162,8 +166,9 @@ defmodule Module.Types.Descr do
   defp collect_generators_from_bdd(:bdd_bot, _leaf_fn), do: []
   defp collect_generators_from_bdd({_, _} = leaf, leaf_fn), do: leaf_fn.(leaf)
 
-  defp collect_generators_from_bdd({_lit, c, u, d}, leaf_fn) do
-    collect_generators_from_bdd(c, leaf_fn) ++
+  defp collect_generators_from_bdd({lit, c, u, d}, leaf_fn) do
+    leaf_fn.(lit) ++
+      collect_generators_from_bdd(c, leaf_fn) ++
       collect_generators_from_bdd(u, leaf_fn) ++
       collect_generators_from_bdd(d, leaf_fn)
   end
@@ -179,8 +184,13 @@ defmodule Module.Types.Descr do
   end
 
   # Map leaf: {tag, %{key => value, ...}} or {%{domains}, %{fields}}
-  defp collect_generators_map_leaf({_tag, fields}) when is_map(fields) do
-    :maps.fold(fn _k, v, acc -> collect_generators(v) ++ acc end, [], fields)
+  defp collect_generators_map_leaf({tag, fields}) when is_map(fields) do
+    field_gens = :maps.fold(fn _k, v, acc -> collect_generators(v) ++ acc end, [], fields)
+
+    case tag do
+      %{} -> :maps.fold(fn _k, v, acc -> collect_generators(v) ++ acc end, field_gens, tag)
+      _ -> field_gens
+    end
   end
 
   defp collect_generators_map_leaf(_), do: []
@@ -228,8 +238,7 @@ defmodule Module.Types.Descr do
   Builds recursive type nodes from a set of mutually recursive equations.
 
   Takes a map `%{name => generator}` where each generator is a function
-  `fn state -> descr` that may refer to recursion variables by building
-  nodes from the state: `{make_ref(), state, state[name]}`.
+  `fn recur -> descr` and `recur.(name)` builds the recursive node for `name`.
 
   Returns a map `%{name => node}` with one self-contained node per variable.
 
@@ -246,20 +255,20 @@ defmodule Module.Types.Descr do
 
   Correct: node inside a constructor, set operations on the result:
 
-      tuple([integer(), {make_ref(), state, state[:X]}])
+      tuple([integer(), recur.(:X)])
       |> union(atom([:nil]))
 
   Wrong: node passed directly to a set operation:
 
-      union({make_ref(), state, state[:X]}, atom([:nil]))
+      union(recur.(:X), atom([:nil]))
 
   ## Example
 
   The recursive type `X = {integer(), X} | nil` is defined as:
 
       %{X: node_x} = recursive(%{
-        X: fn state ->
-          tuple([integer(), {make_ref(), state, state[:X]}])
+        X: fn recur ->
+          tuple([integer(), recur.(:X)])
           |> union(atom([:nil]))
         end
       })
@@ -267,19 +276,19 @@ defmodule Module.Types.Descr do
   For mutually recursive types `X = {int, Y} | nil` and `Y = {bool, X} | nil`:
 
       %{X: node_x, Y: node_y} = recursive(%{
-        X: fn state ->
-          tuple([integer(), {make_ref(), state, state[:Y]}])
+        X: fn recur ->
+          tuple([integer(), recur.(:Y)])
           |> union(atom([:nil]))
         end,
-        Y: fn state ->
-          tuple([boolean(), {make_ref(), state, state[:X]}])
+        Y: fn recur ->
+          tuple([boolean(), recur.(:X)])
           |> union(atom([:nil]))
         end
       })
   """
   def recursive(equations) when is_map(equations) do
-    # The generators ARE the state: each variable maps to its generator function.
-    # This is the state map from Section 4, Step 3.
+    # The generators are the recursive environment: each variable maps to its
+    # generator function and is resolved lazily via recur.(name).
     state = equations
 
     # Step 4: build one node per variable with the shared state.
@@ -538,7 +547,7 @@ defmodule Module.Types.Descr do
   Returns true if the type has a gradual part.
   """
   def gradual?(:term), do: false
-  def gradual?({_id, state, generator}), do: gradual?(generator.(state))
+  def gradual?({_id, _state, _generator} = node), do: gradual?(to_descr(node))
   def gradual?(descr), do: is_map_key(descr, :dynamic)
 
   @doc """
@@ -708,15 +717,40 @@ defmodule Module.Types.Descr do
 
   defp iterator_difference_static(:none, map), do: map
 
-  # Returning 0 from the callback is taken as none() for that subtype.
-  defp difference(:atom, v1, v2), do: atom_difference(v1, v2)
-  defp difference(:bitmap, v1, v2), do: v1 - (v1 &&& v2)
+  # Fused difference + emptiness check that short-circuits per-key.
+  # This is Algorithm 1 from Laurent & Nguyen, fused with subtyping.
+  defp empty_difference_subtype?(%{dynamic: dyn_left} = left, %{dynamic: dyn_right} = right) do
+    empty_difference_subtype?(dyn_left, dyn_right) and
+      empty_difference_subtype?(Map.delete(left, :dynamic), Map.delete(right, :dynamic))
+  end
 
-  defp difference(:dynamic, v1, v2) do
-    descr = difference_static(v1, v2)
-    if descr == @none, do: 0, else: descr
+  defp empty_difference_subtype?(left, :term), do: keep_optional(left) == @none
+
+  defp empty_difference_subtype?(left, right) do
+    iterator_empty_difference_subtype?(
+      :maps.next(:maps.iterator(unfold(left))),
+      unfold(right),
+      %{}
+    )
+  end
+
+  defp iterator_empty_difference_subtype?({key, v1, iterator}, map, seen) do
+    case map do
+      %{^key => v2} ->
+        value = difference(key, v1, v2)
+        value in @empty_difference or empty_key?(key, value, seen)
+
+      %{} ->
+        empty_key?(key, v1, seen)
+    end and
+      iterator_empty_difference_subtype?(:maps.next(iterator), map, seen)
   end
 
+  defp iterator_empty_difference_subtype?(:none, _map, _seen), do: true
+
+  # Returning 0 from the callback is taken as none() for that subtype.
+  defp difference(:atom, v1, v2), do: atom_difference(v1, v2)
+  defp difference(:bitmap, v1, v2), do: v1 - (v1 &&& v2)
   defp difference(:list, v1, v2), do: list_difference(v1, v2)
   defp difference(:map, v1, v2), do: map_difference(v1, v2)
   defp difference(:optional, 1, 1), do: 0
@@ -779,17 +813,15 @@ defmodule Module.Types.Descr do
   end
 
   # Node: check for cycle via generator identity, then unfold
-  defp empty_seen?({_id, state, generator}, seen) do
+  defp empty_seen?({_id, _state, generator} = node, seen) do
     if :erlang.is_map_key(generator, seen) do
       true
     else
       seen = Map.put(seen, generator, true)
-      empty_seen?(generator.(state), seen)
+      empty_seen?(to_descr(node), seen)
     end
   end
 
-  defp empty_or_optional?(type), do: empty?(remove_optional(type))
-
   # For atom, bitmap, tuple, and optional, if the key is present,
   # then they are not empty,
   defp empty_key?(:fun, value, seen), do: fun_empty?(value, seen)
@@ -1025,92 +1057,9 @@ defmodule Module.Types.Descr do
   defp subtype_static?(same, same), do: true
   defp subtype_static?(left, right), do: empty_difference_subtype?(left, right)
 
-  # Fused difference + emptiness check that short-circuits per-key.
-  # This is Algorithm 1 from Laurent & Nguyen, fused with subtyping.
-  defp empty_difference_subtype?(%{dynamic: dyn_left} = left, %{dynamic: dyn_right} = right) do
-    empty_difference_subtype?(dyn_left, dyn_right) and
-      empty_difference_subtype?(Map.delete(left, :dynamic), Map.delete(right, :dynamic))
-  end
-
-  defp empty_difference_subtype?(left, :term), do: keep_optional(left) == @none
-
-  defp empty_difference_subtype?(left, right) do
-    iterator_empty_difference_subtype?(
-      :maps.next(:maps.iterator(unfold(left))),
-      unfold(right),
-      %{}
-    )
-  end
-
-  defp iterator_empty_difference_subtype?({key, v1, iterator}, map, seen) do
-    case map do
-      %{^key => v2} ->
-        value = difference(key, v1, v2)
-        value in @empty_difference or empty_key?(key, value, seen)
-
-      %{} ->
-        empty_key?(key, v1, seen)
-    end and
-      iterator_empty_difference_subtype?(:maps.next(iterator), map, seen)
-  end
-
-  defp iterator_empty_difference_subtype?(:none, _map, _seen), do: true
-
   # Recursive subtype check that reuses the unary emptiness memo by reducing
   # subtyping to emptiness of the set difference under the current `seen` map.
-  defp subtype_seen?(left, right, seen) do
-    do_subtype_seen?(unfold(left), unfold(right), seen)
-  end
-
-  defp do_subtype_seen?(left, right, seen) do
-    is_grad_left = gradual?(left)
-    is_grad_right = gradual?(right)
-
-    cond do
-      is_grad_left and not is_grad_right ->
-        left_dynamic = Map.get(left, :dynamic)
-        subtype_static_seen?(left_dynamic, right, seen)
-
-      is_grad_right and not is_grad_left ->
-        right_static = Map.delete(right, :dynamic)
-        subtype_static_seen?(left, right_static, seen)
-
-      is_grad_left ->
-        subtype_static_seen?(Map.get(left, :dynamic), Map.get(right, :dynamic), seen) and
-          subtype_static_seen?(Map.delete(left, :dynamic), Map.delete(right, :dynamic), seen)
-
-      true ->
-        subtype_static_seen?(left, right, seen)
-    end
-  end
-
-  defp subtype_static_seen?(same, same, _seen), do: true
-
-  defp subtype_static_seen?(left, right, seen),
-    do: empty_difference_subtype_seen?(left, right, seen)
-
-  # Fused difference + emptiness with the caller's coinductive context.
-  # Mirrors empty_difference_subtype? but passes `seen` for memoization.
-  # We must register a memo key for the overall difference before iterating,
-  # so that recursive encounters with the same subtype obligation short-circuit.
-  defp empty_difference_subtype_seen?(left, :term, _seen), do: keep_optional(left) == @none
-
-  defp empty_difference_subtype_seen?(left, right, seen) do
-    diff = difference_static(left, right)
-    key = empty_memo_key(diff)
-
-    if :erlang.is_map_key(key, seen) do
-      true
-    else
-      seen = Map.put(seen, key, true)
-
-      iterator_empty_difference_subtype?(
-        :maps.next(:maps.iterator(unfold(left))),
-        unfold(right),
-        seen
-      )
-    end
-  end
+  defp subtype_seen?(left, right, seen), do: empty_seen?(difference(left, right), seen)
 
   @doc """
   Check if a type is equal to another.
@@ -1846,7 +1795,7 @@ defmodule Module.Types.Descr do
     Enum.any?(negatives, fn {neg_arguments, neg_return} ->
       # Check if the negative function's domain is a supertype of the positive
       # domain and if the phi function determines emptiness.
-      subtype?(args_to_domain(neg_arguments), fetch_domain(positives)) and
+      subtype_seen?(args_to_domain(neg_arguments), fetch_domain(positives), seen) and
         phi_starter(neg_arguments, neg_return, positives, seen)
     end)
   end
@@ -2361,8 +2310,8 @@ defmodule Module.Types.Descr do
 
   defp list_tail_unfold(:term), do: @not_non_empty_list
 
-  defp list_tail_unfold({id, state, gen}) when is_reference(id),
-    do: Map.delete(gen.(state), :list)
+  defp list_tail_unfold({id, _state, _gen} = node) when is_reference(id),
+    do: Map.delete(to_descr(node), :list)
 
   defp list_tail_unfold(other), do: Map.delete(other, :list)
 
@@ -2488,6 +2437,18 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # X = {int, X} | nil
+  # %{X: fn recur -> tuple([int(), recur.(X)]) |> union(atom([nil]))
+  # %{X: fn recur -> tuple([int(), recur.(X)])|> intersection(tuple([int(), float()])
+
+  # {int, X}  /\ {int, float}
+
+  # X = list(list(X, [])) and list(list(Y, []))
+  # X & Y
+  # X & Y
+  # X \ Y
+  # X | Y
+
   defp list_leaf_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
     has_node =
       collect_generators(list1) != [] or
@@ -2968,6 +2929,14 @@ defmodule Module.Types.Descr do
     map_descr_pairs(rest, [{key, node} | fields], domain, dynamic?)
   end
 
+  defp map_descr_pairs([{key, {id, _state, _gen} = node} | rest], fields, domain, dynamic?)
+       when is_reference(id) do
+    # For domain keys, store node directly. We cannot call if_set/union on nodes
+    # as those would unfold the generator and loop during construction.
+    domain = Enum.reduce(key, domain, fn k, acc when is_atom(k) -> Map.put(acc, k, node) end)
+    map_descr_pairs(rest, fields, domain, dynamic?)
+  end
+
   defp map_descr_pairs([{key, value} | rest], fields, domain, dynamic?) do
     value_descr = to_descr(value)
 
@@ -3034,25 +3003,37 @@ defmodule Module.Types.Descr do
   defp map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
   defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do
-    case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do
-      :all_equal ->
-        map1
+    has_node =
+      :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, pos1) or
+        :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, pos2) or
+        (is_map(tag1) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, tag1)) or
+        (is_map(tag2) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, tag2))
 
-      :any_map ->
-        {:open, %{}, []}
+    if has_node do
+      nil
+    else
+      case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do
+        :all_equal ->
+          map1
 
-      {:one_key_difference, key, v1, v2} ->
-        new_pos = Map.put(pos1, key, union(v1, v2))
-        {tag1, new_pos, []}
+        :any_map ->
+          {:open, %{}, []}
 
-      :left_subtype_of_right ->
-        map2
+        {:one_key_difference, key, v1, v2} ->
+          new_pos = Map.put(pos1, key, union(v1, v2))
+          {tag1, new_pos, []}
 
-      :right_subtype_of_left ->
-        map1
+        :left_subtype_of_right ->
+          map2
 
-      nil ->
-        nil
+        :right_subtype_of_left ->
+          map1
+
+        nil ->
+          nil
+      end
     end
   end
 
@@ -3099,6 +3080,7 @@ defmodule Module.Types.Descr do
   defp do_map_union_optimization_strategy({key, v1, iterator}, pos2, status) do
     case pos2 do
       %{^key => {id, _, _}} when is_reference(id) ->
+        # Abort the optimization when a recursive node is encountered
         nil
 
       _ ->
@@ -3191,35 +3173,62 @@ defmodule Module.Types.Descr do
     bdd_intersection(bdd1, bdd2)
   end
 
-  defp map_leaf_intersection(bdd_leaf(tag1, fields1), bdd_leaf(tag2, fields2)) do
-    try do
-      {tag, fields} = map_literal_intersection(tag1, fields1, tag2, fields2)
-      bdd_leaf(tag, fields)
-    catch
-      :empty -> :bdd_bot
+  defp map_leaf_intersection(bdd_leaf(tag1, fields1) = l1, bdd_leaf(tag2, fields2) = l2) do
+    has_node =
+      :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, fields1) or
+        :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, fields2) or
+        (is_map(tag1) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, tag1)) or
+        (is_map(tag2) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, tag2))
+
+    if has_node do
+      bdd_intersection(l1, l2)
+    else
+      try do
+        {tag, fields} = map_literal_intersection(tag1, fields1, tag2, fields2)
+        bdd_leaf(tag, fields)
+      catch
+        :empty -> :bdd_bot
+      end
     end
   end
 
+  # When bdd_leaf_intersection recurses with a BDD tree (from previous has_node fallback)
+  defp map_leaf_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2)
+
   # Optimizations on single maps.
   defp map_difference(bdd_leaf(tag, fields) = map1, bdd_leaf(neg_tag, neg_fields) = map2) do
-    # Case 1: we are removing an open map with one field. Just do the difference of that field.
-    if neg_tag == :open and map_size(neg_fields) == 1 do
-      [{key, value}] = Map.to_list(neg_fields)
-      t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value)
+    has_node =
+      :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, fields) or
+        :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, neg_fields) or
+        (is_map(tag) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, tag)) or
+        (is_map(neg_tag) and
+           :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, neg_tag))
 
-      if empty?(t_diff) do
-        :bdd_bot
-      else
-        bdd_leaf(tag, Map.put(fields, key, t_diff))
-      end
+    if has_node do
+      bdd_difference(map1, map2)
     else
-      # Case 2: the maps have all but one key in common. Do the difference of that key.
-      case map_all_but_one(tag, fields, neg_tag, neg_fields) do
-        {diff_key, type1, type2} ->
-          bdd_leaf(tag, Map.replace!(fields, diff_key, difference(type1, type2)))
+      # Case 1: we are removing an open map with one field. Just do the difference of that field.
+      if neg_tag == :open and map_size(neg_fields) == 1 do
+        [{key, value}] = Map.to_list(neg_fields)
+        t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value)
 
-        _ ->
-          bdd_difference(map1, map2, &map_leaf_disjoint?/2)
+        if empty?(t_diff) do
+          :bdd_bot
+        else
+          bdd_leaf(tag, Map.put(fields, key, t_diff))
+        end
+      else
+        # Case 2: the maps have all but one key in common. Do the difference of that key.
+        case map_all_but_one(tag, fields, neg_tag, neg_fields) do
+          {diff_key, type1, type2} ->
+            bdd_leaf(tag, Map.replace!(fields, diff_key, difference(type1, type2)))
+
+          _ ->
+            bdd_difference(map1, map2, &map_leaf_disjoint?/2)
+        end
       end
     end
   end
@@ -3228,7 +3237,15 @@ defmodule Module.Types.Descr do
     do: bdd_difference(bdd1, bdd2, &map_leaf_disjoint?/2)
 
   defp map_leaf_disjoint?(bdd_leaf(_tag1, fields1), bdd_leaf(_tag2, fields2)) do
-    disjoint_structs?(fields1, fields2)
+    has_node =
+      :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, fields1) or
+        :maps.fold(fn _k, v, acc -> acc or collect_generators(v) != [] end, false, fields2)
+
+    if has_node do
+      false
+    else
+      disjoint_structs?(fields1, fields2)
+    end
   end
 
   defp disjoint_structs?(%{__struct__: %{atom: atom} = d1}, %{__struct__: d2})
@@ -3244,21 +3261,25 @@ defmodule Module.Types.Descr do
   defp disjoint_structs?(_, _), do: false
 
   # Intersects two map literals; throws if their intersection is empty.
+
+  defp map_literal_intersection(tag1, fields1, tag2, fields2),
+    do: map_literal_intersection(tag1, fields1, tag2, fields2, %{})
+
   # Both open: the result is open.
-  defp map_literal_intersection(:open, map1, :open, map2) do
+  defp map_literal_intersection(:open, map1, :open, map2, seen) do
     new_fields =
       symmetrical_merge(map1, map2, fn _, type1, type2 ->
-        non_empty_intersection!(type1, type2)
+        non_empty_intersection!(type1, type2, seen)
       end)
 
     {:open, new_fields}
   end
 
   # Both closed: the result is closed.
-  defp map_literal_intersection(:closed, map1, :closed, map2) do
+  defp map_literal_intersection(:closed, map1, :closed, map2, seen) do
     new_fields =
       symmetrical_intersection(map1, map2, fn _, type1, type2 ->
-        non_empty_intersection!(type1, type2)
+        non_empty_intersection!(type1, type2, seen)
       end)
 
     if map_size(new_fields) < map_size(map1) or map_size(new_fields) < map_size(map2) do
@@ -3269,16 +3290,16 @@ defmodule Module.Types.Descr do
   end
 
   # Open and closed: result is closed, all fields from open should be in closed, except not_set ones.
-  defp map_literal_intersection(:open, open, :closed, closed) do
-    :maps.iterator(open) |> :maps.next() |> map_literal_intersection_loop(closed)
+  defp map_literal_intersection(:open, open, :closed, closed, seen) do
+    :maps.iterator(open) |> :maps.next() |> map_literal_intersection_loop(closed, seen)
   end
 
-  defp map_literal_intersection(:closed, closed, :open, open) do
-    :maps.iterator(open) |> :maps.next() |> map_literal_intersection_loop(closed)
+  defp map_literal_intersection(:closed, closed, :open, open, seen) do
+    :maps.iterator(open) |> :maps.next() |> map_literal_intersection_loop(closed, seen)
   end
 
   # At least one tag is a tag-domain pair.
-  defp map_literal_intersection(tag_or_domains1, map1, tag_or_domains2, map2) do
+  defp map_literal_intersection(tag_or_domains1, map1, tag_or_domains2, map2, seen) do
     # For a closed map with domains intersected with an open map with domains:
     # 1. The result is closed (more restrictive)
     # 2. We need to check each domain in the open map against the closed map
@@ -3286,7 +3307,7 @@ defmodule Module.Types.Descr do
     default2 = map_key_tag_to_type(tag_or_domains2)
 
     # Compute the new domain
-    tag_or_domains = map_domain_intersection(tag_or_domains1, tag_or_domains2)
+    tag_or_domains = map_domain_intersection(tag_or_domains1, tag_or_domains2, seen)
 
     # Go over all fields in map1 and map2 with default atom types atom1 and atom2
     # 1. If key is in both maps, compute non empty intersection (:error if it is none)
@@ -3296,17 +3317,17 @@ defmodule Module.Types.Descr do
     # using default values when a key is not present.
     {tag_or_domains,
      symmetrical_merge(map1, default1, map2, default2, fn _key, v1, v2 ->
-       non_empty_intersection!(v1, v2)
+       non_empty_intersection!(v1, v2, seen)
      end)}
   end
 
   # Compute the intersection of two tags or tag-domain pairs.
-  defp map_domain_intersection(:closed, _), do: :closed
-  defp map_domain_intersection(_, :closed), do: :closed
-  defp map_domain_intersection(:open, tag_or_domains), do: tag_or_domains
-  defp map_domain_intersection(tag_or_domains, :open), do: tag_or_domains
+  defp map_domain_intersection(:closed, _, _seen), do: :closed
+  defp map_domain_intersection(_, :closed, _seen), do: :closed
+  defp map_domain_intersection(:open, tag_or_domains, _seen), do: tag_or_domains
+  defp map_domain_intersection(tag_or_domains, :open, _seen), do: tag_or_domains
 
-  defp map_domain_intersection(domains1 = %{}, domains2 = %{}) do
+  defp map_domain_intersection(domains1 = %{}, domains2 = %{}, seen) do
     new_domains =
       for {domain_key, type1} <- domains1, reduce: %{} do
         acc_domains ->
@@ -3314,7 +3335,7 @@ defmodule Module.Types.Descr do
             %{^domain_key => type2} ->
               inter = intersection(type1, type2)
 
-              if empty_or_optional?(inter) do
+              if empty_seen?(remove_optional(inter), seen) do
                 acc_domains
               else
                 Map.put(acc_domains, domain_key, inter)
@@ -3329,18 +3350,18 @@ defmodule Module.Types.Descr do
     if map_size(new_domains) == 0, do: :closed, else: new_domains
   end
 
-  defp map_literal_intersection_loop(:none, acc), do: {:closed, acc}
+  defp map_literal_intersection_loop(:none, acc, _seen), do: {:closed, acc}
 
-  defp map_literal_intersection_loop({key, type1, iterator}, acc) do
+  defp map_literal_intersection_loop({key, type1, iterator}, acc, seen) do
     case acc do
       %{^key => type2} ->
-        acc = %{acc | key => non_empty_intersection!(type1, type2)}
-        :maps.next(iterator) |> map_literal_intersection_loop(acc)
+        acc = %{acc | key => non_empty_intersection!(type1, type2, seen)}
+        :maps.next(iterator) |> map_literal_intersection_loop(acc, seen)
 
       _ ->
         # If the key is optional in the open map, we can ignore it
         case type1 do
-          %{optional: 1} -> :maps.next(iterator) |> map_literal_intersection_loop(acc)
+          %{optional: 1} -> :maps.next(iterator) |> map_literal_intersection_loop(acc, seen)
           _ -> throw(:empty)
         end
     end
@@ -4270,10 +4291,10 @@ defmodule Module.Types.Descr do
     {[], [], nil, to_domain_keys(key_descr), []}
   end
 
-  defp non_empty_map_literals_intersection(maps) do
+  defp non_empty_map_literals_intersection(maps, seen \\ %{}) do
     try do
       Enum.reduce(maps, {:open, %{}}, fn {next_tag, next_fields}, {tag, fields} ->
-        map_literal_intersection(tag, fields, next_tag, next_fields)
+        map_literal_intersection(tag, fields, next_tag, next_fields, seen)
       end)
     catch
       :empty -> :empty
@@ -4286,7 +4307,8 @@ defmodule Module.Types.Descr do
   defp map_empty?(bdd, seen) do
     bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, negs} ->
-      case non_empty_map_literals_intersection(pos) do
+      # We pass seen down to the literal intersection because it may need to check emptiness of elements, which may contain recursive nodes.
+      case non_empty_map_literals_intersection(pos, seen) do
         :empty ->
           true
 
@@ -4316,7 +4338,7 @@ defmodule Module.Types.Descr do
   defp map_line_empty?(tag, fields, all_negs, seen) when all_negs != [] do
     [{neg_tag, neg_fields} | negs] = all_negs
 
-    if map_check_domain_keys(tag, neg_tag) do
+    if map_check_domain_keys(tag, neg_tag, seen) do
       atom_default = map_key_tag_to_type(tag)
       neg_atom_default = map_key_tag_to_type(neg_tag)
 
@@ -4383,24 +4405,28 @@ defmodule Module.Types.Descr do
   # Verify the domain condition from equation (22) in paper ICFP'23 https://www.irif.fr/~gc/papers/icfp23.pdf
   # which is that every domain key type in the positive map is a subtype
   # of the corresponding domain key type in the negative map.
-  defp map_check_domain_keys(:closed, _), do: true
-  defp map_check_domain_keys(_, :open), do: true
+  defp map_check_domain_keys(:closed, _, _seen), do: true
+  defp map_check_domain_keys(_, :open, _seen), do: true
 
   # An open map is a subtype iff the negative domains are all present as term_or_optional()
-  defp map_check_domain_keys(:open, neg_domains) do
+  defp map_check_domain_keys(:open, neg_domains, seen) do
     map_size(neg_domains) == length(@domain_key_types) and
-      Enum.all?(neg_domains, fn {_domain_key, type} -> subtype?(term_or_optional(), type) end)
+      Enum.all?(neg_domains, fn {_domain_key, type} ->
+        subtype_seen?(term_or_optional(), type, seen)
+      end)
   end
 
   # A positive domains is smaller than a closed map iff all its keys are empty or optional
-  defp map_check_domain_keys(pos_domains, :closed) do
-    Enum.all?(pos_domains, fn {_domain_key, type} -> empty_or_optional?(type) end)
+  defp map_check_domain_keys(pos_domains, :closed, seen) do
+    Enum.all?(pos_domains, fn {_domain_key, type} ->
+      empty_seen?(remove_optional(type), seen)
+    end)
   end
 
   # Component-wise comparison of domains
-  defp map_check_domain_keys(pos_domains, neg_domains) do
+  defp map_check_domain_keys(pos_domains, neg_domains, seen) do
     Enum.all?(pos_domains, fn {domain_key, type} ->
-      subtype?(type, Map.get(neg_domains, domain_key, not_set()))
+      subtype_seen?(type, Map.get(neg_domains, domain_key, not_set()), seen)
     end)
   end
 
@@ -4754,6 +4780,10 @@ defmodule Module.Types.Descr do
 
   # defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2)
 
+  # X = {X, int} | nil
+  # fn recur -> {:tuple, [recur.(X), int()]}
+  # {:tuple, [recur.(X), int()]}
+
   defp tuple_intersection(bdd1, bdd2) do
     bdd_intersection(bdd1, bdd2, &tuple_leaf_intersection/2)
   end
@@ -4773,14 +4803,17 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp tuple_literal_intersection(:open, [], tag, elements), do: {tag, elements}
+  defp tuple_literal_intersection(tag1, elems1, tag2, elems2),
+    do: tuple_literal_intersection(tag1, elems1, tag2, elems2, %{})
+
+  defp tuple_literal_intersection(:open, [], tag, elements, _seen), do: {tag, elements}
 
-  defp tuple_literal_intersection(tag1, elements1, tag2, elements2) do
+  defp tuple_literal_intersection(tag1, elements1, tag2, elements2, seen) do
     if mismatched_tuple_sizes?(tag1, elements1, tag2, elements2) do
       :empty
     else
       try do
-        zip_non_empty_intersection!(elements1, elements2, [])
+        zip_non_empty_intersection!(elements1, elements2, [], seen)
       catch
         :empty -> :empty
       else
@@ -4803,11 +4836,16 @@ defmodule Module.Types.Descr do
     do: false
 
   # Intersects two lists of types, and _appends_ the extra elements to the result.
-  defp zip_non_empty_intersection!([], types2, acc), do: Enum.reverse(acc, types2)
-  defp zip_non_empty_intersection!(types1, [], acc), do: Enum.reverse(acc, types1)
-
-  defp zip_non_empty_intersection!([type1 | rest1], [type2 | rest2], acc) do
-    zip_non_empty_intersection!(rest1, rest2, [non_empty_intersection!(type1, type2) | acc])
+  defp zip_non_empty_intersection!([], types2, acc, _seen), do: Enum.reverse(acc, types2)
+  defp zip_non_empty_intersection!(types1, [], acc, _seen), do: Enum.reverse(acc, types1)
+
+  defp zip_non_empty_intersection!([type1 | rest1], [type2 | rest2], acc, seen) do
+    zip_non_empty_intersection!(
+      rest1,
+      rest2,
+      [non_empty_intersection!(type1, type2, seen) | acc],
+      seen
+    )
   end
 
   defp zip_empty_intersection?([], _types2), do: false
@@ -4849,10 +4887,10 @@ defmodule Module.Types.Descr do
   defp disjoint_atom_descr?(atom1, %{atom: atom2}), do: atom_intersection(atom1, atom2) === 0
   defp disjoint_atom_descr?(_atom, %{}), do: true
 
-  defp non_empty_tuple_literals_intersection(tuples) do
+  defp non_empty_tuple_literals_intersection(tuples, seen \\ %{}) do
     try do
       Enum.reduce(tuples, {:open, []}, fn {next_tag, next_elements}, {tag, elements} ->
-        case tuple_literal_intersection(tag, elements, next_tag, next_elements) do
+        case tuple_literal_intersection(tag, elements, next_tag, next_elements, seen) do
           :empty -> throw(:empty)
           next -> next
         end
@@ -4865,7 +4903,8 @@ defmodule Module.Types.Descr do
   defp tuple_empty?(bdd, seen) do
     bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, negs} ->
-      case non_empty_tuple_literals_intersection(pos) do
+      # We pass seen down to the literal intersection because it may need to check emptiness of elements, which may contain recursive nodes.
+      case non_empty_tuple_literals_intersection(pos, seen) do
         :empty -> true
         {tag, fields} -> tuple_line_empty?(tag, fields, negs, seen)
       end
@@ -5171,18 +5210,19 @@ defmodule Module.Types.Descr do
 
   # Transforms a bdd into a union of tuples with no negations.
   # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates
-  defp tuple_bdd_to_dnf(bdd) do
+  defp tuple_bdd_to_dnf(bdd, seen \\ %{}) do
     bdd_to_dnf(bdd)
     |> Enum.reduce([], fn {positive_tuples, negative_tuples}, acc ->
-      case non_empty_tuple_literals_intersection(positive_tuples) do
+      case non_empty_tuple_literals_intersection(positive_tuples, seen) do
         :empty ->
           acc
 
         {tag, elements} ->
-          if tuple_line_empty?(tag, elements, negative_tuples, %{}) do
+          if tuple_line_empty?(tag, elements, negative_tuples, seen) do
             acc
           else
-            tuple_eliminate_negations(tag, elements, negative_tuples) |> tuple_dnf_union(acc)
+            tuple_eliminate_negations(tag, elements, negative_tuples)
+            |> tuple_dnf_union(acc)
           end
       end
     end)
@@ -5335,6 +5375,8 @@ defmodule Module.Types.Descr do
     |> Enum.reduce(none(), fn
       {tag, elements}, acc -> Enum.at(elements, index, tuple_tag_to_type(tag)) |> union(acc)
     end)
+    # As we work on nodes (the elements of a tuple), we ensure the result is a descr.
+    |> to_descr()
   end
 
   @doc """
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index eb804650afb..7797e69e697 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -3266,55 +3266,132 @@ defmodule Module.Types.DescrTest do
     end
   end
 
-  ## Node infrastructure
-
   describe "recursive types" do
-    test "building a node" do
-      # "a node is a triple {id, state, generator}
-      state = %{x: 1}
-      gen = fn s -> s end
-      node = make_node(state, gen)
+    # Helper: recursive linked list type. Returns a descr.
+    # linked_list(T) = {T, linked_list(T)} | nil
+    defp linked_list(descr) do
+      recursive(%{
+        X: fn recur -> tuple([descr, recur.(:X)]) |> union(atom([nil])) end
+      })
+      |> Map.fetch!(:X)
+      |> to_descr()
+    end
+
+    defp int_linked_list(), do: linked_list(integer())
+    defp number_linked_list(), do: linked_list(union(integer(), float()))
+
+    # Helper: recursive binary tree type. Returns a descr.
+    # binary_tree(T) = {T, binary_tree(T), binary_tree(T)} | nil
+    defp binary_tree(descr) do
+      recursive(%{
+        T: fn recur ->
+          tuple([descr, recur.(:T), recur.(:T)])
+          |> union(atom([nil]))
+        end
+      })
+      |> Map.fetch!(:T)
+      |> to_descr()
+    end
+
+    # Helper: recursive Macro.t() approximation. Returns a descr.
+    # ast = {ast | atom, keyword, atom | [ast]} | {ast, ast} | [ast] | atom | number | binary
+    defp macro_ast() do
+      recursive(%{
+        Ast: fn recur ->
+          node = recur.(:Ast)
 
-      assert {id, ^state, ^gen} = node
-      assert is_reference(id)
+          call =
+            tuple([union(node, atom()), list(tuple([atom(), term()])), union(atom(), list(node))])
 
-      # each call produces a fresh id
-      gen = fn _ -> :ok end
-      {id1, _, _} = make_node(%{}, gen)
-      {id2, _, _} = make_node(%{}, gen)
-      assert id1 != id2
+          pair = tuple([node, node])
+
+          list(node)
+          |> union(call)
+          |> union(pair)
+          |> union(atom())
+          |> union(number())
+          |> union(binary())
+        end
+      })
+      |> Map.fetch!(:Ast)
+      |> to_descr()
+    end
+
+    # Helper: recursive Inspect.Algebra.t(). Returns a descr.
+    defp inspect_doc() do
+      recursive(%{
+        Doc: fn recur ->
+          child = recur.(:Doc)
+
+          binary()
+          |> union(empty_list())
+          |> union(atom([:doc_line]))
+          |> union(non_empty_list(child, child))
+          |> union(tuple([atom([:doc_string]), binary(), integer()]))
+          |> union(tuple([atom([:doc_limit]), child, integer() |> union(atom([:infinity]))]))
+          |> union(
+            tuple([
+              atom([:doc_nest]),
+              child,
+              integer() |> union(atom([:cursor, :reset])),
+              atom([:always, :break])
+            ])
+          )
+          |> union(tuple([atom([:doc_break]), binary(), atom([:flex, :strict])]))
+          |> union(
+            tuple([
+              atom([:doc_group]),
+              child,
+              atom([:normal, :optimistic, :pessimistic, :inherit])
+            ])
+          )
+          |> union(tuple([atom([:doc_fits]), child, atom([:enabled, :disabled])]))
+          |> union(tuple([atom([:doc_force]), child]))
+          |> union(tuple([atom([:doc_collapse]), integer()]))
+          |> union(tuple([atom([:doc_color]), child, term()]))
+        end
+      })
+      |> Map.fetch!(:Doc)
+      |> to_descr()
+    end
+
+    # Helper: recursive iodata() approximation. Returns a descr.
+    # iodata = binary | [] | [byte | binary | iodata | ...]
+    defp iodata_descr() do
+      recursive(%{
+        Iodata: fn recur ->
+          node = recur.(:Iodata)
+          head = integer() |> union(binary()) |> union(node)
+
+          binary()
+          |> union(empty_list())
+          |> union(non_empty_list(head, node))
+        end
+      })
+      |> Map.fetch!(:Iodata)
+      |> to_descr()
     end
 
-    test "to_descr (from node)" do
+    test "node infrastructure" do
       # stepping a node applies the generator to the state
       descr = integer()
-      node = make_node(%{}, fn _state -> descr end)
+      node = make_node(%{}, fn _recur -> descr end)
       assert to_descr(node) == descr
 
-      # stepping a node with non-trivial state
-      node = make_node(%{val: float()}, fn state -> state.val end)
-      assert to_descr(node) == float()
-
       # to_descr is identity on :term
       assert to_descr(:term) == :term
 
       # to_descr is identity on a descr map
       d = union(integer(), atom())
       assert to_descr(d) == d
-    end
 
-    test "to_node (from descr) / fresh_node" do
       # wrapping a descr map produces a node whose step returns the original
       d = integer()
       node = to_node(d)
-      assert {id, %{}, _gen} = node
-      assert is_reference(id)
       assert to_descr(node) == d
 
       # wrapping :term produces a node whose step returns :term
       node = to_node(:term)
-      assert {id, :term, _gen} = node
-      assert is_reference(id)
       assert to_descr(node) == :term
 
       # to_node on an existing node returns it unchanged
@@ -3326,9 +3403,7 @@ defmodule Module.Types.DescrTest do
       assert to_descr(to_node(d)) == d
     end
 
-    ## Kind internals accept nodes
-
-    test "tuple constructor accepts nodes and descrs" do
+    test "constructors accept nodes and descrs" do
       # tuple/1 accepts nodes and produces a non-empty tuple descr
       n1 = to_node(integer())
       n2 = to_node(atom())
@@ -3341,10 +3416,6 @@ defmodule Module.Types.DescrTest do
       result = tuple([n, float()])
       assert equal?(result, tuple([integer(), float()]))
 
-      # todo: test tuple operations (index access) on recursive tuples
-    end
-
-    test "list constructor accepts nodes" do
       # list/1 accepts a node element type
       n = to_node(integer())
       from_node = list(n)
@@ -3359,10 +3430,6 @@ defmodule Module.Types.DescrTest do
       from_descrs = non_empty_list(integer(), empty_list())
       assert equal?(from_nodes, from_descrs)
 
-      # todo: test list operations (head, tail, cons) on recursive lists
-    end
-
-    test "map constructor accepts nodes" do
       # closed_map accepts node values
       n = to_node(integer())
       result = closed_map(a: n)
@@ -3372,408 +3439,301 @@ defmodule Module.Types.DescrTest do
       n = to_node(atom())
       result = open_map(b: n)
       refute empty?(result)
-
-      # map with mixed node and descr values" do
-      n = to_node(float())
-      result = closed_map(x: n, y: integer())
-      assert is_map_key(result, :map)
-      assert map_size(result) > 0
-
-      # todo: test map operations (fetch, update, ...) on recursive maps
-    end
-
-    ## Set operations accept nodes polymorphically
-
-    test "union on nodes" do
-      # union works on nodes
-      n1 = to_node(integer())
-      n2 = to_node(float())
-      assert equal?(union(n1, n2), union(integer(), float()))
-
-      # union of a node and a descr
-      n = to_node(integer())
-      assert equal?(union(n, float()), union(integer(), float()))
-      assert equal?(union(atom(), n), union(atom(), integer()))
-
-      # union with none() node is identity
-      n = to_node(atom())
-      n_none = to_node(none())
-      assert equal?(union(n, n_none), atom())
-
-      # union with term() node is term
-      n = to_node(integer())
-      n_term = to_node(:term)
-      assert union(n, n_term) == :term
-    end
-
-    test "intersection on nodes" do
-      # intersection of two nodes is equivalent to the intersection descr
-      n1 = to_node(union(integer(), atom()))
-      n2 = to_node(integer())
-      assert equal?(intersection(n1, n2), integer())
-
-      # intersection of a node and a descr
-      n = to_node(union(integer(), atom()))
-      assert equal?(intersection(n, integer()), integer())
-      assert equal?(intersection(atom(), n), atom())
-
-      # intersection of disjoint nodes is none
-      n1 = to_node(integer())
-      n2 = to_node(atom())
-      assert equal?(intersection(n1, n2), none())
-
-      # intersection with term() node is identity
-      n = to_node(float())
-      n_term = to_node(:term)
-      assert equal?(intersection(n, n_term), float())
-    end
-
-    test "negation on nodes" do
-      # negation of a node is equivalent to the negation descr
-      n = to_node(integer())
-      assert equal?(negation(n), negation(integer()))
-
-      # double negation round-trips
-      n = to_node(atom())
-      assert equal?(negation(negation(n)), atom())
-    end
-
-    test "difference on nodes" do
-      # difference of two nodes returns the difference descr
-      n1 = to_node(union(integer(), atom()))
-      n2 = to_node(atom())
-      assert equal?(difference(n1, n2), integer())
-
-      # difference of a node and a descr
-      n = to_node(union(integer(), float()))
-      assert equal?(difference(n, float()), integer())
-      assert equal?(difference(union(integer(), float()), to_node(float())), integer())
-
-      # difference from itself is none
-      n = to_node(float())
-      assert equal?(difference(n, n), none())
-
-      # difference from none() is identity
-      n = to_node(integer())
-      n_none = to_node(none())
-      assert equal?(difference(n, n_none), integer())
     end
 
-    ## Recursive type builder
-
-    test "recursive builder" do
-      ## simple recursive list: X = {integer(), X} | nil
-      %{X: node_x} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # node_x is a proper node triple
-      assert {id, state, gen} = node_x
-      assert is_reference(id)
-      assert is_map_key(state, :X)
-      assert is_function(gen, 1)
+    test "real-world types" do
+      ## integer linked list: X = {integer(), X} | nil
+      int_list = int_linked_list()
+      assert is_map_key(int_list, :tuple) and is_map_key(int_list, :atom)
 
-      # stepping once produces a descr with :tuple and :atom keys
-      d = to_descr(node_x)
-      assert is_map_key(d, :tuple)
-      assert is_map_key(d, :atom)
-
-      # some subtypes
       # {integer(), nil} <: X
-      assert subtype?(tuple([integer(), atom([nil])]), node_x)
+      assert subtype?(tuple([integer(), atom([nil])]), int_list)
       # nil <: X
-      assert subtype?(atom([nil]), node_x)
+      assert subtype?(atom([nil]), int_list)
       # {integer(), {integer(), nil}} <: X
-      assert subtype?(tuple([integer(), tuple([integer(), atom([nil])])]), node_x)
+      assert subtype?(tuple([integer(), tuple([integer(), atom([nil])])]), int_list)
       # {integer(), integer()} </: X
-      refute subtype?(tuple([integer(), integer()]), node_x)
-    end
-
-    test "mutually recursive nodes" do
-      # X = {int, Y} | nil, Y = {bool, X} | nil
-      %{X: node_x, Y: node_y} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([boolean(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # both are valid node triples sharing the same state
-      assert {id_x, state_x, _} = node_x
-      assert {id_y, state_y, _} = node_y
-      assert is_reference(id_x)
-      assert is_reference(id_y)
-      assert id_x != id_y
-
-      # they share the same state
-      assert state_x === state_y
+      refute subtype?(tuple([integer(), integer()]), int_list)
 
-      # both variables are present in the shared state
-      assert is_map_key(state_x, :X)
-      assert is_map_key(state_x, :Y)
-    end
-
-    test "stepping mutually recursive nodes" do
-      %{X: node_x, Y: node_y} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([boolean(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      dx = to_descr(node_x)
-      dy = to_descr(node_y)
-
-      # Both produce non-empty descriptors with tuple and atom parts
-      assert is_map_key(dx, :tuple)
-      assert is_map_key(dx, :atom)
-      assert is_map_key(dy, :tuple)
-      assert is_map_key(dy, :atom)
-    end
+      # Y = {number(), Y} | nil — integer list <: number list
+      number_list = number_linked_list()
+      assert subtype?(int_list, number_list)
+      refute subtype?(number_list, int_list)
 
-    test "iterated stepping of a recursive node" do
-      %{X: node_x} =
+      ## json_value recursive type
+      # json_value = nil | boolean() | number() | String.t() | [json_value()]
+      #            | %{optional(String.t()) => json_value}
+      %{Json: json_value} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
+          Json: fn recur ->
+            scalar =
+              atom([nil])
+              |> union(boolean())
+              |> union(integer())
+              |> union(float())
+              |> union(binary())
+
+            array = list(recur.(:Json))
+            object = open_map([{to_domain_keys(binary()), recur.(:Json)}])
+
+            scalar
+            |> union(array)
+            |> union(object)
           end
         })
 
-      # Step multiple times without crashing (coinductive stepping is lazy)
-      d1 = to_descr(node_x)
-      assert is_map(d1)
-
-      # The node can be stepped again (it regenerates a fresh node inside)
-      d2 = to_descr(node_x)
-      assert is_map(d2)
-    end
+      assert subtype?(atom([nil]), json_value)
+      assert subtype?(list(binary()), json_value)
+      assert subtype?(empty_map(), json_value)
+      refute subtype?(pid(), json_value)
 
-    test "single non-recursive equation degenerates to a plain node" do
-      %{X: node_x} =
+      ## IO.chardata recursive type
+      %{Char: chardata} =
         recursive(%{
-          X: fn _state -> integer() end
-        })
+          Char: fn recur ->
+            head = integer() |> union(binary())
+            tail = recur.(:Char)
 
-      assert {id, _state, _gen} = node_x
-      assert is_reference(id)
-      assert equal?(to_descr(node_x), integer())
-    end
-  end
-
-  ## Emptiness on recursive types
-
-  describe "emptiness of recursive types" do
-    test "non-recursive nodes" do
-      # a node wrapping integer() is not empty
-      node = make_node(%{}, fn _state -> integer() end)
-      refute empty?(node)
-
-      # a node wrapping none() is empty
-      node_none = make_node(%{}, fn _state -> none() end)
-      assert empty?(node_none)
-    end
-
-    test "simple recursive types" do
-      # X = {integer(), X} | nil is not empty (inhabited by nil, {1,nil}, ...)
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
+            binary()
+            |> union(empty_list())
+            |> union(non_empty_list(head, tail))
           end
         })
 
-      refute empty?(nx)
+      assert subtype?(binary(), chardata)
+      assert subtype?(empty_list(), chardata)
+      assert subtype?(non_empty_list(integer(), empty_list()), chardata)
+      assert subtype?(non_empty_list(binary(), binary()), chardata)
+      refute subtype?(pid(), chardata)
 
-      # X = {X} is empty (no base case)
-      %{X: nx} =
+      ## Inspect.Algebra.t recursive type
+      %{Doc: doc} =
         recursive(%{
-          X: fn state -> tuple([make_node(state, state[:X])]) end
-        })
-
-      assert empty?(nx)
+          Doc: fn recur ->
+            child = recur.(:Doc)
 
-      # X = {X, X} is empty (no base case)
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:X]), make_node(state, state[:X])])
+            binary()
+            |> union(empty_list())
+            |> union(atom([:doc_line]))
+            |> union(non_empty_list(child, child))
+            |> union(tuple([atom([:doc_string]), binary(), integer()]))
+            |> union(tuple([atom([:doc_limit]), child, integer() |> union(atom([:infinity]))]))
+            |> union(
+              tuple([
+                atom([:doc_nest]),
+                child,
+                integer() |> union(atom([:cursor, :reset])),
+                atom([:always, :break])
+              ])
+            )
+            |> union(tuple([atom([:doc_break]), binary(), atom([:flex, :strict])]))
+            |> union(
+              tuple([
+                atom([:doc_group]),
+                child,
+                atom([:normal, :optimistic, :pessimistic, :inherit])
+              ])
+            )
+            |> union(tuple([atom([:doc_fits]), child, atom([:enabled, :disabled])]))
+            |> union(tuple([atom([:doc_force]), child]))
+            |> union(tuple([atom([:doc_collapse]), integer()]))
+            |> union(tuple([atom([:doc_color]), child, term()]))
           end
         })
 
-      assert empty?(nx)
+      assert subtype?(binary(), doc)
+      assert subtype?(atom([:doc_line]), doc)
+      assert subtype?(tuple([atom([:doc_force]), binary()]), doc)
+      assert subtype?(non_empty_list(binary(), binary()), doc)
+      refute subtype?(pid(), doc)
 
-      # X = {integer()} | {X, X} has base case, not empty
-      %{X: nx} =
+      ## expression trees
+      # Expr = integer() | {atom, Expr, Expr}, Binop = {atom, Expr, Expr}
+      %{Expr: nexpr, Binop: nbinop} =
         recursive(%{
-          X: fn state ->
+          Expr: fn recur ->
             union(
-              tuple([integer()]),
-              tuple([make_node(state, state[:X]), make_node(state, state[:X])])
+              integer(),
+              tuple([
+                atom(),
+                recur.(:Expr),
+                recur.(:Expr)
+              ])
             )
+          end,
+          Binop: fn recur ->
+            tuple([atom(), recur.(:Expr), recur.(:Expr)])
           end
         })
 
-      refute empty?(nx)
-    end
+      texpr = to_descr(nexpr)
+      tbinop = to_descr(nbinop)
 
-    test "mutual recursion" do
-      # X = {int,Y}|nil, Y = {bool,X}|nil: both not empty
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([boolean(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
+      refute empty?(texpr)
+      refute empty?(tbinop)
 
-      refute empty?(nx)
-      refute empty?(ny)
+      # 42 is an Expr
+      assert subtype?(integer(), texpr)
 
-      # X = {Y}, Y = {X}: both empty (no base case)
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state -> tuple([make_node(state, state[:Y])]) end,
-          Y: fn state -> tuple([make_node(state, state[:X])]) end
-        })
+      # {:+, 1, 2} is an Expr and a Binop
+      assert subtype?(tuple([atom(), integer(), integer()]), texpr)
+      assert subtype?(tuple([atom(), integer(), integer()]), tbinop)
+
+      # {:*, {:+, 1, 2}, 3} is an Expr
+      inner = tuple([atom(), integer(), integer()])
+      assert subtype?(tuple([atom(), inner, integer()]), texpr)
+    end
+
+    # test "recursive function types" do
+    #   ast = macro_ast()
+    #   doc = inspect_doc()
+    #   iodata = iodata_descr()
+    #   width = integer() |> union(atom([:infinity]))
+    #   ast_transform = fun([ast], ast)
+    #   ast_transform_acc = fun([ast, term()], tuple([ast, term()]))
+
+    #   # Macro.prewalk/2 and Macro.postwalk/2:
+    #   # (Macro.t(), (Macro.t() -> Macro.t()) -> Macro.t())
+    #   prewalk_type = fun([ast, ast_transform], ast)
+    #   assert subtype?(fun([integer(), fun([integer()], integer())], integer()), prewalk_type)
+    #   refute subtype?(fun([integer(), fun([integer()], atom())], integer()), prewalk_type)
+    #   assert fun_apply(prewalk_type, [tuple([integer(), integer()]), ast_transform]) == {:ok, ast}
+
+    #   # Macro.traverse/4:
+    #   # (Macro.t(), acc, (Macro.t(), acc -> {Macro.t(), acc}), (Macro.t(), acc -> {Macro.t(), acc})
+    #   #  -> {Macro.t(), acc})
+    #   traverse_type = fun([ast, term(), ast_transform_acc, ast_transform_acc], tuple([ast, term()]))
+
+    #   assert subtype?(
+    #            fun(
+    #              [integer(), atom(), fun([integer(), atom()], tuple([integer(), atom()])),
+    #               fun([integer(), atom()], tuple([integer(), atom()]))],
+    #              tuple([integer(), atom()])
+    #            ),
+    #            traverse_type
+    #          )
+
+    #   refute subtype?(
+    #            fun(
+    #              [integer(), atom(), fun([integer(), atom()], tuple([atom(), atom()])),
+    #               fun([integer(), atom()], tuple([integer(), atom()]))],
+    #              tuple([integer(), atom()])
+    #            ),
+    #            traverse_type
+    #          )
+
+    #   assert fun_apply(traverse_type, [integer(), atom(), ast_transform_acc, ast_transform_acc]) ==
+    #            {:ok, tuple([ast, term()])}
+
+    #   # Inspect.Algebra.format/2: (Inspect.Algebra.t(), non_neg_integer() | :infinity -> iodata())
+    #   format_type = fun([doc, width], iodata)
+    #   assert subtype?(fun([binary(), integer()], binary()), format_type)
+    #   assert subtype?(fun([tuple([atom([:doc_force]), binary()]), atom([:infinity])], iodata), format_type)
+    #   refute subtype?(fun([integer(), integer()], binary()), format_type)
+
+    #   # Inspect.Opts.default_inspect_fun/0:
+    #   # (() -> (term(), Inspect.Opts.t() -> Inspect.Algebra.t()))
+    #   default_inspect_fun_type = fun([], fun([term(), term()], doc))
+    #   assert subtype?(fun([], fun([term(), term()], binary())), default_inspect_fun_type)
+    #   refute subtype?(fun([], fun([term(), term()], integer())), default_inspect_fun_type)
+    #   assert fun_apply(default_inspect_fun_type, []) == {:ok, fun([term(), term()], doc)}
+    # end
+
+    test "emptiness" do
+      # X = {X, X} is empty (no base case)
+      %{X: nx} = recursive(%{X: fn recur -> tuple([recur.(:X), recur.(:X)]) end})
 
       assert empty?(nx)
-      assert empty?(ny)
 
-      # X = {Y}|nil, Y = {X}: X not empty, Y not empty (Y can hold {nil})
-      %{X: nx, Y: ny} =
+      # X = {integer()} | {X, X} has base case, not empty
+      %{X: nx} =
         recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([make_node(state, state[:X])])
-          end
+          X: fn recur -> union(tuple([integer()]), tuple([recur.(:X), recur.(:X)])) end
         })
 
       refute empty?(nx)
-      refute empty?(ny)
-    end
 
-    test "cycle detection" do
-      # direct self-reference: X = {X} is empty
-      %{X: nx} =
+      ## mutual recursion
+      # X = {int,Y} | nil, Y = {bool,X} | nil: both not empty
+      %{X: node_x, Y: node_y} =
         recursive(%{
-          X: fn state -> tuple([make_node(state, state[:X])]) end
+          X: fn recur -> tuple([integer(), recur.(:Y)]) |> union(atom([nil])) end,
+          Y: fn recur -> tuple([boolean(), recur.(:X)]) |> union(atom([nil])) end
         })
 
-      assert empty?(nx)
+      tx = to_descr(node_x)
+      ty = to_descr(node_y)
 
-      # 2-cycle: X = {Y}, Y = {X}, both empty
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state -> tuple([make_node(state, state[:Y])]) end,
-          Y: fn state -> tuple([make_node(state, state[:X])]) end
-        })
+      refute empty?(tx)
+      refute empty?(ty)
 
-      assert empty?(nx)
-      assert empty?(ny)
+      # {int, {bool, nil}} <: X
+      inner_y = tuple([boolean(), atom([nil])])
+      assert subtype?(tuple([integer(), inner_y]), node_x)
 
-      # 3-cycle: X→Y→Z→X, no base case, all empty
-      %{X: nx, Y: ny, Z: nz} =
-        recursive(%{
-          X: fn state -> tuple([make_node(state, state[:Y])]) end,
-          Y: fn state -> tuple([make_node(state, state[:Z])]) end,
-          Z: fn state -> tuple([make_node(state, state[:X])]) end
-        })
+      # {bool, {int, nil}} <: Y
+      inner_x = tuple([integer(), atom([nil])])
+      assert subtype?(tuple([boolean(), inner_x]), node_y)
 
-      assert empty?(nx)
-      assert empty?(ny)
-      assert empty?(nz)
+      # {int, {bool, {int, nil}}} <: X
+      level3 = tuple([integer(), atom([nil])])
+      level2 = tuple([boolean(), level3])
+      assert subtype?(tuple([integer(), level2]), node_x)
 
-      # 3-cycle with nil base case on Z: none empty
-      %{X: nx, Y: ny, Z: nz} =
+      # X = {Y}|nil, Y = {X}: X not empty, Y not empty (Y can hold {nil})
+      %{X: nx, Y: ny} =
         recursive(%{
-          X: fn state -> tuple([make_node(state, state[:Y])]) end,
-          Y: fn state -> tuple([make_node(state, state[:Z])]) end,
-          Z: fn state ->
-            tuple([make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
+          X: fn recur -> tuple([recur.(:Y)]) |> union(atom([nil])) end,
+          Y: fn recur -> tuple([recur.(:X)]) end
         })
 
       refute empty?(nx)
       refute empty?(ny)
-      refute empty?(nz)
 
-      # 4-cycle: A→B→C→D→A, no base case, all empty
-      %{A: na, B: nb, C: nc, D: nd} =
-        recursive(%{
-          A: fn state -> tuple([make_node(state, state[:B])]) end,
-          B: fn state -> tuple([make_node(state, state[:C])]) end,
-          C: fn state -> tuple([make_node(state, state[:D])]) end,
-          D: fn state -> tuple([make_node(state, state[:A])]) end
-        })
+      ## cycle detection
+      cases = [
+        # X -> {Y}, Y -> {Z}, Z -> {X}
+        {"3-cycle no base", true,
+         %{
+           X: fn recur -> tuple([recur.(:Y)]) end,
+           Y: fn recur -> tuple([recur.(:Z)]) end,
+           Z: fn recur -> tuple([recur.(:X)]) end
+         }},
+        # X -> {Y}, Y -> {Z}, Z -> {X} or nil
+        {"3-cycle with base", false,
+         %{
+           X: fn recur -> tuple([recur.(:Y)]) end,
+           Y: fn recur -> tuple([recur.(:Z)]) end,
+           Z: fn recur -> tuple([recur.(:X)]) |> union(atom([nil])) end
+         }}
+      ]
 
-      assert empty?(na)
-      assert empty?(nb)
-      assert empty?(nc)
-      assert empty?(nd)
+      for {desc, expected_empty, gen} <- cases do
+        nodes = recursive(gen)
 
-      # 4-cycle with nil base case on D: none empty
-      %{A: na, B: nb, C: nc, D: nd} =
-        recursive(%{
-          A: fn state -> tuple([make_node(state, state[:B])]) end,
-          B: fn state -> tuple([make_node(state, state[:C])]) end,
-          C: fn state -> tuple([make_node(state, state[:D])]) end,
-          D: fn state ->
-            tuple([make_node(state, state[:A])])
-            |> union(atom([nil]))
+        for {_key, node} <- nodes do
+          if expected_empty do
+            assert empty?(node), "#{desc}: expected empty but wasn't"
+          else
+            refute empty?(node), "#{desc}: expected not empty but was"
           end
-        })
-
-      refute empty?(na)
-      refute empty?(nb)
-      refute empty?(nc)
-      refute empty?(nd)
-    end
+        end
+      end
 
-    test "diamond patterns" do
+      ## diamond patterns
       # X->{Y,Z}, Y->{W}, Z->{W}, W->{X}
-      # the dependency graph has a diamond shape:
-      #
       #       X
       #      / \
       #     Y   Z
       #      \ /
-      #       W
-      #       |
-      #       X  (cycle)
-      #
+      #       W -> X (cycle)
       # no base case: all empty
       %{X: nx, Y: ny, Z: nz, W: nw} =
         recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:Y]), make_node(state, state[:Z])])
-          end,
-          Y: fn state -> tuple([make_node(state, state[:W])]) end,
-          Z: fn state -> tuple([make_node(state, state[:W])]) end,
-          W: fn state -> tuple([make_node(state, state[:X])]) end
+          X: fn recur -> tuple([recur.(:Y), recur.(:Z)]) end,
+          Y: fn recur -> tuple([recur.(:W)]) end,
+          Z: fn recur -> tuple([recur.(:W)]) end,
+          W: fn recur -> tuple([recur.(:X)]) end
         })
 
       assert empty?(nx)
@@ -3784,1141 +3744,362 @@ defmodule Module.Types.DescrTest do
       # same with base case on W: none empty
       %{X: nx, Y: ny, Z: nz, W: nw} =
         recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:Y]), make_node(state, state[:Z])])
-          end,
-          Y: fn state -> tuple([make_node(state, state[:W])]) end,
-          Z: fn state -> tuple([make_node(state, state[:W])]) end,
-          W: fn state ->
-            tuple([make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
+          X: fn recur -> tuple([recur.(:Y), recur.(:Z)]) end,
+          Y: fn recur -> tuple([recur.(:W)]) end,
+          Z: fn recur -> tuple([recur.(:W)]) end,
+          W: fn recur -> tuple([recur.(:X)]) |> union(atom([nil])) end
         })
 
       refute empty?(nx)
       refute empty?(ny)
       refute empty?(nz)
       refute empty?(nw)
-    end
 
-    test "recursive lists" do
-      # X = non_empty_list(integer(), X) | []: not empty
+      ## binary trees
+      # Tree = {atom, Tree, Tree} | nil: not empty
+      refute empty?(binary_tree(atom()))
+
+      ## list-head recursion with base case is not empty
+      # X = non_empty_list(X, []) | non_empty_list(integer(), [])
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            non_empty_list(integer(), make_node(state, state[:X]))
-            |> union(empty_list())
+          X: fn recur ->
+            non_empty_list(recur.(:X), empty_list())
+            |> union(non_empty_list(integer(), empty_list()))
           end
         })
 
       refute empty?(nx)
+    end
 
-      # X = non_empty_list(X, []): empty (no scalar base)
-      %{X: nx} =
+    test "regular expressions" do
+      # bool_list = {boolean(), bool_list} | nil
+      # int_or_bool_list = {integer() | boolean(), int_or_bool_list} | nil
+      # int_then_bool_list = {integer(), int_then_bool_list} | bool_list
+      bool_list = linked_list(boolean())
+      int_or_bool_list = linked_list(union(integer(), boolean()))
+
+      int_then_bool_list =
         recursive(%{
-          X: fn state ->
-            non_empty_list(make_node(state, state[:X]), empty_list())
+          IntThenBoolList: fn recur ->
+            tuple([integer(), recur.(:IntThenBoolList)]) |> union(bool_list)
           end
         })
+        |> Map.fetch!(:IntThenBoolList)
+        |> to_descr()
 
-      assert empty?(nx)
+      refute empty?(int_then_bool_list)
+      refute empty?(bool_list)
+      refute empty?(int_or_bool_list)
+      assert subtype?(bool_list, int_or_bool_list)
+      assert subtype?(int_then_bool_list, int_or_bool_list)
+    end
 
-      # workaround encoding with union of constructors: not empty
+    test "subtyping" do
+      ## recursion on list tail
+      # X = non_empty_list(integer(), X) | []
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            union(
-              non_empty_list(integer(), make_node(state, state[:X])),
-              union(non_empty_list(integer(), empty_list()), empty_list())
-            )
+          X: fn recur -> non_empty_list(integer(), recur.(:X)) |> union(empty_list()) end
+        })
+
+      # [] <: X
+      assert subtype?(empty_list(), nx)
+
+      # non_empty_list(integer()) <: X (terminates with [])
+      assert subtype?(non_empty_list(integer()), nx)
+
+      ## binary trees
+      int_bin_tree = binary_tree(integer())
+
+      # nil is a valid tree
+      assert subtype?(atom([nil]), int_bin_tree)
+
+      # {42, nil, nil} is a valid tree
+      assert subtype?(tuple([integer(), atom([nil]), atom([nil])]), int_bin_tree)
+
+      # {1, {2, nil, nil}, {3, nil, nil}} is a valid tree
+      leaf = tuple([integer(), atom([nil]), atom([nil])])
+      assert subtype?(tuple([integer(), leaf, leaf]), int_bin_tree)
+
+      # wrong arity: {1, nil} not a subtype
+      refute subtype?(tuple([integer(), atom([nil])]), int_bin_tree)
+
+      # wrong tag type: {float, nil, nil} not a subtype
+      refute subtype?(tuple([float(), atom([nil]), atom([nil])]), int_bin_tree)
+
+      # X = non_empty_list(integer(), X) | non_empty_list(integer()) | []
+      # Y = list(integer())
+      gen = %{
+        X: fn recur ->
+          non_empty_list(integer(), recur.(:X))
+          |> union(non_empty_list(integer(), empty_list()))
+          |> union(empty_list())
+        end
+      }
+
+      tx = recursive(gen)[:X] |> to_descr()
+      assert equal?(tx, list(integer()))
+
+      # X = %{outer: %{inner: X}} | nil
+      # Y = %{outer: %{inner: Y}} | %{outer: %{inner: integer}} | nil
+      %{X: nx, Y: ny} =
+        recursive(%{
+          X: fn recur ->
+            closed_map(outer: closed_map(inner: recur.(:X))) |> union(atom([nil]))
+          end,
+          Y: fn recur ->
+            closed_map(outer: closed_map(inner: recur.(:Y)))
+            |> union(closed_map(outer: closed_map(inner: integer())))
+            |> union(atom([nil]))
           end
         })
 
-      refute empty?(nx)
+      assert subtype?(nx, ny), "nested map wrapping map with recursive field"
 
-      # X = non_empty_list(X, []) | []
-      # Y = non_empty_list(Y, []) | non_empty_list(integer(), []) | []
-      nodes =
+      # X = non_empty_list(non_empty_list(X, empty_list()), empty_list()) | nil
+      # Y = non_empty_list(non_empty_list(Y, empty_list()), empty_list())
+      #        | non_empty_list(non_empty_list(integer(), empty_list()), empty_list()) | nil
+      %{X: nx, Y: ny} =
         recursive(%{
-          x: fn state ->
-            union(
-              non_empty_list({make_ref(), state, state[:x]}, empty_list()),
+          X: fn recur ->
+            non_empty_list(
+              non_empty_list(recur.(:X), empty_list()),
               empty_list()
             )
+            |> union(atom([nil]))
           end,
-          y: fn state ->
-            union(
-              union(
-                non_empty_list({make_ref(), state, state[:y]}, empty_list()),
-                non_empty_list(integer(), empty_list())
-              ),
+          Y: fn recur ->
+            non_empty_list(
+              non_empty_list(recur.(:Y), empty_list()),
               empty_list()
             )
+            |> union(non_empty_list(non_empty_list(integer(), empty_list()), empty_list()))
+            |> union(atom([nil]))
           end
         })
 
-      nx = nodes[:x]
-      ny = nodes[:y]
+      assert subtype?(nx, ny), "nested list wrapping list with recursive element"
 
-      # Just check if the difference is computable (without emptiness check)
-      d = difference(nx, ny)
-      assert empty?(d)
-      assert subtype?(nx, ny)
-    end
-
-    test "binary trees" do
-      # Tree = {atom, Tree, Tree} | nil: not empty
-      %{T: nt} =
+      ## nested tuple wrapping tuple with recursive element
+      # X = {{X}} | nil, Y = {{Y}} | {{integer()}} | nil
+      %{X: nx, Y: ny} =
         recursive(%{
-          T: fn state ->
-            tuple([
-              atom(),
-              make_node(state, state[:T]),
-              make_node(state, state[:T])
-            ])
+          X: fn recur -> tuple([tuple([recur.(:X)])]) |> union(atom([nil])) end,
+          Y: fn recur ->
+            tuple([tuple([recur.(:Y)])])
+            |> union(tuple([tuple([integer()])]))
             |> union(atom([nil]))
           end
         })
 
-      refute empty?(nt)
-    end
+      assert subtype?(nx, ny)
 
-    test "regular expressions (on lists)" do
-      # int_then_bool_list = {integer(), int_list} or bool_list
-      # bool_list = {boolean(), bool_list} or []
-      # int_or_bool_list = {integer() or boolean(), int_or_bool_list} or []
-      %{IntThenBoolList: int_then_bool_list, BoolList: bool_list, IntOrBoolList: int_or_bool_list} =
+      ## map linked list: BoolChain <: IntOrBoolChain
+      # BoolChain = %{val: boolean(), next: BoolChain} | %{}
+      # IntOrBoolChain = %{val: integer() | boolean(), next: IntOrBoolChain} | %{}
+      %{BoolChain: bc, IntOrBoolChain: iobc} =
         recursive(%{
-          IntThenBoolList: fn state ->
-            union(
-              tuple([integer(), make_node(state, state[:IntThenBoolList])]),
-              make_node(state, state[:BoolList])
-            )
-          end,
-          BoolList: fn state ->
-            union(
-              tuple([boolean(), make_node(state, state[:BoolList])]),
-              empty_list()
-            )
+          BoolChain: fn recur ->
+            closed_map(val: boolean(), next: recur.(:BoolChain)) |> union(empty_map())
           end,
-          IntOrBoolList: fn state ->
-            union(
-              tuple([union(integer(), boolean()), make_node(state, state[:IntOrBoolList])]),
-              empty_list()
+          IntOrBoolChain: fn recur ->
+            closed_map(
+              val: union(integer(), boolean()),
+              next: recur.(:IntOrBoolChain)
             )
+            |> union(empty_map())
           end
         })
 
-      refute empty?(int_then_bool_list)
-      refute empty?(bool_list)
-      refute empty?(int_or_bool_list)
-      assert subtype?(bool_list, int_or_bool_list)
-      assert subtype?(int_then_bool_list, int_or_bool_list)
+      assert subtype?(bc, iobc)
     end
 
-    test "regular expressions (on maps)" do
-      # bool_chain = %{val: boolean(), next: bool_chain} | %{}
-      # int_or_bool_chain = %{val: integer() | boolean(), next: int_or_bool_chain} | %{}
-      # int_then_bool_chain = %{val: integer(), next: int_then_bool_chain} | bool_chain
-      %{
-        IntThenBoolChain: int_then_bool_chain,
-        BoolChain: bool_chain,
-        IntOrBoolChain: int_or_bool_chain
-      } =
-        recursive(%{
-          IntThenBoolChain: fn state ->
-            union(
-              closed_map(val: integer(), next: make_node(state, state[:IntThenBoolChain])),
-              make_node(state, state[:BoolChain])
-            )
-          end,
-          BoolChain: fn state ->
-            union(
-              closed_map(val: boolean(), next: make_node(state, state[:BoolChain])),
-              empty_map()
-            )
-          end,
-          IntOrBoolChain: fn state ->
-            union(
-              closed_map(
-                val: union(integer(), boolean()),
-                next: make_node(state, state[:IntOrBoolChain])
-              ),
-              empty_map()
-            )
-          end
-        })
+    test "set operations accept nodes" do
+      # union works on nodes and descrs
+      n = to_node(integer())
+      assert equal?(union(n, float()), union(integer(), float()))
+      assert equal?(union(atom(), n), union(atom(), integer()))
+
+      # intersection of a node and a descr
+      n = to_node(union(integer(), atom()))
+      assert equal?(intersection(n, integer()), integer())
+      assert equal?(intersection(atom(), n), atom())
 
-      refute empty?(int_then_bool_chain)
-      refute empty?(bool_chain)
-      refute empty?(int_or_bool_chain)
-      assert subtype?(bool_chain, int_or_bool_chain)
-      assert subtype?(int_then_bool_chain, int_or_bool_chain)
+      # difference of a node and a descr
+      n = to_node(union(integer(), float()))
+      assert equal?(difference(n, float()), integer())
+      assert equal?(difference(union(integer(), float()), to_node(float())), integer())
     end
 
-    test "regular expressions (on non-empty lists)" do
-      # bool_list = non_empty_list(boolean(), bool_list) | []
-      # int_or_bool_list = non_empty_list(integer() | boolean(), int_or_bool_list) | []
-      # int_then_bool_list = non_empty_list(integer(), int_then_bool_list) | bool_list
-      %{IntThenBoolList: int_then_bool_list, BoolList: bool_list, IntOrBoolList: int_or_bool_list} =
+    test "set operations on nodes built with constructors" do
+      ## map intersection inside nodes
+      # X = %{a: %{a: X}} | %{a: %{a: atom()}}
+      # Y = %{a: %{a: X}} | %{a: %{a: atom()}}
+      %{X: nx, Y: ny} =
         recursive(%{
-          IntThenBoolList: fn state ->
-            union(
-              non_empty_list(integer(), make_node(state, state[:IntThenBoolList])),
-              make_node(state, state[:BoolList])
-            )
-          end,
-          BoolList: fn state ->
-            union(
-              non_empty_list(boolean(), make_node(state, state[:BoolList])),
-              empty_list()
-            )
+          X: fn recur ->
+            closed_map(a: closed_map(a: recur.(:X)))
+            |> union(closed_map(a: closed_map(a: atom())))
           end,
-          IntOrBoolList: fn state ->
-            union(
-              non_empty_list(
-                union(integer(), boolean()),
-                make_node(state, state[:IntOrBoolList])
-              ),
-              empty_list()
-            )
+          Y: fn recur ->
+            closed_map(a: closed_map(a: recur.(:Y)))
+            |> union(closed_map(a: closed_map(a: atom())))
           end
         })
 
-      refute empty?(int_then_bool_list)
-      refute empty?(bool_list)
-      refute empty?(int_or_bool_list)
-      assert subtype?(bool_list, int_or_bool_list)
-      assert subtype?(int_then_bool_list, int_or_bool_list)
-    end
+      refute empty?(intersection(nx, ny))
+      assert equal?(union(nx, ny), nx)
 
-    test "mixed constructors" do
-      # X = {integer(), X} | non_empty_list(X, []) | nil: not empty
-      %{X: nx} =
+      # This example loops if we do not make a deep search for recursive nodes when disabling
+      # map union optimizations.
+      # X = %{a: open_map(), b: open_map()} | nil
+      # Y = %{a: %{inner: Y}, b: %{inner: Y}}
+      #   | %{a: %{inner: atom()}, b: %{inner: atom()}}
+      %{X: nx, Y: ny} =
         recursive(%{
-          X: fn state ->
-            union(
-              tuple([integer(), make_node(state, state[:X])]),
-              union(
-                non_empty_list(make_node(state, state[:X]), empty_list()),
-                atom([nil])
-              )
+          X: fn _recur -> closed_map(a: open_map(), b: open_map()) |> union(atom([nil])) end,
+          Y: fn recur ->
+            closed_map(
+              a: closed_map(inner: recur.(:Y)),
+              b: closed_map(inner: recur.(:Y))
             )
+            |> union(closed_map(a: closed_map(inner: atom()), b: closed_map(inner: atom())))
           end
         })
 
-      refute empty?(nx)
-      assert subtype?(atom([nil]), nx)
-      assert subtype?(tuple([integer(), atom([nil])]), nx)
-    end
-
-    test "non-recursive equations" do
-      # X = integer(): not empty
-      %{X: nx} = recursive(%{X: fn _state -> integer() end})
-      refute empty?(nx)
-
-      # X = none(): empty
-      %{X: nx} = recursive(%{X: fn _state -> none() end})
-      assert empty?(nx)
-
-      # X = term(): not empty
-      %{X: nx} = recursive(%{X: fn _state -> :term end})
-      refute empty?(nx)
-
-      # empty equation map
-      result = recursive(%{})
-      assert result == %{}
-    end
-
-    test "difference of node with itself" do
-      # difference(node, node) is empty for non-recursive node
-      node = to_node(union(integer(), atom([nil])))
-      assert empty?(difference(node, node))
-    end
-  end
+      assert equal?(union(nx, ny), nx)
 
-  ## Subtyping on recursive types
-
-  describe "subtyping on recursive types" do
-    test "simple recursive list" do
-      # X = {integer(), X} | nil
-      %{X: nx} =
+      # X = {{X}} | {{atom()}}
+      # Y = {{Y}} | {{atom()}}
+      %{X: nx, Y: ny} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
+          X: fn recur -> tuple([tuple([recur.(:X)])]) |> union(tuple([tuple([atom()])])) end,
+          Y: fn recur -> tuple([tuple([recur.(:Y)])]) |> union(tuple([tuple([atom()])])) end
         })
 
-      # nil <: X
-      assert subtype?(atom([nil]), nx)
-
-      # {integer(), nil} <: X
-      assert subtype?(tuple([integer(), atom([nil])]), nx)
-
-      # {integer(), {integer(), nil}} <: X
-      inner = tuple([integer(), atom([nil])])
-      assert subtype?(tuple([integer(), inner]), nx)
-
-      # depth 3: {int, {int, {int, nil}}} <: X
-      d2 = tuple([integer(), inner])
-      assert subtype?(tuple([integer(), d2]), nx)
-
-      # depth 4
-      d3 = tuple([integer(), d2])
-      assert subtype?(tuple([integer(), d3]), nx)
-
-      # atom(:foo) is not a subtype
-      refute subtype?(atom([:foo]), nx)
-
-      # a plain integer is not a subtype
-      refute subtype?(integer(), nx)
-
-      # wrong element type: {float(), nil}
-      refute subtype?(tuple([float(), atom([nil])]), nx)
-
-      # {integer(), atom(:foo)}: :foo is not X
-      refute subtype?(tuple([integer(), atom([:foo])]), nx)
-
-      # union of finite unfoldings is a subtype
-      d1 = tuple([integer(), atom([nil])])
-      d2 = tuple([integer(), d1])
-      assert subtype?(union(atom([nil]), union(d1, d2)), nx)
-
-      # X <: term()
-      assert subtype?(nx, :term)
-
-      # none() <: X
-      assert subtype?(none(), nx)
-    end
+      refute empty?(intersection(nx, ny))
+      assert equal?(union(nx, ny), nx)
 
-    test "mutual recursion" do
-      # X = {int, Y} | nil, Y = {bool, X} | nil
+      # X = %{integer() => X} | %{integer() => atom()}
+      # Y = %{integer() => Y} | %{integer() => atom()}
       %{X: nx, Y: ny} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
+          X: fn recur ->
+            closed_map([{[:integer], recur.(:X)}]) |> union(closed_map([{[:integer], atom()}]))
           end,
-          Y: fn state ->
-            tuple([boolean(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # nil <: X, nil <: Y
-      assert subtype?(atom([nil]), nx)
-      assert subtype?(atom([nil]), ny)
-
-      # {integer(), nil} <: X
-      assert subtype?(tuple([integer(), atom([nil])]), nx)
-
-      # {boolean(), nil} <: Y
-      assert subtype?(tuple([boolean(), atom([nil])]), ny)
-
-      # {int, {bool, nil}} <: X
-      inner_y = tuple([boolean(), atom([nil])])
-      assert subtype?(tuple([integer(), inner_y]), nx)
-
-      # {bool, {int, nil}} <: Y
-      inner_x = tuple([integer(), atom([nil])])
-      assert subtype?(tuple([boolean(), inner_x]), ny)
-
-      # {int, {bool, {int, nil}}} <: X
-      level3 = tuple([integer(), atom([nil])])
-      level2 = tuple([boolean(), level3])
-      assert subtype?(tuple([integer(), level2]), nx)
-
-      # both X and Y <: term()
-      assert subtype?(nx, :term)
-      assert subtype?(ny, :term)
-    end
-
-    test "recursive lists" do
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(integer(), make_node(state, state[:X]))
-            |> union(empty_list())
-          end
-        })
-
-      # [] <: X
-      assert subtype?(empty_list(), nx)
-
-      # non_empty_list(integer()) <: X (terminates with [])
-      assert subtype?(non_empty_list(integer()), nx)
-    end
-
-    test "binary trees" do
-      %{T: nt} =
-        recursive(%{
-          T: fn state ->
-            tuple([
-              integer(),
-              make_node(state, state[:T]),
-              make_node(state, state[:T])
-            ])
-            |> union(atom([nil]))
+          Y: fn recur ->
+            closed_map([{[:integer], recur.(:Y)}]) |> union(closed_map([{[:integer], atom()}]))
           end
         })
 
-      # nil is a valid tree
-      assert subtype?(atom([nil]), nt)
-
-      # {42, nil, nil} is a valid tree
-      assert subtype?(tuple([integer(), atom([nil]), atom([nil])]), nt)
-
-      # {1, {2, nil, nil}, {3, nil, nil}} is a valid tree
-      leaf = tuple([integer(), atom([nil]), atom([nil])])
-      assert subtype?(tuple([integer(), leaf, leaf]), nt)
-
-      # wrong arity: {1, nil} not a subtype
-      refute subtype?(tuple([integer(), atom([nil])]), nt)
-
-      # wrong tag type: {float, nil, nil} not a subtype
-      refute subtype?(tuple([float(), atom([nil]), atom([nil])]), nt)
-    end
+      refute empty?(intersection(nx, ny))
+      assert equal?(union(nx, ny), nx)
 
-    test "expression trees" do
-      # Expr = integer() | {atom, Expr, Expr}, Binop = {atom, Expr, Expr}
-      %{Expr: nexpr, Binop: nbinop} =
+      ## three recursive maps
+      # A = %{x: A} | %{x: atom()}, B = %{x: B} | %{x: integer()}, C = %{x: C} | %{x: term()}
+      # intersection(A, intersection(B, C)) should be empty (atom ∩ integer = ∅)
+      %{A: na, B: nb, C: nc} =
         recursive(%{
-          Expr: fn state ->
-            union(
-              integer(),
-              tuple([
-                atom(),
-                make_node(state, state[:Expr]),
-                make_node(state, state[:Expr])
-              ])
-            )
-          end,
-          Binop: fn state ->
-            tuple([atom(), make_node(state, state[:Expr]), make_node(state, state[:Expr])])
-          end
+          A: fn recur -> closed_map(x: recur.(:A)) |> union(closed_map(x: atom())) end,
+          B: fn recur -> closed_map(x: recur.(:B)) |> union(closed_map(x: integer())) end,
+          C: fn recur -> closed_map(x: recur.(:C)) |> union(closed_map(x: term())) end
         })
 
-      refute empty?(nexpr)
-      refute empty?(nbinop)
+      assert empty?(intersection(na, intersection(nb, nc)))
+      assert subtype?(na, nc)
+      refute subtype?(nc, na)
 
-      # 42 is an Expr
-      assert subtype?(integer(), nexpr)
+      ## union then intersection of recursive maps
+      # X = %{a: X} | %{a: atom()}, Y = %{a: Y} | %{a: atom()}
+      # intersection(union(X, Y), X) should be non-empty
+      gen = %{
+        X: fn recur -> closed_map(a: recur.(:X)) |> union(closed_map(a: atom())) end,
+        Y: fn recur -> closed_map(a: recur.(:Y)) |> union(closed_map(a: atom())) end
+      }
 
-      # {:+, 1, 2} is an Expr and a Binop
-      assert subtype?(tuple([atom(), integer(), integer()]), nexpr)
-      assert subtype?(tuple([atom(), integer(), integer()]), nbinop)
+      %{X: nx, Y: ny} = recursive(gen)
 
-      # {:*, {:+, 1, 2}, 3} is an Expr
-      inner = tuple([atom(), integer(), integer()])
-      assert subtype?(tuple([atom(), inner, integer()]), nexpr)
+      refute empty?(intersection(union(nx, ny), nx))
+      assert equal?(intersection(union(nx, ny), nx), nx)
     end
 
-    test "disjoint?" do
+    test "type operators" do
+      ## tuple operators on descr with recursive node element
+      # X = {integer(), X} | {integer(), atom()}
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
+          X: fn recur -> tuple([integer(), recur.(:X)]) |> union(tuple([integer(), atom()])) end
         })
 
-      # recursive type is disjoint from unrelated scalars
-      assert disjoint?(nx, float())
-      assert disjoint?(nx, binary())
-      assert disjoint?(nx, pid())
-
-      # not disjoint from base case
-      refute disjoint?(nx, atom([nil]))
-
-      # not disjoint from tuple()
-      refute disjoint?(nx, tuple())
-    end
-  end
-
-  ## Set operations on recursive types
-
-  describe "set operations on recursive types" do
-    test "union" do
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
+      t = to_descr(nx)
 
-      # union with none() is identity
-      assert equal?(union(nx, none()), nx)
+      # tuple_fetch
+      assert {false, type} = tuple_fetch(t, 0)
+      assert equal?(type, integer())
+      assert {false, _type} = tuple_fetch(t, 1)
 
-      # union of two distinct recursive types is not empty
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            tuple([float(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end
-        })
+      # tuple_values
+      result = tuple_values(t)
+      assert subtype?(integer(), result)
 
-      refute empty?(union(nx, ny))
+      # tuple_delete_at
+      result = tuple_delete_at(t, 0)
+      assert {false, _type} = tuple_fetch(result, 0)
 
-      # union of stepped recursive type with another type
-      dx = to_descr(nx)
-      refute empty?(union(dx, float()))
-    end
+      # tuple_insert_at
+      result = tuple_insert_at(t, 0, boolean())
+      assert {false, type} = tuple_fetch(result, 0)
+      assert equal?(type, boolean())
 
-    test "intersection" do
+      # tuple fetch
+      # X = {X} | {atom()}
       %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # intersection with term() is identity
-      assert equal?(intersection(nx, :term), nx)
-
-      # intersection with disjoint type is empty
-      assert empty?(intersection(nx, float()))
-
-      # intersection of two recursive types sharing base case is not empty
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            tuple([float(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end
-        })
-
-      refute empty?(intersection(nx, ny))
+        recursive(%{X: fn recur -> tuple([recur.(:X)]) |> union(tuple([atom()])) end})
 
-      # intersection of stepped type with its base case
-      dx = to_descr(nx)
-      assert equal?(intersection(dx, atom()), atom([nil]))
-    end
+      tx = to_descr(nx)
+      t = difference(tx, tuple([atom()]))
+      assert {false, type} = tuple_fetch(t, 0)
+      assert equal?(type, tx)
 
-    test "difference" do
+      ## map_fetch_key on descr with recursive node value
+      # X = %{a: integer(), b: X} | %{a: integer(), b: atom()}
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
+          X: fn recur ->
+            closed_map(a: integer(), b: recur.(:X)) |> union(closed_map(a: integer(), b: atom()))
           end
         })
 
-      # difference of stepped type minus base case: only tuple part remains
-      dx = to_descr(nx)
-      result = difference(dx, atom([nil]))
-      assert is_map_key(result, :tuple)
-      refute is_map_key(result, :atom)
-    end
-  end
-
-  ## Recursive type edge cases
-
-  describe "recursive type edge cases" do
-    test "non-recursive equations" do
-      # X = integer()
-      %{X: nx} = recursive(%{X: fn _state -> integer() end})
-      assert equal?(to_descr(nx), integer())
-
-      # X = none()
-      %{X: nx} = recursive(%{X: fn _state -> none() end})
-      assert empty?(nx)
-
-      # X = term()
-      %{X: nx} = recursive(%{X: fn _state -> :term end})
-      assert equal?(to_descr(nx), :term)
-
-      # two independent non-recursive equations
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn _state -> integer() end,
-          Y: fn _state -> atom() end
-        })
-
-      assert equal?(to_descr(nx), integer())
-      assert equal?(to_descr(ny), atom())
-
-      # compound type
-      %{X: nx} =
-        recursive(%{
-          X: fn _state -> union(integer(), tuple([atom(), float()])) end
-        })
-
-      assert equal?(to_descr(nx), union(integer(), tuple([atom(), float()])))
-    end
+      assert {false, type} = map_fetch_key(to_descr(nx), :a)
+      assert equal?(type, integer())
+      assert {false, _type} = map_fetch_key(to_descr(nx), :b)
 
-    test "multiple base cases" do
-      # X = {int, X} | nil | :done | :error
+      ## list_hd and list_tl on descr with recursive node tail
+      # X = non_empty_list(integer(), X) | non_empty_list(integer(), [])
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil, :done, :error]))
+          X: fn recur ->
+            non_empty_list(integer(), recur.(:X))
+            |> union(non_empty_list(integer(), empty_list()))
           end
         })
 
-      refute empty?(nx)
-      assert subtype?(atom([nil]), nx)
-      assert subtype?(atom([:done]), nx)
-      assert subtype?(atom([:error]), nx)
-    end
+      assert {:ok, type} = list_hd(to_descr(nx))
+      assert equal?(type, integer())
+      assert {:ok, _type} = list_tl(to_descr(nx))
 
-    test "broad tuple elements" do
-      # X = {term(), X} | nil
+      ## list_hd on descr with recursive node as head element
+      # X = non_empty_list(X, []) | non_empty_list(atom(), [])
       %{X: nx} =
         recursive(%{
-          X: fn state ->
-            tuple([:term, make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      refute empty?(nx)
-      assert subtype?(tuple([:term, atom([nil])]), nx)
-    end
-
-    test "parallel independent recursion" do
-      # X = {int, X}|nil, Y = {float, Y}|nil (independent)
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([float(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end
-        })
-
-      refute empty?(nx)
-      refute empty?(ny)
-
-      # they share a state but are independent types
-      assert subtype?(tuple([integer(), atom([nil])]), nx)
-      assert subtype?(tuple([float(), atom([nil])]), ny)
-      refute subtype?(tuple([float(), atom([nil])]), nx)
-      refute subtype?(tuple([integer(), atom([nil])]), ny)
-    end
-
-    test "empty equation map" do
-      result = recursive(%{})
-      assert result == %{}
-    end
-
-    test "node identity" do
-      # each node from recursive/1 gets a unique id
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([boolean(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      {id_x, _, _} = nx
-      {id_y, _, _} = ny
-      assert id_x != id_y
-
-      # make_ref ensures distinct ids even for same generator
-      gen = fn _state -> integer() end
-      {id1, _, _} = make_node(%{}, gen)
-      {id2, _, _} = make_node(%{}, gen)
-      assert id1 != id2
-
-      # memoization prevents infinite loop on cyclic X = {X}
-      %{X: nx} =
-        recursive(%{
-          X: fn state -> tuple([make_node(state, state[:X])]) end
-        })
-
-      assert empty?(nx)
-
-      # memoization prevents infinite loop on mutual cycle X = {Y}, Y = {X}
-      %{X: nx, Y: ny} =
-        recursive(%{
-          X: fn state -> tuple([make_node(state, state[:Y])]) end,
-          Y: fn state -> tuple([make_node(state, state[:X])]) end
-        })
-
-      assert empty?(nx)
-      assert empty?(ny)
-    end
-
-    test "stepping recursive nodes" do
-      # stepping produces a descr with :tuple and :atom keys
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      d = to_descr(nx)
-      assert is_map_key(d, :tuple)
-      assert is_map_key(d, :atom)
-
-      # stepping twice does not crash (coinductive laziness)
-      d1 = to_descr(nx)
-      assert is_map(d1)
-      d2 = to_descr(nx)
-      assert is_map(d2)
-    end
-  end
-
-  ## Cross-recursive subtyping (two-node blind spots)
-
-  describe "cross-recursive subtyping" do
-    test "list tail recursion: X <: Y where both recurse in tail position" do
-      # X = non_empty_list(integer(), X) | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(integer(), make_node(state, state[:X]))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = non_empty_list(integer(), Y) | non_empty_list(integer(), nil) | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            non_empty_list(integer(), make_node(state, state[:Y]))
-            |> union(non_empty_list(integer(), atom([nil])))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "list element recursion: X <: Y where both recurse in element type" do
-      # X = [X] | nil  (list whose elements are themselves X)
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(make_node(state, state[:X]))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = [Y] | [integer()] | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            non_empty_list(make_node(state, state[:Y]))
-            |> union(non_empty_list(integer()))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "list negative case: recursive list is NOT subtype of unrelated type" do
-      # X = non_empty_list(integer(), X) | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(integer(), make_node(state, state[:X]))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = non_empty_list(float()) | nil (different element type)
-      ny = union(non_empty_list(float()), atom([nil]))
-
-      refute subtype?(nx, ny)
-    end
-
-    test "tuple element recursion: X <: Y where both recurse in element" do
-      # X = {X} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = {Y} | {integer()} | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            tuple([make_node(state, state[:Y])])
-            |> union(tuple([integer()]))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "map value recursion: X <: Y where both recurse in field value" do
-      # X = %{a: X} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            closed_map(a: make_node(state, state[:X]))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = %{a: Y} | %{a: integer()} | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            closed_map(a: make_node(state, state[:Y]))
-            |> union(closed_map(a: integer()))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "mutual recursion across systems" do
-      # X = {Y} | nil, Y = {X} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            tuple([make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # A = {B} | nil, B = {A} | {integer()} | nil
-      %{A: na} =
-        recursive(%{
-          A: fn state ->
-            tuple([make_node(state, state[:B])])
-            |> union(atom([nil]))
-          end,
-          B: fn state ->
-            tuple([make_node(state, state[:A])])
-            |> union(tuple([integer()]))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, na)
-    end
-
-    test "tuple negative: recursive tuple NOT subtype of finite tuple" do
-      # X = {X} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      ny = union(tuple([integer()]), atom([nil]))
-      refute subtype?(nx, ny)
-    end
-
-    test "tuple 2-element, recursive in 2nd position" do
-      # X = {int, X} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([integer(), make_node(state, state[:X])])
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = {int, Y} | {int, nil} | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            tuple([integer(), make_node(state, state[:Y])])
-            |> union(tuple([integer(), atom([nil])]))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "map negative: recursive map NOT subtype when base cases differ" do
-      # X = %{a: X} | %{a: atom()}
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            closed_map(a: make_node(state, state[:X]))
-            |> union(closed_map(a: atom()))
-          end
-        })
-
-      # Y = %{a: Y} | %{a: integer()}
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            closed_map(a: make_node(state, state[:Y]))
-            |> union(closed_map(a: integer()))
-          end
-        })
-
-      refute subtype?(nx, ny)
-    end
-
-    test "list element negative: recursive list NOT subtype when base cases differ" do
-      # X = [X] | [atom()] | []
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(make_node(state, state[:X]))
-            |> union(non_empty_list(atom()))
-            |> union(empty_list())
-          end
-        })
-
-      # Y = [Y] | [integer()] | []
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            non_empty_list(make_node(state, state[:Y]))
-            |> union(non_empty_list(integer()))
-            |> union(empty_list())
-          end
-        })
-
-      refute subtype?(nx, ny)
-    end
-
-    test "same-shape recursive list: BoolList <: IntOrBoolList" do
-      # BoolList = non_empty_list(boolean(), BoolList) | []
-      # IntOrBoolList = non_empty_list(integer() | boolean(), IntOrBoolList) | []
-      %{BoolList: bl, IntOrBoolList: iobl} =
-        recursive(%{
-          BoolList: fn state ->
-            non_empty_list(boolean(), make_node(state, state[:BoolList]))
-            |> union(empty_list())
-          end,
-          IntOrBoolList: fn state ->
-            non_empty_list(union(integer(), boolean()), make_node(state, state[:IntOrBoolList]))
-            |> union(empty_list())
-          end
-        })
-
-      assert subtype?(bl, iobl)
-    end
-
-    test "recursive list with different tail: IntThenBoolList <: IntOrBoolList" do
-      # IntThenBoolList = non_empty_list(integer(), IntThenBoolList) | BoolList
-      # BoolList = non_empty_list(boolean(), BoolList) | []
-      # IntOrBoolList = non_empty_list(integer() | boolean(), IntOrBoolList) | []
-      %{IntThenBoolList: itbl, IntOrBoolList: iobl} =
-        recursive(%{
-          IntThenBoolList: fn state ->
-            non_empty_list(integer(), make_node(state, state[:IntThenBoolList]))
-            |> union(make_node(state, state[:BoolList]))
-          end,
-          BoolList: fn state ->
-            non_empty_list(boolean(), make_node(state, state[:BoolList]))
-            |> union(empty_list())
-          end,
-          IntOrBoolList: fn state ->
-            non_empty_list(union(integer(), boolean()), make_node(state, state[:IntOrBoolList]))
-            |> union(empty_list())
-          end
-        })
-
-      assert subtype?(itbl, iobl)
-    end
-
-    test "map linked list: BoolChain <: IntOrBoolChain" do
-      # BoolChain = %{val: boolean(), next: BoolChain} | %{}
-      # IntOrBoolChain = %{val: integer() | boolean(), next: IntOrBoolChain} | %{}
-      %{BoolChain: bc, IntOrBoolChain: iobc} =
-        recursive(%{
-          BoolChain: fn state ->
-            closed_map(val: boolean(), next: make_node(state, state[:BoolChain]))
-            |> union(empty_map())
-          end,
-          IntOrBoolChain: fn state ->
-            closed_map(
-              val: union(integer(), boolean()),
-              next: make_node(state, state[:IntOrBoolChain])
-            )
-            |> union(empty_map())
-          end
-        })
-
-      assert subtype?(bc, iobc)
-    end
-
-    test "cross-container mutual recursion: tuple + list" do
-      # X = {Y} | nil, Y = [X]
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([make_node(state, state[:Y])])
-            |> union(atom([nil]))
-          end,
-          Y: fn state ->
-            non_empty_list(make_node(state, state[:X]), empty_list())
-            |> union(empty_list())
-          end
-        })
-
-      # A = {B} | {[integer()]} | nil, B = [A] | [integer()]
-      %{A: na} =
-        recursive(%{
-          A: fn state ->
-            tuple([make_node(state, state[:B])])
-            |> union(tuple([non_empty_list(integer(), empty_list())]))
-            |> union(atom([nil]))
-          end,
-          B: fn state ->
-            non_empty_list(make_node(state, state[:A]), empty_list())
-            |> union(non_empty_list(integer(), empty_list()))
-            |> union(empty_list())
-          end
-        })
-
-      assert subtype?(nx, na)
-    end
-
-    # TODO: nested container recursion — node is inside a tuple inside a tuple.
-    # X = {{X}} | nil, Y = {{Y}} | {{integer()}} | nil
-    # @tag :skip
-    test "nested tuple wrapping tuple with recursive element" do
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            tuple([tuple([make_node(state, state[:X])])])
-            |> union(atom([nil]))
-          end
-        })
-
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            tuple([tuple([make_node(state, state[:Y])])])
-            |> union(tuple([tuple([integer()])]))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "nested map wrapping map with recursive field" do
-      # X = %{outer: %{inner: X}} | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            closed_map(outer: closed_map(inner: make_node(state, state[:X])))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = %{outer: %{inner: Y}} | %{outer: %{inner: integer()}} | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            closed_map(outer: closed_map(inner: make_node(state, state[:Y])))
-            |> union(closed_map(outer: closed_map(inner: integer())))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "nested map negative with recursive field" do
-      # X = %{outer: %{inner: X}} | %{outer: %{inner: atom()}}
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            closed_map(outer: closed_map(inner: make_node(state, state[:X])))
-            |> union(closed_map(outer: closed_map(inner: atom())))
-          end
-        })
-
-      # Y = %{outer: %{inner: Y}} | %{outer: %{inner: integer()}}
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            closed_map(outer: closed_map(inner: make_node(state, state[:Y])))
-            |> union(closed_map(outer: closed_map(inner: integer())))
-          end
-        })
-
-      refute subtype?(nx, ny)
-    end
-
-    test "nested list wrapping list with recursive element" do
-      # X = [[X]] | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(
-              non_empty_list(make_node(state, state[:X]), empty_list()),
-              empty_list()
-            )
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = [[Y]] | [[integer()]] | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            non_empty_list(
-              non_empty_list(make_node(state, state[:Y]), empty_list()),
-              empty_list()
-            )
-            |> union(non_empty_list(non_empty_list(integer(), empty_list()), empty_list()))
-            |> union(atom([nil]))
-          end
-        })
-
-      assert subtype?(nx, ny)
-    end
-
-    test "nested list negative with recursive element" do
-      # X = [[X]] | [[atom()]] | nil
-      %{X: nx} =
-        recursive(%{
-          X: fn state ->
-            non_empty_list(
-              non_empty_list(make_node(state, state[:X]), empty_list()),
-              empty_list()
-            )
-            |> union(non_empty_list(non_empty_list(atom(), empty_list()), empty_list()))
-            |> union(atom([nil]))
-          end
-        })
-
-      # Y = [[Y]] | [[integer()]] | nil
-      %{Y: ny} =
-        recursive(%{
-          Y: fn state ->
-            non_empty_list(
-              non_empty_list(make_node(state, state[:Y]), empty_list()),
-              empty_list()
-            )
-            |> union(non_empty_list(non_empty_list(integer(), empty_list()), empty_list()))
-            |> union(atom([nil]))
+          X: fn recur ->
+            non_empty_list(recur.(:X), empty_list())
+            |> union(non_empty_list(atom(), empty_list()))
           end
         })
 
-      refute subtype?(nx, ny)
+      assert {:ok, _type} = list_hd(to_descr(nx))
     end
   end
 end