checkpoint tuples

.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

@@ -332,6 +332,51 @@ defmodule Tdd do
   end
 
   defp check_assumptions_consistency(assumptions_map) do
+    # 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}}
+        {{4, :element, index, _nested_var}, _value} -> {:elem, index}
+        # All other variables
+        _ -> :top_level
+      end)
+
+    # 2. Extract and 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 ->
+        # 3. If top-level is consistent, check each tuple element's assumptions.
+        element_partitions = Map.drop(partitioned_assumptions, [:top_level])
+
+        Enum.reduce_while(element_partitions, :consistent, fn
+          # The key is {:elem, index}, the value is a list of {var, val} tuples
+          {{: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)
+
+            # 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
+        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
@@ -508,40 +553,23 @@ defmodule Tdd do
                                   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
                         end
 
-                      # End case for calculate_final_interval
-                      # No integer specific preds or not relevant to check integer logic
                       true ->
                         :consistent
                     end
-
-                    # End cond for integer checks
                   end
-
-                  # End else for tuple_size_trues
               end
-
-              # End true for tuple_specific_pred
             end
-
-            # End cond for tuple_specific_pred
         end
-
-        # End else for atom_value_trues
       end
 
     raw_result
@@ -558,7 +586,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))
@@ -682,9 +710,12 @@ defmodule Tdd do
 
   @v_is_atom {0, :is_atom}
   @v_is_tuple {0, :is_tuple}
-  # New primary type
   @v_is_integer {0, :is_integer}
 
+  def v_is_atom, do: @v_is_atom
+  def v_is_tuple, do: @v_is_tuple
+  def v_is_integer, do: @v_is_integer
+
   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}
@@ -732,6 +763,70 @@ 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
+    node_details = 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
+        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 = v_tuple_elem_pred(element_index, original_var)
+
+        yes_branch_tdd = type_tuple_elem(element_index, y_id, success_path_id)
+        no_branch_tdd = type_tuple_elem(element_index, n_id, success_path_id)
+        dc_branch_tdd = type_tuple_elem(element_index, d_id, success_path_id)
+        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(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 ->
+        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(
+        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(),
+        # 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
+
   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)
@@ -1313,18 +1408,183 @@ defmodule IntegerTests do
       Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
     )
 
-     Tdd.print_tdd(union_disjoint_ranges)
     IO.inspect(Process.get(:test_failures, []))
   end
 end
 
-# test_all.()
+defmodule TupleTests do
-# IntegerTests.run(test)
+  import Tdd
 
-tdd_int_gt_10 = Tdd.type_int_gt(10)
+  def run(test_fn) do
-tdd_int_gt_3 = Tdd.type_int_gt(3)
+    Process.put(:test_failures, [])
+    # Re-init the system for a clean slate for these tests
+    Tdd.init_tdd_system()
+    IO.puts("\n--- Running TupleTests ---")
 
-tdd_int = Tdd.type_integer()
+    # --- Basic Types for convenience ---
-Tdd.intersect(Tdd.sum(tdd_int_gt_10, tdd_int_gt_3), tdd_int)
+    t_atom = type_atom()
-|> Tdd.print_tdd(asd)
+    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()
+    t_tuple = type_tuple() # any 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
+
+test_all.()
+IntegerTests.run(test)
+TupleTests.run(test)