From 760552c9ed52e49a1b30bd5ec4b0af42f85857c6 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 29 Sep 2025 12:32:50 +0200
Subject: [PATCH 1/8] Unify fun BDD ops with the rest

---
 lib/elixir/lib/module/types/descr.ex | 63 +++-------------------------
 1 file changed, 5 insertions(+), 58 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index b1d2c02914..c755c5310c 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1610,19 +1610,9 @@ defmodule Module.Types.Descr do
       all_disjoint_arguments?(rest)
   end
 
-  defp fun_union(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_top, _} -> :bdd_top
-      {_, :bdd_top} -> :bdd_top
-      {:bdd_bot, bdd} -> bdd
-      {bdd, :bdd_bot} -> bdd
-      {{fun, l1, r1}, {fun, l2, r2}} -> {fun, fun_union(l1, l2), fun_union(r1, r2)}
-      # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it.
-      # It is the same as going down bdd1 to insert bdd1 into it.
-      # Possible opti: insert into the bdd with smallest height
-      {{fun, l, r}, bdd} -> {fun, fun_union(l, bdd), fun_union(r, bdd)}
-    end
-  end
+  defp fun_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
+
+  defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
 
   defp is_fun_top?(bdd, {{args, return}, :bdd_top, :bdd_bot}) do
     return == :term and Enum.all?(args, &(&1 == %{})) and
@@ -1636,49 +1626,7 @@ defmodule Module.Types.Descr do
       # If intersecting with the top type for that arity, no-op
       is_tuple(bdd2) and is_fun_top?(bdd2, bdd1) -> bdd2
       is_tuple(bdd1) and is_fun_top?(bdd1, bdd2) -> bdd1
-      true -> fun_bdd_intersection(bdd1, bdd2)
-    end
-  end
-
-  # Note: using this for functions instead of bdd_intersection because the printing
-  # fun_denormalize relies on the order of functions in the bdd.
-  defp fun_bdd_intersection(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      # Base cases
-      {_, :bdd_bot} ->
-        :bdd_bot
-
-      {:bdd_bot, _} ->
-        :bdd_bot
-
-      {:bdd_top, bdd} ->
-        bdd
-
-      {bdd, :bdd_top} ->
-        bdd
-
-      # Optimizations
-      # If intersecting with a single positive or negative function, we insert
-      # it at the root instead of merging the trees (this avoids going down the
-      # whole bdd).
-      {bdd, {fun, :bdd_top, :bdd_bot}} ->
-        {fun, bdd, :bdd_bot}
-
-      {bdd, {fun, :bdd_bot, :bdd_top}} ->
-        {fun, :bdd_bot, bdd}
-
-      {{fun, :bdd_top, :bdd_bot}, bdd} ->
-        {fun, bdd, :bdd_bot}
-
-      {{fun, :bdd_bot, :bdd_top}, bdd} ->
-        {fun, :bdd_bot, bdd}
-
-      # General cases
-      {{fun, l1, r1}, {fun, l2, r2}} ->
-        {fun, fun_bdd_intersection(l1, l2), fun_bdd_intersection(r1, r2)}
-
-      {{fun, l, r}, bdd} ->
-        {fun, fun_bdd_intersection(l, bdd), fun_bdd_intersection(r, bdd)}
+      true -> bdd_intersection(bdd1, bdd2)
     end
   end
 
@@ -3462,8 +3410,7 @@ defmodule Module.Types.Descr do
           # in that case, this field is not_set(), and its difference with the negative map type is empty iff
           # the negative type is optional.
           tag == :closed ->
-            is_optional_static(neg_type) or
-              map_line_empty?(tag, fields, negs)
+            is_optional_static(neg_type) or map_line_empty?(tag, fields, negs)
 
           # There may be value in common
           tag == :open ->

From a88388809bdb0a37599d56bc112e32bdd82808b9 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 29 Sep 2025 13:28:34 +0200
Subject: [PATCH 2/8] Add lazy bdd for funs. Solves spitfire perf issue.

Lazy BDDS: ternary trees (instead of binary) where the additional node encodes a lazy union.
See "COVARIANCE AND CONTRAVARIANCE:
A FRESH LOOK AT AN OLD ISSUE"
---
 lib/elixir/lib/module/types/descr.ex          | 140 +++++++++++++++---
 .../test/elixir/module/types/descr_test.exs   |   7 +
 2 files changed, 126 insertions(+), 21 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index c755c5310c..69b663f91a 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1089,7 +1089,8 @@ defmodule Module.Types.Descr do
   # Note: Function domains are expressed as tuple types. We use separate representations
   # rather than unary functions with tuple domains to handle special cases like representing
   # functions of a specific arity (e.g., (none,none->term) for arity 2).
-  defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot}
+  # NOTE: this is a ternary (lazy) BDD where the middle node encodes unions.
+  defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot, :bdd_bot}
 
   # Creates a function type from a list of inputs and an output
   # where the inputs and/or output may be dynamic.
@@ -1407,19 +1408,9 @@ defmodule Module.Types.Descr do
   # Takes all the paths from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Positive nodes are
   # those followed by a left path, negative nodes are those followed by a right path.
-  defp fun_bdd_to_dnf(bdd), do: fun_bdd_to_dnf([], [], [], bdd)
-
-  defp fun_bdd_to_dnf(acc, pos, neg, bdd) do
-    case bdd do
-      :bdd_bot ->
-        acc
-
-      :bdd_top ->
-        if fun_line_empty?(pos, neg), do: acc, else: [{pos, neg} | acc]
-
-      {fun, left, right} ->
-        fun_bdd_to_dnf(fun_bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right)
-    end
+  defp fun_bdd_to_dnf(bdd) do
+    lazy_bdd_to_dnf(bdd)
+    |> Enum.filter(fn {pos, neg} -> not fun_line_empty?(pos, neg) end)
   end
 
   # Checks if a function type is empty.
@@ -1435,7 +1426,7 @@ 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
-    bdd_to_dnf(bdd)
+    lazy_bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, neg} -> fun_line_empty?(pos, neg) end)
   end
 
@@ -1451,7 +1442,6 @@ defmodule Module.Types.Descr do
   # - `{[fun(1), fun(2)], []}` is empty (different arities)
   # - `{[fun(integer() -> atom())], [fun(none() -> term())]}` is empty
   # - `{[], _}` (representing the top function type fun()) is never empty
-  #
   defp fun_line_empty?([], _), do: false
 
   defp fun_line_empty?(positives, negatives) do
@@ -1610,9 +1600,7 @@ defmodule Module.Types.Descr do
       all_disjoint_arguments?(rest)
   end
 
-  defp fun_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
-
-  defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
+  defp fun_union(bdd1, bdd2), do: lazy_bdd_union(bdd1, bdd2)
 
   defp is_fun_top?(bdd, {{args, return}, :bdd_top, :bdd_bot}) do
     return == :term and Enum.all?(args, &(&1 == %{})) and
@@ -1626,7 +1614,7 @@ defmodule Module.Types.Descr do
       # If intersecting with the top type for that arity, no-op
       is_tuple(bdd2) and is_fun_top?(bdd2, bdd1) -> bdd2
       is_tuple(bdd1) and is_fun_top?(bdd1, bdd2) -> bdd1
-      true -> bdd_intersection(bdd1, bdd2)
+      true -> lazy_bdd_intersection(bdd1, bdd2)
     end
   end
 
@@ -1642,7 +1630,7 @@ defmodule Module.Types.Descr do
 
   defp matching_arity_right?(_, _arity), do: true
 
-  defp fun_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2)
+  defp fun_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
 
   # Converts the static and dynamic parts of descr to its quoted
   # representation. The goal here is to the opposite of fun_descr
@@ -4546,6 +4534,116 @@ defmodule Module.Types.Descr do
     end
   end
 
+  def lazy_bdd_union(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_top, _bdd} ->
+        :bdd_top
+
+      {_bdd, :bdd_top} ->
+        :bdd_top
+
+      {:bdd_bot, bdd} ->
+        bdd
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {{lit, l1, u1, r1}, {lit, l2, u2, r2}} ->
+        {lit, lazy_bdd_union(l1, l2), lazy_bdd_union(u1, u2), lazy_bdd_union(r1, r2)}
+
+      {{lit1, l1, u1, r1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
+        {lit1, l1, lazy_bdd_union(u1, bdd2), r1}
+
+      {{lit1, _, _, _} = bdd1, {lit2, l2, u2, r2}} when lit1 > lit2 ->
+        {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
+    end
+  end
+
+  def lazy_bdd_difference(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {_bdd, :bdd_top} ->
+        :bdd_bot
+
+      {:bdd_bot, _bdd} ->
+        :bdd_bot
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
+        {lit, lazy_bdd_difference(lazy_bdd_union(c1, u1), lazy_bdd_union(c2, u2)), :bdd_bot,
+         lazy_bdd_difference(lazy_bdd_union(d1, u1), lazy_bdd_union(d2, u2))}
+
+      {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
+        {lit1, lazy_bdd_difference(lazy_bdd_union(c1, u1), bdd2), :bdd_bot,
+         lazy_bdd_difference(lazy_bdd_union(d1, u1), bdd2)}
+
+      {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} when lit1 > lit2 ->
+        {lit2, lazy_bdd_difference(bdd1, lazy_bdd_union(c2, u2)), :bdd_bot,
+         lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
+
+      {:bdd_top, {lit, c2, u2, d2}} ->
+        lazy_bdd_negation({lit, c2, u2, d2})
+    end
+  end
+
+  # To do lazy negation: eliminate the union, then perform normal negation (switching leaves)
+  def lazy_bdd_negation(:bdd_top), do: :bdd_bot
+  def lazy_bdd_negation(:bdd_bot), do: :bdd_top
+
+  def lazy_bdd_negation({lit, c, u, d}) do
+    {lit, lazy_bdd_negation(lazy_bdd_union(c, u)), :bdd_bot,
+     lazy_bdd_negation(lazy_bdd_union(d, u))}
+  end
+
+  def lazy_bdd_intersection(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_top, bdd} ->
+        bdd
+
+      {bdd, :bdd_top} ->
+        bdd
+
+      {:bdd_bot, _bdd} ->
+        :bdd_bot
+
+      {_, :bdd_bot} ->
+        :bdd_bot
+
+      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
+        {lit, lazy_bdd_intersection(lazy_bdd_union(c1, u1), lazy_bdd_union(c2, u2)), :bdd_bot,
+         lazy_bdd_intersection(lazy_bdd_union(d1, u1), lazy_bdd_union(d2, u2))}
+
+      {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
+        {lit1, lazy_bdd_intersection(c1, bdd2), lazy_bdd_intersection(u1, bdd2),
+         lazy_bdd_intersection(d1, bdd2)}
+
+      {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} when lit1 > lit2 ->
+        {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
+         lazy_bdd_intersection(bdd1, d2)}
+    end
+  end
+
+  def lazy_bdd_to_dnf(bdd), do: lazy_bdd_to_dnf([], [], [], bdd)
+
+  defp lazy_bdd_to_dnf(acc, _pos, _neg, :bdd_bot), do: acc
+  defp lazy_bdd_to_dnf(acc, pos, neg, :bdd_top), do: [{pos, neg} | acc]
+
+  # Lazy node: {lit, C, U, D}  ≡  (lit ∧ C) ∪ U ∪ (¬lit ∧ D)
+  defp lazy_bdd_to_dnf(acc, pos, neg, {lit, c, u, d}) do
+    # U is a bdd in itself, we accumulate its lines first
+    lazy_bdd_to_dnf(acc, [], [], u)
+    # C-part
+    |> lazy_bdd_to_dnf([lit | pos], neg, c)
+    # D-part
+    |> lazy_bdd_to_dnf(pos, [lit | neg], d)
+  end
+
+  # Optional guard: blow up if someone passes a binary node by mistake
+  defp lazy_bdd_to_dnf(_acc, _pos, _neg, {_lit, _t, _e}) do
+    raise ArgumentError, "lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d}"
+  end
+
   ## Pairs
 
   # To simplify disjunctive normal forms of e.g., map types, it is useful to
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 507f17ebad..8374714993 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -2214,6 +2214,13 @@ defmodule Module.Types.DescrTest do
              |> intersection(fun([float()], boolean()))
              |> to_quoted_string() ==
                "(integer() -> boolean()) and (float() -> boolean())"
+
+      # Thanks to lazy BDDs, consecutive union of functions come out as the original union
+      assert fun([integer()], integer())
+             |> union(fun([float()], float()))
+             |> union(fun([pid()], pid()))
+             |> to_quoted_string() ==
+               "(integer() -> integer()) or (float() -> float()) or (pid() -> pid())"
     end
 
     test "function with optimized intersections" do

From 580fb134db237d10ba16c61e5a0136b38632772d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 30 Sep 2025 14:02:31 +0200
Subject: [PATCH 3/8] Do not require ordering when matching statics and
 dynamics

---
 lib/elixir/lib/module/types/descr.ex | 31 ++++++++++++++--------------
 1 file changed, 16 insertions(+), 15 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 69b663f91a..01071a5f4a 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1686,22 +1686,23 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # We assume those pairs are always formed in the same order
-  defp fun_denormalize_intersections(
-         [{static_args, static_return} | statics],
-         [{dynamic_args, dynamic_return} | dynamics],
-         acc
-       ) do
-    if subtype?(static_return, dynamic_return) and args_subtype?(dynamic_args, static_args) do
-      args =
-        Enum.zip_with(static_args, dynamic_args, fn static_arg, dynamic_arg ->
-          union(dynamic(static_arg), dynamic_arg)
-        end)
+  defp fun_denormalize_intersections([{static_args, static_return} | statics], dynamics, acc) do
+    dynamics
+    |> Enum.split_while(fn {dynamic_args, dynamic_return} ->
+      not (subtype?(static_return, dynamic_return) and args_subtype?(dynamic_args, static_args))
+    end)
+    |> case do
+      {_dynamics, []} ->
+        :error
 
-      return = union(dynamic(dynamic_return), static_return)
-      fun_denormalize_intersections(statics, dynamics, [{args, return} | acc])
-    else
-      :error
+      {pre, [{dynamic_args, dynamic_return} | post]} ->
+        args =
+          Enum.zip_with(static_args, dynamic_args, fn static_arg, dynamic_arg ->
+            union(dynamic(static_arg), dynamic_arg)
+          end)
+
+        return = union(dynamic(dynamic_return), static_return)
+        fun_denormalize_intersections(statics, pre ++ post, [{args, return} | acc])
     end
   end
 

From 8cd653eb54bec272392e7f6a7a62a72a984de3fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 30 Sep 2025 15:39:54 +0200
Subject: [PATCH 4/8] Fix fun_top?

---
 lib/elixir/lib/module/types/descr.ex | 32 +++++++++++++++-------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 01071a5f4a..8d226ba591 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1602,36 +1602,38 @@ defmodule Module.Types.Descr do
 
   defp fun_union(bdd1, bdd2), do: lazy_bdd_union(bdd1, bdd2)
 
-  defp is_fun_top?(bdd, {{args, return}, :bdd_top, :bdd_bot}) do
-    return == :term and Enum.all?(args, &(&1 == %{})) and
-      matching_arity_left?(bdd, length(args))
-  end
-
-  defp is_fun_top?(_, _), do: false
-
   defp fun_intersection(bdd1, bdd2) do
     cond do
       # If intersecting with the top type for that arity, no-op
-      is_tuple(bdd2) and is_fun_top?(bdd2, bdd1) -> bdd2
-      is_tuple(bdd1) and is_fun_top?(bdd1, bdd2) -> bdd1
+      is_tuple(bdd2) and fun_top?(bdd2, bdd1) -> bdd2
+      is_tuple(bdd1) and fun_top?(bdd1, bdd2) -> bdd1
       true -> lazy_bdd_intersection(bdd1, bdd2)
     end
   end
 
-  defp matching_arity_left?({{args, _return}, l, r}, arity) do
-    length(args) == arity and matching_arity_left?(l, arity) and matching_arity_right?(r, arity)
+  defp fun_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
+
+  defp fun_top?(bdd, {{args, return}, :bdd_top, :bdd_bot, :bdd_bot}) do
+    return == :term and Enum.all?(args, &(&1 == %{})) and
+      matching_arity_left?(bdd, length(args))
+  end
+
+  defp fun_top?(_, _), do: false
+
+  defp matching_arity_left?({{args, _return}, l, u, r}, arity) do
+    length(args) == arity and matching_arity_left?(l, arity) and matching_arity_left?(u, arity) and
+      matching_arity_right?(r, arity)
   end
 
   defp matching_arity_left?(_, _arity), do: true
 
-  defp matching_arity_right?({_, l, r}, arity) do
-    matching_arity_left?(l, arity) and matching_arity_right?(r, arity)
+  defp matching_arity_right?({_, l, u, r}, arity) do
+    matching_arity_left?(l, arity) and matching_arity_left?(u, arity) and
+      matching_arity_right?(r, arity)
   end
 
   defp matching_arity_right?(_, _arity), do: true
 
-  defp fun_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
-
   # Converts the static and dynamic parts of descr to its quoted
   # representation. The goal here is to the opposite of fun_descr
   # and put static and dynamic parts back together to improve

From d57266be0e995fac80fd136951c6601d20791d2d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 30 Sep 2025 16:08:52 +0200
Subject: [PATCH 5/8] Eliminate fun unions

---
 lib/elixir/lib/module/types/descr.ex | 47 +++++++++++++++++++++-------
 1 file changed, 35 insertions(+), 12 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 8d226ba591..ec0a1292c6 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1691,7 +1691,7 @@ defmodule Module.Types.Descr do
   defp fun_denormalize_intersections([{static_args, static_return} | statics], dynamics, acc) do
     dynamics
     |> Enum.split_while(fn {dynamic_args, dynamic_return} ->
-      not (subtype?(static_return, dynamic_return) and args_subtype?(dynamic_args, static_args))
+      not arrow_subtype?(static_args, static_return, dynamic_args, dynamic_return)
     end)
     |> case do
       {_dynamics, []} ->
@@ -1739,23 +1739,46 @@ defmodule Module.Types.Descr do
 
   defp fun_bdd_to_pos_dnf(bdd) do
     for {pos, _negs} <- fun_bdd_to_dnf(bdd) do
-      fun_filter_subset(pos, [])
+      fun_eliminate_intersections(pos, [])
     end
+    |> fun_eliminate_unions([])
   end
 
-  defp fun_filter_subset([], acc), do: acc
+  defp fun_eliminate_unions([], acc), do: acc
 
-  defp fun_filter_subset([{args, return} | tail], acc) do
+  defp fun_eliminate_unions([[{args, return}] | tail], acc) do
+    # If another arrow is a superset of the current one, we skip it
+    superset = fn
+      [{other_args, other_return}] ->
+        arrow_subtype?(args, return, other_args, other_return)
+
+      _ ->
+        false
+    end
+
+    if Enum.any?(tail, superset) or Enum.any?(acc, superset) do
+      fun_eliminate_unions(tail, acc)
+    else
+      fun_eliminate_unions(tail, [[{args, return}] | acc])
+    end
+  end
+
+  defp fun_eliminate_unions([head | tail], acc) do
+    fun_eliminate_unions(tail, [head | acc])
+  end
+
+  defp fun_eliminate_intersections([], acc), do: acc
+
+  defp fun_eliminate_intersections([{args, return} | tail], acc) do
     # If another arrow is a subset of the current one, we skip it
-    if Enum.any?(tail, fn {other_args, other_return} ->
-         arrow_subtype?(other_args, other_return, args, return)
-       end) or
-         Enum.any?(acc, fn {other_args, other_return} ->
-           arrow_subtype?(other_args, other_return, args, return)
-         end) do
-      fun_filter_subset(tail, acc)
+    subset = fn {other_args, other_return} ->
+      arrow_subtype?(other_args, other_return, args, return)
+    end
+
+    if Enum.any?(tail, subset) or Enum.any?(acc, subset) do
+      fun_eliminate_intersections(tail, acc)
     else
-      fun_filter_subset(tail, [{args, return} | acc])
+      fun_eliminate_intersections(tail, [{args, return} | acc])
     end
   end
 

From 4a29c67edb3a497a1e63fa17a5c7859458d80b3c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 30 Sep 2025 16:19:46 +0200
Subject: [PATCH 6/8] Remove fun_eliminate_intersections

Now it only seems to appear in artificial examples.
---
 lib/elixir/lib/module/types/descr.ex          | 20 ++-----------------
 .../test/elixir/module/types/descr_test.exs   |  2 +-
 2 files changed, 3 insertions(+), 19 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index ec0a1292c6..7cdc23ef8e 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1738,9 +1738,8 @@ defmodule Module.Types.Descr do
   end
 
   defp fun_bdd_to_pos_dnf(bdd) do
-    for {pos, _negs} <- fun_bdd_to_dnf(bdd) do
-      fun_eliminate_intersections(pos, [])
-    end
+    fun_bdd_to_dnf(bdd)
+    |> Enum.map(fn {pos, _negs} -> pos end)
     |> fun_eliminate_unions([])
   end
 
@@ -1767,21 +1766,6 @@ defmodule Module.Types.Descr do
     fun_eliminate_unions(tail, [head | acc])
   end
 
-  defp fun_eliminate_intersections([], acc), do: acc
-
-  defp fun_eliminate_intersections([{args, return} | tail], acc) do
-    # If another arrow is a subset of the current one, we skip it
-    subset = fn {other_args, other_return} ->
-      arrow_subtype?(other_args, other_return, args, return)
-    end
-
-    if Enum.any?(tail, subset) or Enum.any?(acc, subset) do
-      fun_eliminate_intersections(tail, acc)
-    else
-      fun_eliminate_intersections(tail, [{args, return} | acc])
-    end
-  end
-
   defp fun_pos_to_quoted([_ | _] = pos, opts) do
     opts = Keyword.put(opts, :skip_dynamic_for_indivisible, false)
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 8374714993..223b362823 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -2231,7 +2231,7 @@ defmodule Module.Types.DescrTest do
              |> difference(none_fun(2))
              |> intersection(none_fun(1))
              |> to_quoted_string() ==
-               "(integer() -> atom())"
+               "(none() -> term()) and (integer() -> atom())"
     end
 
     test "function with dynamic signatures" do

From a58f713a28dde15804e260d41307487edb677279 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 29 Sep 2025 18:51:22 +0200
Subject: [PATCH 7/8] Refactor bdd creation

---
 lib/elixir/lib/module/types/descr.ex | 45 ++++++++++++++++------------
 1 file changed, 26 insertions(+), 19 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 7cdc23ef8e..be041cca57 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1090,7 +1090,7 @@ defmodule Module.Types.Descr do
   # rather than unary functions with tuple domains to handle special cases like representing
   # functions of a specific arity (e.g., (none,none->term) for arity 2).
   # NOTE: this is a ternary (lazy) BDD where the middle node encodes unions.
-  defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot, :bdd_bot}
+  defp fun_new(inputs, output), do: lazy_bdd_new({inputs, output})
 
   # Creates a function type from a list of inputs and an output
   # where the inputs and/or output may be dynamic.
@@ -1847,9 +1847,7 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp list_new(list_type, last_type) do
-    {{list_type, last_type}, :bdd_top, :bdd_bot}
-  end
+  defp list_new(list_type, last_type), do: bdd_new({list_type, last_type})
 
   # Takes all the lines from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Positive nodes are
@@ -1934,10 +1932,7 @@ defmodule Module.Types.Descr do
   @compile {:inline, list_union: 2}
   defp list_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
-  defp is_list_top?({{list, tail}, :bdd_top, :bdd_bot}) do
-    list == :term and tail == :term
-  end
-
+  defp is_list_top?(list_literal(list, tail)), do: list == :term and tail == :term
   defp is_list_top?(_), do: false
 
   defp list_intersection(list_literal(list1, last1), list_literal(list2, last2)) do
@@ -2425,7 +2420,7 @@ defmodule Module.Types.Descr do
   defguardp is_optional_static(map)
             when is_map(map) and is_map_key(map, :optional)
 
-  defp map_new(tag, fields = %{}), do: {{tag, fields}, :bdd_top, :bdd_bot}
+  defp map_new(tag, fields = %{}), do: bdd_new({tag, fields})
 
   defp map_only?(descr), do: empty?(Map.delete(descr, :map))
 
@@ -2443,12 +2438,13 @@ defmodule Module.Types.Descr do
 
       nil ->
         case {{tag1, fields1}, {tag2, fields2}} do
-          {r, l} when l < r -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}}
-          {l, r} -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}}
+          {r, l} when l < r -> bdd_new(l, :bdd_top, bdd_new(r))
+          {l, r} -> bdd_new(l, :bdd_top, bdd_new(r))
         end
     end
   end
 
+  @compile {:inline, map_union: 2}
   def map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
   defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do
@@ -2549,8 +2545,8 @@ defmodule Module.Types.Descr do
 
   defp map_intersection(map_literal(tag1, fields1), map_literal(tag2, fields2)) do
     try do
-      map = map_literal_intersection(tag1, fields1, tag2, fields2)
-      {map, :bdd_top, :bdd_bot}
+      map_literal = map_literal_intersection(tag1, fields1, tag2, fields2)
+      bdd_new(map_literal)
     catch
       :empty -> :bdd_bot
     end
@@ -2762,7 +2758,7 @@ defmodule Module.Types.Descr do
 
   # Optimization: if the key does not exist in the map, avoid building
   # if_set/not_set pairs and return the popped value directly.
-  defp map_fetch_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key)
+  defp map_fetch_static(%{map: map_literal(tag_or_domains, fields)}, key)
        when not is_map_key(fields, key) do
     map_key_tag_to_type(tag_or_domains) |> pop_optional_static()
   end
@@ -2936,8 +2932,8 @@ defmodule Module.Types.Descr do
     end
   end
 
-  def map_refresh_domain(%{map: {{tag, fields}, :bdd_top, :bdd_bot}}, domain, type) do
-    %{map: {{map_refresh_tag(tag, domain, type), fields}, :bdd_top, :bdd_bot}}
+  def map_refresh_domain(%{map: map_literal(tag, fields)}, domain, type) do
+    %{map: bdd_new({map_refresh_tag(tag, domain, type), fields})}
   end
 
   def map_refresh_domain(%{map: bdd}, domain, type) do
@@ -3305,7 +3301,7 @@ defmodule Module.Types.Descr do
 
   # Takes a static map type and removes a key from it.
   # This allows the key to be put or deleted later on.
-  defp map_take_static(%{map: {{tag, fields}, :bdd_top, :bdd_bot}} = descr, key, initial)
+  defp map_take_static(%{map: map_literal(tag, fields)} = descr, key, initial)
        when not is_map_key(fields, key) do
     case tag do
       :open -> {true, maybe_union(initial, fn -> term() end), descr}
@@ -4026,6 +4022,7 @@ defmodule Module.Types.Descr do
     end
   end
 
+  @compile {:inline, tuple_union: 2}
   defp tuple_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
   defp maybe_optimize_tuple_union({tag1, pos1} = tuple1, {tag2, pos2} = tuple2) do
@@ -4470,6 +4467,10 @@ defmodule Module.Types.Descr do
 
   ## BDD helpers
 
+  # Creation of a BDD
+  defp bdd_new(literal), do: {literal, :bdd_top, :bdd_bot}
+  defp bdd_new(literal, left, right), do: {literal, left, right}
+
   # Leaf cases
   defp bdd_intersection(_, :bdd_bot), do: :bdd_bot
   defp bdd_intersection(:bdd_bot, _), do: :bdd_bot
@@ -4544,6 +4545,10 @@ defmodule Module.Types.Descr do
     end
   end
 
+  ## Lazy BDD helpers
+  defp lazy_bdd_new(literal), do: {literal, :bdd_top, :bdd_bot, :bdd_bot}
+  defp lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}
+
   def lazy_bdd_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:bdd_top, _bdd} ->
@@ -4650,8 +4655,10 @@ defmodule Module.Types.Descr do
   end
 
   # Optional guard: blow up if someone passes a binary node by mistake
-  defp lazy_bdd_to_dnf(_acc, _pos, _neg, {_lit, _t, _e}) do
-    raise ArgumentError, "lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d}"
+  defp lazy_bdd_to_dnf(_acc, _pos, _neg, {_lit, _t, _e} = node) do
+    raise ArgumentError,
+          "lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d} #{inspect(node)}\n
+          #{inspect(Process.info(self(), :current_stacktrace))}"
   end
 
   ## Pairs

From 3ab4ee1c06376e9d316f467a00172820b904aaa3 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 30 Sep 2025 16:03:23 +0200
Subject: [PATCH 8/8] Prepare for lazy BDD switch

Remark: best 1.19 performance, similar to 1.18 speed!
---
 lib/elixir/lib/module/types/descr.ex | 178 +++++++++++++++------------
 1 file changed, 98 insertions(+), 80 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index be041cca57..e9e8bae9eb 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -27,6 +27,7 @@ defmodule Module.Types.Descr do
   @bit_top (1 <<< 7) - 1
   @bit_number @bit_integer ||| @bit_float
 
+  # Remark: those use AST for BDDs
   defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot]}
   defmacrop tuple_literal(tag, elements), do: {:{}, [], [{tag, elements}, :bdd_top, :bdd_bot]}
   defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot]}
@@ -48,6 +49,7 @@ defmodule Module.Types.Descr do
     {:domain_key, :list}
   ]
 
+  # Remark: those are explicit BDD constructors. The functional constructors are `bdd_new/1` and `bdd_new/3`.
   @fun_top :bdd_top
   @atom_top {:negation, :sets.new(version: 2)}
   @map_top {{:open, %{}}, :bdd_top, :bdd_bot}
@@ -1849,30 +1851,32 @@ defmodule Module.Types.Descr do
 
   defp list_new(list_type, last_type), do: bdd_new({list_type, last_type})
 
+  defp non_empty_list_literals_intersection(list_literals) do
+    try do
+      Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} ->
+        {non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)}
+      end)
+    catch
+      :empty -> :empty
+    end
+  end
+
   # Takes all the lines from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Positive nodes are
   # those followed by a left path, negative nodes are those followed by a right path.
-  defp list_bdd_to_dnf(bdd), do: list_bdd_to_dnf([], {:term, :term}, [], bdd)
-
-  defp list_bdd_to_dnf(acc, {list_acc, tail_acc} = pos, negs, bdd) do
-    case bdd do
-      :bdd_bot ->
-        acc
-
-      :bdd_top ->
-        if list_line_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc]
-
-      {{list, tail} = next_list, left, right} ->
-        try do
-          li = non_empty_intersection!(list_acc, list)
-          la = non_empty_intersection!(tail_acc, tail)
+  defp list_bdd_to_dnf(bdd) do
+    bdd_to_dnf(bdd)
+    |> Enum.reduce([], fn {pos_list, neg_list}, acc ->
+      case non_empty_list_literals_intersection(pos_list) do
+        :empty ->
+          acc
 
-          list_bdd_to_dnf(acc, {li, la}, negs, left)
-          |> list_bdd_to_dnf(pos, [next_list | negs], right)
-        catch
-          :empty -> list_bdd_to_dnf(acc, pos, [next_list | negs], right)
-        end
-    end
+        {list, last} ->
+          if list_line_empty?(list, last, neg_list),
+            do: acc,
+            else: [{{list, last}, neg_list} | acc]
+      end
+    end)
   end
 
   # Takes all the lines from the root to the leaves finishing with a 1,
@@ -1882,40 +1886,51 @@ defmodule Module.Types.Descr do
   # if the negative list type is a supertype of the positive list type. In that case,
   # we can remove the negative last type from the positive one.
   # (If this subtracted type was empty, the whole type would be empty)
-  defp list_bdd_to_pos_dnf(bdd), do: list_bdd_to_pos_dnf(:term, :term, bdd, [])
+  defp list_bdd_to_pos_dnf(bdd) do
+    bdd_to_dnf(bdd)
+    |> Enum.reduce([], fn {pos_list, neg_list}, acc ->
+      case non_empty_list_literals_intersection(pos_list) do
+        :empty ->
+          acc
 
-  defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do
-    case bdd do
-      :bdd_bot ->
-        lines_acc
+        {list, last} ->
+          if list_line_empty?(list, last, neg_list), do: acc, else: [{list, last} | acc]
+      end
+    end)
+  end
 
-      :bdd_top ->
-        [{list_acc, last_acc} | lines_acc]
+  # defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do
+  #   case bdd do
+  #     :bdd_bot ->
+  #       lines_acc
 
-      {{list, last}, left, right} ->
-        # Case 1: count the list_type negatively. Check condition when it affects the positive one.
-        lines_acc =
-          if subtype?(list_acc, list) do
-            last = difference(last_acc, last)
+  #     :bdd_top ->
+  #       [{list_acc, last_acc} | lines_acc]
 
-            if empty?(last),
-              do: lines_acc,
-              else: list_bdd_to_pos_dnf(list_acc, last, right, lines_acc)
-          else
-            list_bdd_to_pos_dnf(list_acc, last_acc, right, lines_acc)
-          end
+  #     {{list, last}, left, right} ->
+  #       # Case 1: count the list_type negatively. Check condition when it affects the positive one.
+  #       lines_acc =
+  #         if subtype?(list_acc, list) do
+  #           last = difference(last_acc, last)
 
-        # Case 2: count the list_type positively.
-        list_acc = intersection(list_acc, list)
-        last_acc = intersection(last_acc, last)
+  #           if empty?(last),
+  #             do: lines_acc,
+  #             else: list_bdd_to_pos_dnf(list_acc, last, right, lines_acc)
+  #         else
+  #           list_bdd_to_pos_dnf(list_acc, last_acc, right, lines_acc)
+  #         end
 
-        if empty?(list_acc) or empty?(last_acc) do
-          lines_acc
-        else
-          list_bdd_to_pos_dnf(list_acc, last_acc, left, lines_acc)
-        end
-    end
-  end
+  #       # Case 2: count the list_type positively.
+  #       list_acc = intersection(list_acc, list)
+  #       last_acc = intersection(last_acc, last)
+
+  #       if empty?(list_acc) or empty?(last_acc) do
+  #         lines_acc
+  #       else
+  #         list_bdd_to_pos_dnf(list_acc, last_acc, left, lines_acc)
+  #       end
+  #   end
+  # end
 
   defp list_pop_dynamic(:term), do: {false, :term}
 
@@ -1983,16 +1998,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp non_empty_list_literals_intersection(list_literals) do
-    try do
-      Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} ->
-        {non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)}
-      end)
-    catch
-      :empty -> :empty
-    end
-  end
-
   defp list_empty?(@non_empty_list_top), do: false
 
   defp list_empty?(bdd) do
@@ -4119,30 +4124,21 @@ defmodule Module.Types.Descr do
 
   # Transforms a bdd into a union of tuples with no negations.
   # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates
-  defp tuple_normalize(bdd), do: tuple_normalize([], {:open, []}, [], bdd)
-
-  defp tuple_normalize(acc, {tag, elements} = tuple, negs, bdd) do
-    case bdd do
-      :bdd_bot ->
-        acc
-
-      :bdd_top ->
-        if tuple_line_empty?(tag, elements, negs) do
+  defp tuple_normalize(bdd) do
+    bdd_to_dnf(bdd)
+    |> Enum.reduce([], fn {positive_tuples, negative_tuples}, acc ->
+      case non_empty_tuple_literals_intersection(positive_tuples) do
+        :empty ->
           acc
-        else
-          tuple_eliminate_negations(tag, elements, negs) |> tuple_dnf_union(acc)
-        end
 
-      {{next_tag, next_elements} = next_tuple, left, right} ->
-        # If an intersection of tuples is empty, the line is empty and we skip it.
-        acc =
-          case tuple_literal_intersection(tag, elements, next_tag, next_elements) do
-            :empty -> acc
-            new_tuple -> tuple_normalize(acc, new_tuple, negs, left)
+        {tag, elements} ->
+          if tuple_line_empty?(tag, elements, negative_tuples) do
+            acc
+          else
+            tuple_eliminate_negations(tag, elements, negative_tuples) |> tuple_dnf_union(acc)
           end
-
-        tuple_normalize(acc, tuple, [next_tuple | negs], right)
-    end
+      end
+    end)
   end
 
   # Given a union of tuples, fuses the tuple unions when possible,
@@ -4467,7 +4463,16 @@ defmodule Module.Types.Descr do
 
   ## BDD helpers
 
-  # Creation of a BDD
+  # defp bdd_new(literal), do: lazy_bdd_new(literal)
+  # defp bdd_new(literal, left, right), do: lazy_bdd_new(literal, left, right)
+
+  # defp bdd_intersection(bdd1, bdd2), do: lazy_bdd_intersection(bdd1, bdd2)
+  # defp bdd_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
+  # defp bdd_union(bdd1, bdd2), do: lazy_bdd_union(bdd1, bdd2)
+  # defp bdd_negation(bdd), do: lazy_bdd_negation(bdd)
+  # defp bdd_map(bdd, fun), do: lazy_bdd_map(bdd, fun)
+  # defp bdd_to_dnf(bdd), do: lazy_bdd_to_dnf(bdd)
+
   defp bdd_new(literal), do: {literal, :bdd_top, :bdd_bot}
   defp bdd_new(literal, left, right), do: {literal, left, right}
 
@@ -4661,6 +4666,19 @@ defmodule Module.Types.Descr do
           #{inspect(Process.info(self(), :current_stacktrace))}"
   end
 
+  defp lazy_bdd_map(bdd, fun) do
+    case bdd do
+      :bdd_bot ->
+        :bdd_bot
+
+      :bdd_top ->
+        :bdd_top
+
+      {literal, left, union, right} ->
+        {fun.(literal), bdd_map(left, fun), bdd_map(union, fun), bdd_map(right, fun)}
+    end
+  end
+
   ## Pairs
 
   # To simplify disjunctive normal forms of e.g., map types, it is useful to