deps

spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
assert_equivalent_specs(spec, :integer)

lib/debug.ex

@@ -606,9 +606,9 @@ defmodule Tdd.Debug do
 
   # --- TDD Graph Printing (Kept as it was, assuming it's for a different purpose) ---
   @doc "Prints a formatted representation of a TDD graph structure."
-  def print_tdd_graph(id, store_module \\ Tdd.Store) do
-    IO.puts("--- TDD Graph (ID: #{id}) ---")
-    do_print_tdd_node(id, 0, MapSet.new(), store_module)
+  def print_tdd_graph(id, label \\ "") do
+    IO.puts("---#{label} TDD Graph (ID: #{id}) ---")
+    do_print_tdd_node(id, 0, MapSet.new(), Tdd.Store)
     IO.puts("------------------------")
   end
 
@@ -630,6 +630,15 @@ defmodule Tdd.Debug do
 
         {:ok, {var, y_id, n_id, dc_id}} ->
           IO.puts("#{prefix}ID #{id}: IF #{inspect(var)}")
+
+          case var do
+            {_, :c_head, nested_id, _} when nested_id != nil ->
+              print_tdd_graph(nested_id, "Var in #{id}")
+
+            _ ->
+              ""
+          end
+
           IO.puts("#{prefix}  ├─ Yes (to ID #{y_id}):")
           do_print_tdd_node(y_id, indent_level + 2, new_visited, store_module)
           IO.puts("#{prefix}  ├─ No  (to ID #{n_id}):")
@@ -685,4 +694,159 @@ defmodule Tdd.Debug do
     # Return the value
     value
   end
+
+  @doc """
+  Builds a map representation of the TDD starting from a root ID.
+
+  This is the main entry point. It initializes the process with an empty set
+  of visited nodes.
+  """
+  def build_graph_map(root_id, label) do
+    # The result of the recursive build is a tuple {map_data, visited_set}.
+    # We only need the map_data, so we extract it with elem().
+    asd =
+      elem(do_build_node_map(root_id, MapSet.new(), Tdd.Store), 0)
+      |> IO.inspect(label: label)
+  end
+
+  def to_json(kv_list) do
+    kv_list
+    # Jason.encode!(kv_list, pretty: true)
+  end
+
+  @doc false
+  # This private helper does the actual recursive work.
+  # It returns a tuple: {node_map, visited_set} so the set of visited
+  # nodes can be tracked through the recursion.
+  defp do_build_node_map(0, visited, _), do: {false, visited}
+  defp do_build_node_map(1, visited, _), do: {true, visited}
+
+  defp do_build_node_map(id, visited, store_module) do
+    if MapSet.member?(visited, id) do
+      # A cycle or a previously processed node. Return a reference.
+      {[id: id, ref: "recursive_or_seen"], visited}
+    else
+      # Add the current ID to the visited set before any recursion.
+      new_visited = MapSet.put(visited, id)
+
+      case store_module.get_node(id) do
+        {:ok, :true_terminal} ->
+          {[id: id, value: true], new_visited}
+
+        {:ok, :false_terminal} ->
+          {[id: id, value: false], new_visited}
+
+        {:ok, {var, y_id, n_id, dc_id}} ->
+          # First, process the variable. This is important because the variable
+          # itself might contain a sub-TDD that adds nodes to our visited set.
+          {var_map, visited_after_var} = format_variable(var, new_visited, store_module)
+
+          # Now, recursively build the children, threading the visited set through each call.
+          {yes_map, visited_after_yes} = do_build_node_map(y_id, visited_after_var, store_module)
+          {no_map, visited_after_no} = do_build_node_map(n_id, visited_after_yes, store_module)
+          {dc_map, final_visited} = do_build_node_map(dc_id, visited_after_no, store_module)
+
+          node = [
+            id: id,
+            # The (potentially expanded) variable map
+            variable: var_map,
+            yes: yes_map,
+            no: no_map,
+            dont_care: dc_map
+          ]
+
+          {node, final_visited}
+
+        {:error, reason} ->
+          {[id: id, type: "error", reason: reason], new_visited}
+      end
+    end
+    |> case do
+      {node, v} ->
+        n = Enum.sort_by(node, fn {k, _} -> Enum.find_index([:id, :value], &(&1 == k)) end)
+        # {Jason.OrderedObject.new(n), v}
+        {n, v}
+    end
+  end
+
+  @doc false
+  # This helper now takes the visited set and store_module to handle nested TDDs.
+  # It returns a tuple: {variable_map, updated_visited_set}.
+  defp format_variable(var, visited, store_module) do
+    case var do
+      # --- Variables with nested TDDs ---
+      {4, :b_element, index, sub_tdd_id} ->
+        # Recursively build the map for the sub-TDD.
+        {sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
+
+        var_map = [
+          type: "tuple_element_predicate",
+          index: index,
+          predicate_tdd: sub_tdd_map
+        ]
+
+        {var_map, new_visited}
+
+      {5, :c_head, sub_tdd_id, nil} ->
+        {sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
+
+        var_map = [
+          type: "list_head_predicate",
+          predicate_tdd: sub_tdd_map
+        ]
+
+        {var_map, new_visited}
+
+      {5, :d_tail, sub_tdd_id, nil} ->
+        {sub_tdd_map, new_visited} = do_build_node_map(sub_tdd_id, visited, store_module)
+
+        var_map = [
+          type: "list_tail_predicate",
+          predicate_tdd: sub_tdd_map
+        ]
+
+        {var_map, new_visited}
+
+      # --- Simple variables (no nested TDDs) ---
+      {0, :is_atom, _, _} ->
+        {[type: "is_atom"], visited}
+
+      {0, :is_integer, _, _} ->
+        {[type: "is_integer"], visited}
+
+      {0, :is_list, _, _} ->
+        {[type: "is_list"], visited}
+
+      {0, :is_tuple, _, _} ->
+        {[type: "is_tuple"], visited}
+
+      {1, :value, atom_val, _} ->
+        {[type: "atom_equals", value: atom_val], visited}
+
+      {2, :alt, n, _} ->
+        {[type: "integer_less_than", value: n], visited}
+
+      {2, :beq, n, _} ->
+        {[type: "integer_equals", value: n], visited}
+
+      {2, :cgt, n, _} ->
+        {[type: "integer_greater_than", value: n], visited}
+
+      {4, :a_size, size, _} ->
+        {[type: "tuple_size_equals", value: size], visited}
+
+      {5, :b_is_empty, _, _} ->
+        {[type: "list_is_empty"], visited}
+
+      # --- Fallback for any other format ---
+      _ ->
+        {[type: "unknown", value: inspect(var)], visited}
+    end
+    |> case do
+      {node, v} ->
+        n = Enum.sort_by(node, fn {k, _} -> Enum.find_index([:id, :value], &(&1 == k)) end)
+        # {Jason.OrderedObject.new(n), v}
+        {n, v}
+    end
+  end
 end

lib/til.ex

@@ -78,37 +78,65 @@ defmodule Tdd.TypeSpec do
         end
 
       {:intersect, members} ->
-        recursively_reduced_members = Enum.map(members, &apply_subtype_reduction/1)
-
-        expanded_flattened_members =
-          Enum.flat_map(recursively_reduced_members, fn
+        # First, recursively reduce all members and flatten any nested intersections.
+        flattened_members =
+          members
+          |> Enum.map(&apply_subtype_reduction/1)
+          |> Enum.flat_map(fn
             {:intersect, sub_members} -> sub_members
-            # get_supertypes expects normalized spec, and its output is also normalized
-            # Pass flag
-            m -> get_supertypes(m, true)
+            # :any is the identity for intersection, so we can remove it.
+            m when m == :any -> []
+            m -> [m]
           end)
-
-        unique_no_any =
-          expanded_flattened_members
-          |> Enum.reject(&(&1 == :any))
           |> Enum.uniq()
 
-        if Enum.member?(unique_no_any, :none) do
+        # If :none (the absorbing element) is present, the whole intersection is :none.
+        if Enum.member?(flattened_members, :none) do
           :none
         else
-          # Pass `true` for already_normalized flag to is_subtype?
-          final_members =
-            Enum.reject(unique_no_any, fn member_to_check ->
-              Enum.any?(unique_no_any, fn other_member ->
-                member_to_check != other_member and
-                  is_subtype?(other_member, member_to_check, true)
-              end)
-            end)
+          # Separate the members into unions and non-unions.
+          {unions, non_unions} = Enum.split_with(flattened_members, &match?({:union, _}, &1))
 
-          case Enum.sort(final_members) do
-            [] -> :any
-            [single] -> single
-            list_members -> {:intersect, list_members}
+          if Enum.empty?(unions) do
+            # BASE CASE: No unions to distribute. Just a simple intersection.
+            # We remove any member that is a supertype of another member.
+            final_members =
+              Enum.reject(non_unions, fn member_to_check ->
+                Enum.any?(non_unions, fn other_member ->
+                  member_to_check != other_member and
+                    is_subtype?(other_member, member_to_check, true)
+                end)
+              end)
+
+            # Further check for contradictions, e.g., intersect(:atom, :integer)
+            # This is an advanced step, but for now, the TDD compiler handles it.
+            # A simple check could be added here if needed.
+
+            case Enum.sort(final_members) do
+              [] -> :any
+              [single] -> single
+              list_members -> {:intersect, list_members}
+            end
+          else
+            # RECURSIVE CASE: Distribute the intersection over a union.
+            [{:union, union_to_distribute} | other_unions] = unions
+
+            remaining_intersection =
+              case non_unions ++ other_unions do
+                [] -> :any
+                [single] -> single
+                multiple -> {:intersect, multiple}
+              end
+
+            # Distribute: (A | B | ...) & Remainder  =>  (A & Remainder) | (B & Remainder) | ...
+            new_union_members =
+              Enum.map(union_to_distribute, fn member_of_union ->
+                # Recursively call apply_subtype_reduction on the new, smaller intersections.
+                apply_subtype_reduction({:intersect, [member_of_union, remaining_intersection]})
+              end)
+
+            # The result is a new union, which we also need to simplify.
+            apply_subtype_reduction({:union, new_union_members})
           end
         end
 
@@ -685,8 +713,6 @@ defmodule Tdd.TypeSpec do
               (min == :neg_inf or val >= min) and (max == :pos_inf or val <= max)
 
             {{:mu, v1, b1_body}, {:mu, v2, b2_body}} ->
-              # This logic is from the original file, which is correct in principle
-              # but was failing due to the TDD layer bug.
               cond do
                 is_list_mu_form(b1_body, v1) and is_list_mu_form(b2_body, v2) ->
                   e1 = extract_list_mu_element(b1_body, v1)
@@ -798,8 +824,6 @@ defmodule Tdd.TypeSpec do
 end
 
 defmodule Tdd.Store do
-  # NOTE: This module remains unchanged.
-  # The original provided code for this module is correct and complete.
   @moduledoc """
   Manages the state of the TDD system's node graph and operation cache.
   """
@@ -848,6 +872,7 @@ defmodule Tdd.Store do
   def get_node(id) do
     case Process.get(@node_by_id_key, %{}) do
       %{^id => details} -> {:ok, details}
+      %{^id => {:placeholder, _spec}} -> {:ok, {:placeholder, "Knot-tying placeholder"}}
       %{} -> {:error, :not_found}
     end
   end
@@ -908,11 +933,20 @@ defmodule Tdd.Store do
   """
   @spec create_placeholder(TypeSpec.t()) :: non_neg_integer()
   def create_placeholder(spec) do
-    find_or_create_node({:placeholder, spec}, 1, 0, 0)
+    next_id = Process.get(@next_id_key)
+    node_by_id = Process.get(@node_by_id_key)
+
+    # Associate the ID with a temporary detail for debugging and identification.
+    # This does NOT create an entry in the main `nodes` (reverse-lookup) map.
+    Process.put(@node_by_id_key, Map.put(node_by_id, next_id, {:placeholder, spec}))
+    Process.put(@next_id_key, next_id + 1)
+
+    next_id
   end
 
   @doc """
   Updates a node's details directly. Used for knot-tying.
+  UNUSED RN
   """
   @spec update_node_in_place(
           non_neg_integer(),
@@ -926,6 +960,8 @@ defmodule Tdd.Store do
     nodes = Process.get(@nodes_key)
     node_by_id = Process.get(@node_by_id_key)
 
+    # The old_details will be `{:placeholder, ...}`
+    # which does not exist as a key in the `nodes` map, so Map.delete is a no-op.
     old_details = Map.get(node_by_id, id)
     nodes = Map.delete(nodes, old_details)
 
@@ -946,8 +982,6 @@ end
 defmodule Tdd.Variable do
   @moduledoc """
   Defines the canonical structure for all Tdd predicate variables.
-  REFAC: This module is unchanged, but its functions for recursive types will
-  now be called with TDD IDs instead of TypeSpecs by the Tdd.Compiler.
   """
 
   # --- Category 0: Primary Type Discriminators ---
@@ -985,7 +1019,6 @@ defmodule Tdd.Variable do
   @spec v_tuple_elem_pred(non_neg_integer(), sub_problem_tdd_id :: non_neg_integer()) :: term()
   def v_tuple_elem_pred(index, sub_problem_tdd_id)
       when is_integer(index) and index >= 0 and is_integer(sub_problem_tdd_id) do
-    # REFAC: The nested term is now a TDD ID, not a spec or a variable.
     {4, :b_element, index, sub_problem_tdd_id}
   end
 
@@ -1006,8 +1039,6 @@ defmodule Tdd.Variable do
 end
 
 defmodule Tdd.Predicate.Info do
-  # NOTE: This module remains largely unchanged. The traits for recursive variables
-  # correctly identify them by structure, independent of what's inside.
   @moduledoc "A knowledge base for the properties of TDD predicate variables."
   alias Tdd.Variable
 
@@ -1079,7 +1110,6 @@ defmodule Tdd.Predicate.Info do
     %{type: :tuple_prop, category: :tuple, implies: [{Variable.v_is_tuple(), true}]}
   end
 
-  # REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
   def get_traits({4, :b_element, index, _tdd_id}) do
     %{
       type: :tuple_recursive,
@@ -1093,7 +1123,6 @@ defmodule Tdd.Predicate.Info do
     %{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]}
   end
 
-  # REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
   def get_traits({5, :c_head, _tdd_id, _}) do
     %{
       type: :list_recursive,
@@ -1103,7 +1132,6 @@ defmodule Tdd.Predicate.Info do
     }
   end
 
-  # REFAC: The trait recognizes the structure. The content `_tdd_id` is opaque here.
   def get_traits({5, :d_tail, _tdd_id, _}) do
     %{
       type: :list_recursive,
@@ -1119,8 +1147,6 @@ end
 defmodule Tdd.Consistency.Engine do
   @moduledoc """
   A rule-based engine for checking the semantic consistency of a set of assumptions.
-  REFAC: This module is largely unchanged, but we now make `remap_sub_problem_vars`
-  and `unwrap_var` public so they can be shared with Tdd.Algo.
   """
   alias Tdd.Predicate.Info
   alias Tdd.Variable
@@ -1173,8 +1199,6 @@ defmodule Tdd.Consistency.Engine do
   @spec unwrap_var(term()) :: term()
   def unwrap_var(var) do
     case var do
-      # REFAC: These variables now contain TDD IDs, but this function just extracts
-      # whatever is inside. The consumer (`handle_recursive_subproblem`) will know it's an ID.
       {4, :b_element, _index, inner_content} -> inner_content
       {5, :c_head, inner_content, _} -> inner_content
       {5, :d_tail, inner_content, _} -> inner_content
@@ -1344,84 +1368,152 @@ defmodule Tdd.Algo do
         Store.put_op_cache(cache_key, result_id)
         result_id
     end
+    |> simplify()
   end
 
   # This function is correct and does not need to be changed.
   defp do_apply(op_name, op_lambda, u1_id, u2_id) do
-    with {:ok, u1_details} <- Store.get_node(u1_id),
-         {:ok, u2_details} <- Store.get_node(u2_id) do
-      cond do
-        (u1_details == :true_terminal or u1_details == :false_terminal) and
-            (u2_details == :true_terminal or u2_details == :false_terminal) ->
-          if op_lambda.(u1_details, u2_details) == :true_terminal,
-            do: Store.true_node_id(),
-            else: Store.false_node_id()
+    if u1_id == u2_id do
+      # If both nodes are the same, the result of the operation is idempotent.
+      u1_id
+    else
+      # The core logic for distinct nodes.
+      with {:ok, u1_details} <- Store.get_node(u1_id),
+           {:ok, u2_details} <- Store.get_node(u2_id) do
+        cond do
+          # --- Start of Logic for Placeholders ---
 
-        u1_details == :true_terminal or u1_details == :false_terminal ->
-          {var2, y2, n2, d2} = u2_details
+          # Case 1: u2 is a placeholder. We must handle this based on u1.
+          match?({:placeholder, _}, u2_details) ->
+            case u1_details do
+              # op(true, placeholder) depends on the operation.
+              :true_terminal ->
+                case op_name do
+                  :sum -> Store.true_node_id()
+                  # intersect(any, p) = p
+                  :intersect -> u2_id
+                end
 
-          Store.find_or_create_node(
-            var2,
-            apply(op_name, op_lambda, u1_id, y2),
-            apply(op_name, op_lambda, u1_id, n2),
-            apply(op_name, op_lambda, u1_id, d2)
-          )
+              # op(false, placeholder) also depends on the operation.
+              :false_terminal ->
+                case op_name do
+                  # sum(none, p) = p
+                  :sum -> u2_id
+                  :intersect -> Store.false_node_id()
+                end
 
-        u2_details == :true_terminal or u2_details == :false_terminal ->
-          {var1, y1, n1, d1} = u1_details
+              # op(node, placeholder) -> recursively apply op to children and placeholder.
+              {var1, y1, n1, d1} ->
+                Store.find_or_create_node(
+                  var1,
+                  apply(op_name, op_lambda, y1, u2_id),
+                  apply(op_name, op_lambda, n1, u2_id),
+                  apply(op_name, op_lambda, d1, u2_id)
+                )
+            end
 
-          Store.find_or_create_node(
-            var1,
-            apply(op_name, op_lambda, y1, u2_id),
-            apply(op_name, op_lambda, n1, u2_id),
-            apply(op_name, op_lambda, d1, u2_id)
-          )
+          # Case 2: Symmetric case where u1 is the placeholder.
+          match?({:placeholder, _}, u1_details) ->
+            case u2_details do
+              :true_terminal ->
+                case op_name do
+                  :sum -> Store.true_node_id()
+                  # intersect(p, any) = p
+                  :intersect -> u1_id
+                end
 
-        true ->
-          {var1, y1, n1, d1} = u1_details
-          {var2, y2, n2, d2} = u2_details
-          top_var = Enum.min([var1, var2])
+              :false_terminal ->
+                case op_name do
+                  # sum(p, none) = p
+                  :sum -> u1_id
+                  :intersect -> Store.false_node_id()
+                end
 
-          res_y =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: y1, else: u1_id),
-              if(var2 == top_var, do: y2, else: u2_id)
+              {var2, y2, n2, d2} ->
+                Store.find_or_create_node(
+                  var2,
+                  apply(op_name, op_lambda, u1_id, y2),
+                  apply(op_name, op_lambda, u1_id, n2),
+                  apply(op_name, op_lambda, u1_id, d2)
+                )
+            end
+
+          # --- End of Placeholder Logic ---
+          # The rest of the function is the standard apply algorithm.
+
+          (u1_details == :true_terminal or u1_details == :false_terminal) and
+              (u2_details == :true_terminal or u2_details == :false_terminal) ->
+            if op_lambda.(u1_details, u2_details) == :true_terminal,
+              do: Store.true_node_id(),
+              else: Store.false_node_id()
+
+          u1_details == :true_terminal or u1_details == :false_terminal ->
+            {var2, y2, n2, d2} = u2_details
+
+            Store.find_or_create_node(
+              var2,
+              apply(op_name, op_lambda, u1_id, y2),
+              apply(op_name, op_lambda, u1_id, n2),
+              apply(op_name, op_lambda, u1_id, d2)
             )
 
-          res_n =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: n1, else: u1_id),
-              if(var2 == top_var, do: n2, else: u2_id)
+          u2_details == :true_terminal or u2_details == :false_terminal ->
+            {var1, y1, n1, d1} = u1_details
+
+            Store.find_or_create_node(
+              var1,
+              apply(op_name, op_lambda, y1, u2_id),
+              apply(op_name, op_lambda, n1, u2_id),
+              apply(op_name, op_lambda, d1, u2_id)
             )
 
-          res_d =
-            apply(
-              op_name,
-              op_lambda,
-              if(var1 == top_var, do: d1, else: u1_id),
-              if(var2 == top_var, do: d2, else: u2_id)
-            )
+          true ->
+            {var1, y1, n1, d1} = u1_details
+            {var2, y2, n2, d2} = u2_details
+            top_var = Enum.min([var1, var2])
 
-          Store.find_or_create_node(top_var, res_y, res_n, res_d)
+            res_y =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: y1, else: u1_id),
+                if(var2 == top_var, do: y2, else: u2_id)
+              )
+
+            res_n =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: n1, else: u1_id),
+                if(var2 == top_var, do: n2, else: u2_id)
+              )
+
+            res_d =
+              apply(
+                op_name,
+                op_lambda,
+                if(var1 == top_var, do: d1, else: u1_id),
+                if(var2 == top_var, do: d2, else: u2_id)
+              )
+
+            Store.find_or_create_node(top_var, res_y, res_n, res_d)
+        end
       end
     end
   end
 
   # --- Unary Operation: Negation ---
-  # This function is correct and does not need to be changed.
   @spec negate(non_neg_integer) :: non_neg_integer
   def negate(tdd_id) do
     cache_key = {:negate, tdd_id}
 
     case Store.get_op_cache(cache_key) do
+      # If the result is already cached (or in progress), return it.
       {:ok, result_id} ->
         result_id
 
       :not_found ->
+        # On cache miss, compute the negation.
         result_id =
           case Store.get_node(tdd_id) do
             {:ok, :true_terminal} ->
@@ -1430,21 +1522,54 @@ defmodule Tdd.Algo do
             {:ok, :false_terminal} ->
               Store.true_node_id()
 
+            # This is the main recursive case for an internal node.
             {:ok, {var, y, n, d}} ->
-              Store.find_or_create_node(var, negate(y), negate(n), negate(d))
+              # 1. Create a temporary placeholder and cache it immediately.
+              #    This acts as a co-inductive "hook". Any recursive call to negate
+              #    this same `tdd_id` will hit the cache and get this placeholder,
+              #    breaking the infinite recursion.
+              placeholder = Store.create_placeholder({:negation_of, tdd_id})
+              Store.put_op_cache(cache_key, placeholder)
+
+              # 2. Recursively negate the children.
+              neg_y = negate(y)
+              neg_n = negate(n)
+              neg_d = negate(d)
+
+              # 3. Build the main body of the negated TDD. If there was a cycle,
+              #    this structure will refer to the `placeholder` ID at its leaves.
+              body_id = Store.find_or_create_node(var, neg_y, neg_n, neg_d)
+
+              # 4. "Tie the knot": Replace any occurrences of the placeholder within the
+              #    newly created graph with the ID of the graph's root (`body_id`).
+              #    This correctly forms the cycle in the negated graph.
+              final_id = substitute(body_id, placeholder, body_id)
+
+              # 5. The canonical graph is now built. Update the cache with the
+              #    final, correct ID before returning.
+              Store.put_op_cache(cache_key, final_id)
+              final_id
+
+            # This case indicates a logical error. A fully compiled TDD passed to `negate`
+            # should not be a placeholder itself. This new implementation avoids the
+            # previous incorrect handling.
+            {:ok, {:placeholder, _spec}} ->
+              raise "Tdd.Algo.negate: Attempted to negate a raw placeholder node. This indicates a logic error in the calling algorithm."
+
+            {:error, reason} ->
+              raise "Tdd.Algo.negate: Failed to get node #{tdd_id}: #{reason}"
           end
 
-        Store.put_op_cache(cache_key, result_id)
         result_id
     end
   end
 
   # --- Unary Operation: Semantic Simplification ---
-  # This function is correct and does not need to be changed.
   @spec simplify(non_neg_integer(), map()) :: non_neg_integer
   def simplify(tdd_id, assumptions \\ %{}) do
     sorted_assumptions = Enum.sort(assumptions)
     cache_key = {:simplify, tdd_id, sorted_assumptions}
+    require Logger
 
     case Store.get_op_cache(cache_key) do
       {:ok, result_id} ->
@@ -1457,14 +1582,14 @@ defmodule Tdd.Algo do
     end
   end
 
-  # This function is correct and does not need to be changed.
   defp do_simplify(tdd_id, sorted_assumptions, context) do
-    current_state = {tdd_id, sorted_assumptions}
-
-    if MapSet.member?(context, current_state) do
-      Store.true_node_id()
+    # The context now only tracks the node ID. If we see the same ID again,
+    # it's an unproductive loop, regardless of the path taken to get here.
+    if MapSet.member?(context, tdd_id) do
+      Store.false_node_id()
     else
-      new_context = MapSet.put(context, current_state)
+      # Add the current ID to the context for all subsequent recursive calls.
+      new_context = MapSet.put(context, tdd_id)
       assumptions = Map.new(sorted_assumptions)
 
       if Engine.check(assumptions) == :contradiction do
@@ -1477,8 +1602,13 @@ defmodule Tdd.Algo do
           {:ok, :false_terminal} ->
             Store.false_node_id()
 
+          {:ok, {:placeholder, _}} ->
+            # A placeholder should not exist in a fully formed graph being simplified.
+            # This indicates that the knot-tying in the compiler did not fully resolve
+            # the cycle. Encountering it means this path is unsatisfiable.
+            Store.false_node_id()
+
           {:ok, {var, y, n, d}} ->
-            # Dispatch to the handler for recursive variables.
             case var do
               {5, :c_head, constraint_id, _} ->
                 handle_recursive_subproblem(
@@ -1511,7 +1641,6 @@ defmodule Tdd.Algo do
                 )
 
               _ ->
-                # The rest of the logic for standard variables is unchanged.
                 case Map.get(assumptions, var) do
                   true ->
                     do_simplify(y, sorted_assumptions, new_context)
@@ -1559,7 +1688,7 @@ defmodule Tdd.Algo do
   end
 
   # --- Unary Operation: Substitute ---
-  # FIX: The implementation of substitute needs to change.
+  # TODO: does the implementation of substitute need to change?
 
   @spec substitute(non_neg_integer(), non_neg_integer(), non_neg_integer()) :: non_neg_integer()
   def substitute(root_id, from_id, to_id) do
@@ -1593,7 +1722,6 @@ defmodule Tdd.Algo do
               Store.false_node_id()
 
             {:ok, {var, y, n, d}} ->
-              # FIX: Substitute within the variable term itself.
               new_var = substitute_in_var(var, from_id, to_id)
               new_y = substitute(y, from_id, to_id)
               new_n = substitute(n, from_id, to_id)
@@ -1610,7 +1738,6 @@ defmodule Tdd.Algo do
   end
 
   # --- Coinductive Emptiness Check ---
-  # This function is correct and does not need to be changed.
   @spec check_emptiness(non_neg_integer()) :: non_neg_integer()
   def check_emptiness(tdd_id) do
     cache_key = {:check_emptiness, tdd_id}
@@ -1627,7 +1754,6 @@ defmodule Tdd.Algo do
     end
   end
 
-  # This function is correct and does not need to be changed.
   defp do_check_emptiness(tdd_id, sorted_assumptions, context) do
     current_state = {tdd_id, sorted_assumptions}
 
@@ -1640,6 +1766,9 @@ defmodule Tdd.Algo do
       if Engine.check(assumptions) == :contradiction do
         Store.false_node_id()
       else
+        # IO.inspect(tdd_id, label: "Fetching node in do_check_emptiness")
+        # Debug.print_tdd_graph(tdd_id)
+
         case Store.get_node(tdd_id) do
           {:ok, :true_terminal} ->
             Store.true_node_id()
@@ -1748,7 +1877,6 @@ defmodule Tdd.Algo do
     end
   end
 
-  # This function, containing our previous fix, is correct and does not need to be changed.
   defp handle_recursive_subproblem(
          algo_type,
          sub_key,
@@ -1759,108 +1887,109 @@ defmodule Tdd.Algo do
          # This is the coinductive context (a MapSet).
          context
        ) do
-    {var, y, n, d} = node_details
-    assumptions = Map.new(sorted_assumptions)
+    # --- BEGIN IMPROVEMENT ---
+    # Co-inductive check for the constraint ID itself. If we are being asked to
+    # reason about a constraint that is a placeholder (i.e., part of a cycle
+    # currently being built), we must avoid operating on it directly. The correct
+    # co-inductive assumption is that the check succeeds, so we proceed down
+    # the 'yes' path without performing invalid logic on the placeholder.
+    case Store.get_node(constraint_id) do
+      {:ok, {:placeholder, _}} ->
+        {_var, y, _n, _d} = node_details
 
-    # 1. Build the TDD for the sub-problem's effective type by intersecting all
-    #    its constraints from the current assumption set.
-    op_intersect = fn
-      :false_terminal, _ -> :false_terminal
-      _, :false_terminal -> :false_terminal
-      t, :true_terminal -> t
-      :true_terminal, t -> t
-    end
-
-    sub_problem_constraints =
-      Enum.filter(assumptions, fn {v, _} ->
-        (Tdd.Predicate.Info.get_traits(v) || %{})[:sub_key] == sub_key
-      end)
-
-    sub_problem_tdd_id =
-      Enum.reduce(sub_problem_constraints, Store.true_node_id(), fn {var, val}, acc_id ->
-        constraint_for_this_assumption = Engine.unwrap_var(var)
-
-        id_to_intersect =
-          if val, do: constraint_for_this_assumption, else: negate(constraint_for_this_assumption)
-
-        apply(:intersect, op_intersect, acc_id, id_to_intersect)
-      end)
-
-    # 2. Check for the three logical outcomes:
-    #    - Does the path imply the constraint is satisfied?
-    #    - Does the path imply the constraint is violated?
-    #    - Or are both outcomes still possible?
-
-    # Implies satisfied: `sub_problem_tdd_id <: constraint_id`
-    # This is equivalent to `(sub_problem_tdd_id & !constraint_id)` being empty.
-    neg_constraint_id = negate(constraint_id)
-
-    intersect_sub_with_neg_constraint =
-      apply(:intersect, op_intersect, sub_problem_tdd_id, neg_constraint_id)
-
-    implies_satisfied =
-      check_emptiness(intersect_sub_with_neg_constraint) == Store.false_node_id()
-
-    # Implies violated: `sub_problem_tdd_id` and `constraint_id` are disjoint.
-    # This is equivalent to `(sub_problem_tdd_id & constraint_id)` being empty.
-    intersect_sub_with_constraint =
-      apply(:intersect, op_intersect, sub_problem_tdd_id, constraint_id)
-
-    implies_violated = check_emptiness(intersect_sub_with_constraint) == Store.false_node_id()
-
-    # 3. Branch based on the logical outcome.
-    cond do
-      implies_satisfied and implies_violated ->
-        # The sub-problem itself must be empty/impossible under the current assumptions.
-        # This whole path is a contradiction.
-        Store.false_node_id()
-
-      implies_satisfied ->
-        # The constraint is guaranteed by the path. Follow the 'yes' branch.
-        # The assumptions already imply this, so no change to them is needed.
         case algo_type do
           :simplify -> do_simplify(y, sorted_assumptions, context)
           :check_emptiness -> do_check_emptiness(y, sorted_assumptions, context)
         end
 
-      implies_violated ->
-        # The constraint is impossible given the path. Follow the 'no' branch.
-        # We can add this new fact `{var, false}` to strengthen the assumptions.
-        new_assumptions = Map.put(assumptions, var, false) |> Enum.sort()
+      # If the constraint_id is a valid, fully-formed node, proceed with the original logic.
+      _ ->
+        # --- END IMPROVEMENT ---
+        {var, y, n, d} = node_details
+        assumptions = Map.new(sorted_assumptions)
 
-        case algo_type do
-          :simplify -> do_simplify(n, new_assumptions, context)
-          :check_emptiness -> do_check_emptiness(n, new_assumptions, context)
+        # 1. Build the TDD for the sub-problem's effective type by intersecting all
+        #    its constraints from the current assumption set.
+        op_intersect = fn
+          :false_terminal, _ -> :false_terminal
+          _, :false_terminal -> :false_terminal
+          t, :true_terminal -> t
+          :true_terminal, t -> t
         end
 
-      true ->
-        # Neither outcome is guaranteed. Both are possible.
-        # We must explore both branches and combine the results.
-        new_assumptions_for_no_branch = Map.put(assumptions, var, false) |> Enum.sort()
+        sub_problem_constraints =
+          Enum.filter(assumptions, fn {v, _} ->
+            (Tdd.Predicate.Info.get_traits(v) || %{})[:sub_key] == sub_key
+          end)
 
-        case algo_type do
-          :check_emptiness ->
-            # Is there ANY path to true? Explore both and take their union.
-            res_y = do_check_emptiness(y, sorted_assumptions, context)
-            res_n = do_check_emptiness(n, new_assumptions_for_no_branch, context)
+        sub_problem_tdd_id =
+          Enum.reduce(sub_problem_constraints, Store.true_node_id(), fn {var, val}, acc_id ->
+            constraint_for_this_assumption = Engine.unwrap_var(var)
 
-            # Define local terminal logic for union
-            op_union = fn
-              :true_terminal, _ -> :true_terminal
-              _, :true_terminal -> :true_terminal
-              t, :false_terminal -> t
-              :false_terminal, t -> t
+            id_to_intersect =
+              if val,
+                do: constraint_for_this_assumption,
+                else: negate(constraint_for_this_assumption)
+
+            apply(:intersect, op_intersect, acc_id, id_to_intersect)
+          end)
+
+        # 2. Check for the three logical outcomes...
+        neg_constraint_id = negate(constraint_id)
+
+        intersect_sub_with_neg_constraint =
+          apply(:intersect, op_intersect, sub_problem_tdd_id, neg_constraint_id)
+
+        implies_satisfied =
+          check_emptiness(intersect_sub_with_neg_constraint) == Store.false_node_id()
+
+        intersect_sub_with_constraint =
+          apply(:intersect, op_intersect, sub_problem_tdd_id, constraint_id)
+
+        implies_violated = check_emptiness(intersect_sub_with_constraint) == Store.false_node_id()
+
+        # 3. Branch based on the logical outcome.
+        cond do
+          implies_satisfied and implies_violated ->
+            Store.false_node_id()
+
+          implies_satisfied ->
+            case algo_type do
+              :simplify -> do_simplify(y, sorted_assumptions, context)
+              :check_emptiness -> do_check_emptiness(y, sorted_assumptions, context)
             end
 
-            apply(:sum, op_union, res_y, res_n)
+          implies_violated ->
+            new_assumptions = Map.put(assumptions, var, false) |> Enum.sort()
 
-          :simplify ->
-            # Simplify both sub-trees and rebuild the node, as we cannot simplify this node away.
-            res_y = do_simplify(y, sorted_assumptions, context)
-            res_n = do_simplify(n, new_assumptions_for_no_branch, context)
-            # 'dc' branch is independent of 'var'
-            res_d = do_simplify(d, sorted_assumptions, context)
-            Store.find_or_create_node(var, res_y, res_n, res_d)
+            case algo_type do
+              :simplify -> do_simplify(n, new_assumptions, context)
+              :check_emptiness -> do_check_emptiness(n, new_assumptions, context)
+            end
+
+          true ->
+            new_assumptions_for_no_branch = Map.put(assumptions, var, false) |> Enum.sort()
+
+            case algo_type do
+              :check_emptiness ->
+                res_y = do_check_emptiness(y, sorted_assumptions, context)
+                res_n = do_check_emptiness(n, new_assumptions_for_no_branch, context)
+
+                op_union = fn
+                  :true_terminal, _ -> :true_terminal
+                  _, :true_terminal -> :true_terminal
+                  t, :false_terminal -> t
+                  :false_terminal, t -> t
+                end
+
+                apply(:sum, op_union, res_y, res_n)
+
+              :simplify ->
+                res_y = do_simplify(y, sorted_assumptions, context)
+                res_n = do_simplify(n, new_assumptions_for_no_branch, context)
+                res_d = do_simplify(d, sorted_assumptions, context)
+                Store.find_or_create_node(var, res_y, res_n, res_d)
+            end
         end
     end
   end
@@ -1869,8 +1998,6 @@ end
 defmodule Tdd.Compiler do
   @moduledoc """
   Compiles a `TypeSpec` into a canonical TDD ID.
-  REFAC: This module now embeds TDD IDs into recursive predicate variables
-  instead of raw TypeSpecs, a key part of the architectural decoupling.
   """
   alias Tdd.TypeSpec
   alias Tdd.Variable
@@ -1881,50 +2008,58 @@ defmodule Tdd.Compiler do
   @doc "The main public entry point. Takes a spec and returns its TDD ID."
   @spec spec_to_id(TypeSpec.t()) :: non_neg_integer()
   def spec_to_id(spec) do
-    # It's crucial to initialize the store for each top-level compilation
-    # to ensure a clean slate for caches and node IDs. This makes calls independent.
     normalized_spec = TypeSpec.normalize(spec)
+    IO.inspect(normalized_spec, label: "NORMALIZED SPEC")
     compile_normalized_spec(normalized_spec, %{})
   end
 
   defp compile_normalized_spec(normalized_spec, context) do
-    cache_key = {:spec_to_id, normalized_spec}
+    sorted_context = Enum.sort(context)
+    cache_key = {:compile_spec_with_context, normalized_spec, sorted_context}
 
-    case normalized_spec do
-      {:type_var, var_name} ->
-        case Map.get(context, var_name) do
-          nil ->
-            raise "Tdd.Compiler: Unbound type variable during TDD compilation: #{inspect(var_name)}. Full spec: #{inspect(normalized_spec)}. Context: #{inspect(context)}"
+    case Store.get_op_cache(cache_key) do
+      {:ok, id} ->
+        id
 
-          placeholder_id when is_integer(placeholder_id) ->
-            placeholder_id
-        end
+      :not_found ->
+        id_to_cache =
+          case normalized_spec do
+            {:type_var, var_name} ->
+              Debug.log(Map.get(context, var_name), "{:type_var, var_name}")
 
-      _other_form ->
-        case Store.get_op_cache(cache_key) do
-          {:ok, id} ->
-            id
+              Map.get(context, var_name) ||
+                raise "Tdd.Compiler: Unbound type variable: #{inspect(var_name)}"
 
-          :not_found ->
-            id_to_cache =
-              case normalized_spec do
-                {:mu, var_name, body_spec} ->
-                  placeholder_node_variable_tag = {:mu_placeholder_for_var, var_name}
-                  placeholder_id = Store.create_placeholder(placeholder_node_variable_tag)
-                  new_context = Map.put(context, var_name, placeholder_id)
-                  compiled_body_id = compile_normalized_spec(body_spec, new_context)
-                  # The substitution is the "knot-tying" step for recursion
-                  final_id = Algo.substitute(compiled_body_id, placeholder_id, compiled_body_id)
-                  Algo.simplify(final_id)
+            {:mu, var_name, body_spec} ->
+              # Create a placeholder ID to represent the recursive reference.
+              placeholder_id = Store.create_placeholder({:mu_knot_tying_for, var_name, body_spec})
 
-                other ->
-                  raw_id = do_structural_compile(other, context)
-                  Algo.simplify(raw_id)
-              end
+              # Compile the body using the placeholder in the context. The resulting TDD
+              # will have `placeholder_id` at its recursive leaves.
+              new_context = Map.put(context, var_name, placeholder_id)
+              body_id_with_placeholder = compile_normalized_spec(body_spec, new_context)
 
-            Store.put_op_cache(cache_key, id_to_cache)
-            id_to_cache
-        end
+              # "Tie the knot": substitute the placeholder with the ID of the body's root.
+              # This correctly forms the cyclic TDD graph using the standard algorithm.
+              final_id =
+                Algo.substitute(
+                  body_id_with_placeholder,
+                  placeholder_id,
+                  body_id_with_placeholder
+                )
+
+              # The resulting graph may have new simplification opportunities after the knot is tied.
+              # This call to simplify, with the corrected algorithm from Fix #1, is CRITICAL.
+              Algo.simplify(final_id)
+
+            other_spec ->
+              raw_id = do_structural_compile(other_spec, context)
+              # Debug.build_graph_map(raw_id, "other spec id, before simplify")
+              Algo.simplify(raw_id)
+          end
+
+        Store.put_op_cache(cache_key, id_to_cache)
+        id_to_cache
     end
   end
 
@@ -1975,33 +2110,36 @@ defmodule Tdd.Compiler do
       {:negation, sub_spec} ->
         Algo.negate(compile_normalized_spec(sub_spec, context))
 
-      # REFAC: This is a key change. We now compile sub-specs to TDD IDs
-      # and embed those IDs in the predicate variables.
       {:cons, head_spec, tail_spec} ->
-        id_list = compile_normalized_spec(:list, context)
-        id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
-        id_not_is_empty = Algo.negate(id_is_empty)
+        # --- NEW GUARD CLAUSE ---
+        # If the head or tail of a cons is known to be impossible (:none),
+        # then the entire cons expression is impossible to construct.
+        if head_spec == :none or tail_spec == :none do
+          Store.false_node_id()
+        else
+          # --- EXISTING LOGIC (now safely in the 'else' block) ---
+          id_list = compile_normalized_spec(:list, context)
+          id_is_empty = create_base_type_tdd(Variable.v_list_is_empty())
+          id_not_is_empty = Algo.negate(id_is_empty)
 
-        non_empty_list_id =
-          Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
+          non_empty_list_id =
+            Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_not_is_empty)
 
-        # 1. Compile sub-specs to get their TDD IDs.
-        head_id = compile_normalized_spec(head_spec, context)
-        tail_id = compile_normalized_spec(tail_spec, context)
+          head_id = compile_normalized_spec(head_spec, context)
+          tail_id = compile_normalized_spec(tail_spec, context)
 
-        # 2. Embed the TDD IDs into the variables.
-        head_checker_var = Variable.v_list_head_pred(head_id)
-        head_checker_tdd = create_base_type_tdd(head_checker_var)
+          head_checker_var = Variable.v_list_head_pred(head_id)
+          head_checker_tdd = create_base_type_tdd(head_checker_var)
 
-        tail_checker_var = Variable.v_list_tail_pred(tail_id)
-        tail_checker_tdd = create_base_type_tdd(tail_checker_var)
+          tail_checker_var = Variable.v_list_tail_pred(tail_id)
+          tail_checker_tdd = create_base_type_tdd(tail_checker_var)
 
-        [non_empty_list_id, head_checker_tdd, tail_checker_tdd]
-        |> Enum.reduce(Store.true_node_id(), fn id, acc ->
-          Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
-        end)
+          [non_empty_list_id, head_checker_tdd, tail_checker_tdd]
+          |> Enum.reduce(Store.true_node_id(), fn id, acc ->
+            Algo.apply(:intersect, &op_intersect_terminals/2, id, acc)
+          end)
+        end
 
-      # REFAC: Same change for tuples.
       {:tuple, elements_specs} ->
         size = length(elements_specs)
         base_id = compile_normalized_spec(:tuple, context)
@@ -2011,9 +2149,7 @@ defmodule Tdd.Compiler do
         elements_specs
         |> Enum.with_index()
         |> Enum.reduce(initial_id, fn {elem_spec, index}, acc_id ->
-          # 1. Compile element spec to get its TDD ID.
           elem_id = compile_normalized_spec(elem_spec, context)
-          # 2. Embed the TDD ID into the variable.
           elem_checker_var = Variable.v_tuple_elem_pred(index, elem_id)
           elem_checker_tdd = create_base_type_tdd(elem_checker_var)
 
@@ -2078,10 +2214,17 @@ defmodule Tdd.Compiler do
   @doc "Checks if spec1 is a subtype of spec2 using TDDs."
   @spec is_subtype(TypeSpec.t(), TypeSpec.t()) :: boolean
   def is_subtype(spec1, spec2) do
+    Store.init()
+
     id1 = spec_to_id(spec1)
     id2 = spec_to_id(spec2)
+    Debug.build_graph_map(id1, "IS_SUBTYPE id1")
+    Debug.build_graph_map(id2, "IS_SUBTYPE id2")
+    IO.inspect("___________________________________")
     neg_id2 = Algo.negate(id2)
+    Debug.build_graph_map(neg_id2, "IS_SUBTYPE neg_id2")
     intersect_id = Algo.apply(:intersect, &op_intersect_terminals/2, id1, neg_id2)
+    Debug.build_graph_map(intersect_id, "IS_SUBTYPE intersect")
     final_id = Algo.check_emptiness(intersect_id)
     final_id == Store.false_node_id()
   end

mix.exs

@@ -26,6 +26,7 @@ defmodule Til.MixProject do
     [
       # {:dep_from_hexpm, "~> 0.3.0"},
       # {:dep_from_git, git: "https://github.com/elixir-lang/my_dep.git", tag: "0.1.0"}
+      {:jason, "~> 1.4"},
       {:ex_unit_summary, "~> 0.1.0", only: [:dev, :test]}
     ]
   end

mix.lock

@@ -1,3 +1,4 @@
 %{
   "ex_unit_summary": {:hex, :ex_unit_summary, "0.1.0", "7b0352afc5e6a933c805df0a539b66b392ac12ba74d8b208db7d83f77cb57049", [:mix], [], "hexpm", "8c87d0deade3657102902251d2ec60b5b94560004ce0e2c2fa5b466232716bd6"},
+  "jason": {:hex, :jason, "1.4.4", "b9226785a9aa77b6857ca22832cffa5d5011a667207eb2a0ad56adb5db443b8a", [:mix], [{:decimal, "~> 1.0 or ~> 2.0", [hex: :decimal, repo: "hexpm", optional: true]}], "hexpm", "c5eb0cab91f094599f94d55bc63409236a8ec69a21a67814529e8d5f6cc90b3b"},
 }

test/til_test.exs

@@ -8,6 +8,7 @@ defmodule TddSystemTest do
   alias Tdd.Compiler
   alias Tdd.Consistency.Engine
   alias Tdd.Algo
+  alias Tdd.Debug
 
   # Helper to mimic the old test structure and provide better failure messages
   # for spec comparisons.
@@ -29,14 +30,25 @@ defmodule TddSystemTest do
   # Helper to check for equivalence by comparing TDD IDs.
   defmacro assert_equivalent_specs(spec1, spec2) do
     quote do
-      assert Compiler.spec_to_id(unquote(spec1)) == Compiler.spec_to_id(unquote(spec2))
+      id1 = Compiler.spec_to_id(unquote(spec1))
+      id2 = Compiler.spec_to_id(unquote(spec2))
+      # Debug.build_graph_map(id1, "assert_equivalent_specs id1")
+      # Debug.build_graph_map(id2, "assert_equivalent_specs id2")
+      Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
+      Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
+      IO.inspect("equvalent specs? #{id1} #{id2}")
+      assert id1 == id2
     end
   end
 
   # Helper to check for subtyping using the TDD compiler.
   defmacro assert_subtype(spec1, spec2) do
     quote do
-      assert Compiler.is_subtype(unquote(spec1), unquote(spec2))
+      IO.inspect("assert is_subtype #{inspect(unquote(spec1))}, #{inspect(unquote(spec2))}")
+      is_subtype? = Compiler.is_subtype(unquote(spec1), unquote(spec2))
+      Process.get(:tdd_node_by_id) |> IO.inspect(label: ":tdd_node_by_id")
+      Process.get(:tdd_nodes) |> IO.inspect(label: ":tdd_nodes")
+      assert is_subtype?
     end
   end
 
@@ -165,7 +177,7 @@ defmodule TddSystemTest do
       assert_spec_normalized({:negation, :integer}, {:negation, :integer})
     end
 
-    @doc "Tests that an odd number of negations simplifies to a single negation."
+    @doc "Tests that an odd integer of negations simplifies to a single negation."
     test "¬(¬(¬atom)) simplifies to ¬atom" do
       assert_spec_normalized({:negation, :atom}, {:negation, {:negation, {:negation, :atom}}})
     end
@@ -380,22 +392,20 @@ defmodule TddSystemTest do
   # These tests target the most complex features: recursive and polymorphic types.
   # ---
   describe "Tdd.Compiler: Advanced Features (μ, Λ, Apply)" do
-    @doc """
-    It checks for covariance in generic types: a list of integers is a subtype of a list of anything,
-    but the reverse is not true. This requires the system to correctly handle coinductive reasoning
-    on the recursive TDD nodes.
-    """
-    test "the previously crashing recursive subtype test now passes" do
+    test "list subtyping: list(int) <: list(any)" do
       int_list = {:list_of, :integer}
       any_list = {:list_of, :any}
       assert_subtype(:integer, :any)
-      # The key test that was failing due to the bug
       assert_subtype(int_list, any_list)
-      refute_subtype(any_list, int_list)
-
-      # Also test instances against the recursive type
       assert_subtype({:cons, {:literal, 1}, {:literal, []}}, int_list)
+    end
+
+    test "list subtyping: list(any) <! list(integer)" do
+      int_list = {:list_of, :integer}
+      any_list = {:list_of, :any}
+      assert_subtype(:integer, :any)
       refute_subtype({:cons, {:literal, :a}, {:literal, []}}, int_list)
+      refute_subtype(any_list, int_list)
     end
 
     @doc "Tests that manually-defined recursive types (like a binary tree) can be compiled and checked correctly."
@@ -430,5 +440,178 @@ defmodule TddSystemTest do
 
       assert_equivalent_specs(list_of_int_from_apply, int_list)
     end
+
+    test "negate list type" do
+      refute_subtype({:negation, {:list_of, :integer}}, :none)
+    end
+  end
+
+  describe "Logical Equivalences: De Morgan's Laws & Distributivity" do
+    @doc "Tests ¬(A ∪ B) <=> (¬A ∩ ¬B)"
+    test "De Morgan's Law for negated unions" do
+      # ¬(atom | integer)
+      spec1 = {:negation, {:union, [:atom, :integer]}}
+      # ¬atom & ¬integer
+      spec2 = {:intersect, [{:negation, :atom}, {:negation, :integer}]}
+      assert_equivalent_specs(spec1, spec2)
+    end
+
+    @doc "Tests ¬(A ∩ B) <=> (¬A ∪ ¬B)"
+    test "De Morgan's Law for negated intersections" do
+      # ¬(integer & atom)
+      spec1 = {:negation, {:intersect, [:integer, :atom]}}
+      # ¬integer | ¬atom
+      spec2 = {:union, [{:negation, :integer}, {:negation, :atom}]}
+      assert_equivalent_specs(spec1, spec2)
+    end
+
+    @doc "Tests A ∩ (B ∪ C) <=> (A ∩ B) ∪ (A ∩ C)"
+    test "Distributive Law: intersection over union" do
+      # We'll use types where some intersections are meaningful and others are :none
+      # `integer` is a supertype of `integer` and `tuple`
+      # `(integer | tuple) & (atom | integer)`
+      spec1 =
+        {:intersect, [{:union, [:integer, :tuple]}, {:union, [:atom, :integer]}]}
+
+      # Should be equivalent to:
+      # (integer & atom) | (integer & integer) | (tuple & atom) | (tuple & integer)
+      # which simplifies to:
+      # :none | :integer | :none | :none
+      # which is just :integer
+      Debug.print_tdd_graph(Compiler.spec_to_id(spec1))
+      assert_equivalent_specs(spec1, :integer)
+    end
+
+    @doc "Tests A | (B & C) versus (A | B) & (A | C) -- they are NOT always equivalent"
+    test "subtyping with distributivity" do
+      # Let's test `A | (B & C) <: (A | B) & (A | C)`
+      spec_left = {:union, [:atom, {:intersect, [:integer, {:integer_range, 0, :pos_inf}]}]}
+
+      spec_right =
+        {:intersect,
+         [{:union, [:atom, :integer]}, {:union, [:atom, {:integer_range, 0, :pos_inf}]}]}
+
+      # `spec_left` normalizes to `atom | positive_integer`
+      # `spec_right` normalizes to `(atom | integer) & (atom | positive_integer)`
+      # Since `atom | positive_integer` is a subtype of `atom | integer`, the intersection on the right
+      # simplifies to `atom | positive_integer`. Therefore, they are equivalent in this case.
+      assert_equivalent_specs(spec_left, spec_right)
+
+      spec_sub = {:union, [:integer, {:intersect, [:atom, :tuple]}]}
+      spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :tuple]}]}
+      assert_subtype(spec_sub, spec_super)
+    end
+  end
+
+  # ---
+  # Advanced Negation and Contradiction Tests
+  # ---
+  describe "Tdd.Compiler: Advanced Negation and Contradiction" do
+    @doc "Tests that a type and its negation correctly partition the universal set (:any)."
+    test "A | ¬A <=> :any" do
+      spec = {:union, [:integer, {:negation, :integer}]}
+      assert_equivalent_specs(spec, :any)
+    end
+
+    @doc "Tests that a subtype relationship holds against a negated supertype"
+    test "subtyping with negation: integer <: ¬atom" do
+      # An integer is never an atom, so it should be a subtype of "not atom".
+      assert_subtype(:integer, {:negation, :atom})
+      # The reverse is not true: `not atom` includes lists, integers, etc.
+      refute_subtype({:negation, :atom}, :integer)
+    end
+
+    @doc "A complex type that should resolve to :none"
+    test "complex contradiction involving subtype logic" do
+      # This is `(integer and not a integer)`. Since all integers are integers, this is impossible.
+      spec = {:intersect, [:integer, {:negation, :integer}]}
+      assert_equivalent_specs(spec, :none)
+    end
+
+    @doc "The type 'list of integers that are also atoms' should be impossible"
+    test "contradiction inside a recursive type structure" do
+      # list_of(integer & atom) is list_of(:none).
+      # A list of :none can only be the empty list, as no element can ever exist.
+      spec = {:list_of, {:intersect, [:integer, :atom]}}
+      Tdd.Store.init()
+      Debug.print_tdd_graph(Compiler.spec_to_id(spec))
+      Debug.print_tdd_graph(Compiler.spec_to_id({:literal, []}))
+      assert_equivalent_specs(spec, {:literal, []})
+    end
+  end
+
+  # ---
+  # Complex Recursive (μ) and Polymorphic (Λ, Apply) Tests
+  # These tests probe the interaction between recursion, polymorphism, and subtyping.
+  # ---
+  describe "Tdd.Compiler: Interplay of μ, Λ, and Subtyping" do
+    @doc "Tests subtyping between structurally similar, but not identical, recursive types."
+    test "subtyping of structural recursive types: list_of(1|2) <: list_of(integer)" do
+      list_of_1_or_2 = {:list_of, {:union, [{:literal, 1}, {:literal, 2}]}}
+      list_of_integer = {:list_of, :integer}
+
+      assert_subtype(list_of_1_or_2, list_of_integer)
+      refute_subtype(list_of_integer, list_of_1_or_2)
+    end
+
+    @doc "Tests a non-sensical recursion that should simplify away"
+    test "μ-types that should normalize to a non-recursive form" do
+      # A type defined as "a cons of an atom and itself, or none" should be equivalent to `list_of(atom)`.
+      # This tests if our manual mu-calculus definition matches the syntactic sugar.
+      manual_list_of_atom = {:mu, :L, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :L}}]}}
+      sugar_list_of_atom = {:list_of, :atom}
+      assert_equivalent_specs(manual_list_of_atom, sugar_list_of_atom)
+    end
+
+    test "infer termination of recursive types" do
+      spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
+      assert_equivalent_specs(spec, :integer)
+    end
+
+    @doc "Tests polymorphism with multiple type parameters."
+    test "lambda with multiple parameters: (Λ(A,B). {A,B})(int, atom)" do
+      # λ(A, B). {A, B}
+      map_constructor = {:type_lambda, [:A, :B], {:tuple, [{:type_var, :A}, {:type_var, :B}]}}
+      # Apply it to integer and atom
+      applied_spec = {:type_apply, map_constructor, [:integer, :atom]}
+      # The result should be the concrete type {integer, atom}
+      expected_spec = {:tuple, [:integer, :atom]}
+
+      assert_equivalent_specs(applied_spec, expected_spec)
+    end
+
+    @doc "Tests that applying a lambda to a complex recursive type works correctly"
+    test "applying a polymorphic list constructor to a tree type" do
+      # First, define our tree type from a previous test
+      leaf_node = {:literal, :empty_tree}
+
+      tree_spec =
+        {:mu, :Tree,
+         {:union,
+          [
+            leaf_node,
+            {:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]}
+          ]}}
+
+      # Now, apply the generic list lambda to this tree_spec
+      gen_list_lambda = {:type_lambda, [:T], {:list_of, {:type_var, :T}}}
+      list_of_trees = {:type_apply, gen_list_lambda, [tree_spec]}
+
+      # Check if a concrete instance is a subtype of this new complex type
+      tree_instance_1 = {:tuple, [{:literal, :a}, leaf_node, leaf_node]}
+      tree_instance_2 = {:tuple, [{:literal, :b}, leaf_node, leaf_node]}
+      list_of_trees_instance = {:cons, tree_instance_1, {:cons, tree_instance_2, {:literal, []}}}
+
+      assert_subtype(list_of_trees_instance, list_of_trees)
+    end
+
+    # failing 
+    @doc "An 'ill-formed' recursive type that should evaluate to :none"
+    test "μ-types that are self-contradictory should be :none" do
+      # A type defined as `μX. cons(integer, X)`. This describes an infinite list
+      # of integers with no base case (`[]`). No finite value can ever satisfy this type.
+      infinite_list = {:mu, :X, {:cons, :integer, {:type_var, :X}}}
+      assert_equivalent_specs(infinite_list, :none)
+    end
   end
 end