From b7498d93ba6ce0455fd112735725a228079b10b2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Wed, 18 Jun 2025 07:20:11 -0700
Subject: [PATCH 01/10] Add fun from inferred clauses

---
 lib/elixir/lib/module/types/apply.ex          |  4 +-
 lib/elixir/lib/module/types/descr.ex          | 18 ++---
 lib/elixir/lib/module/types/expr.ex           |  2 +-
 .../test/elixir/module/types/descr_test.exs   | 68 ++++++++++++-------
 .../test/elixir/module/types/expr_test.exs    | 31 ++++++---
 .../elixir/module/types/integration_test.exs  |  4 +-
 6 files changed, 80 insertions(+), 47 deletions(-)

diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index b03889546d..2b3be0bd3b 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -487,7 +487,7 @@ defmodule Module.Types.Apply do
                 {union(type, fun_from_non_overlapping_clauses(clauses)), fallback?, context}
 
               {{:infer, _, clauses}, context} when length(clauses) <= @max_clauses ->
-                {union(type, fun_from_overlapping_clauses(clauses)), fallback?, context}
+                {union(type, fun_from_inferred_clauses(clauses)), fallback?, context}
 
               {_, context} ->
                 {type, true, context}
@@ -705,7 +705,7 @@ defmodule Module.Types.Apply do
         result =
           case info do
             {:infer, _, clauses} when length(clauses) <= @max_clauses ->
-              fun_from_overlapping_clauses(clauses)
+              fun_from_inferred_clauses(clauses)
 
             _ ->
               dynamic(fun(arity))
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index be375e4d83..44a7a41e12 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -137,18 +137,20 @@ defmodule Module.Types.Descr do
   @doc """
   Creates a function from overlapping function clauses.
   """
-  def fun_from_overlapping_clauses(args_clauses) do
+  def fun_from_inferred_clauses(args_clauses) do
     domain_clauses =
       Enum.reduce(args_clauses, [], fn {args, return}, acc ->
-        pivot_overlapping_clause(args_to_domain(args), return, acc)
+        domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
+        pivot_overlapping_clause(domain, upper_bound(return), acc)
       end)
 
     funs =
       for {domain, return} <- domain_clauses,
           args <- domain_to_args(domain),
-          do: fun(args, return)
+          do: fun(args, dynamic(return))
 
     Enum.reduce(funs, &intersection/2)
+    # dynamic(fun())
   end
 
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
@@ -200,10 +202,10 @@ defmodule Module.Types.Descr do
   def domain_to_args(descr) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        tuple_elim_negations_static(descr, &Function.identity/1)
+        tuple_elim_negations_static(descr, & &1)
 
       {dynamic, static} ->
-        tuple_elim_negations_static(static, &Function.identity/1) ++
+        tuple_elim_negations_static(static, & &1) ++
           tuple_elim_negations_static(dynamic, fn elems -> Enum.map(elems, &dynamic/1) end)
     end
   end
@@ -2115,9 +2117,6 @@ defmodule Module.Types.Descr do
 
   defp dynamic_to_quoted(descr, opts) do
     cond do
-      descr == %{} ->
-        []
-
       # We check for :term literally instead of using term_type?
       # because we check for term_type? in to_quoted before we
       # compute the difference(dynamic, static).
@@ -2127,6 +2126,9 @@ defmodule Module.Types.Descr do
       single = indivisible_bitmap(descr, opts) ->
         [single]
 
+      empty?(descr) ->
+        []
+
       true ->
         case non_term_type_to_quoted(descr, opts) do
           {:none, _meta, []} = none -> [none]
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 2aafe9ea6c..66231639da 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -340,7 +340,7 @@ defmodule Module.Types.Expr do
             add_inferred(acc, args, body)
         end)
 
-      {fun_from_overlapping_clauses(acc), context}
+      {fun_from_inferred_clauses(acc), context}
     end
   end
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index e7d199396e..d76a944f74 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -767,54 +767,72 @@ defmodule Module.Types.DescrTest do
                intersection(fun([integer()], atom()), fun([float()], binary()))
     end
 
-    test "fun_from_overlapping_clauses" do
+    test "fun_from_inferred_clauses" do
       # No overlap
-      assert fun_from_overlapping_clauses([{[integer()], atom()}, {[float()], binary()}])
+      assert fun_from_inferred_clauses([{[integer()], atom()}, {[float()], binary()}])
              |> equal?(
-               fun_from_non_overlapping_clauses([{[integer()], atom()}, {[float()], binary()}])
+               intersection(
+                 fun_from_non_overlapping_clauses([{[integer()], atom()}, {[float()], binary()}]),
+                 fun([number()], dynamic())
+               )
              )
 
       # Subsets
-      assert fun_from_overlapping_clauses([{[integer()], atom()}, {[number()], binary()}])
+      assert fun_from_inferred_clauses([{[integer()], atom()}, {[number()], binary()}])
              |> equal?(
-               fun_from_non_overlapping_clauses([
-                 {[integer()], union(atom(), binary())},
-                 {[float()], binary()}
-               ])
+               intersection(
+                 fun_from_non_overlapping_clauses([
+                   {[integer()], union(atom(), binary())},
+                   {[float()], binary()}
+                 ]),
+                 fun([number()], dynamic())
+               )
              )
 
-      assert fun_from_overlapping_clauses([{[number()], binary()}, {[integer()], atom()}])
+      assert fun_from_inferred_clauses([{[number()], binary()}, {[integer()], atom()}])
              |> equal?(
-               fun_from_non_overlapping_clauses([
-                 {[integer()], union(atom(), binary())},
-                 {[float()], binary()}
-               ])
+               intersection(
+                 fun_from_non_overlapping_clauses([
+                   {[integer()], union(atom(), binary())},
+                   {[float()], binary()}
+                 ]),
+                 fun([number()], dynamic())
+               )
              )
 
       # Partial
-      assert fun_from_overlapping_clauses([
+      assert fun_from_inferred_clauses([
                {[union(integer(), pid())], atom()},
                {[union(float(), pid())], binary()}
              ])
              |> equal?(
-               fun_from_non_overlapping_clauses([
-                 {[integer()], atom()},
-                 {[float()], binary()},
-                 {[pid()], union(atom(), binary())}
-               ])
+               intersection(
+                 fun_from_non_overlapping_clauses([
+                   {[integer()], atom()},
+                   {[float()], binary()},
+                   {[pid()], union(atom(), binary())}
+                 ]),
+                 fun([union(number(), pid())], dynamic())
+               )
              )
 
       # Difference
-      assert fun_from_overlapping_clauses([
+      assert fun_from_inferred_clauses([
                {[integer(), union(pid(), atom())], atom()},
                {[number(), pid()], binary()}
              ])
              |> equal?(
-               fun_from_non_overlapping_clauses([
-                 {[float(), pid()], binary()},
-                 {[integer(), atom()], atom()},
-                 {[integer(), pid()], union(atom(), binary())}
-               ])
+               intersection(
+                 fun_from_non_overlapping_clauses([
+                   {[float(), pid()], binary()},
+                   {[integer(), atom()], atom()},
+                   {[integer(), pid()], union(atom(), binary())}
+                 ]),
+                 fun_from_non_overlapping_clauses([
+                   {[integer(), union(pid(), atom())], dynamic()},
+                   {[number(), pid()], dynamic()}
+                 ])
+               )
              )
     end
   end
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index f81631c61a..2c3055567e 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -138,24 +138,37 @@ defmodule Module.Types.ExprTest do
     end
 
     test "infers functions" do
-      assert typecheck!(& &1) == fun([dynamic()], dynamic())
-      assert typecheck!(fn -> :ok end) == fun([], atom([:ok]))
+      assert typecheck!(& &1) |> equal?(fun([term()], dynamic()))
+
+      assert typecheck!(fn -> :ok end) |> equal?(fun([], dynamic(atom([:ok]))))
 
       assert typecheck!(fn
                <<"ok">>, {} -> :ok
                <<"error">>, {} -> :error
                [_ | _], %{} -> :list
-             end) ==
+             end)
+             |> equal?(
                intersection(
                  fun(
-                   [dynamic(non_empty_list(term(), term())), dynamic(open_map())],
-                   atom([:list])
+                   [non_empty_list(term(), term()), open_map()],
+                   dynamic(atom([:list]))
                  ),
                  fun(
-                   [dynamic(binary()), dynamic(tuple([]))],
-                   atom([:ok, :error])
+                   [binary(), tuple([])],
+                   dynamic(atom([:ok, :error]))
                  )
                )
+             )
+    end
+
+    test "application" do
+      assert typecheck!(
+               [map],
+               (fn
+                  %{a: a} = data -> %{data | b: a}
+                  data -> data
+                end).(map)
+             ) == dynamic()
     end
 
     test "bad function" do
@@ -253,7 +266,7 @@ defmodule Module.Types.ExprTest do
 
              but function has type:
 
-                 (dynamic(map()) -> :map)
+                 (map() -> dynamic(:map))
              """
     end
 
@@ -265,7 +278,7 @@ defmodule Module.Types.ExprTest do
 
              because the right-hand side has type:
 
-                 (dynamic() -> dynamic({:ok, term()}))
+                 (term() -> dynamic({:ok, term()}))
              """
     end
   end
diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs
index 97cb75bd0c..8d115d6aab 100644
--- a/lib/elixir/test/elixir/module/types/integration_test.exs
+++ b/lib/elixir/test/elixir/module/types/integration_test.exs
@@ -180,8 +180,8 @@ defmodule Module.Types.IntegrationTest do
       assert return.(:captured, 0)
              |> equal?(
                fun_from_non_overlapping_clauses([
-                 {[dynamic(binary())], atom([:ok, :error])},
-                 {[dynamic(non_empty_list(term(), term()))], atom([:list])}
+                 {[binary()], dynamic(atom([:ok, :error]))},
+                 {[non_empty_list(term(), term())], dynamic(atom([:list]))}
                ])
              )
     end

From c151f61c8590ce7f92329fc58ffdbd9f47296b69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Fri, 20 Jun 2025 05:26:08 -0700
Subject: [PATCH 02/10] Use clearer names

---
 lib/elixir/lib/module/types/descr.ex | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 44a7a41e12..345774e7ca 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -150,7 +150,6 @@ defmodule Module.Types.Descr do
           do: fun(args, dynamic(return))
 
     Enum.reduce(funs, &intersection/2)
-    # dynamic(fun())
   end
 
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
@@ -202,19 +201,19 @@ defmodule Module.Types.Descr do
   def domain_to_args(descr) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        tuple_elim_negations_static(descr, & &1)
+        unwrap_domain_tuple(descr, fn {:closed, elems} -> elems end)
 
       {dynamic, static} ->
-        tuple_elim_negations_static(static, & &1) ++
-          tuple_elim_negations_static(dynamic, fn elems -> Enum.map(elems, &dynamic/1) end)
+        unwrap_domain_tuple(static, fn {:closed, elems} -> elems end) ++
+          unwrap_domain_tuple(dynamic, fn {:closed, elems} -> Enum.map(elems, &dynamic/1) end)
     end
   end
 
-  defp tuple_elim_negations_static(%{tuple: dnf} = descr, transform) when map_size(descr) == 1 do
-    Enum.map(dnf, fn {:closed, elements} -> transform.(elements) end)
+  defp unwrap_domain_tuple(%{tuple: dnf} = descr, transform) when map_size(descr) == 1 do
+    Enum.map(dnf, transform)
   end
 
-  defp tuple_elim_negations_static(descr, _transform) when descr == %{}, do: []
+  defp unwrap_domain_tuple(descr, _transform) when descr == %{}, do: []
 
   defp domain_to_flat_args(domain, arity) do
     case domain_to_args(domain) do

From b08657ca332bf3744389e8cc0efae4f76d1d18b8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Fri, 20 Jun 2025 05:59:48 -0700
Subject: [PATCH 03/10] Skip apply on traversal

---
 lib/elixir/lib/module/types/expr.ex | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 66231639da..e03c6e2f17 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -461,7 +461,11 @@ defmodule Module.Types.Expr do
     {args_types, context} =
       Enum.map_reduce(args, context, &of_expr(&1, @pending, &1, stack, &2))
 
-    Apply.fun_apply(fun_type, args_types, call, stack, context)
+    if stack.mode == :traversal do
+      {dynamic(), context}
+    else
+      Apply.fun_apply(fun_type, args_types, call, stack, context)
+    end
   end
 
   def of_expr({{:., _, [callee, key_or_fun]}, meta, []} = call, expected, expr, stack, context)

From 1d6c3d1a65e29069e1bf1ab38fe1b33f45d8c2d5 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 23 Jun 2025 19:06:48 +0200
Subject: [PATCH 04/10] Optis with prints

---
 lib/elixir/lib/module/types/descr.ex          | 325 ++++++++++++++++--
 .../test/elixir/module/types/descr_test.exs   |   3 +
 2 files changed, 301 insertions(+), 27 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 345774e7ca..dd206f1387 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -46,8 +46,8 @@ defmodule Module.Types.Descr do
   @not_non_empty_list Map.delete(@term, :list)
   @not_list Map.replace!(@not_non_empty_list, :bitmap, @bit_top - @bit_empty_list)
 
-  @empty_intersection [0, @none, []]
-  @empty_difference [0, []]
+  @empty_intersection [0, @none, [], :fun_bottom]
+  @empty_difference [0, [], :fun_bottom]
 
   # Type definitions
 
@@ -138,18 +138,22 @@ defmodule Module.Types.Descr do
   Creates a function from overlapping function clauses.
   """
   def fun_from_inferred_clauses(args_clauses) do
-    domain_clauses =
-      Enum.reduce(args_clauses, [], fn {args, return}, acc ->
-        domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
-        pivot_overlapping_clause(domain, upper_bound(return), acc)
-      end)
+    if true do
+      domain_clauses =
+        Enum.reduce(args_clauses, [], fn {args, return}, acc ->
+          domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
+          pivot_overlapping_clause(domain, upper_bound(return), acc)
+        end)
 
-    funs =
-      for {domain, return} <- domain_clauses,
-          args <- domain_to_args(domain),
-          do: fun(args, dynamic(return))
+      funs =
+        for {domain, return} <- domain_clauses,
+            args <- domain_to_args(domain),
+            do: fun(args, dynamic(return))
 
-    Enum.reduce(funs, &intersection/2)
+      Enum.reduce(funs, &intersection/2)
+    else
+      dynamic(fun())
+    end
   end
 
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
@@ -511,6 +515,9 @@ defmodule Module.Types.Descr do
   def empty?(:term), do: false
 
   def empty?(%{} = descr) do
+    # IO.puts("empty?")
+
+    # IO.puts("checking if the type is empty")
     case :maps.get(:dynamic, descr, descr) do
       :term ->
         false
@@ -519,6 +526,13 @@ defmodule Module.Types.Descr do
         true
 
       descr ->
+        # cond do
+        #   not (Map.has_key?(descr, :tuple) or Map.has_key?(descr, :list) or Map.has_key?(descr, :fun)) ->
+        #     IO.puts("descr: #{inspect(descr)}")
+        #   true ->
+        #     :ok
+        # end
+
         not Map.has_key?(descr, :atom) and
           not Map.has_key?(descr, :bitmap) and
           not Map.has_key?(descr, :optional) and
@@ -529,6 +543,8 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # defp ahah(), do: IO.puts("empty?")
+
   # For atom, bitmap, tuple, and optional, if the key is present,
   # then they are not empty,
   defp empty_key?(:fun, value), do: fun_empty?(value)
@@ -1382,6 +1398,8 @@ defmodule Module.Types.Descr do
   # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty
   # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty
   defp fun_empty?(bdd) do
+    # IO.puts("fun_empty?")
+    # IO.puts("on bdd: #{inspect(bdd)}")
     case bdd do
       :fun_bottom -> true
       :fun_top -> false
@@ -1461,28 +1479,261 @@ defmodule Module.Types.Descr do
   # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
   #
   # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
+  def descr_size(:term), do: 1
+
+  def descr_size(%{} = descr) do
+    Enum.reduce(descr, 0, fn {key, value}, acc ->
+      acc + descr_size(key, value)
+    end)
+  end
+
+  def descr_size(:tuple, dnf) do
+    Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
+  end
+
+  def descr_size(:fun, bdd), do: bdd_size(bdd)
+
+  def descr_size(:map, dnf) do
+    Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
+      acc + 1 + length(negs)
+    end)
+  end
+
+  def descr_size(:list, dnf) do
+    Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
+      acc + 1 + length(negs)
+    end)
+  end
+
+  def descr_size(_, _), do: 1
+
+  defp bdd_size({fun, l, r}) do
+    bdd_size(l) + bdd_size(r) + 1
+  end
+
+  defp bdd_size(:fun_top), do: 1
+  defp bdd_size(:fun_bottom), do: 0
+
+  defp list_dnf_size(dnf) do
+    Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
+      1 + length(negs)
+    end)
+  end
+
+  defp all_distinct_non_empty_domains?([{args, _ret}]) do
+    not empty?(args_to_domain(args))
+  end
+
+  defp all_distinct_non_empty_domains?(positives) do
+    # For each two elements of positives, their domains are distinct
+    for {args1, _ret1} <- positives,
+        {args2, _ret2} <- positives,
+        args1 != args2,
+        reduce: true do
+      acc ->
+        # 1. check there are no empty args
+        dom1 = args_to_domain(args1)
+        dom2 = args_to_domain(args2)
+        if empty?(dom1) or empty?(dom2) do
+          IO.puts("We found that #{to_quoted_string(dom1)} or #{to_quoted_string(dom2)} is empty")
+          false
+        else
+          d = disjoint?(dom1, dom2)
+          if not d do
+            IO.puts("We found that #{to_quoted_string(dom1)} and #{to_quoted_string(dom2)} are not disjoint")
+          end
+          acc and d
+        end
+    end
+  end
+
+  defp all_non_empty_domains?(positives) do
+    Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
+  end
+
   defp phi_starter(arguments, return, positives) do
-    n = length(arguments)
-    # Arity mismatch: if there is one positive function with a different arity,
-    # then it cannot be a subtype of the (arguments->type) functions.
-    if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do
-      false
+    ### SPECIAL CASE: all the positives (intersection) functions have distinct domains
+    # In that case, checking subtyping of it with a single arrow is simply:
+    # checking that the union of the domains of the positives is a supertype of the domain of the arrow
+    # and that applying the input type of the arrow to the intersection gives sth that is a subtype of the return type of the arrow
+    IO.puts("Checking if all the positives have distinct non empty domains...")
+    if all_non_empty_domains?(positives) and all_non_empty_domains?([{arguments, return}]) do
+      return = negation(return)
+      IO.puts("They DO")
+      IO.puts("All distinct non empty domains")
+      IO.puts("The positives are:")
+      Enum.each(positives, fn {args, ret} ->
+        IO.puts("#{Enum.map(args, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(ret)}")
+      end)
+      IO.puts("--------------------------------")
+      IO.puts("--------------------------------")
+      IO.puts("Checking if the single arrow")
+      IO.puts("#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(return)}")
+      IO.puts("is a supertype of the intersection of these #{length(positives)} positives")
+
+      type_positives =
+        Enum.map(positives, fn {args, ret} -> fun(args, ret) end) |> Enum.reduce(&intersection/2)
+
+      {:ok, _dom, static_arrows} = fun_normalize(type_positives, length(arguments), :static)
+      result = fun_apply_static(arguments, static_arrows, false)
+
+      IO.puts("We are done!")
+      IO.puts("After applying the intersection of positives")
+      IO.puts("to the arguments")
+      IO.puts("(#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")})")
+      IO.puts("We get result:")
+      IO.puts("#{to_quoted_string(result)}")
+      IO.puts("And we are checking if it is a subtype of:")
+      IO.puts("#{to_quoted_string(return)}")
+
+      r = subtype?(result, return)
+      if r do
+        IO.puts("Thus, the single arrow IS a supertype.")
+        r
+      else
+        IO.puts("Thus, the single arrow IS NOT a supertype.")
+        false
+      end
+
+      # positives_domain =
+      #   Enum.reduce(positives, none(), fn {args, _ret}, acc ->
+      #     union(acc, args_to_domain(args))
+      #   end)
+
+      # 1. the positives domain must be a supertype of the domain of the arrow
+      # result1 = subtype?(args_to_domain(arguments), positives_domain)
+
+      # if result1 do
+      #   # 2. if we apply the input type of the arrow to the intersection, the result must be a subtype of the return type of the arrow
+      #   # 2.a) build the intersection of positives
+
+      #   # 2.b) check that the result is a subtype of the return type of the arrow
+      #   result2 = subtype?(apply_result, return)
+      # else
+      #   false
+      # end
     else
-      arguments = Enum.map(arguments, &{false, &1})
-      phi(arguments, {false, return}, positives)
+      # Show the caller of this function
+      IO.puts("They DO NOT")
+      IO.puts("phi_starter")
+      # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
+      # IO.puts("Starting phi starter with return: #{inspect(return)}")
+      # IO.puts("Starting phi starter with positives: #{inspect(positives)}")
+      # Total size of the descrs in arguments, return, and positives
+      total_size =
+        arguments
+        |> Enum.map(&descr_size/1)
+        |> Enum.sum()
+        |> Kernel.+(descr_size(return))
+        |> Kernel.+(
+          Enum.reduce(positives, 0, fn {args, ret}, acc ->
+            acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
+          end)
+        )
+
+      IO.puts("Total size: #{total_size}")
+      IO.puts("Size decomposition:")
+      IO.puts("How many arguments: #{length(arguments)}")
+      IO.puts("arguments: #{Enum.map(arguments, &descr_size/1) |> Enum.sum()}")
+      IO.puts("return: #{descr_size(return)}")
+      IO.puts("We are checking if this function:")
+
+      IO.puts(
+        "#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(return)}"
+      )
+
+      IO.puts(
+        "positives: #{Enum.reduce(positives, 0, fn {args, ret}, acc -> acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret) end)}"
+      )
+
+      # How many negatives there are
+      IO.puts("Is a supertype of the intersection of these #{length(positives)} positives:")
+      IO.puts("here are each of them:")
+
+      Enum.each(positives, fn {args, ret} ->
+        IO.puts(
+          "#{Enum.map(args, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(ret)}\n"
+        )
+      end)
+
+      # start_time = DateTime.utc_now()
+
+      n = length(arguments)
+      # Arity mismatch: if there is one positive function with a different arity,
+      # then it cannot be a subtype of the (arguments->type) functions.
+      if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do
+        false
+      else
+        # Initialize memoization cache
+        # 1. check that the domain is a subtype of the union of all
+        # the domains of the positives
+        # domain = args_to_domain(arguments)
+        # positives_domain = Enum.reduce(positives, none(), fn {args, _ret}, acc -> union(acc, args_to_domain(args)) end)
+        # if not subtype?(domain, positives_domain) do
+        #   false
+        # else
+        # 2. check that the return type is a subtype of the union of all
+        # the return types of the positives
+
+        Process.put(:phi_cache, %{})
+        arguments = Enum.map(arguments, &{false, &1})
+        {result, call_count} = phi(arguments, {false, return}, positives, 0)
+        cache_size = map_size(Process.get(:phi_cache, %{}))
+        # Recursive calls
+        IO.puts("phi recursive calls: #{call_count}")
+        # IO.puts("it took #{DateTime.diff(DateTime.utc_now(), start_time, :millisecond)}ms")
+        IO.puts("--------------------------------")
+
+        result
+      end
+
+      # end
     end
   end
 
-  defp phi(args, {b, t}, []) do
-    Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
+  defp phi(args, {b, t}, [], call_count) do
+    {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), call_count}
   end
 
-  defp phi(args, {b, ret}, [{arguments, return} | rest_positive]) do
-    phi(args, {true, intersection(ret, return)}, rest_positive) and
-      Enum.all?(Enum.with_index(arguments), fn {type, index} ->
-        List.update_at(args, index, fn {_, arg} -> {true, difference(arg, type)} end)
-        |> phi({b, ret}, rest_positive)
-      end)
+  defp phi(args, {b, ret}, [{arguments, return} | rest_positive], call_count) do
+    # Create cache key from function arguments
+    cache_key = {args, {b, ret}, [{arguments, return} | rest_positive]}
+    cache = Process.get(:phi_cache, %{})
+
+    case Map.get(cache, cache_key) do
+      nil ->
+        # Compute result and cache it
+        {result1, call_count1} =
+          phi(args, {true, intersection(ret, return)}, rest_positive, call_count + 1)
+
+        if not result1 do
+          Process.put(:phi_cache, Map.put(cache, cache_key, false))
+          {false, call_count}
+        else
+          # This doesn't stop if one intermediate result is false?
+          {result2, call_count2} =
+            Enum.with_index(arguments)
+            |> Enum.reduce_while({true, call_count1}, fn {type, index}, {acc_result, acc_count} ->
+              {new_result, new_count} =
+                List.update_at(args, index, fn {_, arg} -> {true, difference(arg, type)} end)
+                |> phi({b, ret}, rest_positive, acc_count + 1)
+
+              if new_result do
+                {:cont, {acc_result and new_result, new_count}}
+              else
+                {:halt, {false, new_count}}
+              end
+            end)
+
+          result = {result1 and result2, call_count2}
+          Process.put(:phi_cache, Map.put(cache, cache_key, result))
+          result
+        end
+
+      cached_result ->
+        # Return cached result
+        cached_result
+    end
   end
 
   defp fun_union(bdd1, bdd2) do
@@ -1829,7 +2080,12 @@ defmodule Module.Types.Descr do
   #    b) If only the last type differs, subtracts it
   # 3. Base case: adds dnf2 type to negations of dnf1 type
   # The result may be larger than the initial dnf1, which is maintained in the accumulator.
+  defp list_difference(_, dnf) when dnf == @non_empty_list_top do
+    0
+  end
+
   defp list_difference(dnf1, dnf2) do
+    # IO.puts("list_difference")
     Enum.reduce(dnf2, dnf1, fn {t2, last2, negs2}, acc_dnf1 ->
       last2 = list_tail_unfold(last2)
 
@@ -1856,7 +2112,13 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  defp list_empty?(@non_empty_list_top), do: false
+
   defp list_empty?(dnf) do
+    # IO.puts("list_empty?")
+    # IO.puts("on dnf: #{inspect(dnf)}")
+    # IO.puts("the dnf has #{length(dnf)} elements")
+    # IO.puts("i count #{Enum.reduce(dnf, 0, fn {_, _, negs}, acc -> acc + length(negs) end)} negations")
     Enum.all?(dnf, fn {list_type, last_type, negs} ->
       last_type = list_tail_unfold(last_type)
 
@@ -2396,6 +2658,10 @@ defmodule Module.Types.Descr do
     if empty?(type), do: throw(:empty), else: type
   end
 
+  defp map_difference(_, dnf) when dnf == @map_top do
+    0
+  end
+
   defp map_difference(dnf1, dnf2) do
     Enum.reduce(dnf2, dnf1, fn
       # Optimization: we are removing an open map with one field.
@@ -2684,6 +2950,7 @@ defmodule Module.Types.Descr do
   # Since the algorithm is recursive, we implement the short-circuiting
   # as throw/catch.
   defp map_empty?(dnf) do
+    # IO.puts("map_empty?")
     Enum.all?(dnf, fn {tag, pos, negs} -> map_empty?(tag, pos, negs) end)
   end
 
@@ -3046,6 +3313,10 @@ defmodule Module.Types.Descr do
     zip_non_empty_intersection!(rest1, rest2, [non_empty_intersection!(type1, type2) | acc])
   end
 
+  defp tuple_difference(_, dnf) when dnf == @tuple_top do
+    0
+  end
+
   defp tuple_difference(dnf1, dnf2) do
     Enum.reduce(dnf2, dnf1, fn {tag2, elements2}, dnf1 ->
       Enum.reduce(dnf1, [], fn {tag1, elements1}, acc ->
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index d76a944f74..bdc0a2430c 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -674,6 +674,9 @@ defmodule Module.Types.DescrTest do
       assert subtype?(f, fun([none(), integer()], term()))
       assert subtype?(fun([none(), number()], atom()), f)
       assert subtype?(fun([tuple(), number()], atom()), f)
+      # (none, float)->atom is not a subtype of (none, integer)->atom because float has an empty intersection with integer
+      # it's only possible to find this out by doing the
+      # intersection one by one.
       refute subtype?(fun([none(), float()], atom()), f)
       refute subtype?(fun([pid(), float()], atom()), f)
       # A function with the wrong arity is refused

From 263462d43e0f6b58ea7355cf5ecf96b4cb9e011e Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 23 Jun 2025 19:12:25 +0200
Subject: [PATCH 05/10] Remove IO

---
 lib/elixir/lib/module/types/descr.ex | 207 ++++++++++-----------------
 1 file changed, 76 insertions(+), 131 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index dd206f1387..87ff18bf76 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -138,7 +138,7 @@ defmodule Module.Types.Descr do
   Creates a function from overlapping function clauses.
   """
   def fun_from_inferred_clauses(args_clauses) do
-    if true do
+    if false do
       domain_clauses =
         Enum.reduce(args_clauses, [], fn {args, return}, acc ->
           domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
@@ -1479,73 +1479,71 @@ defmodule Module.Types.Descr do
   # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
   #
   # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
-  def descr_size(:term), do: 1
-
-  def descr_size(%{} = descr) do
-    Enum.reduce(descr, 0, fn {key, value}, acc ->
-      acc + descr_size(key, value)
-    end)
-  end
-
-  def descr_size(:tuple, dnf) do
-    Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
-  end
-
-  def descr_size(:fun, bdd), do: bdd_size(bdd)
-
-  def descr_size(:map, dnf) do
-    Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
-      acc + 1 + length(negs)
-    end)
-  end
-
-  def descr_size(:list, dnf) do
-    Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
-      acc + 1 + length(negs)
-    end)
-  end
-
-  def descr_size(_, _), do: 1
-
-  defp bdd_size({fun, l, r}) do
-    bdd_size(l) + bdd_size(r) + 1
-  end
-
-  defp bdd_size(:fun_top), do: 1
-  defp bdd_size(:fun_bottom), do: 0
-
-  defp list_dnf_size(dnf) do
-    Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
-      1 + length(negs)
-    end)
-  end
-
-  defp all_distinct_non_empty_domains?([{args, _ret}]) do
-    not empty?(args_to_domain(args))
-  end
-
-  defp all_distinct_non_empty_domains?(positives) do
-    # For each two elements of positives, their domains are distinct
-    for {args1, _ret1} <- positives,
-        {args2, _ret2} <- positives,
-        args1 != args2,
-        reduce: true do
-      acc ->
-        # 1. check there are no empty args
-        dom1 = args_to_domain(args1)
-        dom2 = args_to_domain(args2)
-        if empty?(dom1) or empty?(dom2) do
-          IO.puts("We found that #{to_quoted_string(dom1)} or #{to_quoted_string(dom2)} is empty")
-          false
-        else
-          d = disjoint?(dom1, dom2)
-          if not d do
-            IO.puts("We found that #{to_quoted_string(dom1)} and #{to_quoted_string(dom2)} are not disjoint")
-          end
-          acc and d
-        end
-    end
-  end
+  # def descr_size(:term), do: 1
+
+  # def descr_size(%{} = descr) do
+  #   Enum.reduce(descr, 0, fn {key, value}, acc ->
+  #     acc + descr_size(key, value)
+  #   end)
+  # end
+
+  # def descr_size(:tuple, dnf) do
+  #   Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
+  # end
+
+  # def descr_size(:fun, bdd), do: bdd_size(bdd)
+
+  # def descr_size(:map, dnf) do
+  #   Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
+  #     acc + 1 + length(negs)
+  #   end)
+  # end
+
+  # def descr_size(:list, dnf) do
+  #   Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
+  #     acc + 1 + length(negs)
+  #   end)
+  # end
+
+  # def descr_size(_, _), do: 1
+
+  # defp bdd_size({fun, l, r}) do
+  #   bdd_size(l) + bdd_size(r) + 1
+  # end
+
+  # defp bdd_size(:fun_top), do: 1
+  # defp bdd_size(:fun_bottom), do: 0
+
+  # defp list_dnf_size(dnf) do
+  #   Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
+  #     1 + length(negs)
+  #   end)
+  # end
+
+  # defp all_distinct_non_empty_domains?([{args, _ret}]) do
+  #   not empty?(args_to_domain(args))
+  # end
+
+  # defp all_distinct_non_empty_domains?(positives) do
+  #   # For each two elements of positives, their domains are distinct
+  #   for {args1, _ret1} <- positives,
+  #       {args2, _ret2} <- positives,
+  #       args1 != args2,
+  #       reduce: true do
+  #     acc ->
+  #       # 1. check there are no empty args
+  #       dom1 = args_to_domain(args1)
+  #       dom2 = args_to_domain(args2)
+  #       if empty?(dom1) or empty?(dom2) do
+  #         false
+  #       else
+  #         d = disjoint?(dom1, dom2)
+  #         if not d do
+  #         end
+  #         acc and d
+  #       end
+  #   end
+  # end
 
   defp all_non_empty_domains?(positives) do
     Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
@@ -1556,42 +1554,18 @@ defmodule Module.Types.Descr do
     # In that case, checking subtyping of it with a single arrow is simply:
     # checking that the union of the domains of the positives is a supertype of the domain of the arrow
     # and that applying the input type of the arrow to the intersection gives sth that is a subtype of the return type of the arrow
-    IO.puts("Checking if all the positives have distinct non empty domains...")
     if all_non_empty_domains?(positives) and all_non_empty_domains?([{arguments, return}]) do
       return = negation(return)
-      IO.puts("They DO")
-      IO.puts("All distinct non empty domains")
-      IO.puts("The positives are:")
-      Enum.each(positives, fn {args, ret} ->
-        IO.puts("#{Enum.map(args, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(ret)}")
-      end)
-      IO.puts("--------------------------------")
-      IO.puts("--------------------------------")
-      IO.puts("Checking if the single arrow")
-      IO.puts("#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(return)}")
-      IO.puts("is a supertype of the intersection of these #{length(positives)} positives")
-
       type_positives =
         Enum.map(positives, fn {args, ret} -> fun(args, ret) end) |> Enum.reduce(&intersection/2)
 
       {:ok, _dom, static_arrows} = fun_normalize(type_positives, length(arguments), :static)
       result = fun_apply_static(arguments, static_arrows, false)
 
-      IO.puts("We are done!")
-      IO.puts("After applying the intersection of positives")
-      IO.puts("to the arguments")
-      IO.puts("(#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")})")
-      IO.puts("We get result:")
-      IO.puts("#{to_quoted_string(result)}")
-      IO.puts("And we are checking if it is a subtype of:")
-      IO.puts("#{to_quoted_string(return)}")
-
       r = subtype?(result, return)
       if r do
-        IO.puts("Thus, the single arrow IS a supertype.")
         r
       else
-        IO.puts("Thus, the single arrow IS NOT a supertype.")
         false
       end
 
@@ -1614,47 +1588,21 @@ defmodule Module.Types.Descr do
       # end
     else
       # Show the caller of this function
-      IO.puts("They DO NOT")
-      IO.puts("phi_starter")
       # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
       # IO.puts("Starting phi starter with return: #{inspect(return)}")
       # IO.puts("Starting phi starter with positives: #{inspect(positives)}")
       # Total size of the descrs in arguments, return, and positives
-      total_size =
-        arguments
-        |> Enum.map(&descr_size/1)
-        |> Enum.sum()
-        |> Kernel.+(descr_size(return))
-        |> Kernel.+(
-          Enum.reduce(positives, 0, fn {args, ret}, acc ->
-            acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
-          end)
-        )
-
-      IO.puts("Total size: #{total_size}")
-      IO.puts("Size decomposition:")
-      IO.puts("How many arguments: #{length(arguments)}")
-      IO.puts("arguments: #{Enum.map(arguments, &descr_size/1) |> Enum.sum()}")
-      IO.puts("return: #{descr_size(return)}")
-      IO.puts("We are checking if this function:")
-
-      IO.puts(
-        "#{Enum.map(arguments, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(return)}"
-      )
+      # total_size =
+      #   arguments
+      #   |> Enum.map(&descr_size/1)
+      #   |> Enum.sum()
+      #   |> Kernel.+(descr_size(return))
+      #   |> Kernel.+(
+      #     Enum.reduce(positives, 0, fn {args, ret}, acc ->
+      #       acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
+      #     end)
+      #   )
 
-      IO.puts(
-        "positives: #{Enum.reduce(positives, 0, fn {args, ret}, acc -> acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret) end)}"
-      )
-
-      # How many negatives there are
-      IO.puts("Is a supertype of the intersection of these #{length(positives)} positives:")
-      IO.puts("here are each of them:")
-
-      Enum.each(positives, fn {args, ret} ->
-        IO.puts(
-          "#{Enum.map(args, fn arg -> to_quoted_string(arg) end) |> Enum.join(", ")} -> #{to_quoted_string(ret)}\n"
-        )
-      end)
 
       # start_time = DateTime.utc_now()
 
@@ -1680,9 +1628,6 @@ defmodule Module.Types.Descr do
         {result, call_count} = phi(arguments, {false, return}, positives, 0)
         cache_size = map_size(Process.get(:phi_cache, %{}))
         # Recursive calls
-        IO.puts("phi recursive calls: #{call_count}")
-        # IO.puts("it took #{DateTime.diff(DateTime.utc_now(), start_time, :millisecond)}ms")
-        IO.puts("--------------------------------")
 
         result
       end

From 51114482656479e64a300a3814e0fb5110ed9729 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 25 Jun 2025 13:45:33 +0200
Subject: [PATCH 06/10] Full 3 optis

---
 lib/elixir/lib/module/types/descr.ex | 95 ++++++++++++++++------------
 1 file changed, 54 insertions(+), 41 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 87ff18bf76..0a53cb7bdd 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -138,7 +138,7 @@ defmodule Module.Types.Descr do
   Creates a function from overlapping function clauses.
   """
   def fun_from_inferred_clauses(args_clauses) do
-    if false do
+    if true do
       domain_clauses =
         Enum.reduce(args_clauses, [], fn {args, return}, acc ->
           domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
@@ -1187,6 +1187,7 @@ defmodule Module.Types.Descr do
 
         static_arrows == [] ->
           # TODO: We need to validate this within the theory
+          arguments = Enum.map(arguments, &upper_bound/1)
           {:ok, dynamic(fun_apply_static(arguments, dynamic_arrows, false))}
 
         true ->
@@ -1305,22 +1306,25 @@ defmodule Module.Types.Descr do
     type_args = args_to_domain(arguments)
 
     # Optimization: short-circuits when inner loop is none() or outer loop is term()
-    if maybe_empty? and empty?(type_args) do
-      Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
-        Enum.reduce_while(intersection_of_arrows, term(), fn
-          {_dom, _ret}, acc when acc == @none -> {:halt, acc}
-          {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
+    result =
+      if maybe_empty? and empty?(type_args) do
+        Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
+          Enum.reduce_while(intersection_of_arrows, term(), fn
+            {_dom, _ret}, acc when acc == @none -> {:halt, acc}
+            {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
+          end)
+          |> case do
+            :term -> {:halt, :term}
+            inner -> {:cont, union(inner, acc)}
+          end
         end)
-        |> case do
-          :term -> {:halt, :term}
-          inner -> {:cont, union(inner, acc)}
-        end
-      end)
-    else
-      Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
-        aux_apply(acc, type_args, term(), intersection_of_arrows)
-      end)
-    end
+      else
+        Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
+          aux_apply(acc, type_args, term(), intersection_of_arrows)
+        end)
+      end
+
+    result
   end
 
   # Helper function for function application that handles the application of
@@ -1337,11 +1341,32 @@ defmodule Module.Types.Descr do
   # - arrow_intersections: The list of function arrows to process
 
   # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
-  defp aux_apply(result, _input, rets_reached, []) do
+  defp aux_apply(result, _input, rets_reached, arrow_intersections, depth \\ 0)
+
+  defp aux_apply(result, _input, rets_reached, [], depth) do
     if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
   end
 
-  defp aux_apply(result, input, returns_reached, [{dom, ret} | arrow_intersections]) do
+  defp aux_apply(result, input, returns_reached, [{dom, ret} | arrow_intersections], depth) do
+    # Performance warning thresholds
+    if Map.has_key?(input, :dynamic) do
+      IO.puts("aux_apply called with dynamic input")
+      raise "aux_apply called with dynamic input"
+    end
+
+    max_depth = 15
+
+    if depth > max_depth do
+      IO.puts("PERFORMANCE WARNING: aux_apply depth #{depth} (threshold: #{max_depth})")
+      IO.puts("aux_apply [depth:#{depth}]")
+      IO.puts("input: #{inspect(input)}")
+      IO.puts("returns_reached: #{inspect(returns_reached)}")
+      IO.puts("dom: #{inspect(dom)}")
+      IO.puts("ret: #{inspect(ret)}")
+      IO.puts("arrow_intersections: #{inspect(arrow_intersections)}")
+      IO.puts("--------------------------------")
+    end
+
     # Calculate the part of the input not covered by this arrow's domain
     dom_subtract = difference(input, args_to_domain(dom))
 
@@ -1359,7 +1384,7 @@ defmodule Module.Types.Descr do
       if empty?(dom_subtract) do
         result
       else
-        aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
+        aux_apply(result, dom_subtract, returns_reached, arrow_intersections, depth + 1)
       end
 
     # 2. Return type refinement
@@ -1369,7 +1394,7 @@ defmodule Module.Types.Descr do
 
     # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
     # should result in (atom() ∩ pid()), which is none().
-    aux_apply(result, input, ret_refine, arrow_intersections)
+    aux_apply(result, input, ret_refine, arrow_intersections, depth + 1)
   end
 
   # Takes all the paths from the root to the leaves finishing with a 1,
@@ -1556,6 +1581,7 @@ defmodule Module.Types.Descr do
     # and that applying the input type of the arrow to the intersection gives sth that is a subtype of the return type of the arrow
     if all_non_empty_domains?(positives) and all_non_empty_domains?([{arguments, return}]) do
       return = negation(return)
+
       type_positives =
         Enum.map(positives, fn {args, ret} -> fun(args, ret) end) |> Enum.reduce(&intersection/2)
 
@@ -1563,29 +1589,12 @@ defmodule Module.Types.Descr do
       result = fun_apply_static(arguments, static_arrows, false)
 
       r = subtype?(result, return)
+
       if r do
         r
       else
         false
       end
-
-      # positives_domain =
-      #   Enum.reduce(positives, none(), fn {args, _ret}, acc ->
-      #     union(acc, args_to_domain(args))
-      #   end)
-
-      # 1. the positives domain must be a supertype of the domain of the arrow
-      # result1 = subtype?(args_to_domain(arguments), positives_domain)
-
-      # if result1 do
-      #   # 2. if we apply the input type of the arrow to the intersection, the result must be a subtype of the return type of the arrow
-      #   # 2.a) build the intersection of positives
-
-      #   # 2.b) check that the result is a subtype of the return type of the arrow
-      #   result2 = subtype?(apply_result, return)
-      # else
-      #   false
-      # end
     else
       # Show the caller of this function
       # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
@@ -1603,7 +1612,6 @@ defmodule Module.Types.Descr do
       #     end)
       #   )
 
-
       # start_time = DateTime.utc_now()
 
       n = length(arguments)
@@ -3265,7 +3273,8 @@ defmodule Module.Types.Descr do
   defp tuple_difference(dnf1, dnf2) do
     Enum.reduce(dnf2, dnf1, fn {tag2, elements2}, dnf1 ->
       Enum.reduce(dnf1, [], fn {tag1, elements1}, acc ->
-        tuple_eliminate_single_negation(tag1, elements1, {tag2, elements2}) ++ acc
+        tuple_eliminate_single_negation(tag1, elements1, {tag2, elements2})
+        |> tuple_union(acc)
       end)
     end)
   end
@@ -3280,8 +3289,10 @@ defmodule Module.Types.Descr do
     if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do
       [{tag, elements}]
     else
-      tuple_elim_content([], tag, elements, neg_elements) ++
+      tuple_union(
+        tuple_elim_content([], tag, elements, neg_elements),
         tuple_elim_size(n, m, tag, elements, neg_tag)
+      )
     end
   end
 
@@ -3945,4 +3956,6 @@ defmodule Module.Types.Descr do
   defp non_empty_map_or([head | tail], fun) do
     Enum.reduce(tail, fun.(head), &{:or, [], [&2, fun.(&1)]})
   end
+
+  # Performance tracking helpers for aux_apply
 end

From 02d6081e73c4465cf1b8b6245d30240a991c49bd Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 25 Jun 2025 14:02:01 +0200
Subject: [PATCH 07/10] Remove comments/profiling

---
 lib/elixir/lib/module/types/descr.ex | 230 +++++----------------------
 1 file changed, 36 insertions(+), 194 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 0a53cb7bdd..017c3c584f 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -138,22 +138,18 @@ defmodule Module.Types.Descr do
   Creates a function from overlapping function clauses.
   """
   def fun_from_inferred_clauses(args_clauses) do
-    if true do
-      domain_clauses =
-        Enum.reduce(args_clauses, [], fn {args, return}, acc ->
-          domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
-          pivot_overlapping_clause(domain, upper_bound(return), acc)
-        end)
+    domain_clauses =
+      Enum.reduce(args_clauses, [], fn {args, return}, acc ->
+        domain = args |> Enum.map(&upper_bound/1) |> args_to_domain()
+        pivot_overlapping_clause(domain, upper_bound(return), acc)
+      end)
 
-      funs =
-        for {domain, return} <- domain_clauses,
-            args <- domain_to_args(domain),
-            do: fun(args, dynamic(return))
+    funs =
+      for {domain, return} <- domain_clauses,
+          args <- domain_to_args(domain),
+          do: fun(args, dynamic(return))
 
-      Enum.reduce(funs, &intersection/2)
-    else
-      dynamic(fun())
-    end
+    Enum.reduce(funs, &intersection/2)
   end
 
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
@@ -515,9 +511,6 @@ defmodule Module.Types.Descr do
   def empty?(:term), do: false
 
   def empty?(%{} = descr) do
-    # IO.puts("empty?")
-
-    # IO.puts("checking if the type is empty")
     case :maps.get(:dynamic, descr, descr) do
       :term ->
         false
@@ -526,13 +519,6 @@ defmodule Module.Types.Descr do
         true
 
       descr ->
-        # cond do
-        #   not (Map.has_key?(descr, :tuple) or Map.has_key?(descr, :list) or Map.has_key?(descr, :fun)) ->
-        #     IO.puts("descr: #{inspect(descr)}")
-        #   true ->
-        #     :ok
-        # end
-
         not Map.has_key?(descr, :atom) and
           not Map.has_key?(descr, :bitmap) and
           not Map.has_key?(descr, :optional) and
@@ -543,8 +529,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # defp ahah(), do: IO.puts("empty?")
-
   # For atom, bitmap, tuple, and optional, if the key is present,
   # then they are not empty,
   defp empty_key?(:fun, value), do: fun_empty?(value)
@@ -1341,34 +1325,13 @@ defmodule Module.Types.Descr do
   # - arrow_intersections: The list of function arrows to process
 
   # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
-  defp aux_apply(result, _input, rets_reached, arrow_intersections, depth \\ 0)
-
-  defp aux_apply(result, _input, rets_reached, [], depth) do
+  defp aux_apply(result, _input, rets_reached, []) do
     if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
   end
 
-  defp aux_apply(result, input, returns_reached, [{dom, ret} | arrow_intersections], depth) do
-    # Performance warning thresholds
-    if Map.has_key?(input, :dynamic) do
-      IO.puts("aux_apply called with dynamic input")
-      raise "aux_apply called with dynamic input"
-    end
-
-    max_depth = 15
-
-    if depth > max_depth do
-      IO.puts("PERFORMANCE WARNING: aux_apply depth #{depth} (threshold: #{max_depth})")
-      IO.puts("aux_apply [depth:#{depth}]")
-      IO.puts("input: #{inspect(input)}")
-      IO.puts("returns_reached: #{inspect(returns_reached)}")
-      IO.puts("dom: #{inspect(dom)}")
-      IO.puts("ret: #{inspect(ret)}")
-      IO.puts("arrow_intersections: #{inspect(arrow_intersections)}")
-      IO.puts("--------------------------------")
-    end
-
+  defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do
     # Calculate the part of the input not covered by this arrow's domain
-    dom_subtract = difference(input, args_to_domain(dom))
+    dom_subtract = difference(input, args_to_domain(args))
 
     # Refine the return type by intersecting with this arrow's return type
     ret_refine = intersection(returns_reached, ret)
@@ -1384,7 +1347,7 @@ defmodule Module.Types.Descr do
       if empty?(dom_subtract) do
         result
       else
-        aux_apply(result, dom_subtract, returns_reached, arrow_intersections, depth + 1)
+        aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
       end
 
     # 2. Return type refinement
@@ -1394,7 +1357,7 @@ defmodule Module.Types.Descr do
 
     # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
     # should result in (atom() ∩ pid()), which is none().
-    aux_apply(result, input, ret_refine, arrow_intersections, depth + 1)
+    aux_apply(result, input, ret_refine, arrow_intersections)
   end
 
   # Takes all the paths from the root to the leaves finishing with a 1,
@@ -1423,8 +1386,6 @@ defmodule Module.Types.Descr do
   # - `fun(integer() -> atom()) and not fun(none() -> term())` is empty
   # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty
   defp fun_empty?(bdd) do
-    # IO.puts("fun_empty?")
-    # IO.puts("on bdd: #{inspect(bdd)}")
     case bdd do
       :fun_bottom -> true
       :fun_top -> false
@@ -1467,7 +1428,7 @@ defmodule Module.Types.Descr do
           # determines emptiness.
           length(neg_arguments) == positive_arity and
             subtype?(args_to_domain(neg_arguments), positive_domain) and
-            phi_starter(neg_arguments, negation(neg_return), positives)
+            phi_starter(neg_arguments, neg_return, positives)
         end)
     end
   end
@@ -1504,116 +1465,20 @@ defmodule Module.Types.Descr do
   # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
   #
   # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
-  # def descr_size(:term), do: 1
-
-  # def descr_size(%{} = descr) do
-  #   Enum.reduce(descr, 0, fn {key, value}, acc ->
-  #     acc + descr_size(key, value)
-  #   end)
-  # end
-
-  # def descr_size(:tuple, dnf) do
-  #   Enum.sum(Enum.map(dnf, fn {tag, elems} -> length(elems) end))
-  # end
-
-  # def descr_size(:fun, bdd), do: bdd_size(bdd)
-
-  # def descr_size(:map, dnf) do
-  #   Enum.reduce(dnf, 0, fn {tag, pos, negs}, acc ->
-  #     acc + 1 + length(negs)
-  #   end)
-  # end
-
-  # def descr_size(:list, dnf) do
-  #   Enum.reduce(dnf, 0, fn {_, last, negs}, acc ->
-  #     acc + 1 + length(negs)
-  #   end)
-  # end
-
-  # def descr_size(_, _), do: 1
-
-  # defp bdd_size({fun, l, r}) do
-  #   bdd_size(l) + bdd_size(r) + 1
-  # end
-
-  # defp bdd_size(:fun_top), do: 1
-  # defp bdd_size(:fun_bottom), do: 0
-
-  # defp list_dnf_size(dnf) do
-  #   Enum.reduce(dnf, 0, fn {_, _, negs}, acc ->
-  #     1 + length(negs)
-  #   end)
-  # end
-
-  # defp all_distinct_non_empty_domains?([{args, _ret}]) do
-  #   not empty?(args_to_domain(args))
-  # end
-
-  # defp all_distinct_non_empty_domains?(positives) do
-  #   # For each two elements of positives, their domains are distinct
-  #   for {args1, _ret1} <- positives,
-  #       {args2, _ret2} <- positives,
-  #       args1 != args2,
-  #       reduce: true do
-  #     acc ->
-  #       # 1. check there are no empty args
-  #       dom1 = args_to_domain(args1)
-  #       dom2 = args_to_domain(args2)
-  #       if empty?(dom1) or empty?(dom2) do
-  #         false
-  #       else
-  #         d = disjoint?(dom1, dom2)
-  #         if not d do
-  #         end
-  #         acc and d
-  #       end
-  #   end
-  # end
-
   defp all_non_empty_domains?(positives) do
     Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
   end
 
   defp phi_starter(arguments, return, positives) do
-    ### SPECIAL CASE: all the positives (intersection) functions have distinct domains
-    # In that case, checking subtyping of it with a single arrow is simply:
-    # checking that the union of the domains of the positives is a supertype of the domain of the arrow
-    # and that applying the input type of the arrow to the intersection gives sth that is a subtype of the return type of the arrow
+    ### SPECIAL CASE: all the positives (intersection) functions have non-empty arguments
+    # In that case, checking subtyping of it with a single arrow is simply checking that the union
+    # of the domains of the positives is a supertype of the domain of the arrow
+    # and that applying the input type of the arrow to the intersection gives sth that
+    # is a subtype of the return type of the arrow
     if all_non_empty_domains?(positives) and all_non_empty_domains?([{arguments, return}]) do
-      return = negation(return)
-
-      type_positives =
-        Enum.map(positives, fn {args, ret} -> fun(args, ret) end) |> Enum.reduce(&intersection/2)
-
-      {:ok, _dom, static_arrows} = fun_normalize(type_positives, length(arguments), :static)
-      result = fun_apply_static(arguments, static_arrows, false)
-
-      r = subtype?(result, return)
-
-      if r do
-        r
-      else
-        false
-      end
+      fun_apply_static(arguments, [positives], false)
+      |> subtype?(return)
     else
-      # Show the caller of this function
-      # IO.puts("Starting phi starter with arguments: #{inspect(arguments)}")
-      # IO.puts("Starting phi starter with return: #{inspect(return)}")
-      # IO.puts("Starting phi starter with positives: #{inspect(positives)}")
-      # Total size of the descrs in arguments, return, and positives
-      # total_size =
-      #   arguments
-      #   |> Enum.map(&descr_size/1)
-      #   |> Enum.sum()
-      #   |> Kernel.+(descr_size(return))
-      #   |> Kernel.+(
-      #     Enum.reduce(positives, 0, fn {args, ret}, acc ->
-      #       acc + Enum.sum(Enum.map(args, &descr_size/1)) + descr_size(ret)
-      #     end)
-      #   )
-
-      # start_time = DateTime.utc_now()
-
       n = length(arguments)
       # Arity mismatch: if there is one positive function with a different arity,
       # then it cannot be a subtype of the (arguments->type) functions.
@@ -1621,34 +1486,18 @@ defmodule Module.Types.Descr do
         false
       else
         # Initialize memoization cache
-        # 1. check that the domain is a subtype of the union of all
-        # the domains of the positives
-        # domain = args_to_domain(arguments)
-        # positives_domain = Enum.reduce(positives, none(), fn {args, _ret}, acc -> union(acc, args_to_domain(args)) end)
-        # if not subtype?(domain, positives_domain) do
-        #   false
-        # else
-        # 2. check that the return type is a subtype of the union of all
-        # the return types of the positives
-
         Process.put(:phi_cache, %{})
         arguments = Enum.map(arguments, &{false, &1})
-        {result, call_count} = phi(arguments, {false, return}, positives, 0)
-        cache_size = map_size(Process.get(:phi_cache, %{}))
-        # Recursive calls
-
-        result
+        phi(arguments, {false, negation(return)}, positives)
       end
-
-      # end
     end
   end
 
-  defp phi(args, {b, t}, [], call_count) do
-    {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), call_count}
+  defp phi(args, {b, t}, []) do
+    Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
   end
 
-  defp phi(args, {b, ret}, [{arguments, return} | rest_positive], call_count) do
+  defp phi(args, {b, ret}, [{arguments, return} | rest_positive]) do
     # Create cache key from function arguments
     cache_key = {args, {b, ret}, [{arguments, return} | rest_positive]}
     cache = Process.get(:phi_cache, %{})
@@ -1656,29 +1505,28 @@ defmodule Module.Types.Descr do
     case Map.get(cache, cache_key) do
       nil ->
         # Compute result and cache it
-        {result1, call_count1} =
-          phi(args, {true, intersection(ret, return)}, rest_positive, call_count + 1)
+        result1 = phi(args, {true, intersection(ret, return)}, rest_positive)
 
         if not result1 do
           Process.put(:phi_cache, Map.put(cache, cache_key, false))
-          {false, call_count}
+          false
         else
           # This doesn't stop if one intermediate result is false?
-          {result2, call_count2} =
+          result2 =
             Enum.with_index(arguments)
-            |> Enum.reduce_while({true, call_count1}, fn {type, index}, {acc_result, acc_count} ->
-              {new_result, new_count} =
+            |> Enum.reduce_while(true, fn {type, index}, acc_result ->
+              new_result =
                 List.update_at(args, index, fn {_, arg} -> {true, difference(arg, type)} end)
-                |> phi({b, ret}, rest_positive, acc_count + 1)
+                |> phi({b, ret}, rest_positive)
 
               if new_result do
-                {:cont, {acc_result and new_result, new_count}}
+                {:cont, acc_result and new_result}
               else
-                {:halt, {false, new_count}}
+                {:halt, false}
               end
             end)
 
-          result = {result1 and result2, call_count2}
+          result = result1 and result2
           Process.put(:phi_cache, Map.put(cache, cache_key, result))
           result
         end
@@ -2038,7 +1886,6 @@ defmodule Module.Types.Descr do
   end
 
   defp list_difference(dnf1, dnf2) do
-    # IO.puts("list_difference")
     Enum.reduce(dnf2, dnf1, fn {t2, last2, negs2}, acc_dnf1 ->
       last2 = list_tail_unfold(last2)
 
@@ -2068,10 +1915,6 @@ defmodule Module.Types.Descr do
   defp list_empty?(@non_empty_list_top), do: false
 
   defp list_empty?(dnf) do
-    # IO.puts("list_empty?")
-    # IO.puts("on dnf: #{inspect(dnf)}")
-    # IO.puts("the dnf has #{length(dnf)} elements")
-    # IO.puts("i count #{Enum.reduce(dnf, 0, fn {_, _, negs}, acc -> acc + length(negs) end)} negations")
     Enum.all?(dnf, fn {list_type, last_type, negs} ->
       last_type = list_tail_unfold(last_type)
 
@@ -2903,7 +2746,6 @@ defmodule Module.Types.Descr do
   # Since the algorithm is recursive, we implement the short-circuiting
   # as throw/catch.
   defp map_empty?(dnf) do
-    # IO.puts("map_empty?")
     Enum.all?(dnf, fn {tag, pos, negs} -> map_empty?(tag, pos, negs) end)
   end
 

From f01c0782a321436bce76c6a01389329872650dbe Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 25 Jun 2025 14:10:29 +0200
Subject: [PATCH 08/10] Cleanup

---
 lib/elixir/lib/module/types/descr.ex | 60 +++++++++++++---------------
 1 file changed, 27 insertions(+), 33 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 017c3c584f..ef229dcc78 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1290,25 +1290,22 @@ defmodule Module.Types.Descr do
     type_args = args_to_domain(arguments)
 
     # Optimization: short-circuits when inner loop is none() or outer loop is term()
-    result =
-      if maybe_empty? and empty?(type_args) do
-        Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
-          Enum.reduce_while(intersection_of_arrows, term(), fn
-            {_dom, _ret}, acc when acc == @none -> {:halt, acc}
-            {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
-          end)
-          |> case do
-            :term -> {:halt, :term}
-            inner -> {:cont, union(inner, acc)}
-          end
+    if maybe_empty? and empty?(type_args) do
+      Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
+        Enum.reduce_while(intersection_of_arrows, term(), fn
+          {_dom, _ret}, acc when acc == @none -> {:halt, acc}
+          {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
         end)
-      else
-        Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
-          aux_apply(acc, type_args, term(), intersection_of_arrows)
-        end)
-      end
-
-    result
+        |> case do
+          :term -> {:halt, :term}
+          inner -> {:cont, union(inner, acc)}
+        end
+      end)
+    else
+      Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
+        aux_apply(acc, type_args, term(), intersection_of_arrows)
+      end)
+    end
   end
 
   # Helper function for function application that handles the application of
@@ -1465,27 +1462,22 @@ defmodule Module.Types.Descr do
   # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
   #
   # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
-  defp all_non_empty_domains?(positives) do
-    Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
-  end
-
   defp phi_starter(arguments, return, positives) do
-    ### SPECIAL CASE: all the positives (intersection) functions have non-empty arguments
-    # In that case, checking subtyping of it with a single arrow is simply checking that the union
-    # of the domains of the positives is a supertype of the domain of the arrow
-    # and that applying the input type of the arrow to the intersection gives sth that
-    # is a subtype of the return type of the arrow
-    if all_non_empty_domains?(positives) and all_non_empty_domains?([{arguments, return}]) do
+    # Optimization: When all positive functions have non-empty domains,
+    # we can simplify the phi function check to a direct subtyping test.
+    # This avoids the expensive recursive phi computation by checking only that applying the
+    # input to the positive intersection yields a subtype of the return
+    if all_non_empty_domains?([{arguments, return} | positives]) do
       fun_apply_static(arguments, [positives], false)
       |> subtype?(return)
     else
       n = length(arguments)
-      # Arity mismatch: if there is one positive function with a different arity,
-      # then it cannot be a subtype of the (arguments->type) functions.
+      # Arity mismatch: functions with different arities cannot be subtypes
+      # of the target function type (arguments -> return)
       if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do
         false
       else
-        # Initialize memoization cache
+        # Initialize memoization cache for the recursive phi computation
         Process.put(:phi_cache, %{})
         arguments = Enum.map(arguments, &{false, &1})
         phi(arguments, {false, negation(return)}, positives)
@@ -1493,6 +1485,10 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp all_non_empty_domains?(positives) do
+    Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
+  end
+
   defp phi(args, {b, t}, []) do
     Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
   end
@@ -3798,6 +3794,4 @@ defmodule Module.Types.Descr do
   defp non_empty_map_or([head | tail], fun) do
     Enum.reduce(tail, fun.(head), &{:or, [], [&2, fun.(&1)]})
   end
-
-  # Performance tracking helpers for aux_apply
 end

From ae480873022d51ba3c02a9881fcef577e171759d Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 1 Jul 2025 17:36:40 +0200
Subject: [PATCH 09/10] Format and memoize without process cache

---
 lib/elixir/lib/module/types/descr.ex          | 45 ++++++++++---------
 .../test/elixir/module/types/descr_test.exs   |  1 +
 2 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index ef229dcc78..8d8be317d8 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1478,61 +1478,62 @@ defmodule Module.Types.Descr do
         false
       else
         # Initialize memoization cache for the recursive phi computation
-        Process.put(:phi_cache, %{})
         arguments = Enum.map(arguments, &{false, &1})
-        phi(arguments, {false, negation(return)}, positives)
+        {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{})
+        result
       end
     end
   end
 
-  defp all_non_empty_domains?(positives) do
-    Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
-  end
-
-  defp phi(args, {b, t}, []) do
-    Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
+  defp phi(args, {b, t}, [], cache) do
+    {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache}
   end
 
-  defp phi(args, {b, ret}, [{arguments, return} | rest_positive]) do
+  defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do
     # Create cache key from function arguments
     cache_key = {args, {b, ret}, [{arguments, return} | rest_positive]}
-    cache = Process.get(:phi_cache, %{})
 
     case Map.get(cache, cache_key) do
       nil ->
         # Compute result and cache it
-        result1 = phi(args, {true, intersection(ret, return)}, rest_positive)
+        {result1, cache} = phi(args, {true, intersection(ret, return)}, rest_positive, cache)
 
         if not result1 do
-          Process.put(:phi_cache, Map.put(cache, cache_key, false))
-          false
+          # Store false result in cache
+          cache = Map.put(cache, cache_key, false)
+          {false, cache}
         else
           # This doesn't stop if one intermediate result is false?
-          result2 =
+          {result2, cache} =
             Enum.with_index(arguments)
-            |> Enum.reduce_while(true, fn {type, index}, acc_result ->
-              new_result =
+            |> Enum.reduce_while({true, cache}, fn {type, index}, {acc_result, acc_cache} ->
+              {new_result, new_cache} =
                 List.update_at(args, index, fn {_, arg} -> {true, difference(arg, type)} end)
-                |> phi({b, ret}, rest_positive)
+                |> phi({b, ret}, rest_positive, acc_cache)
 
               if new_result do
-                {:cont, acc_result and new_result}
+                {:cont, {acc_result and new_result, new_cache}}
               else
-                {:halt, false}
+                {:halt, {false, new_cache}}
               end
             end)
 
           result = result1 and result2
-          Process.put(:phi_cache, Map.put(cache, cache_key, result))
-          result
+          # Store result in cache
+          cache = Map.put(cache, cache_key, result)
+          {result, cache}
         end
 
       cached_result ->
         # Return cached result
-        cached_result
+        {cached_result, cache}
     end
   end
 
+  defp all_non_empty_domains?(positives) do
+    Enum.all?(positives, fn {args, _ret} -> not empty?(args_to_domain(args)) end)
+  end
+
   defp fun_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:fun_top, _} -> :fun_top
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index bdc0a2430c..4abbbf21bd 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -674,6 +674,7 @@ defmodule Module.Types.DescrTest do
       assert subtype?(f, fun([none(), integer()], term()))
       assert subtype?(fun([none(), number()], atom()), f)
       assert subtype?(fun([tuple(), number()], atom()), f)
+
       # (none, float)->atom is not a subtype of (none, integer)->atom because float has an empty intersection with integer
       # it's only possible to find this out by doing the
       # intersection one by one.

From a53d4483f866b27b241a4c1260d4afe7b1f38e69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Thu, 3 Jul 2025 11:36:40 +0200
Subject: [PATCH 10/10] Update
 lib/elixir/test/elixir/module/types/descr_test.exs

---
 lib/elixir/test/elixir/module/types/descr_test.exs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 4abbbf21bd..7d27daa918 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -675,7 +675,8 @@ defmodule Module.Types.DescrTest do
       assert subtype?(fun([none(), number()], atom()), f)
       assert subtype?(fun([tuple(), number()], atom()), f)
 
-      # (none, float)->atom is not a subtype of (none, integer)->atom because float has an empty intersection with integer
+      # (none, float -> atom) is not a subtype of (none, integer -> atom)
+      # because float has an empty intersection with integer.
       # it's only possible to find this out by doing the
       # intersection one by one.
       refute subtype?(fun([none(), float()], atom()), f)