diff --git a/new.exs b/new.exs
index da15dae..99b16b8 100644
--- a/new.exs
+++ b/new.exs
@@ -548,10 +548,60 @@ defmodule Tdd.Predicate.Info do
 
   @doc "Returns a map of traits for a given predicate variable."
   @spec get_traits(term()) :: map() | nil
-  def get_traits({0, :is_atom, _, _}), do: %{type: :primary, category: :atom}
-  def get_traits({0, :is_integer, _, _}), do: %{type: :primary, category: :integer}
-  def get_traits({0, :is_list, _, _}), do: %{type: :primary, category: :list}
-  def get_traits({0, :is_tuple, _, _}), do: %{type: :primary, category: :tuple}
+
+  # --- THIS IS THE FIX ---
+  # Add explicit negative implications for primary types. When a value is proven
+  # to be of one primary type, it is implicitly proven NOT to be of the others.
+
+  def get_traits({0, :is_atom, _, _}) do
+    %{
+      type: :primary,
+      category: :atom,
+      implies: [
+        {Variable.v_is_integer(), false},
+        {Variable.v_is_list(), false},
+        {Variable.v_is_tuple(), false}
+      ]
+    }
+  end
+
+  def get_traits({0, :is_integer, _, _}) do
+    %{
+      type: :primary,
+      category: :integer,
+      implies: [
+        {Variable.v_is_atom(), false},
+        {Variable.v_is_list(), false},
+        {Variable.v_is_tuple(), false}
+      ]
+    }
+  end
+
+  def get_traits({0, :is_list, _, _}) do
+    %{
+      type: :primary,
+      category: :list,
+      implies: [
+        {Variable.v_is_atom(), false},
+        {Variable.v_is_integer(), false},
+        {Variable.v_is_tuple(), false}
+      ]
+    }
+  end
+
+  def get_traits({0, :is_tuple, _, _}) do
+    %{
+      type: :primary,
+      category: :tuple,
+      implies: [
+        {Variable.v_is_atom(), false},
+        {Variable.v_is_integer(), false},
+        {Variable.v_is_list(), false}
+      ]
+    }
+  end
+
+  # --- The rest of the module is unchanged ---
 
   def get_traits({1, :value, _val, _}) do
     %{type: :atom_value, category: :atom, implies: [{Variable.v_is_atom(), true}]}
@@ -610,7 +660,6 @@ defmodule Tdd.Predicate.Info do
     }
   end
 
-  # Default case for unknown variables
   def get_traits(_), do: nil
 end
 
@@ -623,22 +672,14 @@ defmodule Tdd.Consistency.Engine do
   a set of assumptions about predicate variables (e.g., `{is_atom, true}`,
   `{value == :foo, true}`) and determines if that set is logically consistent.
 
-  The process involves two main steps:
-  1.  **Expansion**: The initial assumptions are expanded with all their logical
-      implications until a fixed point is reached. For example, `{value == :foo, true}`
-      implies `{is_atom, true}`.
-  2.  **Flat Check**: The fully expanded set of assumptions is checked against a
-      series of rules for contradictions (e.g., a value cannot be both an atom
-      and an integer).
-
-  The difficult problem of recursive consistency (checking sub-problems like a
-  list's head against an ambient constraint) is currently disabled, as it creates
-  a logical cycle with the TDD compiler.
+  The check is performed recursively. At each level, it:
+  1.  **Expands** assumptions with their local implications (e.g. `value == :foo` implies `is_atom`).
+  2.  **Checks for flat contradictions** at the current level (e.g., `is_atom` and `is_integer`).
+  3.  **Groups** assumptions by sub-problem (e.g., all `head(...)` predicates).
+  4.  **Recursively calls** the checker on each sub-problem with unwrapped predicates.
   """
 
   alias Tdd.Predicate.Info
-  alias Tdd.TypeReconstructor
-  alias Tdd.Compiler
   alias Tdd.Variable
 
   @doc """
@@ -648,85 +689,116 @@ defmodule Tdd.Consistency.Engine do
   """
   @spec check(map()) :: :consistent | :contradiction
   def check(assumptions) do
+    # The main entry point now calls the recursive helper.
+    # The logic from the old `check/1` is now inside `do_check/1`.
+    do_check(assumptions)
+  end
+
+  # --- The Core Recursive Checker ---
+
+  defp do_check(assumptions) do
+    # 1. Expand assumptions with immediate, local implications.
     with {:ok, expanded} <- expand_with_implications(assumptions),
+         # 2. Check for contradictions among the flat predicates at this level.
          :ok <- check_flat_consistency(expanded) do
-      # --- RECURSIVE CHECK DISABLED ---
-      # The call to `check_recursive_consistency/2` is disabled because it
-      # introduces a logical cycle:
-      #   simplify -> check -> spec_to_id -> simplify
-      # Solving this requires a more advanced architecture, such as passing a
-      # compiler context/handle to break the recursion. For now, we rely
-      # on the power of the main `simplify` algorithm to handle these recursive
-      # constraints by construction, and we focus on robust flat checks.
-      # :ok <- check_recursive_consistency(expanded, assumptions)
-      :consistent
+      # 3. Group the expanded assumptions into sub-problems based on their scope.
+      sub_problems =
+        expanded
+        |> Enum.group_by(fn {var, _val} -> (Info.get_traits(var) || %{})[:sub_key] end)
+        # Drop top-level keys, we only want recursive sub-problems.
+        |> Map.drop([nil])
+
+      # 4. If there are no sub-problems, and we passed the flat check, we're consistent.
+      if map_size(sub_problems) == 0 do
+        :consistent
+      else
+        # 5. Recursively check each sub-problem. Stop at the first contradiction.
+        Enum.find_value(sub_problems, :consistent, fn {_sub_key, sub_assumptions_list} ->
+          # Unwrap the variables for the recursive call
+          # e.g., {{5, :c_head, NESTED_VAR, _}, val} -> {NESTED_VAR, val}
+          remapped_assumptions = remap_sub_problem_vars(sub_assumptions_list)
+
+          # If any sub-problem is a contradiction, the whole set is.
+          case do_check(remapped_assumptions) do
+            # Not a contradiction, continue checking others.
+            :consistent -> nil
+            # Contradiction found, halt and return.
+            :contradiction -> :contradiction
+          end
+        end)
+      end
     else
+      # `expand_with_implications` or `check_flat_consistency` failed.
       :error -> :contradiction
     end
   end
 
-  # --- Step 1: Implication Expansion ---
+  # --- Recursive Checking Helpers ---
+
+  @doc "Converts a list of scoped assumptions into a map of base assumptions for a sub-problem."
+  defp remap_sub_problem_vars(assumptions_list) do
+    Map.new(assumptions_list, fn {var, val} ->
+      {unwrap_var(var), val}
+    end)
+  end
+
+  @doc "Extracts the inner predicate variable from a recursive variable."
+  defp unwrap_var(var) do
+    case var do
+      {4, :b_element, _index, nested_pred_var} -> nested_pred_var
+      {5, :c_head, nested_pred_var, _} -> nested_pred_var
+      {5, :d_tail, nested_pred_var, _} -> nested_pred_var
+      # This function is only called on vars that are known to be recursive,
+      # so other cases are not expected.
+      other -> other
+    end
+  end
+
+  # --- Step 1: Implication Expansion (Unchanged) ---
 
-  @doc "Expands an assumption map with all its logical implications."
   defp expand_with_implications(assumptions) do
-    # Start with the initial set of assumptions and expand until a fixed point is reached.
     expand_loop(assumptions, assumptions)
   end
 
   defp expand_loop(new_assumptions, all_assumptions) do
-    # For each of the newly added assumptions, find its implications.
     implications =
       Enum.flat_map(new_assumptions, fn
-        # An assumption `var == true` may have implications.
         {var, true} -> Map.get(Info.get_traits(var) || %{}, :implies, [])
-        # An assumption `var == false` has no simple implications in our current model.
         _ -> []
       end)
 
-    # Attempt to merge the new implications into the set of all assumptions.
     case Enum.reduce(implications, {:ok, %{}}, fn {implied_var, implied_val}, acc ->
            reduce_implication({implied_var, implied_val}, all_assumptions, acc)
          end) do
       {:error, :contradiction} ->
-        # A direct contradiction was found during expansion.
         :error
 
       {:ok, newly_added} when map_size(newly_added) == 0 ->
-        # Fixed point reached: no new, non-conflicting implications were found.
         {:ok, all_assumptions}
 
       {:ok, newly_added} ->
-        # Recursively expand with the newly found assumptions.
         expand_loop(newly_added, Map.merge(all_assumptions, newly_added))
     end
   end
 
-  # Helper for the implication reducer.
   defp reduce_implication({var, val}, all_assumptions, {:ok, new_acc}) do
     case Map.get(all_assumptions, var) do
-      nil ->
-        # This is a new piece of information. Add it to the set of newly_added things.
-        {:ok, Map.put(new_acc, var, val)}
-
-      ^val ->
-        # We already knew this. Continue without adding.
-        {:ok, new_acc}
-
-      _other_val ->
-        # Contradiction! The implication conflicts with an existing assumption.
-        {:error, :contradiction}
+      nil -> {:ok, Map.put(new_acc, var, val)}
+      ^val -> {:ok, new_acc}
+      _other_val -> {:error, :contradiction}
     end
   end
 
   defp reduce_implication(_implication, _all_assumptions, error_acc), do: error_acc
 
-  # --- Step 2: Flat Consistency Checks ---
+  # --- Step 2: Flat Consistency Checks (Unchanged) ---
 
   defp check_flat_consistency(assumptions) do
     with :ok <- check_primary_type_exclusivity(assumptions),
          :ok <- check_atom_consistency(assumptions),
          :ok <- check_list_consistency(assumptions),
-         :ok <- check_integer_consistency(assumptions) do
+         :ok <- check_integer_consistency(assumptions),
+         :ok <- check_tuple_consistency(assumptions) do
       :ok
     else
       :error -> :error
@@ -756,12 +828,18 @@ defmodule Tdd.Consistency.Engine do
     if MapSet.size(true_atom_values) > 1, do: :error, else: :ok
   end
 
-  defp check_list_consistency(assumptions) do
-    # This check is actually redundant if `expand_with_implications` works correctly,
-    # as the `implies` rules for head/tail would create an explicit contradiction
-    # with `is_empty == true`. However, it serves as a good safeguard.
-    is_empty = Map.get(assumptions, Variable.v_list_is_empty()) == true
+  defp check_tuple_consistency(assumptions) do
+    true_tuple_sizes =
+      Enum.reduce(assumptions, MapSet.new(), fn
+        {{4, :a_size, size, _}, true}, acc -> MapSet.put(acc, size)
+        _, acc -> acc
+      end)
 
+    if MapSet.size(true_tuple_sizes) > 1, do: :error, else: :ok
+  end
+
+  defp check_list_consistency(assumptions) do
+    is_empty = Map.get(assumptions, Variable.v_list_is_empty()) == true
     has_head_prop = Enum.any?(assumptions, &match?({{5, :c_head, _, _}, true}, &1))
     has_tail_prop = Enum.any?(assumptions, &match?({{5, :d_tail, _, _}, true}, &1))
 
@@ -792,21 +870,18 @@ defmodule Tdd.Consistency.Engine do
         )
   end
 
-  # **IMPROVED**: A clearer implementation for checking range validity.
   defp narrow_range(min, max) do
     is_invalid =
       case {min, max} do
         {:neg_inf, _} -> false
         {_, :pos_inf} -> false
         {m, n} when is_integer(m) and is_integer(n) -> m > n
-        # Should not happen with safe helpers
         _ -> false
       end
 
     if is_invalid, do: {:halt, :invalid}, else: {:cont, {min, max}}
   end
 
-  # **NEW**: Safe comparison helpers that understand :neg_inf and :pos_inf
   defp safe_max(:neg_inf, x), do: x
   defp safe_max(x, :neg_inf), do: x
   defp safe_max(:pos_inf, _), do: :pos_inf
@@ -818,62 +893,6 @@ defmodule Tdd.Consistency.Engine do
   defp safe_min(:neg_inf, _), do: :neg_inf
   defp safe_min(_, :neg_inf), do: :neg_inf
   defp safe_min(a, b), do: :erlang.min(a, b)
-
-  # --- Step 3: Recursive Consistency (Disabled but preserved) ---
-  defp check_recursive_consistency(assumptions, full_context) do
-    # 1. Gather all ambient constraints from the parent context.
-    ambient_constraints =
-      Enum.reduce(full_context, %{}, fn
-        # This now correctly handles all cases, not just `{var, true}`.
-        {var, true}, acc ->
-          case Info.get_traits(var) do
-            %{type: :list_recursive_ambient, ambient_constraint_spec: spec} ->
-              Map.merge(acc, %{head: spec, tail: spec})
-
-            _ ->
-              acc
-          end
-
-        _, acc ->
-          acc
-      end)
-
-    # 2. Partition assumptions into sub-problems (head, tail, tuple elements).
-    sub_problems =
-      Enum.group_by(assumptions, &Info.get_traits(elem(&1, 0))[:sub_key])
-      |> Map.drop([nil])
-
-    # 3. Check each sub-problem against its ambient constraint.
-    Enum.reduce_while(sub_problems, :ok, fn {sub_key, sub_assumptions_list}, _acc ->
-      ambient_spec = Map.get(ambient_constraints, sub_key)
-
-      # Re-map nested vars to base form for reconstruction
-      remapped_assumptions =
-        Map.new(sub_assumptions_list, fn {var, val} ->
-          # Simplified pattern match to extract the inner variable
-          {_cat, _pred, _idx, nested_var} = var
-          {nested_var, val}
-        end)
-
-      reconstructed_spec = TypeReconstructor.spec_from_assumptions(remapped_assumptions)
-
-      # Compile both specs to TDDs and check for subtyping.
-      # THIS IS THE SOURCE OF THE LOGICAL CYCLE
-      reconstructed_id = Compiler.spec_to_id(reconstructed_spec)
-      ambient_id = Compiler.spec_to_id(ambient_spec)
-
-      # if Tdd.is_subtype(reconstructed_id, ambient_id) do
-      # ...
-      # else
-      #   {:halt, :error}
-      # end
-      # For now, we assume it's okay to proceed.
-      case check(remapped_assumptions) do
-        :consistent -> {:cont, :ok}
-        :contradiction -> {:halt, :error}
-      end
-    end)
-  end
 end
 
 defmodule Tdd.Algo do
@@ -990,9 +1009,16 @@ defmodule Tdd.Algo do
   end
 
   # --- Unary Operation: Semantic Simplification ---
+  @doc """
+  Simplifies a TDD under a set of external assumptions.
+
+  This is the main public entry point. It sets up the context for the
+  coinductive cycle detection.
+  """
   @spec simplify(non_neg_integer(), map()) :: non_neg_integer
   def simplify(tdd_id, assumptions \\ %{}) do
-    # Sort assumptions to ensure the cache key is canonical.
+    # The main cache uses a sorted list of assumptions for a canonical key.
+    # The internal context set uses this same canonical form.
     sorted_assumptions = Enum.sort(assumptions)
     cache_key = {:simplify, tdd_id, sorted_assumptions}
 
@@ -1001,65 +1027,159 @@ defmodule Tdd.Algo do
         result_id
 
       :not_found ->
-        result_id = do_simplify(tdd_id, assumptions)
+        # Start the recursive simplification with an empty context.
+        # The context is a MapSet to track visited (id, assumptions) pairs on the call stack.
+        result_id = do_simplify(tdd_id, sorted_assumptions, MapSet.new())
         Store.put_op_cache(cache_key, result_id)
         result_id
     end
   end
 
-  defp do_simplify(tdd_id, assumptions) do
-    # 1. Check if the current path is contradictory. If so, prune this branch.
-    if Engine.check(assumptions) == :contradiction do
+  # The private helper now takes a `context` to detect infinite recursion.
+    # The private helper now takes a `context` to detect infinite recursion.
+  defp do_simplify(tdd_id, sorted_assumptions, context) do
+    current_state = {tdd_id, sorted_assumptions}
+
+    # Coinductive base case: if we have seen this exact state before in this
+    # call stack, we are in a loop. For a least-fixed-point type (like list_of),
+    # this represents an un-satisfiable recursive constraint, which is `none`.
+    if MapSet.member?(context, current_state) do
       Store.false_node_id()
     else
-      case Store.get_node(tdd_id) do
-        # 2. Terminal nodes are already simple.
-        {:ok, :true_terminal} ->
-          Store.true_node_id()
+      new_context = MapSet.put(context, current_state)
+      assumptions = Map.new(sorted_assumptions)
 
-        {:ok, :false_terminal} ->
-          Store.false_node_id()
+      # If the assumptions themselves are contradictory, the result is `none`.
+      if Engine.check(assumptions) == :contradiction do
+        Store.false_node_id()
+      else
+        case Store.get_node(tdd_id) do
+          {:ok, :true_terminal} ->
+            Store.true_node_id()
 
-        # 3. Handle non-terminal nodes.
-        {:ok, {var, y, n, d}} ->
-          # 4. Check if the variable's value is already known or implied.
-          case Map.get(assumptions, var) do
-            true ->
-              simplify(y, assumptions)
+          {:ok, :false_terminal} ->
+            Store.false_node_id()
 
-            false ->
-              simplify(n, assumptions)
+          {:ok, {var, y, n, d}} ->
+            # Check if the variable's value is already explicitly known.
+            case Map.get(assumptions, var) do
+              true ->
+                do_simplify(y, sorted_assumptions, new_context)
 
-            :dc ->
-              simplify(d, assumptions)
+              false ->
+                do_simplify(n, sorted_assumptions, new_context)
 
-            nil ->
-              # The variable is not explicitly constrained. Check for implied constraints.
-              # Note: For now, the Engine only performs flat checks.
-              implies_true = Engine.check(Map.put(assumptions, var, false)) == :contradiction
-              implies_false = Engine.check(Map.put(assumptions, var, true)) == :contradiction
+              :dc ->
+                do_simplify(d, sorted_assumptions, new_context)
 
-              cond do
-                implies_true and implies_false ->
-                  Store.false_node_id()
+              # The variable's value is not explicitly known.
+              # Check if the context of assumptions *implies* its value.
+              nil ->
+                assumptions_imply_true =
+                  Engine.check(Map.put(assumptions, var, false)) == :contradiction
 
-                implies_true ->
-                  simplify(y, assumptions)
+                assumptions_imply_false =
+                  Engine.check(Map.put(assumptions, var, true)) == :contradiction
 
-                implies_false ->
-                  simplify(n, assumptions)
+                cond do
+                  # This case should be caught by the top-level Engine.check, but is here for safety.
+                  assumptions_imply_true and assumptions_imply_false ->
+                    Store.false_node_id()
 
-                true ->
-                  # No constraint, so recursively simplify all branches.
-                  s_y = simplify(y, Map.put(assumptions, var, true))
-                  s_n = simplify(n, Map.put(assumptions, var, false))
-                  s_d = simplify(d, Map.put(assumptions, var, :dc))
-                  Store.find_or_create_node(var, s_y, s_n, s_d)
-              end
-          end
+                  # --- THIS IS THE FIX ---
+                  # If the context implies `var` must be true, we follow the 'yes' path.
+                  # We do NOT add `{var, true}` to the assumptions for the recursive call,
+                  # as that would cause the assumption set to grow infinitely and break
+                  # the coinductive check. The original `assumptions` set already
+                  # contains all the necessary information for the engine to work.
+                  assumptions_imply_true ->
+                    do_simplify(y, sorted_assumptions, new_context)
+
+                  # Likewise, if the context implies `var` must be false, follow the 'no' path
+                  # with the original, unmodified assumptions.
+                  assumptions_imply_false ->
+                    do_simplify(n, sorted_assumptions, new_context)
+
+                  # The variable is truly independent. We must simplify all branches,
+                  # adding the new assumption for each respective path, and reconstruct the node.
+                  true ->
+                    s_y = do_simplify(y, Enum.sort(Map.put(assumptions, var, true)), new_context)
+                    s_n = do_simplify(n, Enum.sort(Map.put(assumptions, var, false)), new_context)
+                    s_d = do_simplify(d, Enum.sort(Map.put(assumptions, var, :dc)), new_context)
+                    Store.find_or_create_node(var, s_y, s_n, s_d)
+                end
+            end
+        end
       end
     end
   end
+
+  # defp do_simplify(tdd_id, assumptions) do
+  #   IO.inspect([tdd_id, assumptions], label: "do_simplify(tdd_id, assumptions)")
+  #   # First, check if the current assumption set is already a contradiction.
+  #   # If so, any TDD under these assumptions is empty (:none).
+  #   if Engine.check(assumptions) == :contradiction do
+  #     Store.false_node_id()
+  #   else
+  #     case Store.get_node(tdd_id) do
+  #       {:ok, :true_terminal} ->
+  #         Store.true_node_id()
+  #
+  #       {:ok, :false_terminal} ->
+  #         Store.false_node_id()
+  #
+  #       {:ok, {var, y, n, d}} ->
+  #         # Check if the variable's value is already known or implied by the assumptions.
+  #         case Map.get(assumptions, var) do
+  #           true ->
+  #             simplify(y, assumptions)
+  #
+  #           false ->
+  #             simplify(n, assumptions)
+  #
+  #           :dc ->
+  #             simplify(d, assumptions)
+  #
+  #           nil ->
+  #             # The variable's value is not explicitly known.
+  #             # We must ask the Consistency.Engine if the assumptions *imply* a value.
+  #
+  #             # Does the context imply `var` must be true?
+  #             # This is true if adding `var == false` creates a contradiction.
+  #             assumptions_imply_true =
+  #               Engine.check(Map.put(assumptions, var, false)) == :contradiction
+  #
+  #             # Does the context imply `var` must be false?
+  #             # This is true if adding `var == true` creates a contradiction.
+  #             assumptions_imply_false =
+  #               Engine.check(Map.put(assumptions, var, true)) == :contradiction
+  #
+  #             cond do
+  #               # This can happen if the base assumptions are contradictory,
+  #               # but it's handled at the top of the function.
+  #               assumptions_imply_true and assumptions_imply_false ->
+  #                 Store.false_node_id()
+  #
+  #               # The context forces `var` to be true, so we only need to follow the 'yes' path.
+  #               assumptions_imply_true ->
+  #                 simplify(y, assumptions)
+  #
+  #               # The context forces `var` to be false, so we only need to follow the 'no' path.
+  #               assumptions_imply_false ->
+  #                 simplify(n, assumptions)
+  #
+  #               # The variable is truly independent of the current assumptions.
+  #               # We must simplify all branches and reconstruct the node.
+  #               true ->
+  #                 s_y = simplify(y, Map.put(assumptions, var, true))
+  #                 s_n = simplify(n, Map.put(assumptions, var, false))
+  #                 s_d = simplify(d, Map.put(assumptions, var, :dc))
+  #                 Store.find_or_create_node(var, s_y, s_n, s_d)
+  #             end
+  #         end
+  #     end
+  #   end
+  # end
 end
 
 defmodule Tdd.TypeReconstructor do
@@ -1166,6 +1286,10 @@ defmodule Tdd.TypeReconstructor do
             # Simplified for now
             {4, :a_size, _, _} -> :tuple
             {5, :b_is_empty, _, _} -> {:literal, []}
+            # --- THIS IS THE FIX ---
+            # Correctly reconstruct a list_of spec from the ambient predicate.
+            {5, :a_all_elements, element_spec, _} ->
+              {:list_of, element_spec}
             # Ignore recursive and ambient vars at this flat level
             _ -> :any
           end
@@ -1203,7 +1327,7 @@ defmodule Tdd.Compiler do
     end
   end
 
-  # The core compilation logic
+  # The core compilation logic.
   defp do_spec_to_id(spec) do
     raw_id =
       case spec do
@@ -1215,183 +1339,66 @@ defmodule Tdd.Compiler do
           Store.false_node_id()
 
         :atom ->
-          Store.find_or_create_node(
-            Variable.v_is_atom(),
-            Store.true_node_id(),
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          create_base_type_tdd(Variable.v_is_atom())
 
         :integer ->
-          Store.find_or_create_node(
-            Variable.v_is_integer(),
-            Store.true_node_id(),
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          create_base_type_tdd(Variable.v_is_integer())
 
-        # Add :list, :tuple etc. here. They are simple structural TDDs.
         :list ->
-          Store.find_or_create_node(
-            Variable.v_is_list(),
-            Store.true_node_id(),
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          create_base_type_tdd(Variable.v_is_list())
+
+        :tuple ->
+          create_base_type_tdd(Variable.v_is_tuple())
 
         # --- Literal Types ---
         {:literal, val} when is_atom(val) ->
-          eq_node =
-            Store.find_or_create_node(
-              Variable.v_atom_eq(val),
-              Store.true_node_id(),
-              Store.false_node_id(),
-              Store.false_node_id()
-            )
-
-          Store.find_or_create_node(
-            Variable.v_is_atom(),
-            eq_node,
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          compile_value_equality(:atom, Variable.v_atom_eq(val))
 
         {:literal, val} when is_integer(val) ->
-          eq_node =
-            Store.find_or_create_node(
-              Variable.v_int_eq(val),
-              Store.true_node_id(),
-              Store.false_node_id(),
-              Store.false_node_id()
-            )
-
-          Store.find_or_create_node(
-            Variable.v_is_integer(),
-            eq_node,
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          compile_value_equality(:integer, Variable.v_int_eq(val))
 
         {:literal, []} ->
-          empty_node =
-            Store.find_or_create_node(
-              Variable.v_list_is_empty(),
-              Store.true_node_id(),
-              Store.false_node_id(),
-              Store.false_node_id()
-            )
-
-          Store.find_or_create_node(
-            Variable.v_is_list(),
-            empty_node,
-            Store.false_node_id(),
-            Store.false_node_id()
-          )
+          compile_value_equality(:list, Variable.v_list_is_empty())
 
+        # --- Integer Range ---
         {:integer_range, min, max} ->
-          # A helper function to define the intersection operation once.
-          op_intersect = fn
-            :false_terminal, _ -> :false_terminal
-            _, :false_terminal -> :false_terminal
-            :true_terminal, t2 -> t2
-            t1, :true_terminal -> t1
-          end
-
-          # Start with the base type, `integer`.
-          # Note: We call spec_to_id here, which is safe because `:integer` is a base case.
-          base_id = spec_to_id(:integer)
-
-          # Intersect with the lower bound condition, if it exists.
-          id_with_min =
-            if min == :neg_inf do
-              base_id
-            else
-              # The condition is `value >= min`, which is equivalent to `NOT (value < min)`.
-              # The variable for `value < min` is `v_int_lt(min)`.
-              lt_min_tdd =
-                Store.find_or_create_node(
-                  Variable.v_int_lt(min),
-                  Store.true_node_id(),
-                  Store.false_node_id(),
-                  Store.false_node_id()
-                )
-
-              gte_min_tdd = Algo.negate(lt_min_tdd)
-              Algo.apply(:intersect, op_intersect, base_id, gte_min_tdd)
-            end
-
-          # Intersect the result with the upper bound condition, if it exists.
-          id_with_max =
-            if max == :pos_inf do
-              id_with_min
-            else
-              # The condition is `value <= max`, which is equivalent to `value < max + 1`.
-              # The variable for this is `v_int_lt(max + 1)`.
-              lt_max_plus_1_tdd =
-                Store.find_or_create_node(
-                  Variable.v_int_lt(max + 1),
-                  Store.true_node_id(),
-                  Store.false_node_id(),
-                  Store.false_node_id()
-                )
-
-              Algo.apply(:intersect, op_intersect, id_with_min, lt_max_plus_1_tdd)
-            end
-
-          # The raw TDD is now built. The final call to Algo.simplify at the end
-          # of do_spec_to_id will canonicalize it.
-          id_with_max
-
-        # Add other literals as needed
+          compile_integer_range(min, max)
 
         # --- Set-Theoretic Combinators ---
         {:union, specs} ->
           ids = Enum.map(specs, &spec_to_id/1)
 
           Enum.reduce(ids, Store.false_node_id(), fn id, acc ->
-            Algo.apply(
-              :sum,
-              fn
-                :true_terminal, _ -> :true_terminal
-                _, :true_terminal -> :true_terminal
-                :false_terminal, t2 -> t2
-                t1, :false_terminal -> t1
-              end,
-              id,
-              acc
-            )
+            Algo.apply(:sum, &op_union_terminals/2, id, acc)
           end)
 
         {:intersect, specs} ->
           ids = Enum.map(specs, &spec_to_id/1)
 
           Enum.reduce(ids, Store.true_node_id(), fn id, acc ->
-            Algo.apply(
-              :intersect,
-              fn
-                :false_terminal, _ -> :false_terminal
-                _, :false_terminal -> :false_terminal
-                :true_terminal, t2 -> t2
-                t1, :true_terminal -> t1
-              end,
-              id,
-              acc
-            )
+            Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
           end)
 
         {:negation, sub_spec} ->
           Algo.negate(spec_to_id(sub_spec))
 
-        # --- Recursive Types (STUBS for now) ---
-        # These will be implemented in Step 3
-        {:list_of, _} ->
-          raise "Tdd.Compiler: :list_of not yet implemented"
+        # --- RECURSIVE TYPES ---
+        #
+        {:list_of, element_spec} ->
+          id_list = spec_to_id(:list)
+          # The element_spec MUST be normalized to be a canonical part of the variable.
+          norm_elem_spec = TypeSpec.normalize(element_spec)
+          var = Variable.v_list_all_elements_are(norm_elem_spec)
+          id_check = create_base_type_tdd(var)
+          Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
+        {:cons, head_spec, tail_spec} ->
+          id_head = spec_to_id(head_spec)
+          id_tail = spec_to_id(tail_spec)
+          compile_cons_from_ids(id_head, id_tail)
 
-        {:tuple, _} ->
-          raise "Tdd.Compiler: {:tuple, [...]} not yet implemented"
+        {:tuple, elements} ->
+          compile_tuple(elements)
 
-        {:cons, _, _} ->
-          raise "Tdd.Compiler: :cons not yet implemented"
 
         # --- Default ---
         _ ->
@@ -1402,6 +1409,174 @@ defmodule Tdd.Compiler do
     # to ensure it's in its canonical, semantically-reduced form.
     Algo.simplify(raw_id)
   end
+
+  # ------------------------------------------------------------------
+  # Private Compilation Helpers
+  # ------------------------------------------------------------------
+
+  defp create_base_type_tdd(var) do
+    Store.find_or_create_node(
+      var,
+      Store.true_node_id(),
+      Store.false_node_id(),
+      Store.false_node_id()
+    )
+  end
+
+  defp compile_value_equality(base_type_spec, value_var) do
+    eq_node = create_base_type_tdd(value_var)
+    base_node_id = spec_to_id(base_type_spec)
+    Algo.apply(:intersect, &op_intersect_terminals/2, base_node_id, eq_node)
+  end
+
+  defp compile_integer_range(min, max) do
+    base_id = spec_to_id(:integer)
+
+    id_with_min =
+      if min == :neg_inf do
+        base_id
+      else
+        lt_min_tdd = create_base_type_tdd(Variable.v_int_lt(min))
+        gte_min_tdd = Algo.negate(lt_min_tdd)
+        Algo.apply(:intersect, &op_intersect_terminals/2, base_id, gte_min_tdd)
+      end
+
+    if max == :pos_inf do
+      id_with_min
+    else
+      lt_max_plus_1_tdd = create_base_type_tdd(Variable.v_int_lt(max + 1))
+      Algo.apply(:intersect, &op_intersect_terminals/2, id_with_min, lt_max_plus_1_tdd)
+    end
+  end
+
+  # ------------------------------------------------------------------
+  # Helpers for Compositional Recursive Types (`cons`, `tuple`)
+  # ------------------------------------------------------------------
+
+  defp sub_problem(sub_key_constructor, tdd_id) do
+    cache_key = {:sub_problem, sub_key_constructor, tdd_id}
+
+    case Store.get_op_cache(cache_key) do
+      {:ok, result_id} ->
+        result_id
+
+      :not_found ->
+        result_id = do_sub_problem(sub_key_constructor, tdd_id)
+        Store.put_op_cache(cache_key, result_id)
+        result_id
+    end
+  end
+
+  defp do_sub_problem(sub_key_constructor, tdd_id) do
+    case Store.get_node(tdd_id) do
+      {:ok, :true_terminal} ->
+        Store.true_node_id()
+
+      {:ok, :false_terminal} ->
+        Store.false_node_id()
+
+      {:ok, {var, y, n, d}} ->
+        lifted_var = sub_key_constructor.(var)
+        lifted_y = sub_problem(sub_key_constructor, y)
+        lifted_n = sub_problem(sub_key_constructor, n)
+        lifted_d = sub_problem(sub_key_constructor, d)
+        Store.find_or_create_node(lifted_var, lifted_y, lifted_n, lifted_d)
+    end
+  end
+
+  defp compile_cons_from_ids(h_id, t_id) do
+    non_empty_list_id = spec_to_id({:intersect, [:list, {:negation, {:literal, []}}]})
+    head_checker = sub_problem(&Variable.v_list_head_pred/1, h_id)
+    tail_checker = sub_problem(&Variable.v_list_tail_pred/1, t_id)
+
+    ids_to_intersect = [non_empty_list_id, head_checker, tail_checker]
+
+    Enum.reduce(ids_to_intersect, Store.true_node_id(), fn id, acc ->
+      Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
+    end)
+  end
+
+  defp compile_tuple(elements) do
+    size = length(elements)
+    base_id = spec_to_id(:tuple)
+    size_tdd = create_base_type_tdd(Variable.v_tuple_size_eq(size))
+    initial_id = Algo.apply(:intersect, &op_intersect_terminals/2, base_id, size_tdd)
+
+    elements
+    |> Enum.with_index()
+    |> Enum.reduce(initial_id, fn {elem_spec, index}, acc_id ->
+      elem_id = spec_to_id(elem_spec)
+      elem_key_constructor = &Variable.v_tuple_elem_pred(index, &1)
+      elem_checker = sub_problem(elem_key_constructor, elem_id)
+      Algo.apply(:intersect, &op_intersect_terminals/2, acc_id, elem_checker)
+    end)
+  end
+
+  # ------------------------------------------------------------------
+  # Helper for Self-Recursive Types (`list_of`) via Fixed-Point Iteration
+  # ------------------------------------------------------------------
+
+  defp compile_list_of(element_spec) do
+    cache_key = {:compile_list_of, element_spec}
+
+    case Store.get_op_cache(cache_key) do
+      {:ok, id} ->
+        id
+
+      :not_found ->
+        id = do_compile_list_of(element_spec)
+        Store.put_op_cache(cache_key, id)
+        id
+    end
+  end
+
+  defp do_compile_list_of(element_spec) do
+    id_elem = spec_to_id(element_spec)
+    id_empty_list = spec_to_id({:literal, []})
+
+    step_function = fn id_x ->
+      id_cons = compile_cons_from_ids(id_elem, id_x)
+      Algo.apply(:sum, &op_union_terminals/2, id_empty_list, id_cons)
+    end
+
+    loop_until_stable(Store.false_node_id(), step_function)
+  end
+
+  # --- THIS IS THE FIX ---
+  defp loop_until_stable(prev_id, step_function) do
+    # At each step, we must simplify the result to get its canonical form.
+    # This ensures we are comparing semantic equality, not just structural.
+    raw_next_id = step_function.(prev_id)
+    next_id = Algo.simplify(raw_next_id)
+
+    if next_id == prev_id do
+      next_id
+    else
+      loop_until_stable(next_id, step_function)
+    end
+  end
+
+  # ------------------------------------------------------------------
+  # Private Functions for Terminal Logic
+  # ------------------------------------------------------------------
+
+  defp op_union_terminals(u1_details, u2_details) do
+    case {u1_details, u2_details} do
+      {:true_terminal, _} -> :true_terminal
+      {_, :true_terminal} -> :true_terminal
+      {:false_terminal, t2} -> t2
+      {t1, :false_terminal} -> t1
+    end
+  end
+
+  defp op_intersect_terminals(u1_details, u2_details) do
+    case {u1_details, u2_details} do
+      {:false_terminal, _} -> :false_terminal
+      {_, :false_terminal} -> :false_terminal
+      {:true_terminal, t2} -> t2
+      {t1, :true_terminal} -> t1
+    end
+  end
 end
 
 ####
@@ -1993,7 +2168,8 @@ defmodule TddAlgoTests do
   alias Tdd.Store
   alias Tdd.Variable
   alias Tdd.Algo
-  alias Tdd.TypeSpec # We need this to create stable variables
+  # We need this to create stable variables
+  alias Tdd.TypeSpec
 
   # --- Test Helper ---
   defp test(name, expected, result) do
@@ -2011,16 +2187,24 @@ defmodule TddAlgoTests do
   # Helper to pretty print a TDD for debugging
   defp print_tdd(id, indent \\ 0) do
     prefix = String.duplicate("  ", indent)
+
     case Store.get_node(id) do
       {:ok, details} ->
         IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
+
         case details do
           {_var, y, n, d} ->
-            IO.puts("#{prefix}  Yes ->"); print_tdd(y, indent + 1)
-            IO.puts("#{prefix}  No  ->"); print_tdd(n, indent + 1)
-            IO.puts("#{prefix}  DC  ->"); print_tdd(d, indent + 1)
-          _ -> :ok
+            IO.puts("#{prefix}  Yes ->")
+            print_tdd(y, indent + 1)
+            IO.puts("#{prefix}  No  ->")
+            print_tdd(n, indent + 1)
+            IO.puts("#{prefix}  DC  ->")
+            print_tdd(d, indent + 1)
+
+          _ ->
+            :ok
         end
+
       {:error, reason} ->
         IO.puts("#{prefix}ID #{id}: Error - #{reason}")
     end
@@ -2043,11 +2227,15 @@ defmodule TddAlgoTests do
     t_int = Store.find_or_create_node(Variable.v_is_integer(), true_id, false_id, false_id)
 
     # t_foo = if is_atom then (if value == :foo then true else false) else false
-    foo_val_check = Store.find_or_create_node(Variable.v_atom_eq(:foo), true_id, false_id, false_id)
+    foo_val_check =
+      Store.find_or_create_node(Variable.v_atom_eq(:foo), true_id, false_id, false_id)
+
     t_foo = Store.find_or_create_node(Variable.v_is_atom(), foo_val_check, false_id, false_id)
 
     # t_bar = if is_atom then (if value == :bar then true else false) else false
-    bar_val_check = Store.find_or_create_node(Variable.v_atom_eq(:bar), true_id, false_id, false_id)
+    bar_val_check =
+      Store.find_or_create_node(Variable.v_atom_eq(:bar), true_id, false_id, false_id)
+
     t_bar = Store.find_or_create_node(Variable.v_is_atom(), bar_val_check, false_id, false_id)
 
     # --- Section: Negate Algorithm ---
@@ -2061,13 +2249,19 @@ defmodule TddAlgoTests do
 
     # --- Section: Apply Algorithm (Union & Intersection) ---
     IO.puts("\n--- Section: Algo.apply (raw structural operations) ---")
+
     op_sum = fn
-        :true_terminal, _ -> :true_terminal; _, :true_terminal -> :true_terminal
-        t, :false_terminal -> t; :false_terminal, t -> t
+      :true_terminal, _ -> :true_terminal
+      _, :true_terminal -> :true_terminal
+      t, :false_terminal -> t
+      :false_terminal, t -> t
     end
+
     op_intersect = fn
-        :false_terminal, _ -> :false_terminal; _, :false_terminal -> :false_terminal
-        t, :true_terminal -> t; :true_terminal, t -> t
+      :false_terminal, _ -> :false_terminal
+      _, :false_terminal -> :false_terminal
+      t, :true_terminal -> t
+      :true_terminal, t -> t
     end
 
     # atom | int
@@ -2075,7 +2269,15 @@ defmodule TddAlgoTests do
     # The result should be a node that checks is_atom, then if false, checks is_int
     # We expect a structure like: if is_atom -> true, else -> t_int
     is_atom_node = {Variable.v_is_atom(), true_id, t_int, t_int}
-    expected_sum_structure_id = Store.find_or_create_node(elem(is_atom_node, 0), elem(is_atom_node, 1), elem(is_atom_node, 2), elem(is_atom_node, 3))
+
+    expected_sum_structure_id =
+      Store.find_or_create_node(
+        elem(is_atom_node, 0),
+        elem(is_atom_node, 1),
+        elem(is_atom_node, 2),
+        elem(is_atom_node, 3)
+      )
+
     test("Structure of 'atom | int' is correct", expected_sum_structure_id, sum_atom_int)
 
     # :foo & :bar (structurally, before simplification)
@@ -2092,7 +2294,12 @@ defmodule TddAlgoTests do
     contradictory_assumptions = %{Variable.v_is_atom() => true, Variable.v_is_integer() => true}
     # Simplifying ANYTHING under contradictory assumptions should yield `false`.
     simplified_under_contradiction = Algo.simplify(true_id, contradictory_assumptions)
-    test("Simplifying under contradictory assumptions (atom & int) results in false", false_id, simplified_under_contradiction)
+
+    test(
+      "Simplifying under contradictory assumptions (atom & int) results in false",
+      false_id,
+      simplified_under_contradiction
+    )
 
     # Test implication: A property implies its primary type
     # A value being `:foo` implies it is an atom.
@@ -2101,7 +2308,12 @@ defmodule TddAlgoTests do
     # The engine expands to `{is_atom: true, value==:foo: true}`. Then it sees that
     # the t_int node's variable `is_integer` must be false (from exclusivity rule).
     simplified_int_given_foo = Algo.simplify(t_int, assumptions_with_foo)
-    test("Simplifying 'integer' given 'value==:foo' results in false", false_id, simplified_int_given_foo)
+
+    test(
+      "Simplifying 'integer' given 'value==:foo' results in false",
+      false_id,
+      simplified_int_given_foo
+    )
 
     # Now, let's simplify the raw intersection of :foo and :bar
     simplified_foo_bar = Algo.simplify(intersect_foo_bar_raw, %{})
@@ -2116,14 +2328,25 @@ defmodule TddAlgoTests do
     # Test path collapsing
     # If we simplify 'atom | int' under the assumption 'is_atom == true', it should become `true`.
     simplified_sum_given_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => true})
-    test("Simplifying 'atom | int' given 'is_atom==true' results in true", true_id, simplified_sum_given_atom)
+
+    test(
+      "Simplifying 'atom | int' given 'is_atom==true' results in true",
+      true_id,
+      simplified_sum_given_atom
+    )
+
     # If we simplify 'atom | int' under the assumption 'is_atom == false', it should become `t_int`.
     simplified_sum_given_not_atom = Algo.simplify(sum_atom_int, %{Variable.v_is_atom() => false})
-    test("Simplifying 'atom | int' given 'is_atom==false' results in 'integer'", t_int, simplified_sum_given_not_atom)
 
+    test(
+      "Simplifying 'atom | int' given 'is_atom==false' results in 'integer'",
+      t_int,
+      simplified_sum_given_not_atom
+    )
 
     # --- Final Report ---
     failures = Process.get(:test_failures, [])
+
     if failures == [] do
       IO.puts("\n✅ All Tdd.Algo tests passed!")
     else
@@ -2132,6 +2355,7 @@ defmodule TddAlgoTests do
     end
   end
 end
+
 defmodule TypeReconstructorTests do
   alias Tdd.TypeReconstructor
   alias Tdd.Variable
@@ -2428,6 +2652,218 @@ defmodule CompilerAlgoTests do
   end
 end
 
+defmodule TddCompilerRecursiveTests do
+  alias Tdd.Compiler
+  alias Tdd.Store
+  alias Tdd.Algo
+  alias Tdd.TypeSpec
+
+  # --- Test Runner ---
+  def run() do
+    IO.puts("\n--- Running Tdd.Compiler Recursive Type Tests ---")
+    Process.put(:test_failures, [])
+    Tdd.Store.init()
+
+    # --- Tests for :cons ---
+    IO.puts("\n--- Section: :cons ---")
+    test_subtype(":cons is a subtype of :list", true, {:cons, :atom, :list}, :list)
+
+    test_subtype(
+      ":cons is not a subtype of the empty list",
+      false,
+      {:cons, :atom, :list},
+      {:literal, []}
+    )
+
+    test_subtype(
+      "cons(integer, list) is a subtype of cons(any, any)",
+      true,
+      {:cons, :integer, :list},
+      {:cons, :any, :any}
+    )
+
+    test_subtype(
+      "cons(any, any) is not a subtype of cons(integer, list)",
+      false,
+      {:cons, :any, :any},
+      {:cons, :integer, :list}
+    )
+
+    # --- Tests for :tuple ---
+    IO.puts("\n--- Section: :tuple ---")
+
+    test_subtype(
+      "{:tuple, [atom, int]} is a subtype of :tuple",
+      true,
+      {:tuple, [:atom, :integer]},
+      :tuple
+    )
+
+    test_subtype(
+      "{:tuple, [atom, int]} is not a subtype of :list",
+      false,
+      {:tuple, [:atom, :integer]},
+      :list
+    )
+
+    test_subtype(
+      "a tuple of size 2 is not a subtype of a tuple of size 3",
+      false,
+      {:tuple, [:atom, :integer]},
+      {:tuple, [:atom, :integer, :list]}
+    )
+
+    spec_specific = {:tuple, [{:literal, :a}, {:literal, 1}]}
+    spec_general = {:tuple, [:atom, :integer]}
+    spec_unrelated = {:tuple, [:list, :list]}
+
+    test_subtype(
+      "subtype check works element-wise (specific <: general)",
+      true,
+      spec_specific,
+      spec_general
+    )
+
+    test_subtype(
+      "subtype check works element-wise (general </: specific)",
+      false,
+      spec_general,
+      spec_specific
+    )
+
+    test_subtype(
+      "subtype check works element-wise (specific </: unrelated)",
+      false,
+      spec_specific,
+      spec_unrelated
+    )
+
+    # --- Tests for :list_of ---
+    IO.puts("\n--- Section: :list_of ---")
+    test_subtype("list_of(E) is a subtype of list", true, {:list_of, :integer}, :list)
+
+    test_subtype(
+      "empty list is a subtype of any list_of(E)",
+      true,
+      {:literal, []},
+      {:list_of, :integer}
+    )
+
+    test_subtype(
+      "list_of(subtype) is a subtype of list_of(supertype)",
+      true,
+      {:list_of, {:literal, 1}},
+      {:list_of, :integer}
+    )
+
+    test_subtype(
+      "list_of(supertype) is not a subtype of list_of(subtype)",
+      false,
+      {:list_of, :integer},
+      {:list_of, {:literal, 1}}
+    )
+
+    list_with_int = {:cons, :integer, {:literal, []}}
+    list_of_atoms = {:list_of, :atom}
+
+    test_subtype(
+      "a list with a wrong element type is not a subtype of list_of(E)",
+      false,
+      list_with_int,
+      list_of_atoms
+    )
+
+    list_with_atom = {:cons, :atom, {:literal, []}}
+
+    test_subtype(
+      "a list with a correct element type is a subtype of list_of(E)",
+      true,
+      list_with_atom,
+      list_of_atoms
+    )
+
+    # --- Equivalence tests ---
+    IO.puts("\n--- Section: Equivalence ---")
+    e_spec = :integer
+    list_of_e = {:list_of, e_spec}
+    recursive_def = TypeSpec.normalize({:union, [{:literal, []}, {:cons, e_spec, list_of_e}]})
+
+    test_equiv(
+      "the recursive definition holds: list_of(E) == [] | cons(E, list_of(E))",
+      true,
+      list_of_e,
+      recursive_def
+    )
+
+    int_range_1 = {:integer_range, 0, 10}
+    int_range_2 = {:integer_range, 5, 15}
+    int_range_intersect = {:integer_range, 5, 10}
+    list_of_1 = {:list_of, int_range_1}
+    list_of_2 = {:list_of, int_range_2}
+    list_of_intersect = {:list_of, int_range_intersect}
+    combined_spec = {:intersect, [list_of_1, list_of_2]}
+
+    test_equiv(
+      "intersection of two list_of types works correctly",
+      true,
+      combined_spec,
+      list_of_intersect
+    )
+
+    # --- Final Report ---
+    failures = Process.get(:test_failures, [])
+
+    if failures == [] do
+      IO.puts("\n✅ All Tdd.Compiler Recursive Type tests passed!")
+    else
+      IO.puts("\n❌ Found #{length(failures)} test failures.")
+    end
+  end
+
+  # --- Private Test Helpers ---
+  defp test(name, expected, result) do
+    if expected == result do
+      IO.puts("[PASS] #{name}")
+    else
+      IO.puts("[FAIL] #{name}")
+      IO.puts("       Expected: #{inspect(expected)}")
+      IO.puts("       Got:      #{inspect(result)}")
+      Process.put(:test_failures, [name | Process.get(:test_failures, [])])
+    end
+  end
+
+  defp test_equiv(name, expected, spec1, spec2) do
+    result = Compiler.spec_to_id(spec1) == Compiler.spec_to_id(spec2)
+    test(name, expected, result)
+  end
+
+  defp test_subtype(name, expected, spec1, spec2) do
+    result = do_is_subtype(spec1, spec2)
+    test(name, expected, result)
+  end
+
+  # --- Private Logic Helpers ---
+  defp do_is_subtype(spec1, spec2) do
+    id1 = Compiler.spec_to_id(spec1)
+    id2 = Compiler.spec_to_id(spec2)
+    # A <: B  <=>  A & ~B == none
+    intersect_id = Algo.apply(:intersect, &op_intersect_terminals/2, id1, Algo.negate(id2))
+    final_id = Algo.simplify(intersect_id)
+    final_id == Store.false_node_id()
+  end
+
+  defp op_intersect_terminals(u1_details, u2_details) do
+    case {u1_details, u2_details} do
+      {:false_terminal, _} -> :false_terminal
+      {_, :false_terminal} -> :false_terminal
+      {:true_terminal, t2} -> t2
+      {t1, :true_terminal} -> t1
+    end
+  end
+end
+
+# To run this new test, add the following to your main test runner script:
+# TddCompilerRecursiveTests.run()
 TypeSpecTests.run()
 TddStoreTests.run()
 TddVariableTests.run()
@@ -2435,3 +2871,4 @@ TddAlgoTests.run()
 ConsistencyEngineTests.run()
 TypeReconstructorTests.run()
 CompilerAlgoTests.run()
+TddCompilerRecursiveTests.run()