wip lists

test.exs

@@ -148,23 +148,22 @@ defmodule Tdd do
     *   `lt(N)` and `gt(M)` if `N <= M+1` (or `N <= M` if `gt` means `>=`) -> contradiction. (e.g., `x < 5` and `x > 4` has no integer solution).
     *   *Strategy for complex integer constraints*: Maintain a "current allowed interval" `[min_assumed, max_assumed]` based on `assumptions_map`. If this interval becomes empty or invalid, it's a contradiction. Each new integer assumption (`lt, gt, eq`) refines this interval.
 
-  ### 3.4. Lists (Planned)
+  ### 3.4. Lists (Implemented)
 
   *   **Variables**:
     *   `@v_is_list = {0, :is_list}`.
-    *   `v_list_is_empty = {LIST_CAT, :is_empty}`.
+    *   `v_list_is_empty = {5, :is_empty}`.
     *   *If not empty*:
-        *   `v_list_head_VAR = {LIST_CAT, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head.
+        *   `v_list_head_pred = {5, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head.
-        *   `v_list_tail_VAR = {LIST_CAT, :tail, NESTED_PREDICATE_ID_FOR_TAIL_LIST}`: Applies a global predicate (usually list predicates) to the tail.
+        *   `v_list_tail_pred = {5, :tail, NESTED_PREDICATE_ID_FOR_TAIL}`: Applies a global predicate (usually list predicates) to the tail.
-    *   *(Alternative for fixed-length lists/known structure: `{LIST_CAT, :elem, Index_I, NESTED_PREDICATE_ID}` similar to tuples).*
   *   **Constructors**:
-    *   `type_list_any()`.
+    *   `type_list()`: Represents any list.
-    *   `type_empty_list()`.
+    *   `type_empty_list()`: Represents the empty list `[]`.
-    *   `type_cons(head_type_id, tail_type_id)`.
+    *   `type_cons(head_type_id, tail_type_id)`: Represents a non-empty list `[H|T]` where `H` is of type `head_type_id` and `T` is of type `tail_type_id`.
-    *   `type_list_of(element_type_id)`: e.g., `list(integer())`.
   *   **Semantic Constraints**:
     *   `is_list=true` vs. other primary types.
-    *   If `is_empty=true`, then any predicate about `head` or non-empty `tail` structure is contradictory if it implies existence.
+    *   If `is_empty=true`, any predicate on the `head` or `tail` is a contradiction.
+    *   Recursive consistency checks on `head` and `tail` sub-types.
 
   ### 3.5. Strings & Binaries (Planned)
 
@@ -331,45 +330,96 @@ defmodule Tdd do
     end
   end
 
-  defp check_assumptions_consistency(assumptions_map) do
+  defp check_assumptions_consistency(assumptions_map, ambient_constraints \\ %{}) do
+ # 1. Merge ambient constraints into the main map.
+    # This ensures, for example, that if we are checking the `head` of a `list(X)`,
+    # the constraint `is_subtype(head, X)` is enforced.
+    assumptions_map = Map.merge(ambient_constraints, assumptions_map)
     # 1. Partition assumptions by the entity they apply to.
-    # :top_level for the main value, and {:elem, index} for tuple elements.
     partitioned_assumptions =
       Enum.group_by(assumptions_map, fn
-        # Variable for a tuple element's property. Example: {4, :element, 0, {0, :is_integer}}
+        # Tuple element property: {4, :element, 0, {0, :is_integer}}
         {{4, :element, index, _nested_var}, _value} -> {:elem, index}
+        # List head property: {5, :head, {0, :is_atom}}
+        {{5, :head, _nested_var}, _value} -> :head
+        # List tail property: {5, :tail, {5, :is_empty}}
+        {{5, :tail, _nested_var}, _value} -> :tail
         # All other variables
         _ -> :top_level
       end)
 
-    # 2. Extract and check the assumptions for the top-level entity.
+    # 2. Check the assumptions for the top-level entity.
-    top_level_assumptions =
+    top_level_assumptions = Map.get(partitioned_assumptions, :top_level, []) |> Map.new()
-      Map.get(partitioned_assumptions, :top_level, [])
-      |> Map.new()
 
     case do_check_flat_consistency(top_level_assumptions) do
       :contradiction ->
         :contradiction
 
       :consistent ->
-        # 3. If top-level is consistent, check each tuple element's assumptions.
+        # 4. If top-level is consistent, gather new ambient constraints and check sub-problems.
-        element_partitions = Map.drop(partitioned_assumptions, [:top_level])
+        all_elems_constraints =
+          Enum.reduce(top_level_assumptions, [], fn
+            {{5, :all_elements, type_id}, true}, acc -> [type_id | acc]
+            _, acc -> acc
+          end)
 
-        Enum.reduce_while(element_partitions, :consistent, fn
+        sub_problems = Map.drop(partitioned_assumptions, [:top_level])
-          # The key is {:elem, index}, the value is a list of {var, val} tuples
+
+        Enum.reduce_while(sub_problems, :consistent, fn
+          # For a tuple element (no ambient constraints from parent needed for now)
           {{:elem, _index}, assumptions_list}, _acc ->
-            # Transform the list of assumptions into a "flat" map for the element,
-            # by extracting the nested predicate.
             sub_assumptions =
               assumptions_list
-              |> Map.new(fn {{_vcat, _ptype, _idx, nested_var}, value} -> {nested_var, value} end)
+              |> Map.new(fn {{_, :element, _, nested_var}, value} -> {nested_var, value} end)
 
-            # 4. Recursively call the main consistency checker on the sub-problem.
-            #    This allows for arbitrarily nested tuple types.
             case check_assumptions_consistency(sub_assumptions) do
               :contradiction -> {:halt, :contradiction}
               :consistent -> {:cont, :consistent}
             end
+
+          # For a list head
+          {:head, assumptions_list}, _acc ->
+            # The head must conform to every `all_elements` constraint on the list.
+            # We build a TDD for the intersection of all these constraints.
+            ambient_type_for_head =
+              Enum.reduce(all_elems_constraints, type_any(), &intersect/2)
+
+            head_sub_assumptions =
+              assumptions_list
+              |> Map.new(fn {{_, :head, nested_var}, value} -> {nested_var, value} end)
+
+            # Check if the explicitly assumed head type contradicts the ambient one.
+            head_type_from_assumptions =
+              simplify_with_constraints(@true_node_id, head_sub_assumptions)
+
+            if is_subtype(head_type_from_assumptions, ambient_type_for_head) do
+              # Recursively check internal consistency of the head's own assumptions.
+              case check_assumptions_consistency(head_sub_assumptions) do
+                :contradiction -> {:halt, :contradiction}
+                :consistent -> {:cont, :consistent}
+              end
+            else
+              {:halt, :contradiction}
+            end
+
+          # For a list tail
+          {:tail, assumptions_list}, _acc ->
+            # The tail must also be a list conforming to the same `all_elements` constraints.
+            # So we pass the parent's `all_elements` assumptions down as ambient constraints for the tail.
+            ambient_for_tail =
+              Enum.reduce(all_elems_constraints, %{}, fn type_id, acc ->
+                Map.put(acc, v_list_all_elements_are(type_id), true)
+              end)
+
+            tail_sub_assumptions =
+              assumptions_list
+              |> Map.new(fn {{_, :tail, nested_var}, value} -> {nested_var, value} end)
+
+            # Recursively check the tail's assumptions *with the ambient constraints*.
+            case check_assumptions_consistency(tail_sub_assumptions, ambient_for_tail) do
+              :contradiction -> {:halt, :contradiction}
+              :consistent -> {:cont, :consistent}
+            end
         end)
     end
   end
@@ -384,61 +434,71 @@ defmodule Tdd do
         _otherwise, acc_set -> acc_set
       end)
 
-    raw_result =
     if MapSet.size(primary_true_predicates) > 1 do
       :contradiction
     else
-        # --- Atom-specific checks ---
+      # Perform checks for each type category...
+      # (Existing atom, tuple, integer checks are chained via `cond`)
+      # If no specific checks resulted in contradiction, it's consistent.
+      check_atom_logic(assumptions_map, primary_true_predicates) ||
+        check_tuple_logic(assumptions_map, primary_true_predicates) ||
+        check_integer_logic(assumptions_map, primary_true_predicates) ||
+        check_list_logic(assumptions_map, primary_true_predicates) ||
+        :consistent
+    end
+  end
+
+  # Helper functions to break down the massive cond block
+  defp check_atom_logic(assumptions_map, primary_true_predicates) do
     has_true_atom_specific_pred =
       Enum.any?(assumptions_map, fn {var_id, truth_value} ->
         elem(var_id, 0) == 1 && truth_value == true
       end)
 
-        is_explicitly_not_atom_or_different_primary =
+    is_explicitly_not_atom =
       Map.get(assumptions_map, @v_is_atom) == false ||
         (MapSet.size(primary_true_predicates) == 1 &&
            !MapSet.member?(primary_true_predicates, :is_atom))
 
-        cond do
+    if has_true_atom_specific_pred && is_explicitly_not_atom do
-          has_true_atom_specific_pred && is_explicitly_not_atom_or_different_primary ->
       :contradiction
-
+    else
-          true ->
       atom_value_trues =
         Enum.reduce(assumptions_map, MapSet.new(), fn
           {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val)
           _otherwise, acc_set -> acc_set
         end)
 
-            if MapSet.size(atom_value_trues) > 1 do
+      if MapSet.size(atom_value_trues) > 1, do: :contradiction, else: false
-              :contradiction
+    end
-            else
+  end
-              # --- Tuple-specific checks ---
+
+  defp check_tuple_logic(assumptions_map, primary_true_predicates) do
     has_true_tuple_specific_pred =
       Enum.any?(assumptions_map, fn {var_id, truth_value} ->
         elem(var_id, 0) == 4 && truth_value == true
       end)
 
-              is_explicitly_not_tuple_or_different_primary =
+    is_explicitly_not_tuple =
       Map.get(assumptions_map, @v_is_tuple) == false ||
         (MapSet.size(primary_true_predicates) == 1 &&
            !MapSet.member?(primary_true_predicates, :is_tuple))
 
-              cond do
+    if has_true_tuple_specific_pred && is_explicitly_not_tuple do
-                has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary ->
       :contradiction
-
+    else
-                true ->
       tuple_size_trues =
         Enum.reduce(assumptions_map, MapSet.new(), fn
           {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val)
           _otherwise, acc_set -> acc_set
         end)
 
-                  if MapSet.size(tuple_size_trues) > 1 do
+      if MapSet.size(tuple_size_trues) > 1, do: :contradiction, else: false
-                    :contradiction
+    end
-                  else
+  end
-                    # --- Integer predicate checks (REVISED LOGIC) ---
+
+  # (The original integer checking logic is moved into this helper)
+defp check_integer_logic(assumptions_map, primary_true_predicates) do
     has_true_integer_specific_pred =
       Enum.any?(assumptions_map, fn {var_id, truth_value} ->
         elem(var_id, 0) == 2 && truth_value == true
@@ -498,7 +558,7 @@ defmodule Tdd do
                 new_max_b = if is_nil(acc.max_b), do: n, else: min(acc.max_b, n)
                 %{acc | max_b: new_max_b}
 
-                              # Ignore non-integer or :dc preds for this pass
+              # Ignore other preds for this pass
               _otherwise, acc ->
                 acc
             end
@@ -509,7 +569,9 @@ defmodule Tdd do
             :contradiction
 
           {:consistent, current_interval_min, current_interval_max} ->
-                            # Interval from true/false preds is consistent. Now check :dc preds against it.
+            # Interval from true/false preds is consistent. Now check for other implied contradictions.
+            # This logic was missing from my simplified version and is critical.
+            res =
               Enum.reduce_while(assumptions_map, :consistent, fn
                 {{2, pred_type, n_val}, :dc}, _acc_status ->
                   is_implied_true =
@@ -521,13 +583,9 @@ defmodule Tdd do
                              current_interval_max == n_val)
 
                       :alt ->
-                                      is_integer(current_interval_max) &&
+                        is_integer(current_interval_max) && current_interval_max < n_val
-                                        current_interval_max < n_val
-
                       :cgt ->
-                                      is_integer(current_interval_min) &&
+                        is_integer(current_interval_min) && current_interval_min > n_val
-                                        current_interval_min > n_val
-
                       _ ->
                         false
                     end
@@ -535,19 +593,12 @@ defmodule Tdd do
                   is_implied_false =
                     case pred_type do
                       :beq ->
-                                      (is_integer(current_interval_min) &&
+                        (is_integer(current_interval_min) && current_interval_min > n_val) ||
-                                         current_interval_min > n_val) ||
+                          (is_integer(current_interval_max) && current_interval_max < n_val)
-                                        (is_integer(current_interval_max) &&
-                                           current_interval_max < n_val)
-
                       :alt ->
-                                      is_integer(current_interval_min) &&
+                        is_integer(current_interval_min) && current_interval_min >= n_val
-                                        current_interval_min >= n_val
-
                       :cgt ->
-                                      is_integer(current_interval_max) &&
+                        is_integer(current_interval_max) && current_interval_max <= n_val
-                                        current_interval_max <= n_val
-
                       _ ->
                         false
                     end
@@ -561,18 +612,46 @@ defmodule Tdd do
                 _other_assumption, acc_status ->
                   {:cont, acc_status}
               end)
+
+            # Return :contradiction if found, otherwise `false` to allow the `||` chain to continue.
+            if res == :contradiction, do: :contradiction, else: false
         end
 
       true ->
-                        :consistent
+        false
-                    end
-                  end
-              end
-            end
     end
   end
 
-    raw_result
+  ### NEW ###
+  # Logic for list consistency checks
+  defp check_list_logic(assumptions_map, primary_true_predicates) do
+    # A predicate like {5, :is_empty} or {5, :head, ...} exists
+    has_list_specific_pred =
+      Enum.any?(assumptions_map, fn {var_id, _} -> elem(var_id, 0) == 5 end)
+
+    is_explicitly_not_list =
+      Map.get(assumptions_map, v_is_list()) == false ||
+        (MapSet.size(primary_true_predicates) == 1 &&
+           !MapSet.member?(primary_true_predicates, :is_list))
+
+    # A predicate on head or tail exists, e.g. {{5, :head, _}, _}
+    has_head_or_tail_pred =
+      Enum.any?(assumptions_map, fn {{_cat, ptype, _}, _} -> ptype == :head or ptype == :tail
+      _ -> false end)
+
+    cond do
+      # Contradiction: list-specific rule is assumed, but type is not a list.
+      has_list_specific_pred && is_explicitly_not_list ->
+        :contradiction
+
+      # Contradiction: assumed to be an empty list, but also has assumptions about head/tail.
+      Map.get(assumptions_map, v_list_is_empty()) == true && has_head_or_tail_pred ->
+        :contradiction
+
+      # No flat contradictions found for lists. Recursive checks are done in the main function.
+      true ->
+        false
+    end
   end
 
   # Helper for min, treating nil as infinity
@@ -711,15 +790,24 @@ defmodule Tdd do
   @v_is_atom {0, :is_atom}
   @v_is_tuple {0, :is_tuple}
   @v_is_integer {0, :is_integer}
+  @v_is_list {0, :is_list}
 
   def v_is_atom, do: @v_is_atom
   def v_is_tuple, do: @v_is_tuple
   def v_is_integer, do: @v_is_integer
+  ### NEW ###
+  def v_is_list, do: @v_is_list
 
   def v_atom_eq(atom_val), do: {1, :value, atom_val}
   def v_tuple_size_eq(size), do: {4, :size, size}
   def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}
 
+  # List Predicates (Category 5)
+  def v_list_is_empty, do: {5, :is_empty}
+  def v_list_head_pred(nested_var), do: {5, :head, nested_var}
+  def v_list_tail_pred(nested_var), do: {5, :tail, nested_var}
+  def v_list_all_elements_are(element_type_id), do: {5, :all_elements, element_type_id}
+
   # Integer Predicates (Category 2)
   # strictly less than n
   def v_int_lt(n) when is_integer(n), do: {2, :alt, n}
@@ -763,70 +851,95 @@ defmodule Tdd do
     make_node_for_constructors(@v_is_integer, @true_node_id, @false_node_id, @false_node_id)
   end
 
-  def type_tuple_elem(element_index, element_type_id, success_path_id) do
+  # A recursive helper that maps a TDD onto a component (e.g., list head, tuple element).
-    node_details = get_node_details(element_type_id)
+  # It takes a tdd_id, a `wrapper_fun` (like `&v_list_head_pred/1`), and the ID to jump to on success.
-
+  defp map_tdd_to_component(tdd_id, wrapper_fun, success_id) do
-    case node_details do
+    case get_node_details(tdd_id) do
       :true_terminal ->
-        # Should be caught by guard Tdd.type_any(), but handle defensively
+        success_id
-        success_path_id
 
       :false_terminal ->
-        # Should be caught by guard Tdd.type_none(), but handle defensively
+        @false_node_id
-        type_none()
 
-      {original_var, y_id, n_id, d_id} ->
+      {var, y, n, d} ->
-        # Adapt original_var to be specific to this element_index
+        # Wrap the original variable to be specific to this component.
-        # The Tdd.v_tuple_elem_pred function creates the correctly prefixed variable
+        component_var = wrapper_fun.(var)
-        element_specific_var = v_tuple_elem_pred(element_index, original_var)
+        # Recurse on children, passing the success_id down.
-
+        res_y = map_tdd_to_component(y, wrapper_fun, success_id)
-        yes_branch_tdd = type_tuple_elem(element_index, y_id, success_path_id)
+        res_n = map_tdd_to_component(n, wrapper_fun, success_id)
-        no_branch_tdd = type_tuple_elem(element_index, n_id, success_path_id)
+        res_d = map_tdd_to_component(d, wrapper_fun, success_id)
-        dc_branch_tdd = type_tuple_elem(element_index, d_id, success_path_id)
+        make_node_raw(component_var, res_y, res_n, res_d)
-        make_node(element_specific_var, yes_branch_tdd, no_branch_tdd, dc_branch_tdd)
     end
   end
 
-  # TDD for a tuple with specific element types
+  def type_tuple_elem(element_index, element_type_id, success_path_id) do
+    map_tdd_to_component(element_type_id, &v_tuple_elem_pred(element_index, &1), success_path_id)
+  end
+
   def type_tuple(element_type_ids) do
     num_elements = length(element_type_ids)
 
-    # Build TDD for element checks from last to first
-    # The 'success_path_id' for the last element's check is Tdd.type_any() (representing TRUE)
     final_elements_check_tdd =
-      Enum.reduce(Enum.reverse(0..(num_elements - 1)), Tdd.type_any(), fn i, acc_tdd ->
+      Enum.reduce(Enum.reverse(0..(num_elements - 1)), type_any(), fn i, acc_tdd ->
         element_type_id = Enum.at(element_type_ids, i)
         type_tuple_elem(i, element_type_id, acc_tdd)
       end)
 
-    # Wrap with size check
     size_check_node =
-      make_node(
+      make_node(v_tuple_size_eq(num_elements), final_elements_check_tdd, type_none(), type_none())
-        v_tuple_size_eq(num_elements),
-        # If size matches, proceed to element checks
-        final_elements_check_tdd,
-        # If size mismatches, it's not this tuple type
-        type_none(),
-        # DC for size usually means not this specific tuple type
-        type_none()
-      )
 
-    # Wrap with primary tuple type check
+    raw_final_tdd = make_node(v_is_tuple(), size_check_node, type_none(), type_none())
-    raw_final_tdd =
-      make_node(
-        v_is_tuple(),
-        # If is_tuple, proceed to size check
-        size_check_node,
-        # If not a tuple, then false
-        type_none(),
-        # DC for is_tuple usually means not this specific type
-        type_none()
-      )
-
-    # Simplify the constructed TDD
     simplify_with_constraints(raw_final_tdd, %{})
   end
 
+  # List Type Constructors
+  def type_list,
+    do: make_node_for_constructors(v_is_list(), @true_node_id, @false_node_id, @false_node_id)
+
+  def type_empty_list,
+    do:
+      make_node_for_constructors(
+        v_is_list(),
+        make_node_raw(v_list_is_empty(), @true_node_id, @false_node_id, @false_node_id),
+        @false_node_id,
+        @false_node_id
+      )
+
+  def type_cons(head_type_id, tail_type_id) do
+    # 1. Build the TDD for the tail constraint.
+    # On success, this will proceed to the head constraint check.
+    tail_check_tdd = map_tdd_to_component(tail_type_id, &v_list_tail_pred/1, @true_node_id)
+
+    # 2. Build the TDD for the head constraint.
+    # On success, it proceeds to the TDD we just built for the tail.
+    head_and_tail_check_tdd =
+      map_tdd_to_component(head_type_id, &v_list_head_pred/1, tail_check_tdd)
+
+    # 3. A cons cell is never empty.
+    # If is_empty is true, it's a failure. If false, proceed to head/tail checks.
+    is_empty_check_node =
+      make_node(v_list_is_empty(), @false_node_id, head_and_tail_check_tdd, @false_node_id)
+
+    # 4. Wrap in the primary list type check.
+    raw_final_tdd = make_node(v_is_list(), is_empty_check_node, @false_node_id, @false_node_id)
+
+    # 5. Simplify the final result.
+    simplify_with_constraints(raw_final_tdd, %{})
+  end
+def type_list_of(element_type_id) when is_integer(element_type_id) do
+  # An empty list satisfies any list_of constraint vacuously.
+  # The type is effectively `[] | [X | list(X)]`
+  # We can't build this recursively, so we use a specialized predicate.
+
+  # This type is trivially `any` if element type is `any`
+  if element_type_id == type_any() do
+    type_list()
+  else
+    all_elems_check = make_node_raw(v_list_all_elements_are(element_type_id), @true_node_id, @false_node_id, @false_node_id)
+    raw_node = make_node_raw(v_is_list(), all_elems_check, @false_node_id, @false_node_id)
+    simplify_with_constraints(raw_node, %{})
+  end
+end
   def type_int_eq(n) do
     int_eq_node = make_node_raw(v_int_eq(n), @true_node_id, @false_node_id, @false_node_id)
     raw_node = make_node_raw(@v_is_integer, int_eq_node, @false_node_id, @false_node_id)
@@ -1431,7 +1544,8 @@ defmodule TupleTests do
     t_int_pos = type_int_gt(0)
     t_any = type_any()
     t_none = type_none()
-    t_tuple = type_tuple() # any tuple
+    # any tuple
+    t_tuple = type_tuple()
     t_empty_tuple = type_empty_tuple()
 
     # --- Specific Tuple Types ---
@@ -1495,23 +1609,48 @@ defmodule TupleTests do
     # {:foo, 5} | {pos_int, atom}
     union1 = sum(tup_foo_5, tup_pos_atom)
     test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))
-    test_fn.("{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_pos_atom, union1))
+
-    test_fn.("{atom, int} <: ({:foo, 5} | {pos_int, atom})", false, is_subtype(tup_atom_int, union1))
+    test_fn.(
+      "{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
+      true,
+      is_subtype(tup_pos_atom, union1)
+    )
+
+    test_fn.(
+      "{atom, int} <: ({:foo, 5} | {pos_int, atom})",
+      false,
+      is_subtype(tup_atom_int, union1)
+    )
 
     # {atom, any} | {any, int} -> a complex type, let's check subtyping against it
     union2 = sum(tup_atom_any, tup_any_int)
     # {atom, int} is in both parts of the union.
     test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
     # {:foo, :bar} is only in {atom, any}.
-    test_fn.("{:foo, :bar} <: ({atom,any} | {any,int})", true, is_subtype(type_tuple([t_foo, t_bar]), union2))
+    test_fn.(
+      "{:foo, :bar} <: ({atom,any} | {any,int})",
+      true,
+      is_subtype(type_tuple([t_foo, t_bar]), union2)
+    )
+
     # {5, 6} is only in {any, int}.
-    test_fn.("{5, 6} <: ({atom,any} | {any,int})", true, is_subtype(type_tuple([t_int_5, t_int_6]), union2))
+    test_fn.(
+      "{5, 6} <: ({atom,any} | {any,int})",
+      true,
+      is_subtype(type_tuple([t_int_5, t_int_6]), union2)
+    )
+
     # {5, :foo} is in neither part of the union.
-    test_fn.("{5, :foo} <: ({atom,any} | {any,int})", false, is_subtype(type_tuple([t_int_5, t_foo]), union2))
+    test_fn.(
+      "{5, :foo} <: ({atom,any} | {any,int})",
+      false,
+      is_subtype(type_tuple([t_int_5, t_foo]), union2)
+    )
 
     IO.puts("\n--- Section: Negation and Type Difference ---")
     # atom is disjoint from tuple, so atom <: ¬tuple
     test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))
+
     # A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
     test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
     # {int, atom} is a subtype of ¬{atom, int} because their elements differ
@@ -1521,10 +1660,16 @@ defmodule TupleTests do
 
     # Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
     diff1 = intersect(tup_s2_any, negate(tup_atom_any))
+
     # {integer, integer} has a first element that is not an atom, so it should be in the difference.
     tup_int_int = type_tuple([t_int, t_int])
     test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
-    test_fn.("{atom, int} <: (tuple_size_2 - {atom, any})", false, is_subtype(tup_atom_int, diff1))
+
+    test_fn.(
+      "{atom, int} <: (tuple_size_2 - {atom, any})",
+      false,
+      is_subtype(tup_atom_int, diff1)
+    )
 
     IO.puts("\n--- Section: Nested Tuples ---")
     test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
@@ -1535,8 +1680,18 @@ defmodule TupleTests do
     # Union of nested types
     union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
     test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))
-    test_fn.("{{:bar}} <: ({{:foo}} | {{:bar}})", true, is_subtype(type_tuple([type_tuple([t_bar])]), union_nested))
+
-    test_fn.("{{atom}} <: ({{:foo}} | {{:bar}})", false, is_subtype(tup_nested_atom, union_nested))
+    test_fn.(
+      "{{:bar}} <: ({{:foo}} | {{:bar}})",
+      true,
+      is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
+    )
+
+    test_fn.(
+      "{{atom}} <: ({{:foo}} | {{:bar}})",
+      false,
+      is_subtype(tup_nested_atom, union_nested)
+    )
 
     IO.puts("\n--- Section: Edge Cases (any, none) ---")
     # A type `{any, none}` should not be possible. The value `none` cannot exist.
@@ -1553,6 +1708,7 @@ defmodule TupleTests do
 
     # --- Original tests from problem description for regression ---
     IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")
+
     test_fn.(
       "{1, :foo} <: {int_gt_0, :foo | :bar}",
       true,
@@ -1561,6 +1717,7 @@ defmodule TupleTests do
         type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
       )
     )
+
     test_fn.(
       "{0, :foo} <: {int_gt_0, :foo | :bar}",
       false,
@@ -1569,6 +1726,7 @@ defmodule TupleTests do
         type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
       )
     )
+
     test_fn.(
       "{1, :kek} <: {int_gt_0, :foo | :bar}",
       false,
@@ -1585,6 +1743,178 @@ defmodule TupleTests do
   end
 end
 
+defmodule ListTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running ListTests ---")
+
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_foo = type_atom_literal(:foo)
+    t_bar = type_atom_literal(:bar)
+    t_any = type_any()
+    t_none = type_none()
+
+    # --- List Types ---
+    t_list = type_list()
+    t_empty_list = type_empty_list()
+    # [atom | list]
+    t_cons_atom_list = type_cons(t_atom, t_list)
+    # [:foo | []]
+    t_cons_foo_empty = type_cons(t_foo, t_empty_list)
+    # [atom | []]
+    t_cons_atom_empty = type_cons(t_atom, t_empty_list)
+    # [any | []]
+    t_cons_any_empty = type_cons(t_any, t_empty_list)
+    # [integer | list]
+    t_cons_int_list = type_cons(t_int, t_list)
+
+    IO.puts("\n--- Section: Basic List Subtyping ---")
+    test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
+    test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
+    test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
+    test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
+    test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
+    test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
+    test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
+    test_fn.("atom <: list", false, is_subtype(t_atom, t_list))
+
+    IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
+    # Head is a subtype
+    test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
+    test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
+    # Tail is a subtype
+    test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
+    test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
+    # Both are subtypes
+    test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
+    # Neither is a subtype
+    test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
+    # A list of length 1 is a subtype of a list of any element of length 1
+    test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))
+
+    IO.puts("\n--- Section: List Intersection ---")
+    # [atom|list] & [integer|list] -> should be none due to head conflict
+    intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
+    test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)
+
+    # [any|[]] & [atom|list] -> should be [atom|[]]
+    intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
+    test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)
+
+    # [] & [atom|list] -> should be none because one is empty and one is not
+    intersect3 = intersect(t_empty_list, t_cons_atom_list)
+    test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)
+
+    IO.puts("\n--- Section: List Union ---")
+    # [] | [atom|[]]
+    union1 = sum(t_empty_list, t_cons_atom_empty)
+    test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
+    test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))
+
+    test_fn.(
+      "[integer|[]] <: ([] | [atom|[]])",
+      false,
+      is_subtype(type_cons(t_int, t_empty_list), union1)
+    )
+
+    # [:foo|[]] | [:bar|[]]
+    union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
+    # This union is a subtype of [atom|[]]
+    test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
+    test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))
+
+    IO.puts("\n--- Section: List Negation ---")
+    # list is a subtype of not(atom)
+    test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
+    # A non-empty list is a subtype of not an empty list
+    test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
+    # [integer|list] is a subtype of not [atom|list]
+    test_fn.(
+      "[integer|list] <: ¬[atom|list]",
+      true,
+      is_subtype(t_cons_int_list, negate(t_cons_atom_list))
+    )
+
+    IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
+  end
+end
+defmodule ListOfTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running ListOfTests ---")
+
+    # --- Basic Types ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_pos_int = type_int_gt(0)
+    t_int_5 = type_int_eq(5)
+
+    # --- list(X) Types ---
+    t_list_of_int = type_list_of(t_int)
+    t_list_of_pos_int = type_list_of(t_pos_int)
+    t_list_of_atom = type_list_of(t_atom)
+
+    # --- Specific List Types ---
+    t_list = type_list()
+    t_empty_list = type_empty_list()
+    t_list_one_int = type_cons(t_int_5, t_empty_list) # [5]
+    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list) # [:foo]
+    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list)) # [5, :foo]
+
+    IO.puts("\n--- Section: Basic list(X) Subtyping ---")
+    test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
+    test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
+    test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
+    test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
+    test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
+    test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))
+    test_fn.("[5, :foo] <: list(any)", true, is_subtype(t_list_int_and_atom, type_list_of(type_any())))
+
+    IO.puts("\n--- Section: Covariance of list(X) ---")
+    test_fn.("list(pos_integer) <: list(integer)", true, is_subtype(t_list_of_pos_int, t_list_of_int))
+    test_fn.("list(integer) <: list(pos_integer)", false, is_subtype(t_list_of_int, t_list_of_pos_int))
+
+    IO.puts("\n--- Section: Intersection of list(X) ---")
+    # list(integer) & list(pos_integer) should be list(pos_integer)
+    intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
+    test_fn.("(list(int) & list(pos_int)) == list(pos_int)", true, intersect1 == t_list_of_pos_int)
+
+    # list(integer) & list(atom) should be just [] (empty list is the only common member)
+    # The system simplifies this intersection to a type that only accepts the empty list.
+    intersect2 = intersect(t_list_of_int, t_list_of_atom)
+    test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
+    test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
+    test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
+    # It should be equivalent to `type_empty_list`
+    test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)
+
+
+    IO.puts("\n--- Section: Intersection of list(X) with cons ---")
+    # list(integer) & [:foo | []] -> should be none
+    intersect3 = intersect(t_list_of_int, t_list_one_atom)
+    test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())
+
+    # list(integer) & [5 | []] -> should be [5 | []]
+    intersect4 = intersect(t_list_of_int, t_list_one_int)
+    test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)
+    
+    # list(integer) & [5, :foo] -> should be none
+    intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
+    test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())
+
+    IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
+  end
+end
 test_all.()
 IntegerTests.run(test)
 TupleTests.run(test)
+ListTests.run(test)
+ListOfTests.run(test)