checkpoint

.aider.chat.history.md

@@ -57232,3 +57232,209 @@ This approach leverages the excellent foundation you've already built in the `ti
 > Model: openrouter/google/gemini-2.5-pro-preview with context edit format  
 > Git repo: .git with 62 files  
 > Repo-map: using 8192 tokens, always refresh  
+>  
+>  
+> ^C again to exit  
+> Unable to list files in git repo: BadObject: b'df8d705509adca9e964524519a1755d8a584e262'  
+> Is your git repo corrupted?  
+>  
+>  
+> ^C KeyboardInterrupt  
+
+# aider chat started at 2025-06-16 11:51:46
+
+> You can skip this check with --no-gitignore  
+> Add .aider* to .gitignore (recommended)? (Y)es/(N)o [Yes]: n  
+> /Users/kacper.marzecki@schibsted.com/.local/bin/aider --model gemini --watch-files --read Conventions.md --thinking-tokens 10k --reasoning-effort high  
+> Warning: gemini/gemini-2.5-pro-preview-05-06 does not support 'reasoning_effort', ignoring.  
+> Use --no-check-model-accepts-settings to force the 'reasoning_effort' setting.  
+> Warning: gemini/gemini-2.5-pro-preview-05-06 does not support 'thinking_tokens', ignoring.  
+> Use --no-check-model-accepts-settings to force the 'thinking_tokens' setting.  
+> Aider v0.84.0  
+> Main model: gemini/gemini-2.5-pro-preview-05-06 with diff-fenced edit format  
+> Weak model: gemini/gemini-2.5-flash-preview-04-17  
+> Git repo: .git with 65 files  
+> Repo-map: using 4096 tokens, auto refresh  
+> Added Conventions.md to the chat (read-only).  
+> Added test.exs to the chat  
+> Processing your request...  
+
+Okay, I will add the test case as requested. This involves defining a couple of helper functions to construct TDDs for tuples with specific element types, as this functionality doesn't appear to be available as a built-in constructor. These helpers will use existing TDD primitives.
+
+Here's the plan:
+1.  Define two helper functions:
+    *   `build_tuple_element_tdd_h(element_index, element_type_id, success_path_id)`: Recursively builds the TDD part for a single element by adapting the element's type TDD variables to be specific to that element's index.
+    *   `create_specific_tuple_type_h(element_type_ids)`: Uses `build_tuple_element_tdd_h` to construct the full TDD for a tuple with a list of specified element types.
+2.  Use these helpers to create the TDDs for `{1, :foo}` and `{int_gt_0, :foo | :bar}`.
+3.  Add the subtyping test using the existing `test` function.
+4.  This new code will replace the `#AI! ...` comment at the end of the file.
+
+Here are the *SEARCH/REPLACE* blocks:
+
+```elixir
+test.exs
+<<<<<<< SEARCH
+|> Tdd.print_tdd(asd)
+
+
+#AI! lets add a test case for {1, :foo} <: {int_gt_0, :foo | :bar}
+=======
+|> Tdd.print_tdd(asd)
+
+# Helper function to recursively build TDD for an element's type,
+# adapting its variables to be specific to the element's index.
+defmodule TupleTestHelpers do
+  def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module)
+      when element_type_id == Tdd.type_any() do
+    # If element type is 'any', this part of the check passes, go to success_path_id
+    success_path_id
+  end
+
+  def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module)
+      when element_type_id == Tdd.type_none() do
+    # If element type is 'none', this path fails
+    Tdd.type_none()
+  end
+
+  def build_tuple_element_tdd_h(element_index, element_type_id, success_path_id, variable_prefix_module) do
+    node_details = Tdd.get_node_details(element_type_id)
+
+    case node_details do
+      :true_terminal ->
+        # Should be caught by guard Tdd.type_any(), but handle defensively
+        success_path_id
+
+      :false_terminal ->
+        # Should be caught by guard Tdd.type_none(), but handle defensively
+        Tdd.type_none()
+
+      {original_var, y_id, n_id, d_id} ->
+        # Adapt original_var to be specific to this element_index
+        # The Tdd.v_tuple_elem_pred function creates the correctly prefixed variable
+        element_specific_var = variable_prefix_module.v_tuple_elem_pred(element_index, original_var)
+
+        yes_branch_tdd =
+          build_tuple_element_tdd_h(element_index, y_id, success_path_id, variable_prefix_module)
+
+        no_branch_tdd =
+          build_tuple_element_tdd_h(element_index, n_id, success_path_id, variable_prefix_module)
+
+        dc_branch_tdd =
+          build_tuple_element_tdd_h(element_index, d_id, success_path_id, variable_prefix_module)
+
+        Tdd.make_node_raw(element_specific_var, yes_branch_tdd, no_branch_tdd, dc_branch_tdd)
+    end
+  end
+
+  # Helper function to create a TDD for a tuple with specific element types
+  def create_specific_tuple_type_h(element_type_ids, variable_prefix_module \\ Tdd) 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 ->
+        element_type_id = Enum.at(element_type_ids, i)
+        build_tuple_element_tdd_h(i, element_type_id, acc_tdd, variable_prefix_module)
+      end)
+
+    # Wrap with size check
+    size_check_node =
+      Tdd.make_node_raw(
+        variable_prefix_module.v_tuple_size_eq(num_elements),
+        final_elements_check_tdd, # If size matches, proceed to element checks
+        Tdd.type_none(),          # If size mismatches, it's not this tuple type
+        Tdd.type_none()           # DC for size usually means not this specific tuple type
+      )
+
+    # Wrap with primary tuple type check
+    raw_final_tdd =
+      Tdd.make_node_raw(
+        variable_prefix_module.@v_is_tuple,
+        size_check_node, # If is_tuple, proceed to size check
+        Tdd.type_none(), # If not a tuple, then false
+        Tdd.type_none()  # DC for is_tuple usually means not this specific type
+      )
+
+    # Simplify the constructed TDD
+    Tdd.simplify_with_constraints(raw_final_tdd, %{})
+  end
+end
+
+IO.puts("\n--- Specific Tuple Subtyping Test ---")
+
+# Type for {1, :foo}
+el1_type1 = Tdd.type_int_eq(1)
+el2_type1 = Tdd.type_atom_literal(:foo)
+tdd_tuple_1_foo = TupleTestHelpers.create_specific_tuple_type_h([el1_type1, el2_type1])
+
+# Type for {int_gt_0, :foo | :bar}
+el1_type2 = Tdd.type_int_gt(0)
+el2_type2_foo = Tdd.type_atom_literal(:foo)
+el2_type2_bar = Tdd.type_atom_literal(:bar)
+el2_type2 = Tdd.sum(el2_type2_foo, el2_type2_bar)
+tdd_tuple_int_gt0_foo_or_bar = TupleTestHelpers.create_specific_tuple_type_h([el1_type2, el2_type2])
+
+# IO.puts("TDD for {1, :foo}:")
+# Tdd.print_tdd(tdd_tuple_1_foo)
+# IO.puts("TDD for {int_gt_0, :foo | :bar}:")
+# Tdd.print_tdd(tdd_tuple_int_gt0_foo_or_bar)
+
+test.(
+  "{1, :foo} <: {int_gt_0, :foo | :bar}",
+  true,
+  Tdd.is_subtype(tdd_tuple_1_foo, tdd_tuple_int_gt0_foo_or_bar)
+)
+
+IO.inspect(Process.get(:test_failures, []), label: "Current test failures after tuple test")
+>>>>>>> REPLACE
+```
+
+> Tokens: 23k sent, 1.4k received. Cost: $0.04 message, $0.04 session.  
+> Applied edit to test.exs  
+> Processing your request...  
+
+Okay, I understand. The issue is that Elixir guards have restrictions on what functions can be called within them. Calls to `Tdd.type_any()` and `Tdd.type_none()` are considered "remote" calls in this context, even if they return simple values.
+
+To fix this, I will replace the calls to `Tdd.type_any()` and `Tdd.type_none()` in the guard clauses with their literal return values.
+- `Tdd.type_any()` returns `@true_node_id` which is `1`.
+- `Tdd.type_none()` returns `@false_node_id` which is `0`.
+
+I will make these changes and remove the "AI!" comment.
+
+Here is the *SEARCH/REPLACE block*:
+
+```elixir
+test.exs
+<<<<<<< SEARCH
+defmodule TupleTestHelpers do
+  def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module)
+    # AI! You cannot use remote functions inside function guards 
+      when element_type_id == Tdd.type_any() do
+    # If element type is 'any', this part of the check passes, go to success_path_id
+    success_path_id
+  end
+
+  def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module)
+      when element_type_id == Tdd.type_none() do
+    # If element type is 'none', this path fails
+    Tdd.type_none()
+  end
+=======
+defmodule TupleTestHelpers do
+  def build_tuple_element_tdd_h(_element_index, element_type_id, success_path_id, _variable_prefix_module)
+      when element_type_id == 1 do # Was Tdd.type_any()
+    # If element type is 'any', this part of the check passes, go to success_path_id
+    success_path_id
+  end
+
+  def build_tuple_element_tdd_h(_element_index, element_type_id, _success_path_id, _variable_prefix_module)
+      when element_type_id == 0 do # Was Tdd.type_none()
+    # If element type is 'none', this path fails
+    Tdd.type_none()
+  end
+>>>>>>> REPLACE
+```
+
+> Tokens: 25k sent, 457 received. Cost: $0.04 message, $0.08 session.  
+> Applied edit to test.exs  

.aider.input.history

@@ -4182,3 +4182,6 @@
 
 # 2025-06-15 11:56:09.668461
 +/context
+
+# 2025-06-16 11:51:48.065221
++n

test.exs

@@ -130,9 +130,10 @@ defmodule Tdd do
 
   *   **Variables**:
     *   `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties).
-    *   `v_int_eq_N = {INT_CAT, :eq, N}`.
-    *   `v_int_lt_N = {INT_CAT, :lt, N}` (value < N).
-    *   `v_int_gt_N = {INT_CAT, :gt, N}` (value > N).
+    * INT_CAT variables (names of variables prefixed with `a b c` to force ordering 
+      *   `v_int_lt_N = {INT_CAT, :alt, N}` (value < N).
+      *   `v_int_eq_N = {INT_CAT, :beq, N}`.
+      *   `v_int_gt_N = {INT_CAT, :cgt, N}` (value > N).
       *   *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).*
   *   **Constructors**:
     *   `type_integer()`: Any integer.
@@ -147,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_tail_VAR = {LIST_CAT, :tail, NESTED_PREDICATE_ID_FOR_TAIL_LIST}`: 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).*
+        *   `v_list_head_pred = {5, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head.
+        *   `v_list_tail_pred = {5, :tail, NESTED_PREDICATE_ID_FOR_TAIL}`: Applies a global predicate (usually list predicates) to the tail.
   *   **Constructors**:
-    *   `type_list_any()`.
-    *   `type_empty_list()`.
-    *   `type_cons(head_type_id, tail_type_id)`.
-    *   `type_list_of(element_type_id)`: e.g., `list(integer())`.
+    *   `type_list()`: Represents any list.
+    *   `type_empty_list()`: Represents the empty list `[]`.
+    *   `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`.
   *   **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)
 
@@ -330,7 +330,103 @@ 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.
+    partitioned_assumptions =
+      Enum.group_by(assumptions_map, fn
+        # 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. Check the assumptions for the top-level entity.
+    top_level_assumptions = Map.get(partitioned_assumptions, :top_level, []) |> Map.new()
+
+    case do_check_flat_consistency(top_level_assumptions) do
+      :contradiction ->
+        :contradiction
+
+      :consistent ->
+        # 4. If top-level is consistent, gather new ambient constraints and check sub-problems.
+        all_elems_constraints =
+          Enum.reduce(top_level_assumptions, [], fn
+            {{5, :all_elements, type_id}, true}, acc -> [type_id | acc]
+            _, acc -> acc
+          end)
+
+        sub_problems = Map.drop(partitioned_assumptions, [:top_level])
+
+        Enum.reduce_while(sub_problems, :consistent, fn
+          # For a tuple element (no ambient constraints from parent needed for now)
+          {{:elem, _index}, assumptions_list}, _acc ->
+            sub_assumptions =
+              assumptions_list
+              |> Map.new(fn {{_, :element, _, nested_var}, value} -> {nested_var, value} end)
+
+            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
+
+  # The original check_assumptions_consistency function is renamed to this.
+  # It performs the actual logic for a "flat" set of assumptions about a single entity.
+  defp do_check_flat_consistency(assumptions_map) do
     # Check 1: Primary type mutual exclusivity
     primary_true_predicates =
       Enum.reduce(assumptions_map, MapSet.new(), fn
@@ -338,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
-          has_true_atom_specific_pred && is_explicitly_not_atom_or_different_primary ->
+    if has_true_atom_specific_pred && is_explicitly_not_atom do
       :contradiction
-
-          true ->
+    else
       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
-              :contradiction
-            else
-              # --- Tuple-specific checks ---
+      if MapSet.size(atom_value_trues) > 1, do: :contradiction, else: false
+    end
+  end
+
+  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
-                has_true_tuple_specific_pred && is_explicitly_not_tuple_or_different_primary ->
+    if has_true_tuple_specific_pred && is_explicitly_not_tuple do
       :contradiction
-
-                true ->
+    else
       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
-                    :contradiction
-                  else
-                    # --- Integer predicate checks (REVISED LOGIC) ---
+      if MapSet.size(tuple_size_trues) > 1, do: :contradiction, else: false
+    end
+  end
+
+  # (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
@@ -420,7 +526,7 @@ defmodule Tdd do
             assumptions_map,
             initial_bounds_from_true_false,
             fn
-                              {{2, :eq, n}, true}, acc ->
+              {{2, :beq, n}, true}, acc ->
                 cond do
                   acc.eq_val == :conflict -> acc
                   is_nil(acc.eq_val) -> %{acc | eq_val: n}
@@ -429,30 +535,30 @@ defmodule Tdd do
                 end
 
               # value < n  => value <= n-1
-                              {{2, :lt, n}, true}, acc ->
+              {{2, :alt, n}, true}, acc ->
                 new_max_b =
                   if is_nil(acc.max_b), do: n - 1, else: min(acc.max_b, n - 1)
 
                 %{acc | max_b: new_max_b}
 
               # value > n  => value >= n+1
-                              {{2, :gt, n}, true}, acc ->
+              {{2, :cgt, n}, true}, acc ->
                 new_min_b =
                   if is_nil(acc.min_b), do: n + 1, else: max(acc.min_b, n + 1)
 
                 %{acc | min_b: new_min_b}
 
               # value >= n
-                              {{2, :lt, n}, false}, acc ->
+              {{2, :alt, n}, false}, acc ->
                 new_min_b = if is_nil(acc.min_b), do: n, else: max(acc.min_b, n)
                 %{acc | min_b: new_min_b}
 
               # value <= n
-                              {{2, :gt, n}, false}, acc ->
+              {{2, :cgt, n}, false}, acc ->
                 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
@@ -463,24 +569,24 @@ 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 =
                     case pred_type do
-                                    :eq ->
+                      :beq ->
                         is_integer(current_interval_min) &&
                           current_interval_min == n_val &&
                           (is_integer(current_interval_max) &&
                              current_interval_max == n_val)
 
-                                    :lt ->
-                                      is_integer(current_interval_max) &&
-                                        current_interval_max < n_val
+                      :alt ->
+                        is_integer(current_interval_max) && current_interval_max < n_val
 
-                                    :gt ->
-                                      is_integer(current_interval_min) &&
-                                        current_interval_min > n_val
+                      :cgt ->
+                        is_integer(current_interval_min) && current_interval_min > n_val
 
                       _ ->
                         false
@@ -488,62 +594,71 @@ defmodule Tdd do
 
                   is_implied_false =
                     case pred_type do
-                                    :eq ->
-                                      (is_integer(current_interval_min) &&
-                                         current_interval_min > n_val) ||
-                                        (is_integer(current_interval_max) &&
-                                           current_interval_max < n_val)
+                      :beq ->
+                        (is_integer(current_interval_min) && current_interval_min > n_val) ||
+                          (is_integer(current_interval_max) && current_interval_max < n_val)
 
-                                    :lt ->
-                                      is_integer(current_interval_min) &&
-                                        current_interval_min >= n_val
+                      :alt ->
+                        is_integer(current_interval_min) && current_interval_min >= n_val
 
-                                    :gt ->
-                                      is_integer(current_interval_max) &&
-                                        current_interval_max <= n_val
+                      :cgt ->
+                        is_integer(current_interval_max) && current_interval_max <= n_val
 
                       _ ->
                         false
                     end
 
                   if is_implied_true || is_implied_false do
-                                  # IO.inspect({assumptions_map, pred_type, n_val, current_interval_min, current_interval_max, implied_true, implied_false}, label: "CAC Int DC Contradiction")
-                                  # :dc assumption contradicted by derived interval
                     {:halt, :contradiction}
                   else
                     {:cont, :consistent}
                   end
 
                 _other_assumption, acc_status ->
-                                # Continue with current status
                   {:cont, acc_status}
               end)
 
-                            # End reduce_while for :dc checks
+            # Return :contradiction if found, otherwise `false` to allow the `||` chain to continue.
+            if res == :contradiction, do: :contradiction, else: false
         end
 
-                      # End case for calculate_final_interval
-                      # No integer specific preds or not relevant to check integer logic
       true ->
-                        :consistent
+        false
+    end
   end
 
-                    # End cond for integer checks
-                  end
+  ### 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)
 
-                  # End else for tuple_size_trues
-              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))
 
-              # End true for tuple_specific_pred
-            end
+    # 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)
 
-            # End cond for tuple_specific_pred
-        end
+    cond do
+      # Contradiction: list-specific rule is assumed, but type is not a list.
+      has_list_specific_pred && is_explicitly_not_list ->
+        :contradiction
 
-        # End else for atom_value_trues
-      end
+      # 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
 
-    raw_result
+      # 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
@@ -557,7 +672,7 @@ defmodule Tdd do
   defp max_opt(x, y), do: max(x, y)
 
   # --- Semantic Simplification (Memoized) ---
-  defp simplify_with_constraints(tdd_id, assumptions_map) do
+  def simplify_with_constraints(tdd_id, assumptions_map) do
     state = get_state()
     # Sort assumptions for cache key consistency
     sorted_assumptions_list = Enum.sort(Map.to_list(assumptions_map))
@@ -681,19 +796,31 @@ defmodule Tdd do
 
   @v_is_atom {0, :is_atom}
   @v_is_tuple {0, :is_tuple}
-  # New primary type
   @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)
-  def v_int_eq(n) when is_integer(n), do: {2, :eq, n}
   # strictly less than n
-  def v_int_lt(n) when is_integer(n), do: {2, :lt, n}
+  def v_int_lt(n) when is_integer(n), do: {2, :alt, n}
+  def v_int_eq(n) when is_integer(n), do: {2, :beq, n}
   # strictly greater than n
-  def v_int_gt(n) when is_integer(n), do: {2, :gt, n}
+  def v_int_gt(n) when is_integer(n), do: {2, :cgt, n}
 
   def type_any, do: @true_node_id
   def type_none, do: @false_node_id
@@ -731,6 +858,104 @@ defmodule Tdd do
     make_node_for_constructors(@v_is_integer, @true_node_id, @false_node_id, @false_node_id)
   end
 
+  # A recursive helper that maps a TDD onto a component (e.g., list head, tuple element).
+  # 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 get_node_details(tdd_id) do
+      :true_terminal ->
+        success_id
+
+      :false_terminal ->
+        @false_node_id
+
+      {var, y, n, d} ->
+        # Wrap the original variable to be specific to this component.
+        component_var = wrapper_fun.(var)
+        # Recurse on children, passing the success_id down.
+        res_y = map_tdd_to_component(y, wrapper_fun, success_id)
+        res_n = map_tdd_to_component(n, wrapper_fun, success_id)
+        res_d = map_tdd_to_component(d, wrapper_fun, success_id)
+        make_node_raw(component_var, res_y, res_n, res_d)
+    end
+  end
+
+  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)
+
+    final_elements_check_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)
+
+    size_check_node =
+      make_node(v_tuple_size_eq(num_elements), final_elements_check_tdd, type_none(), type_none())
+
+    raw_final_tdd = make_node(v_is_tuple(), size_check_node, type_none(), type_none())
+    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)
@@ -1316,10 +1541,420 @@ defmodule IntegerTests do
   end
 end
 
+defmodule TupleTests do
+  import Tdd
+
+  def run(test_fn) do
+    Process.put(:test_failures, [])
+    # Re-init the system for a clean slate for these tests
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running TupleTests ---")
+
+    # --- Basic Types for convenience ---
+    t_atom = type_atom()
+    t_int = type_integer()
+    t_foo = type_atom_literal(:foo)
+    t_bar = type_atom_literal(:bar)
+    t_int_5 = type_int_eq(5)
+    t_int_6 = type_int_eq(6)
+    t_int_pos = type_int_gt(0)
+    t_any = type_any()
+    t_none = type_none()
+    # any tuple
+    t_tuple = type_tuple()
+    t_empty_tuple = type_empty_tuple()
+
+    # --- Specific Tuple Types ---
+    # {atom(), integer()}
+    tup_atom_int = type_tuple([t_atom, t_int])
+    # {:foo, 5}
+    tup_foo_5 = type_tuple([t_foo, t_int_5])
+    # {pos_integer(), atom()}
+    tup_pos_atom = type_tuple([t_int_pos, t_atom])
+    # {atom(), any}
+    tup_atom_any = type_tuple([t_atom, t_any])
+    # {any, integer()}
+    tup_any_int = type_tuple([t_any, t_int])
+    # a tuple of size 2, {any, any}
+    tup_s2_any = type_tuple_sized_any(2)
+    # a tuple of size 3, {any, any, any}
+    tup_s3_any = type_tuple_sized_any(3)
+    # {integer(), atom()}
+    tup_int_atom = type_tuple([t_int, t_atom])
+    # {{:foo}}
+    tup_nested_foo = type_tuple([type_tuple([t_foo])])
+    # {{atom()}}
+    tup_nested_atom = type_tuple([type_tuple([t_atom])])
+    # {any, none} -> this should resolve to none
+    tup_with_none = type_tuple([t_any, t_none])
+
+    IO.puts("\n--- Section: Basic Subtyping ---")
+    test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
+    test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
+    test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
+    test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
+    test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
+    test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))
+
+    IO.puts("\n--- Section: Size-related Subtyping ---")
+    test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
+    test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
+    test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
+    test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
+    test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
+    test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))
+
+    IO.puts("\n--- Section: Intersection ---")
+    # {atom, any} & {any, int} -> {atom, int}
+    intersect1 = intersect(tup_atom_any, tup_any_int)
+    test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)
+
+    # {atom, int} & {int, atom} -> none
+    intersect2 = intersect(tup_atom_int, tup_int_atom)
+    test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)
+
+    # tuple_size_2 & tuple_size_3 -> none
+    intersect3 = intersect(tup_s2_any, tup_s3_any)
+    test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)
+
+    # tuple() & {atom, int} -> {atom, int}
+    intersect4 = intersect(t_tuple, tup_atom_int)
+    test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)
+
+    IO.puts("\n--- Section: Union ---")
+    # {: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)
+    )
+
+    # {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)
+    )
+
+    # {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)
+    )
+
+    # {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)
+    )
+
+    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
+    test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
+    # tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
+    test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))
+
+    # 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)
+    )
+
+    IO.puts("\n--- Section: Nested Tuples ---")
+    test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
+    test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
+    # Intersection of disjoint nested types: {{:foo}} & {{:bar}}
+    intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
+    test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
+    # 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)
+    )
+
+    IO.puts("\n--- Section: Edge Cases (any, none) ---")
+    # A type `{any, none}` should not be possible. The value `none` cannot exist.
+    # The simplification logic should reduce this to `type_none`.
+    test_fn.("{any, none} == none", true, tup_with_none == t_none)
+
+    # Intersection with a tuple containing none should result in none
+    intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
+    test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)
+
+    # Union with a tuple containing none should be a no-op
+    union_with_none_tuple = sum(tup_atom_int, tup_with_none)
+    test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)
+
+    # --- 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,
+      is_subtype(
+        type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
+        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,
+      is_subtype(
+        type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
+        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,
+      is_subtype(
+        type_tuple([
+          type_int_eq(1),
+          type_atom_literal(:kek)
+        ]),
+        type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
+      )
+    )
+
+    IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
+  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()
+    # [5]
+    t_list_one_int = type_cons(t_int_5, t_empty_list)
+    # [:foo]
+    t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
+    # [5, :foo]
+    t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
+
+    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)
-
-# tdd_int_gt_10 = Tdd.type_int_gt(10)
-# tdd_int_gt_3 = Tdd.type_int_gt(3)
-# test.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
-
+TupleTests.run(test)
+ListTests.run(test)
+ListOfTests.run(test)