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 01/24] 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 02/24] 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 03/24] 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 04/24] 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 05/24] 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 06/24] 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 07/24] 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 08/24] 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

From c92813e03f7653e58a484626f61d71aa844fecc9 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 1 Oct 2025 14:50:18 +0200
Subject: [PATCH 09/24] Use only lazy BDDs for all types

---
 lib/elixir/lib/module/types/descr.ex | 235 +++++++++++++--------------
 1 file changed, 114 insertions(+), 121 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e9e8bae9eb..61a755948e 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -28,9 +28,12 @@ defmodule Module.Types.Descr do
   @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]}
+  defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot, :bdd_bot]}
+
+  defmacrop tuple_literal(tag, elements),
+    do: {:{}, [], [{tag, elements}, :bdd_top, :bdd_bot, :bdd_bot]}
+
+  defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot, :bdd_bot]}
 
   defmacrop domain_key(key), do: {:domain_key, key}
 
@@ -52,10 +55,10 @@ defmodule Module.Types.Descr do
   # 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}
-  @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot}
-  @tuple_top {{:open, []}, :bdd_top, :bdd_bot}
-  @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot}
+  @map_top {{:open, %{}}, :bdd_top, :bdd_bot, :bdd_bot}
+  @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot, :bdd_bot}
+  @tuple_top {{:open, []}, :bdd_top, :bdd_bot, :bdd_bot}
+  @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot, :bdd_bot}
 
   @none %{}
   @term %{
@@ -1899,39 +1902,6 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  # defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do
-  #   case bdd do
-  #     :bdd_bot ->
-  #       lines_acc
-
-  #     :bdd_top ->
-  #       [{list_acc, last_acc} | 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)
-
-  #           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
-
-  #       # 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}
 
   defp list_pop_dynamic(descr) do
@@ -4463,96 +4433,112 @@ defmodule Module.Types.Descr do
 
   ## BDD helpers
 
-  # defp bdd_new(literal), do: lazy_bdd_new(literal)
-  # defp bdd_new(literal, left, right), do: lazy_bdd_new(literal, left, right)
+  # TODO: find out if using lazy BDDs everywhere is worth it
+  # Remark: uncomment those, and swap the macro and attribute definitions to use lazy BDDs.
+  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_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}
+  defp lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}
 
-  # Leaf cases
-  defp bdd_intersection(_, :bdd_bot), do: :bdd_bot
-  defp bdd_intersection(:bdd_bot, _), do: :bdd_bot
-  defp bdd_intersection(:bdd_top, other), do: other
-  defp bdd_intersection(other, :bdd_top), do: other
+  defp lazy_bdd_map(bdd, fun) do
+    case bdd do
+      :bdd_bot ->
+        :bdd_bot
 
-  # Internal-node cases
-  # Keeping the invariant that literals are ordered ensures nodes are not duplicated down
-  defp bdd_intersection({lit, l1, r1}, {lit, l2, r2}),
-    do: {lit, bdd_intersection(l1, l2), bdd_intersection(r1, r2)}
+      :bdd_top ->
+        :bdd_top
 
-  defp bdd_intersection({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-    do: {lit1, bdd_intersection(l1, bdd2), bdd_intersection(r1, bdd2)}
+      {literal, left, union, right} ->
+        {fun.(literal), bdd_map(left, fun), bdd_map(union, fun), bdd_map(right, fun)}
+    end
+  end
 
-  defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-    do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)}
+  # defp bdd_new(literal), do: {literal, :bdd_top, :bdd_bot}
+  # defp bdd_new(literal, left, right), do: {literal, left, right}
 
-  defp bdd_difference(:bdd_bot, _), do: :bdd_bot
-  defp bdd_difference(other, :bdd_bot), do: other
-  defp bdd_difference(:bdd_top, other), do: bdd_negation(other)
-  defp bdd_difference(_, :bdd_top), do: :bdd_bot
+  # # Leaf cases
+  # defp bdd_intersection(_, :bdd_bot), do: :bdd_bot
+  # defp bdd_intersection(:bdd_bot, _), do: :bdd_bot
+  # defp bdd_intersection(:bdd_top, other), do: other
+  # defp bdd_intersection(other, :bdd_top), do: other
 
-  defp bdd_difference({lit, l1, r1}, {lit, l2, r2}),
-    do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)}
+  # # Internal-node cases
+  # # Keeping the invariant that literals are ordered ensures nodes are not duplicated down
+  # defp bdd_intersection({lit, l1, r1}, {lit, l2, r2}),
+  #   do: {lit, bdd_intersection(l1, l2), bdd_intersection(r1, r2)}
 
-  defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-    do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)}
+  # defp bdd_intersection({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
+  #   do: {lit1, bdd_intersection(l1, bdd2), bdd_intersection(r1, bdd2)}
 
-  defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-    do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)}
+  # defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
+  #   do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)}
 
-  defp bdd_negation(:bdd_bot), do: :bdd_top
-  defp bdd_negation(:bdd_top), do: :bdd_bot
-  defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)}
+  # defp bdd_difference(:bdd_bot, _), do: :bdd_bot
+  # defp bdd_difference(other, :bdd_bot), do: other
+  # defp bdd_difference(:bdd_top, other), do: bdd_negation(other)
+  # defp bdd_difference(_, :bdd_top), do: :bdd_bot
 
-  defp bdd_union(:bdd_top, _), do: :bdd_top
-  defp bdd_union(_, :bdd_top), do: :bdd_top
-  defp bdd_union(:bdd_bot, other), do: other
-  defp bdd_union(other, :bdd_bot), do: other
-  defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)}
+  # defp bdd_difference({lit, l1, r1}, {lit, l2, r2}),
+  #   do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)}
 
-  # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree
-  defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-    do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)}
+  # defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
+  #   do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)}
 
-  defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-    do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)}
+  # defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
+  #   do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)}
 
-  defp bdd_map(bdd, fun) do
-    case bdd do
-      :bdd_bot -> :bdd_bot
-      :bdd_top -> :bdd_top
-      {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)}
-    end
-  end
+  # defp bdd_negation(:bdd_bot), do: :bdd_top
+  # defp bdd_negation(:bdd_top), do: :bdd_bot
+  # defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)}
 
-  defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
+  # defp bdd_union(:bdd_top, _), do: :bdd_top
+  # defp bdd_union(_, :bdd_top), do: :bdd_top
+  # defp bdd_union(:bdd_bot, other), do: other
+  # defp bdd_union(other, :bdd_bot), do: other
+  # defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)}
 
-  defp bdd_to_dnf(acc, pos, neg, bdd) do
-    case bdd do
-      :bdd_bot ->
-        acc
+  # # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree
+  # defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
+  #   do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)}
 
-      :bdd_top ->
-        [{pos, neg} | acc]
+  # defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
+  #   do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)}
+
+  # defp bdd_map(bdd, fun) do
+  #   case bdd do
+  #     :bdd_bot -> :bdd_bot
+  #     :bdd_top -> :bdd_top
+  #     {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)}
+  #   end
+  # end
 
-      {fun, :bdd_top, right} ->
-        bdd_to_dnf([{[fun | pos], neg} | acc], pos, neg, right)
+  # defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
 
-      {fun, left, right} ->
-        bdd_to_dnf(bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right)
-    end
-  end
+  # defp bdd_to_dnf(acc, pos, neg, bdd) do
+  #   case bdd do
+  #     :bdd_bot ->
+  #       acc
+
+  #     :bdd_top ->
+  #       [{pos, neg} | acc]
+
+  #     {fun, :bdd_top, right} ->
+  #       bdd_to_dnf([{[fun | pos], neg} | acc], pos, neg, right)
+
+  #     {fun, left, right} ->
+  #       bdd_to_dnf(bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right)
+  #   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
@@ -4577,6 +4563,11 @@ defmodule Module.Types.Descr do
       {{lit1, _, _, _} = bdd1, {lit2, l2, u2, r2}} when lit1 > lit2 ->
         {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
     end
+    |> case do
+      {lit, l, :bdd_top, r} -> :bdd_top
+      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      bdd -> bdd
+    end
   end
 
   def lazy_bdd_difference(bdd1, bdd2) do
@@ -4605,15 +4596,25 @@ defmodule Module.Types.Descr do
       {:bdd_top, {lit, c2, u2, d2}} ->
         lazy_bdd_negation({lit, c2, u2, d2})
     end
+    |> case do
+      {lit, l, :bdd_top, r} -> :bdd_top
+      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      bdd -> bdd
+    end
   end
 
-  # To do lazy negation: eliminate the union, then perform normal negation (switching leaves)
+  # 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))}
+    |> case do
+      {lit, l, :bdd_top, r} -> :bdd_top
+      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      bdd -> bdd
+    end
   end
 
   def lazy_bdd_intersection(bdd1, bdd2) do
@@ -4642,6 +4643,11 @@ defmodule Module.Types.Descr do
         {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
          lazy_bdd_intersection(bdd1, d2)}
     end
+    |> case do
+      {lit, l, :bdd_top, r} -> :bdd_top
+      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      bdd -> bdd
+    end
   end
 
   def lazy_bdd_to_dnf(bdd), do: lazy_bdd_to_dnf([], [], [], bdd)
@@ -4666,19 +4672,6 @@ 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

From 0a70b0fbaa5bea8fd42916fa037cbc97f0834c0d Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 1 Oct 2025 15:56:30 +0200
Subject: [PATCH 10/24] Fix lazy_bdd_to_dnf

---
 lib/elixir/lib/module/types/descr.ex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 61a755948e..dbb0334439 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4658,7 +4658,7 @@ defmodule Module.Types.Descr do
   # 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)
+    lazy_bdd_to_dnf(acc, pos, neg, u)
     # C-part
     |> lazy_bdd_to_dnf([lit | pos], neg, c)
     # D-part

From 9b1444f0f6569321498092a78f8ee973c85d8e24 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 1 Oct 2025 16:23:23 +0200
Subject: [PATCH 11/24] Map union fix

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index dbb0334439..7716e50c2c 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2408,14 +2408,8 @@ defmodule Module.Types.Descr do
 
   def map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do
     case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do
-      {tag, fields, []} ->
-        map_literal(tag, fields)
-
-      nil ->
-        case {{tag1, fields1}, {tag2, fields2}} do
-          {r, l} when l < r -> bdd_new(l, :bdd_top, bdd_new(r))
-          {l, r} -> bdd_new(l, :bdd_top, bdd_new(r))
-        end
+      {tag, fields, []} -> map_literal(tag, fields)
+      nil -> bdd_union(map_literal(tag1, fields1), map_literal(tag2, fields2))
     end
   end
 
@@ -4436,16 +4430,16 @@ defmodule Module.Types.Descr do
   # TODO: find out if using lazy BDDs everywhere is worth it
   # Remark: uncomment those, and swap the macro and attribute definitions to use lazy BDDs.
   defp bdd_new(literal), do: lazy_bdd_new(literal)
-  defp bdd_new(literal, left, right), do: lazy_bdd_new(literal, left, right)
+  # 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_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 lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}
+  # defp lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}
 
   defp lazy_bdd_map(bdd, fun) do
     case bdd do
@@ -4564,8 +4558,8 @@ defmodule Module.Types.Descr do
         {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
     end
     |> case do
-      {lit, l, :bdd_top, r} -> :bdd_top
-      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      {_lit, _l, :bdd_top, _r} -> :bdd_top
+      {_lit, l, u, l} -> lazy_bdd_union(l, u)
       bdd -> bdd
     end
   end
@@ -4597,8 +4591,8 @@ defmodule Module.Types.Descr do
         lazy_bdd_negation({lit, c2, u2, d2})
     end
     |> case do
-      {lit, l, :bdd_top, r} -> :bdd_top
-      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      {_lit, _l, :bdd_top, _r} -> :bdd_top
+      {_lit, l, u, l} -> lazy_bdd_union(l, u)
       bdd -> bdd
     end
   end
@@ -4611,8 +4605,7 @@ defmodule Module.Types.Descr do
     {lit, lazy_bdd_negation(lazy_bdd_union(c, u)), :bdd_bot,
      lazy_bdd_negation(lazy_bdd_union(d, u))}
     |> case do
-      {lit, l, :bdd_top, r} -> :bdd_top
-      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      {_lit, l, u, l} -> lazy_bdd_union(l, u)
       bdd -> bdd
     end
   end
@@ -4644,8 +4637,8 @@ defmodule Module.Types.Descr do
          lazy_bdd_intersection(bdd1, d2)}
     end
     |> case do
-      {lit, l, :bdd_top, r} -> :bdd_top
-      {lit, l, u, l} -> lazy_bdd_union(l, u)
+      {_lit, _l, :bdd_top, _r} -> :bdd_top
+      {_lit, l, u, l} -> lazy_bdd_union(l, u)
       bdd -> bdd
     end
   end

From 5a8664b2c64711d871b7ebe4d8fd5cee458a176d Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 1 Oct 2025 17:45:49 +0200
Subject: [PATCH 12/24] Fix lazy_bdd_difference :bdd_top, bdd case

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 7716e50c2c..9a695813c6 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1936,10 +1936,6 @@ defmodule Module.Types.Descr do
       is_list_top?(bdd2) and is_tuple(bdd1) -> bdd1
       true -> bdd_intersection(bdd1, bdd2)
     end
-    |> case do
-      {_, :bdd_bot, :bdd_bot} -> :bdd_bot
-      bdd -> bdd
-    end
   end
 
   # Computes the difference between two BDD (Binary Decision Diagram) list types.
@@ -1960,13 +1956,7 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp list_difference(bdd1, bdd2) do
-    bdd_difference(bdd1, bdd2)
-    |> case do
-      {_, :bdd_bot, :bdd_bot} -> :bdd_bot
-      bdd -> bdd
-    end
-  end
+  defp list_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2)
 
   defp list_empty?(@non_empty_list_top), do: false
 
@@ -4534,6 +4524,19 @@ defmodule Module.Types.Descr do
   ## Lazy BDD helpers
   defp lazy_bdd_new(literal), do: {literal, :bdd_top, :bdd_bot, :bdd_bot}
 
+  # defp bdd_union(:bdd_top, _), do: :bdd_top
+  # defp bdd_union(_, :bdd_top), do: :bdd_top
+  # defp bdd_union(:bdd_bot, other), do: other
+  # defp bdd_union(other, :bdd_bot), do: other
+  # defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)}
+
+  # # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree
+  # defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
+  #   do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)}
+
+  # defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
+  #   do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)}
+
   def lazy_bdd_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:bdd_top, _bdd} ->
@@ -4588,7 +4591,7 @@ defmodule Module.Types.Descr do
          lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
 
       {:bdd_top, {lit, c2, u2, d2}} ->
-        lazy_bdd_negation({lit, c2, u2, d2})
+        lazy_bdd_negation({lit, lazy_bdd_union(c2, u2), :bdd_bot, lazy_bdd_union(d2, u2)})
     end
     |> case do
       {_lit, _l, :bdd_top, _r} -> :bdd_top

From c329b4104a452d0ef33b788edb7506a08b45805f Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 1 Oct 2025 17:47:41 +0200
Subject: [PATCH 13/24] Reverse negation change

---
 lib/elixir/lib/module/types/descr.ex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 9a695813c6..41cfe35378 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4591,7 +4591,7 @@ defmodule Module.Types.Descr do
          lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
 
       {:bdd_top, {lit, c2, u2, d2}} ->
-        lazy_bdd_negation({lit, lazy_bdd_union(c2, u2), :bdd_bot, lazy_bdd_union(d2, u2)})
+        lazy_bdd_negation({lit, c2, u2, d2})
     end
     |> case do
       {_lit, _l, :bdd_top, _r} -> :bdd_top

From cfb833f0cce657263cce16826c56842eaf2b0224 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Wed, 1 Oct 2025 17:46:04 +0200
Subject: [PATCH 14/24] Eliminate last redundant guards

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 41cfe35378..2cfc0ac92c 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4557,7 +4557,7 @@ defmodule Module.Types.Descr do
       {{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 ->
+      {{lit1, _, _, _} = bdd1, {lit2, l2, u2, r2}} ->
         {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
     end
     |> case do
@@ -4586,7 +4586,7 @@ defmodule Module.Types.Descr do
         {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 ->
+      {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} ->
         {lit2, lazy_bdd_difference(bdd1, lazy_bdd_union(c2, u2)), :bdd_bot,
          lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
 
@@ -4635,7 +4635,7 @@ defmodule Module.Types.Descr do
         {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 ->
+      {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} ->
         {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
          lazy_bdd_intersection(bdd1, d2)}
     end

From 890c75a1617364fc881c4307383107469c8211ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 02:16:04 +0200
Subject: [PATCH 15/24] Postpone union dematerialization on intersections
 whenever possible

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 2cfc0ac92c..e85f4c4ef9 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4560,11 +4560,6 @@ defmodule Module.Types.Descr do
       {{lit1, _, _, _} = bdd1, {lit2, l2, u2, r2}} ->
         {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
     end
-    |> case do
-      {_lit, _l, :bdd_top, _r} -> :bdd_top
-      {_lit, l, u, l} -> lazy_bdd_union(l, u)
-      bdd -> bdd
-    end
   end
 
   def lazy_bdd_difference(bdd1, bdd2) do
@@ -4579,8 +4574,13 @@ defmodule Module.Types.Descr do
         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))}
+        if u1 == u2 do
+          {lit, lazy_bdd_difference(c1, lazy_bdd_union(c2, u2)), :bdd_bot,
+           lazy_bdd_difference(d1, lazy_bdd_union(d2, u2))}
+        else
+          {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))}
+        end
 
       {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
         {lit1, lazy_bdd_difference(lazy_bdd_union(c1, u1), bdd2), :bdd_bot,
@@ -4593,11 +4593,6 @@ defmodule Module.Types.Descr do
       {:bdd_top, {lit, c2, u2, d2}} ->
         lazy_bdd_negation({lit, c2, u2, d2})
     end
-    |> case do
-      {_lit, _l, :bdd_top, _r} -> :bdd_top
-      {_lit, l, u, l} -> lazy_bdd_union(l, u)
-      bdd -> bdd
-    end
   end
 
   # Lazy negation: eliminate the union, then perform normal negation (switching leaves)
@@ -4607,10 +4602,6 @@ defmodule Module.Types.Descr do
   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))}
-    |> case do
-      {_lit, l, u, l} -> lazy_bdd_union(l, u)
-      bdd -> bdd
-    end
   end
 
   def lazy_bdd_intersection(bdd1, bdd2) do
@@ -4627,9 +4618,24 @@ defmodule Module.Types.Descr do
       {_, :bdd_bot} ->
         :bdd_bot
 
+      # If possible, keep unions without spreading them down
+      {{lit1, c1, u1, :bdd_bot}, bdd2} when u1 != :bdd_bot ->
+        lazy_bdd_intersection({lit1, c1, :bdd_bot, :bdd_bot}, bdd2)
+        |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
+
+      {bdd1, {lit2, c2, u2, :bdd_bot}} when u2 != :bdd_bot ->
+        lazy_bdd_intersection({lit2, c2, :bdd_bot, :bdd_bot}, bdd1)
+        |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
+
       {{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))}
+        # Avoid doing the same operation multiple times when possible
+        if u1 == u2 do
+          {lit, lazy_bdd_union(u1, lazy_bdd_intersection(c1, c2)), :bdd_bot,
+           lazy_bdd_union(u2, lazy_bdd_intersection(d1, d2))}
+        else
+          {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))}
+        end
 
       {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
         {lit1, lazy_bdd_intersection(c1, bdd2), lazy_bdd_intersection(u1, bdd2),
@@ -4639,11 +4645,6 @@ defmodule Module.Types.Descr do
         {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
          lazy_bdd_intersection(bdd1, d2)}
     end
-    |> case do
-      {_lit, _l, :bdd_top, _r} -> :bdd_top
-      {_lit, l, u, l} -> lazy_bdd_union(l, u)
-      bdd -> bdd
-    end
   end
 
   def lazy_bdd_to_dnf(bdd), do: lazy_bdd_to_dnf([], [], [], bdd)

From c1ff7138d2a781ee6e513aee8215e0f2040ec950 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 02:18:34 +0200
Subject: [PATCH 16/24] Move clause around for consistency

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e85f4c4ef9..cc9e80ad3c 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4573,6 +4573,9 @@ defmodule Module.Types.Descr do
       {bdd, :bdd_bot} ->
         bdd
 
+      {:bdd_top, {lit, c2, u2, d2}} ->
+        lazy_bdd_negation({lit, c2, u2, d2})
+
       {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
         if u1 == u2 do
           {lit, lazy_bdd_difference(c1, lazy_bdd_union(c2, u2)), :bdd_bot,
@@ -4589,9 +4592,6 @@ defmodule Module.Types.Descr do
       {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} ->
         {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
 

From 64bcfd172a2db599e33c82154bfceb6d3387d7d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 02:33:06 +0200
Subject: [PATCH 17/24] Refactor

---
 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 cc9e80ad3c..7553436f79 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4618,23 +4618,25 @@ defmodule Module.Types.Descr do
       {_, :bdd_bot} ->
         :bdd_bot
 
-      # If possible, keep unions without spreading them down
-      {{lit1, c1, u1, :bdd_bot}, bdd2} when u1 != :bdd_bot ->
-        lazy_bdd_intersection({lit1, c1, :bdd_bot, :bdd_bot}, bdd2)
-        |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
+      {{lit, c1, u1, d1} = bdd1, {lit, c2, u2, d2} = bdd2} ->
+        cond do
+          # If possible, keep unions without dematerializing them down
+          d1 == :bdd_bot and u1 != :bdd_bot ->
+            {lit, lazy_bdd_intersection(c1, lazy_bdd_union(c2, u2)), :bdd_bot, :bdd_bot}
+            |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
 
-      {bdd1, {lit2, c2, u2, :bdd_bot}} when u2 != :bdd_bot ->
-        lazy_bdd_intersection({lit2, c2, :bdd_bot, :bdd_bot}, bdd1)
-        |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
+          d2 == :bdd_bot and u2 != :bdd_bot ->
+            {lit, lazy_bdd_intersection(c2, lazy_bdd_union(c1, u1)), :bdd_bot, :bdd_bot}
+            |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
 
-      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
-        # Avoid doing the same operation multiple times when possible
-        if u1 == u2 do
-          {lit, lazy_bdd_union(u1, lazy_bdd_intersection(c1, c2)), :bdd_bot,
-           lazy_bdd_union(u2, lazy_bdd_intersection(d1, d2))}
-        else
-          {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))}
+          # Avoid doing the same operation multiple times when possible
+          u1 == u2 ->
+            {lit, lazy_bdd_union(u1, lazy_bdd_intersection(c1, c2)), :bdd_bot,
+             lazy_bdd_union(u2, lazy_bdd_intersection(d1, d2))}
+
+          true ->
+            {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))}
         end
 
       {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->

From 5002c903711238f521701399fa905727607168d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 03:06:20 +0200
Subject: [PATCH 18/24] More cleanups

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 7553436f79..4d5e865e09 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4619,36 +4619,35 @@ defmodule Module.Types.Descr do
         :bdd_bot
 
       {{lit, c1, u1, d1} = bdd1, {lit, c2, u2, d2} = bdd2} ->
-        cond do
-          # If possible, keep unions without dematerializing them down
-          d1 == :bdd_bot and u1 != :bdd_bot ->
-            {lit, lazy_bdd_intersection(c1, lazy_bdd_union(c2, u2)), :bdd_bot, :bdd_bot}
-            |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
-
-          d2 == :bdd_bot and u2 != :bdd_bot ->
-            {lit, lazy_bdd_intersection(c2, lazy_bdd_union(c1, u1)), :bdd_bot, :bdd_bot}
-            |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
-
-          # Avoid doing the same operation multiple times when possible
-          u1 == u2 ->
-            {lit, lazy_bdd_union(u1, lazy_bdd_intersection(c1, c2)), :bdd_bot,
-             lazy_bdd_union(u2, lazy_bdd_intersection(d1, d2))}
-
-          true ->
-            {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))}
+        # If possible, keep unions without dematerializing them down.
+        # We rely on the fact that (t1 ∨ t2) ∧ t3 is the same as (t1 ∧ t3) ∨ (t2 ∧ t3).
+        if u1 != :bdd_bot do
+          {lit, lazy_bdd_intersection_union(c1, c2, u2), :bdd_bot,
+           lazy_bdd_intersection_union(d1, d2, u2)}
+          |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
+        else
+          {lit, lazy_bdd_intersection_union(c2, c1, u1), :bdd_bot,
+           lazy_bdd_intersection_union(d2, d1, u1)}
+          |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
         end
 
       {{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}} ->
+      {bdd1, {lit2, c2, u2, d2}} ->
         {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
          lazy_bdd_intersection(bdd1, d2)}
     end
   end
 
+  # Version of i ^ (u1 v u2) that only computes the union if i is not bottom
+  defp lazy_bdd_intersection_union(:bdd_bot, _u1, _u2),
+    do: :bdd_bot
+
+  defp lazy_bdd_intersection_union(i, u1, u2),
+    do: lazy_bdd_intersection(i, lazy_bdd_union(u1, u2))
+
   def lazy_bdd_to_dnf(bdd), do: lazy_bdd_to_dnf([], [], [], bdd)
 
   defp lazy_bdd_to_dnf(acc, _pos, _neg, :bdd_bot), do: acc

From 394d9f8bc3bdb530b93ae12489a887983ee05d8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 03:14:52 +0200
Subject: [PATCH 19/24] Also avoid materialization on differences

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 4d5e865e09..66439bc88d 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4557,7 +4557,7 @@ defmodule Module.Types.Descr do
       {{lit1, l1, u1, r1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
         {lit1, l1, lazy_bdd_union(u1, bdd2), r1}
 
-      {{lit1, _, _, _} = bdd1, {lit2, l2, u2, r2}} ->
+      {bdd1, {lit2, l2, u2, r2}} ->
         {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
     end
   end
@@ -4576,25 +4576,32 @@ defmodule Module.Types.Descr do
       {:bdd_top, {lit, c2, u2, d2}} ->
         lazy_bdd_negation({lit, c2, u2, d2})
 
-      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
-        if u1 == u2 do
-          {lit, lazy_bdd_difference(c1, lazy_bdd_union(c2, u2)), :bdd_bot,
-           lazy_bdd_difference(d1, lazy_bdd_union(d2, u2))}
-        else
-          {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))}
-        end
+      # If possible, keep unions without dematerializing them down.
+      # We rely on the fact that (t1 ∨ t2) \ t3 is the same as (t1 \ t3) ∨ (t2 \ t3).
+      {{lit, c1, u1, d1}, bdd2} when u1 != :bdd_bot ->
+        lazy_bdd_difference({lit, c1, :bdd_bot, d1}, bdd2)
+        |> lazy_bdd_union(lazy_bdd_difference(u1, bdd2))
 
-      {{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)}
+      {{lit, c1, :bdd_bot, d1}, {lit, c2, u2, d2}} ->
+        {lit, lazy_bdd_difference_union(c1, c2, u2), :bdd_bot,
+         lazy_bdd_difference_union(d1, d2, u2)}
+
+      {{lit1, c1, :bdd_bot, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
+        {lit1, lazy_bdd_difference(c1, bdd2), :bdd_bot, lazy_bdd_difference(d1, bdd2)}
 
-      {{lit1, _, _, _} = bdd1, {lit2, c2, u2, d2}} ->
+      {bdd1, {lit2, c2, u2, d2}} ->
         {lit2, lazy_bdd_difference(bdd1, lazy_bdd_union(c2, u2)), :bdd_bot,
          lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
     end
   end
 
+  # Version of i \ (u1 v u2) that only computes the union if i is not bottom
+  defp lazy_bdd_difference_union(:bdd_bot, _u1, _u2),
+    do: :bdd_bot
+
+  defp lazy_bdd_difference_union(i, u1, u2),
+    do: lazy_bdd_difference(i, lazy_bdd_union(u1, u2))
+
   # 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

From 09f454fa140f352df5bc3ebbf1fca1707f37c185 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 12:48:02 +0200
Subject: [PATCH 20/24] Revert difference

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 66439bc88d..d61be25952 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4576,18 +4576,36 @@ defmodule Module.Types.Descr do
       {:bdd_top, {lit, c2, u2, d2}} ->
         lazy_bdd_negation({lit, c2, u2, d2})
 
-      # If possible, keep unions without dematerializing them down.
-      # We rely on the fact that (t1 ∨ t2) \ t3 is the same as (t1 \ t3) ∨ (t2 \ t3).
-      {{lit, c1, u1, d1}, bdd2} when u1 != :bdd_bot ->
-        lazy_bdd_difference({lit, c1, :bdd_bot, d1}, bdd2)
-        |> lazy_bdd_union(lazy_bdd_difference(u1, bdd2))
-
-      {{lit, c1, :bdd_bot, d1}, {lit, c2, u2, d2}} ->
-        {lit, lazy_bdd_difference_union(c1, c2, u2), :bdd_bot,
-         lazy_bdd_difference_union(d1, d2, u2)}
-
-      {{lit1, c1, :bdd_bot, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
-        {lit1, lazy_bdd_difference(c1, bdd2), :bdd_bot, lazy_bdd_difference(d1, bdd2)}
+      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
+        cond do
+          u2 == :bdd_top ->
+            {lit, :bdd_bot, :bdd_bot, :bdd_bot}
+
+          u1 == u2 ->
+            {lit, lazy_bdd_difference_union(c1, c2, u2), :bdd_bot,
+             lazy_bdd_difference_union(d1, d2, u2)}
+
+          true ->
+            {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))}
+
+            # u =
+            #   if u1 == :bdd_bot or c2 == :bdd_bot or d2 == :bdd_bot do
+            #     :bdd_bot
+            #   else
+            #     u1
+            #     |> lazy_bdd_intersection(c2)
+            #     |> lazy_bdd_intersection(d2)
+            #     |> lazy_bdd_difference(u2)
+            #   end
+
+            # {lit, lazy_bdd_difference(lazy_bdd_intersection(c1, c2), u2), u,
+            #  lazy_bdd_difference(lazy_bdd_intersection(d1, d2), u2)}
+        end
+
+      {{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)}
 
       {bdd1, {lit2, c2, u2, d2}} ->
         {lit2, lazy_bdd_difference(bdd1, lazy_bdd_union(c2, u2)), :bdd_bot,

From c4cfca36bdc07ae1bbee460db64485086b8092da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 15:44:22 +0200
Subject: [PATCH 21/24] Optimize difference

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index d61be25952..21a8eb2e47 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4578,8 +4578,9 @@ defmodule Module.Types.Descr do
 
       {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
         cond do
-          u2 == :bdd_top ->
-            {lit, :bdd_bot, :bdd_bot, :bdd_bot}
+          u2 == :bdd_bot and d2 == :bdd_bot ->
+            {lit, lazy_bdd_difference(c1, c2), lazy_bdd_difference(u1, c2),
+             lazy_bdd_union(u1, d1)}
 
           u1 == u2 ->
             {lit, lazy_bdd_difference_union(c1, c2, u2), :bdd_bot,
@@ -4588,19 +4589,6 @@ defmodule Module.Types.Descr do
           true ->
             {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))}
-
-            # u =
-            #   if u1 == :bdd_bot or c2 == :bdd_bot or d2 == :bdd_bot do
-            #     :bdd_bot
-            #   else
-            #     u1
-            #     |> lazy_bdd_intersection(c2)
-            #     |> lazy_bdd_intersection(d2)
-            #     |> lazy_bdd_difference(u2)
-            #   end
-
-            # {lit, lazy_bdd_difference(lazy_bdd_intersection(c1, c2), u2), u,
-            #  lazy_bdd_difference(lazy_bdd_intersection(d1, d2), u2)}
         end
 
       {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->

From 7655b569ef7fa0d5bc90c6857e2b6aa2e885628c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 15:46:26 +0200
Subject: [PATCH 22/24] Inline intersection implementation

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 21a8eb2e47..cc6ea9cae3 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -4631,18 +4631,27 @@ defmodule Module.Types.Descr do
       {_, :bdd_bot} ->
         :bdd_bot
 
-      {{lit, c1, u1, d1} = bdd1, {lit, c2, u2, d2} = bdd2} ->
-        # If possible, keep unions without dematerializing them down.
-        # We rely on the fact that (t1 ∨ t2) ∧ t3 is the same as (t1 ∧ t3) ∨ (t2 ∧ t3).
-        if u1 != :bdd_bot do
-          {lit, lazy_bdd_intersection_union(c1, c2, u2), :bdd_bot,
-           lazy_bdd_intersection_union(d1, d2, u2)}
-          |> lazy_bdd_union(lazy_bdd_intersection(u1, bdd2))
-        else
-          {lit, lazy_bdd_intersection_union(c2, c1, u1), :bdd_bot,
-           lazy_bdd_intersection_union(d2, d1, u1)}
-          |> lazy_bdd_union(lazy_bdd_intersection(u2, bdd1))
-        end
+      # Notice that (l ? c1, u1, d1) and (l ? c2, u2, d2) is, on paper, equivalent to
+      # [(l /\ c1) \/ u1 \/ (not l /\ d1)] and [(l /\ c2) \/ u2 \/ (not l /\ d2)]
+      # which is equivalent, by distributivity of intersection over union, to
+      # l /\ [(c1 /\ c2) \/ (c1 /\ u2) \/ (u1 /\ c2)]
+      #      \/ (u1 /\ u2)
+      #      \/ [(not l) /\ ((d1 /\ u2) \/ (d1 /\ d2) \/ (u1 /\ d2))]
+      # which is equivalent, by factoring out c1 in the first disjunct, and d1 in the third, to
+      # l /\ [c1 /\ (c2 \/ u2)] \/ (u1 /\ c2)
+      #     \/ (u1 /\ u2)
+      #     \/ (not l) /\ [d1 /\ (u2 \/ d2) \/ (u1 /\ d2)]
+      # This last expression gives the following implementation:
+      {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
+        {lit,
+         lazy_bdd_union(
+           lazy_bdd_intersection_union(c1, c2, u2),
+           lazy_bdd_intersection(u1, c2)
+         ), lazy_bdd_intersection(u1, u2),
+         lazy_bdd_union(
+           lazy_bdd_intersection_union(d1, u2, d2),
+           lazy_bdd_intersection(u1, d2)
+         )}
 
       {{lit1, c1, u1, d1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
         {lit1, lazy_bdd_intersection(c1, bdd2), lazy_bdd_intersection(u1, bdd2),

From 4b30c959df2f7e8c58d9bc1606826e41db4ce98b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 15:52:17 +0200
Subject: [PATCH 23/24] Refactor and clean up

---
 lib/elixir/lib/module/types/descr.ex | 226 ++++++---------------------
 1 file changed, 52 insertions(+), 174 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index cc6ea9cae3..cba44fb40b 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1095,7 +1095,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: lazy_bdd_new({inputs, output})
+  defp fun_new(inputs, output), do: 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.
@@ -1414,7 +1414,7 @@ defmodule Module.Types.Descr do
   # 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
-    lazy_bdd_to_dnf(bdd)
+    bdd_to_dnf(bdd)
     |> Enum.filter(fn {pos, neg} -> not fun_line_empty?(pos, neg) end)
   end
 
@@ -1431,7 +1431,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
-    lazy_bdd_to_dnf(bdd)
+    bdd_to_dnf(bdd)
     |> Enum.all?(fn {pos, neg} -> fun_line_empty?(pos, neg) end)
   end
 
@@ -1605,18 +1605,18 @@ defmodule Module.Types.Descr do
       all_disjoint_arguments?(rest)
   end
 
-  defp fun_union(bdd1, bdd2), do: lazy_bdd_union(bdd1, bdd2)
+  defp fun_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
   defp fun_intersection(bdd1, bdd2) do
     cond do
       # If intersecting with the top type for that arity, no-op
       is_tuple(bdd2) and fun_top?(bdd2, bdd1) -> bdd2
       is_tuple(bdd1) and fun_top?(bdd1, bdd2) -> bdd1
-      true -> lazy_bdd_intersection(bdd1, bdd2)
+      true -> bdd_intersection(bdd1, bdd2)
     end
   end
 
-  defp fun_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
+  defp fun_difference(bdd1, bdd2), do: 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
@@ -2396,7 +2396,7 @@ defmodule Module.Types.Descr do
     end
   end
 
-  def map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do
+  defp map_union(map_literal(tag1, fields1), map_literal(tag2, fields2)) do
     case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do
       {tag, fields, []} -> map_literal(tag, fields)
       nil -> bdd_union(map_literal(tag1, fields1), map_literal(tag2, fields2))
@@ -2404,7 +2404,7 @@ defmodule Module.Types.Descr do
   end
 
   @compile {:inline, map_union: 2}
-  def map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
+  defp map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
 
   defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do
     case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do
@@ -4417,21 +4417,10 @@ defmodule Module.Types.Descr do
 
   ## BDD helpers
 
-  # TODO: find out if using lazy BDDs everywhere is worth it
-  # Remark: uncomment those, and swap the macro and attribute definitions to use lazy BDDs.
-  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 lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}
+  @compile {:inline, bdd_new: 1}
+  defp bdd_new(literal), do: {literal, :bdd_top, :bdd_bot, :bdd_bot}
 
-  defp lazy_bdd_map(bdd, fun) do
+  defp bdd_map(bdd, fun) do
     case bdd do
       :bdd_bot ->
         :bdd_bot
@@ -4444,100 +4433,7 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # 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
-  # defp bdd_intersection(:bdd_top, other), do: other
-  # defp bdd_intersection(other, :bdd_top), do: other
-
-  # # Internal-node cases
-  # # Keeping the invariant that literals are ordered ensures nodes are not duplicated down
-  # defp bdd_intersection({lit, l1, r1}, {lit, l2, r2}),
-  #   do: {lit, bdd_intersection(l1, l2), bdd_intersection(r1, r2)}
-
-  # defp bdd_intersection({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-  #   do: {lit1, bdd_intersection(l1, bdd2), bdd_intersection(r1, bdd2)}
-
-  # defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-  #   do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)}
-
-  # defp bdd_difference(:bdd_bot, _), do: :bdd_bot
-  # defp bdd_difference(other, :bdd_bot), do: other
-  # defp bdd_difference(:bdd_top, other), do: bdd_negation(other)
-  # defp bdd_difference(_, :bdd_top), do: :bdd_bot
-
-  # defp bdd_difference({lit, l1, r1}, {lit, l2, r2}),
-  #   do: {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)}
-
-  # defp bdd_difference({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-  #   do: {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)}
-
-  # defp bdd_difference({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-  #   do: {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)}
-
-  # defp bdd_negation(:bdd_bot), do: :bdd_top
-  # defp bdd_negation(:bdd_top), do: :bdd_bot
-  # defp bdd_negation({lit, l, r}), do: {lit, bdd_negation(l), bdd_negation(r)}
-
-  # defp bdd_union(:bdd_top, _), do: :bdd_top
-  # defp bdd_union(_, :bdd_top), do: :bdd_top
-  # defp bdd_union(:bdd_bot, other), do: other
-  # defp bdd_union(other, :bdd_bot), do: other
-  # defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)}
-
-  # # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree
-  # defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-  #   do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)}
-
-  # defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-  #   do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)}
-
-  # defp bdd_map(bdd, fun) do
-  #   case bdd do
-  #     :bdd_bot -> :bdd_bot
-  #     :bdd_top -> :bdd_top
-  #     {literal, left, right} -> {fun.(literal), bdd_map(left, fun), bdd_map(right, fun)}
-  #   end
-  # end
-
-  # defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
-
-  # defp bdd_to_dnf(acc, pos, neg, bdd) do
-  #   case bdd do
-  #     :bdd_bot ->
-  #       acc
-
-  #     :bdd_top ->
-  #       [{pos, neg} | acc]
-
-  #     {fun, :bdd_top, right} ->
-  #       bdd_to_dnf([{[fun | pos], neg} | acc], pos, neg, right)
-
-  #     {fun, left, right} ->
-  #       bdd_to_dnf(bdd_to_dnf(acc, [fun | pos], neg, left), pos, [fun | neg], right)
-  #   end
-  # end
-
-  ## Lazy BDD helpers
-  defp lazy_bdd_new(literal), do: {literal, :bdd_top, :bdd_bot, :bdd_bot}
-
-  # defp bdd_union(:bdd_top, _), do: :bdd_top
-  # defp bdd_union(_, :bdd_top), do: :bdd_top
-  # defp bdd_union(:bdd_bot, other), do: other
-  # defp bdd_union(other, :bdd_bot), do: other
-  # defp bdd_union({map, l1, r1}, {map, l2, r2}), do: {map, bdd_union(l1, l2), bdd_union(r1, r2)}
-
-  # # Maintaining the invariant that literals are ordered ensures they are not duplicated down the tree
-  # defp bdd_union({lit1, l1, r1}, {lit2, _, _} = bdd2) when lit1 < lit2,
-  #   do: {lit1, bdd_union(l1, bdd2), bdd_union(r1, bdd2)}
-
-  # defp bdd_union({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
-  #   do: {lit2, bdd_union(bdd1, l2), bdd_union(bdd1, r2)}
-
-  def lazy_bdd_union(bdd1, bdd2) do
+  defp bdd_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:bdd_top, _bdd} ->
         :bdd_top
@@ -4552,17 +4448,17 @@ defmodule Module.Types.Descr do
         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)}
+        {lit, bdd_union(l1, l2), bdd_union(u1, u2), bdd_union(r1, r2)}
 
       {{lit1, l1, u1, r1}, {lit2, _, _, _} = bdd2} when lit1 < lit2 ->
-        {lit1, l1, lazy_bdd_union(u1, bdd2), r1}
+        {lit1, l1, bdd_union(u1, bdd2), r1}
 
       {bdd1, {lit2, l2, u2, r2}} ->
-        {lit2, l2, lazy_bdd_union(bdd1, u2), r2}
+        {lit2, l2, bdd_union(bdd1, u2), r2}
     end
   end
 
-  def lazy_bdd_difference(bdd1, bdd2) do
+  defp bdd_difference(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {_bdd, :bdd_top} ->
         :bdd_bot
@@ -4574,50 +4470,39 @@ defmodule Module.Types.Descr do
         bdd
 
       {:bdd_top, {lit, c2, u2, d2}} ->
-        lazy_bdd_negation({lit, c2, u2, d2})
+        bdd_negation({lit, c2, u2, d2})
 
       {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
         cond do
           u2 == :bdd_bot and d2 == :bdd_bot ->
-            {lit, lazy_bdd_difference(c1, c2), lazy_bdd_difference(u1, c2),
-             lazy_bdd_union(u1, d1)}
+            {lit, bdd_difference(c1, c2), bdd_difference(u1, c2), bdd_union(u1, d1)}
 
           u1 == u2 ->
-            {lit, lazy_bdd_difference_union(c1, c2, u2), :bdd_bot,
-             lazy_bdd_difference_union(d1, d2, u2)}
+            {lit, bdd_difference_union(c1, c2, u2), :bdd_bot, bdd_difference_union(d1, d2, u2)}
 
           true ->
-            {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))}
+            {lit, bdd_difference(bdd_union(c1, u1), bdd_union(c2, u2)), :bdd_bot,
+             bdd_difference(bdd_union(d1, u1), bdd_union(d2, u2))}
         end
 
       {{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, bdd_difference(bdd_union(c1, u1), bdd2), :bdd_bot,
+         bdd_difference(bdd_union(d1, u1), bdd2)}
 
       {bdd1, {lit2, c2, u2, d2}} ->
-        {lit2, lazy_bdd_difference(bdd1, lazy_bdd_union(c2, u2)), :bdd_bot,
-         lazy_bdd_difference(bdd1, lazy_bdd_union(d2, u2))}
+        {lit2, bdd_difference(bdd1, bdd_union(c2, u2)), :bdd_bot,
+         bdd_difference(bdd1, bdd_union(d2, u2))}
     end
   end
 
   # Version of i \ (u1 v u2) that only computes the union if i is not bottom
-  defp lazy_bdd_difference_union(:bdd_bot, _u1, _u2),
+  defp bdd_difference_union(:bdd_bot, _u1, _u2),
     do: :bdd_bot
 
-  defp lazy_bdd_difference_union(i, u1, u2),
-    do: lazy_bdd_difference(i, lazy_bdd_union(u1, u2))
+  defp bdd_difference_union(i, u1, u2),
+    do: bdd_difference(i, bdd_union(u1, u2))
 
-  # 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
+  defp bdd_intersection(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:bdd_top, bdd} ->
         bdd
@@ -4643,53 +4528,46 @@ defmodule Module.Types.Descr do
       #     \/ (not l) /\ [d1 /\ (u2 \/ d2) \/ (u1 /\ d2)]
       # This last expression gives the following implementation:
       {{lit, c1, u1, d1}, {lit, c2, u2, d2}} ->
-        {lit,
-         lazy_bdd_union(
-           lazy_bdd_intersection_union(c1, c2, u2),
-           lazy_bdd_intersection(u1, c2)
-         ), lazy_bdd_intersection(u1, u2),
-         lazy_bdd_union(
-           lazy_bdd_intersection_union(d1, u2, d2),
-           lazy_bdd_intersection(u1, d2)
-         )}
+        {lit, bdd_union(bdd_intersection_union(c1, c2, u2), bdd_intersection(u1, c2)),
+         bdd_intersection(u1, u2),
+         bdd_union(bdd_intersection_union(d1, u2, d2), bdd_intersection(u1, d2))}
 
       {{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, bdd_intersection(c1, bdd2), bdd_intersection(u1, bdd2), bdd_intersection(d1, bdd2)}
 
       {bdd1, {lit2, c2, u2, d2}} ->
-        {lit2, lazy_bdd_intersection(bdd1, c2), lazy_bdd_intersection(bdd1, u2),
-         lazy_bdd_intersection(bdd1, d2)}
+        {lit2, bdd_intersection(bdd1, c2), bdd_intersection(bdd1, u2), bdd_intersection(bdd1, d2)}
     end
   end
 
   # Version of i ^ (u1 v u2) that only computes the union if i is not bottom
-  defp lazy_bdd_intersection_union(:bdd_bot, _u1, _u2),
+  defp bdd_intersection_union(:bdd_bot, _u1, _u2),
     do: :bdd_bot
 
-  defp lazy_bdd_intersection_union(i, u1, u2),
-    do: lazy_bdd_intersection(i, lazy_bdd_union(u1, u2))
+  defp bdd_intersection_union(i, u1, u2),
+    do: bdd_intersection(i, bdd_union(u1, u2))
 
-  def lazy_bdd_to_dnf(bdd), do: lazy_bdd_to_dnf([], [], [], bdd)
+  # Lazy negation: eliminate the union, then perform normal negation (switching leaves)
+  defp bdd_negation(:bdd_top), do: :bdd_bot
+  defp bdd_negation(:bdd_bot), do: :bdd_top
 
-  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]
+  defp bdd_negation({lit, c, u, d}) do
+    {lit, bdd_negation(bdd_union(c, u)), :bdd_bot, bdd_negation(bdd_union(d, u))}
+  end
+
+  defp bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd)
+
+  defp bdd_to_dnf(acc, _pos, _neg, :bdd_bot), do: acc
+  defp 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
+  defp 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, pos, neg, u)
+    bdd_to_dnf(acc, pos, neg, u)
     # C-part
-    |> lazy_bdd_to_dnf([lit | pos], neg, c)
+    |> 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} = node) do
-    raise ArgumentError,
-          "lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d} #{inspect(node)}\n
-          #{inspect(Process.info(self(), :current_stacktrace))}"
+    |> bdd_to_dnf(pos, [lit | neg], d)
   end
 
   ## Pairs

From 6f1c5c8e5a01efb7ae6953728ce463c19136a28c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Thu, 2 Oct 2025 15:54:23 +0200
Subject: [PATCH 24/24] Update comments

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index cba44fb40b..a81de9b921 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -33,9 +33,11 @@ defmodule Module.Types.Descr do
   defmacrop tuple_literal(tag, elements),
     do: {:{}, [], [{tag, elements}, :bdd_top, :bdd_bot, :bdd_bot]}
 
-  defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot, :bdd_bot]}
+  defmacrop list_literal(list, last),
+    do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot, :bdd_bot]}
 
-  defmacrop domain_key(key), do: {:domain_key, key}
+  defmacrop domain_key(key),
+    do: {:domain_key, key}
 
   @domain_key_types [
     {:domain_key, :binary},
@@ -1094,7 +1096,6 @@ 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).
-  # NOTE: this is a ternary (lazy) BDD where the middle node encodes unions.
   defp fun_new(inputs, output), do: bdd_new({inputs, output})
 
   # Creates a function type from a list of inputs and an output