From 42f53650c0fc966cb4009181b7ef436fc75aab84 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 22 Jul 2025 14:55:17 +0200
Subject: [PATCH 1/9] Refactor BDD list type handling in Module.Types.Descr

- Updated the representation of non-empty lists and empty intersections/differences to use BDD structures.
- Introduced new functions for BDD operations including list_get, list_get_pos, and list_all? for better handling of BDD paths.
- Modified list normalization and difference functions to work with BDDs
---
 lib/elixir/lib/module/types/descr.ex          | 385 +++++++++++++-----
 .../test/elixir/module/types/descr_test.exs   |   8 +-
 2 files changed, 276 insertions(+), 117 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 765e076467..a508f9be4f 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -46,7 +46,7 @@ defmodule Module.Types.Descr do
   @fun_top :fun_top
   @atom_top {:negation, :sets.new(version: 2)}
   @map_top [{:open, %{}, []}]
-  @non_empty_list_top [{:term, :term, []}]
+  @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot}
   @tuple_top [{:open, []}]
   @map_empty [{:closed, %{}, []}]
 
@@ -68,8 +68,8 @@ defmodule Module.Types.Descr do
   @term_or_dynamic_optional Map.put(@term, :dynamic, %{optional: 1})
   @not_atom_or_optional Map.delete(@term_or_optional, :atom)
 
-  @empty_intersection [0, []]
-  @empty_difference [0, []]
+  @empty_intersection [0, [], :bdd_bot]
+  @empty_difference [0, [], :bdd_bot]
 
   defguard is_descr(descr) when is_map(descr) or descr == :term
 
@@ -1831,17 +1831,30 @@ defmodule Module.Types.Descr do
           :error ->
             list_new(list_type, last_type)
 
-          {dnf, last_type} ->
+          {bdd, last_type} ->
             # It is safe to discard the negations for the tail because
             # `list(term()) and not list(integer())` means a list
             # of all terms except lists where all of them are integer,
             # which means the head is still a term().
-            {list_type, last_type} =
-              Enum.reduce(dnf, {list_type, last_type}, fn {head, tail, _}, {acc_head, acc_tail} ->
+            {list_type, _} =
+              list_get_pos(bdd)
+              |> Enum.reduce({list_type, last_type}, fn {head, tail}, {acc_head, acc_tail} ->
                 {union(head, acc_head), union(tail, acc_tail)}
               end)
 
-            list_new(list_type, last_type)
+            # So for instance if i give term() and `term() and not (list(term())`
+            # what happens?
+            # list_type starts with term() and does not change
+            # last_type starts with everything but :list and []
+            # then we iterate over the bdd, which contains... what? it contains
+            # {:term, :term} and not {:term, %{bitmap: 2}}
+            # what is bitmap: 2? it is empty_list()
+            # we only add the positive {:term, :term} to both things
+            # so we get {:term, :term} lol... that seems wrong, i should not add back the
+            # empty_list()
+            # maybe i should get tl on the bdd?
+
+            list_new(list_type, Map.delete(last_type, :list))
         end
       end
 
@@ -1855,7 +1868,72 @@ defmodule Module.Types.Descr do
   end
 
   defp list_new(list_type, last_type) do
-    [{list_type, last_type, []}]
+    {{list_type, last_type}, :bdd_top, :bdd_bot}
+  end
+
+  # 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 list_get(bdd), do: list_get([], {:term, :term}, [], bdd)
+
+  defp list_get(acc, {list_acc, tail_acc} = pos, negs, bdd) do
+    case bdd do
+      :bdd_bot ->
+        acc
+
+      :bdd_top ->
+        [{pos, negs} | acc]
+
+      {{list, tail} = list_type, left, right} ->
+        new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)}
+        list_get(list_get(acc, new_pos, negs, left), pos, [list_type | negs], right)
+    end
+  end
+
+  # Takes all the paths from the root to the leaves finishing with a 1,
+  # and compile into tuples of positive and negative nodes. Keep only the non-empty positives.
+  defp list_get_pos(bdd), do: list_get_pos([], {:term, :term}, [], bdd)
+
+  defp list_get_pos(acc, {list_acc, tail_acc} = pos, negs, bdd) do
+    case bdd do
+      :bdd_bot ->
+        acc
+
+      :bdd_top ->
+        if list_empty_line?(list_acc, tail_acc, negs) do
+          acc
+        else
+          [pos | acc]
+        end
+
+      {{list, tail} = list_type, left, right} ->
+        new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)}
+        list_get_pos(list_get_pos(acc, new_pos, negs, left), pos, [list_type | negs], right)
+    end
+  end
+
+  # Takes all the paths from the root to the leaves finishing with a 1, computes the intersection
+  # of the positives, and calls the condition on the result. Checks it is true for all of them.
+  # As if calling Enum.all? on all the paths of the bdd.
+  defp list_all?(bdd, condition), do: list_all?({:term, :term}, [], bdd, condition)
+
+  defp list_all?({list_acc, tail_acc} = pos, negs, bdd, condition) do
+    case bdd do
+      :bdd_bot ->
+        true
+
+      :bdd_top ->
+        condition.(list_acc, tail_acc, negs)
+
+      {{list, tail} = list_type, left, right} ->
+        list_all?(
+          {intersection(list_acc, list), intersection(tail_acc, tail)},
+          negs,
+          left,
+          condition
+        ) and
+          list_all?(pos, [list_type | negs], right, condition)
+    end
   end
 
   defp list_pop_dynamic(:term), do: {false, :term}
@@ -1870,86 +1948,148 @@ defmodule Module.Types.Descr do
   defp list_tail_unfold(:term), do: @not_non_empty_list
   defp list_tail_unfold(other), do: Map.delete(other, :list)
 
-  defp list_union(dnf1, dnf2), do: dnf1 ++ (dnf2 -- dnf1)
+  defp list_union(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_top, _} -> :bdd_top
+      {_, :bdd_top} -> :bdd_top
+      {:bdd_bot, bdd} -> bdd
+      {bdd, :bdd_bot} -> bdd
+      {{list, l1, r1}, {list, l2, r2}} -> {list, list_union(l1, l2), list_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
+      {{list, l, r}, bdd} -> {list, list_union(l, bdd), list_union(r, bdd)}
+    end
+  end
 
-  defp list_intersection(dnf1, dnf2) do
-    for {list_type1, last_type1, negs1} <- dnf1,
-        {list_type2, last_type2, negs2} <- dnf2,
-        reduce: [] do
-      acc ->
-        inter = intersection(list_type1, list_type2)
-        last = intersection(last_type1, last_type2)
-        negs = negs1 ++ negs2
+  defp list_intersection(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {bdd, {{list, tail}, :bdd_top, :bdd_bot}} when is_tuple(bdd) ->
+        if list == :term and tail == :term do
+          bdd
+        else
+          list_intersection_recur(bdd1, bdd2)
+        end
 
-        cond do
-          :lists.member({inter, last}, negs) -> acc
-          empty?(inter) or empty?(last) -> acc
-          true -> [{inter, last, negs} | acc]
+      {{{list, tail}, :bdd_top, :bdd_bot}, bdd} when is_tuple(bdd) ->
+        if list == :term and tail == :term do
+          bdd
+        else
+          list_intersection_recur(bdd1, bdd2)
         end
+
+      _ ->
+        list_intersection_recur(bdd1, bdd2)
+    end
+    |> case do
+      {_, :bdd_bot, :bdd_bot} -> :bdd_bot
+      bdd -> bdd
     end
   end
 
-  # Computes the difference between two DNF (Disjunctive Normal Form) list types.
-  # It progressively subtracts each type in dnf2 from all types in dnf1.
-  # The algorithm handles three cases:
-  # 1. Disjoint types: keeps the original type from dnf1
-  # 2. Subtype relationship:
-  #    a) If dnf2 type is a supertype, keeps only the negations
-  #    b) If only the last type differs, subtracts it
-  # 3. Base case: adds dnf2 type to negations of dnf1 type
-  # The result may be larger than the initial dnf1, which is maintained in the accumulator.
-  defp list_difference(_, dnf) when dnf == @non_empty_list_top do
-    []
-  end
+  defp list_intersection_recur(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      # Base cases
+      {_, :bdd_bot} ->
+        :bdd_bot
 
-  defp list_difference(dnf1, dnf2) do
-    Enum.reduce(dnf2, dnf1, fn {t2, last2, negs2}, acc_dnf1 ->
-      last2 = list_tail_unfold(last2)
+      {:bdd_bot, _} ->
+        :bdd_bot
 
-      Enum.flat_map(acc_dnf1, fn {t1, last1, negs1} ->
-        last1 = list_tail_unfold(last1)
+      {:bdd_top, bdd} ->
+        bdd
 
-        new_negs =
-          Enum.reduce(negs2, [], fn {nt, nlast}, nacc ->
-            t = intersection(t1, nt)
-            last = intersection(last1, nlast)
+      {bdd, :bdd_top} ->
+        bdd
 
-            cond do
-              :lists.member({t, last}, negs1) -> nacc
-              empty?(t) or empty?(last) -> nacc
-              true -> [{t, last, negs1} | nacc]
-            end
-          end)
+      # 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).
+      # Note: instead of inserting the bdd at the root, we decided to intersect with
+      # every atom in the bdd. If empty, then replace with the right tree.
+      {bdd, {list, :bdd_top, :bdd_bot}} ->
+        intersect_bdd_with_list(bdd, list)
 
-        i = intersection(t1, t2)
-        l = intersection(last1, last2)
+      {bdd, {list, :bdd_bottom, :bdd_top}} ->
+        {list, :bdd_bottom, bdd}
 
-        cond do
-          empty?(i) or empty?(l) -> [{t1, last1, negs1}]
-          subtype?(t1, t2) and subtype?(last1, last2) -> new_negs
-          subtype?(t1, t2) -> [{t1, difference(last1, last2), negs1} | new_negs]
-          true -> [{t1, last1, [{t2, last2} | negs1]} | new_negs]
+      {{list, :bdd_top, :bdd_bottom}, bdd} ->
+        intersect_bdd_with_list(bdd, list)
+
+      {{list, :bdd_bottom, :bdd_top}, bdd} ->
+        {list, :bdd_bottom, bdd}
+
+      # General cases
+      {{list, l1, r1}, {list, l2, r2}} ->
+        {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)}
+
+      {{list, l, r}, bdd} ->
+        {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)}
+    end
+  end
+
+  # We can only do this if the bdd has :bdd_bot as right child. Otherwise, if `a` is the root,
+  # it contains both formulas `a and left`, and `not a and right`. Thus, intersecting `not a`
+  # with a `{list, last}` is a wrong formula. Then, if the intersection is empty, the whole
+  # bdd is empty.
+  defp intersect_bdd_with_list(bdd, {list, last}) do
+    case bdd do
+      {{bdd_list, bdd_last}, left, :bdd_bot} ->
+        list = intersection(bdd_list, list)
+        last = intersection(bdd_last, last)
+
+        if empty?(list) or empty?(last) do
+          :bdd_bot
+        else
+          {{list, last}, left, :bdd_bot}
         end
-      end)
-    end)
+
+      _ ->
+        # Otherwise, we simply put the positive list at the root.
+        {{list, last}, bdd, :bdd_bot}
+    end
+  end
+
+  # Computes the difference between two BDD (Binary Decision Diagram) list types.
+  # It progressively subtracts each type in bdd2 from all types in bdd1.
+  # The algorithm handles three cases:
+  # 1. Disjoint types: keeps the original type from bdd1
+  # 2. Subtype relationship:
+  #    a) If bdd2 type is a supertype, keeps only the negations
+  #    b) If only the last type differs, subtracts it
+  # 3. Base case: adds bdd2 type to negations of bdd1 type
+  # The result may be larger than the initial bdd1, which is maintained in the accumulator.
+  defp list_difference(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_bot, _} -> :bdd_bot
+      {_, :bdd_top} -> :bdd_bot
+      {bdd, :bdd_bot} -> bdd
+      {:bdd_top, {lst, l, r}} -> {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)}
+      {{lst, l1, r1}, {lst, l2, r2}} -> {lst, list_difference(l1, l2), list_difference(r1, r2)}
+      {{lst, l, r}, bdd} -> {lst, list_difference(l, bdd), list_difference(r, bdd)}
+    end
+    |> case do
+      {_, :bdd_bot, :bdd_bot} -> :bdd_bot
+      bdd -> bdd
+    end
   end
 
   defp list_empty?(@non_empty_list_top), do: false
+  defp list_empty?(bdd), do: list_all?(bdd, &list_empty_line?/3)
 
-  defp list_empty?(dnf) do
-    Enum.all?(dnf, fn {list_type, last_type, negs} ->
-      last_type = list_tail_unfold(last_type)
+  defp list_empty_line?(list_type, last_type, negs) do
+    last_type = list_tail_unfold(last_type)
 
-      empty?(list_type) or empty?(last_type) or
-        Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type ->
-          if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do
-            {:halt, nil}
-          else
-            {:cont, difference(acc_last_type, neg_last)}
-          end
-        end)
-        |> is_nil()
-    end)
+    empty?(list_type) or empty?(last_type) or
+      Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type ->
+        if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do
+          {:halt, nil}
+        else
+          {:cont, difference(acc_last_type, neg_last)}
+        end
+      end)
+      |> is_nil()
   end
 
   defp non_empty_list_only?(descr), do: empty?(Map.delete(descr, :list))
@@ -1987,19 +2127,15 @@ defmodule Module.Types.Descr do
 
   defp list_hd_static(:term), do: :term
 
-  defp list_hd_static(descr) do
-    case descr do
-      %{list: [{type, _last, _negs}]} ->
-        type
-
-      %{list: dnf} ->
-        Enum.reduce(dnf, none(), fn {type, _, _}, acc -> union(type, acc) end)
-
-      %{} ->
-        none()
-    end
+  defp list_hd_static(%{list: bdd}) do
+    list_get_pos(bdd)
+    |> Enum.reduce(none(), fn {list, _}, acc ->
+      union(list, acc)
+    end)
   end
 
+  defp list_hd_static(%{}), do: none()
+
   @doc """
   Returns the tail of a list.
 
@@ -2034,19 +2170,17 @@ defmodule Module.Types.Descr do
 
   defp list_tl_static(:term), do: :term
 
-  defp list_tl_static(%{list: dnf} = descr) do
+  defp list_tl_static(%{list: bdd} = descr) do
     initial =
       case descr do
         %{bitmap: bitmap} when (bitmap &&& @bit_empty_list) != 0 ->
-          %{list: dnf, bitmap: @bit_empty_list}
+          %{list: bdd, bitmap: @bit_empty_list}
 
         %{} ->
-          %{list: dnf}
+          %{list: bdd}
       end
 
-    Enum.reduce(dnf, initial, fn {_, last, _}, acc ->
-      union(last, acc)
-    end)
+    list_get_pos(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end)
   end
 
   defp list_tl_static(%{}), do: none()
@@ -2055,11 +2189,12 @@ defmodule Module.Types.Descr do
   defp list_improper_static?(%{bitmap: bitmap}) when (bitmap &&& @bit_empty_list) != 0, do: false
   defp list_improper_static?(term), do: equal?(term, @not_list)
 
-  defp list_to_quoted(dnf, empty?, opts) do
-    dnf = list_normalize(dnf)
+  defp list_to_quoted(bdd, empty?, opts) do
+    dnf = list_normalize(bdd)
 
     {unions, list_rendered?} =
-      Enum.reduce(dnf, {[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} ->
+      dnf
+      |> Enum.reduce({[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} ->
         {name, arguments, list_rendered?} =
           cond do
             list_type == term() and list_improper_static?(last_type) ->
@@ -2109,37 +2244,61 @@ defmodule Module.Types.Descr do
 
   # Eliminate empty lists from the union, and redundant types (that are subtypes of others,
   # or that can be merged with others).
-  defp list_normalize(dnf) do
-    Enum.reduce(dnf, [], fn {lt, last, negs}, acc ->
-      if list_literal_empty?(lt, last, negs),
-        do: acc,
-        else: add_to_list_normalize(acc, lt, last, negs)
+  defp list_normalize(bdd) do
+    list_get(bdd)
+    |> Enum.reduce([], fn {{list, last}, negs}, acc ->
+      if list_empty_line?(list, last, negs) do
+        acc
+      else
+        # First, try to eliminate the negations from the existing type.
+        {list, last, negs} =
+          Enum.uniq(negs)
+          |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} ->
+            last = list_tail_unfold(last)
+            new_list = intersection(list, nlist)
+            new_last = intersection(last, nlast)
+
+            cond do
+              # No intersection between the list and the negative
+              empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs}
+              subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs}
+              true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]}
+            end
+          end)
+
+        add_to_list_normalize(acc, list, last, negs |> Enum.reverse())
+      end
     end)
   end
 
-  defp list_literal_empty?(list_type, last_type, negations) do
-    empty?(list_type) or empty?(last_type) or
-      Enum.any?(negations, fn {neg_type, neg_last} ->
-        subtype?(list_type, neg_type) and subtype?(last_type, neg_last)
-      end)
+  # List of possible union merges:
+  # Case 1: when a list is a subtype of another
+  # Case 2: when two lists have the same list type, then the last types are united
+  defp add_to_list_normalize([{t, l, []} = cur | rest], list, last, []) do
+    cond do
+      subtype?(list, t) and subtype?(last, l) -> [cur | rest]
+      subtype?(t, list) and subtype?(l, last) -> [{list, last, []} | rest]
+      equal?(t, list) -> [{t, union(l, last), []} | rest]
+      true -> [cur | add_to_list_normalize(rest, list, last, [])]
+    end
   end
 
-  # Inserts a list type into a list of non-subtype list types.
-  # If the {list_type, last_type} is a subtype of an existing type, the negs
-  # are added to that type.
-  # If one list member is a subtype of {list_type, last_type}, it is replaced
-  # and its negations are added to the new type.
-  # If the type of elements are the same, the last types are merged.
-  defp add_to_list_normalize([{t, l, n} | rest], list, last, negs) do
-    cond do
-      subtype?(list, t) and subtype?(last, l) -> [{t, l, n ++ negs} | rest]
-      subtype?(t, list) and subtype?(l, last) -> [{list, last, n ++ negs} | rest]
-      equal?(t, list) -> [{t, union(l, last), n ++ negs} | rest]
-      true -> [{t, l, n} | add_to_list_normalize(rest, list, last, negs)]
+  # Case 3: when a list with negations is united with one of its negations
+  defp add_to_list_normalize([{t, l, n} = cur | rest], list, last, []) do
+    case pop_elem({list, last}, n) do
+      {true, n1} -> [{t, l, n1} | rest]
+      {false, _} -> [cur | add_to_list_normalize(rest, list, last, n)]
     end
   end
 
-  defp add_to_list_normalize([], list, last, negs), do: [{list, last, negs}]
+  defp add_to_list_normalize(rest, list, last, negs), do: [{list, last, negs} | rest]
+
+  defp pop_elem(elem, list) do
+    case :lists.delete(elem, list) do
+      ^list -> {false, list}
+      new_list -> {true, new_list}
+    end
+  end
 
   ## Dynamic
   #
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 74d561e5de..17a6746c4d 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -587,7 +587,7 @@ defmodule Module.Types.DescrTest do
     test "list" do
       # Basic list type differences
       assert difference(list(term()), empty_list()) == non_empty_list(term())
-      assert difference(list(integer()), list(term())) == none()
+      assert difference(list(integer()), list(term())) |> empty?()
 
       assert difference(list(integer()), list(float()))
              |> equal?(non_empty_list(integer()))
@@ -609,7 +609,7 @@ defmodule Module.Types.DescrTest do
       refute difference(list(union(atom(), binary())), list(atom())) == list(binary())
 
       # Tests for list with last element
-      assert difference(list(integer(), atom()), list(number(), term())) == none()
+      assert difference(list(integer(), atom()), list(number(), term())) |> empty?()
 
       assert difference(
                list(atom(), term()),
@@ -657,8 +657,8 @@ defmodule Module.Types.DescrTest do
              )
 
       # Difference with proper list
-      assert difference(list(integer(), atom()), list(integer())) ==
-               non_empty_list(integer(), atom())
+      assert difference(list(integer(), atom()), list(integer()))
+             |> equal?(non_empty_list(integer(), atom()))
     end
 
     test "fun" do

From d3fc8b2f6016155249b290a7216bc2a8a1c5c627 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 24 Jul 2025 15:02:55 +0200
Subject: [PATCH 2/9] Fix list_get_pos bug

---
 lib/elixir/lib/module/types/descr.ex          | 77 +++++++++++++------
 .../test/elixir/module/types/expr_test.exs    | 24 ++++++
 2 files changed, 78 insertions(+), 23 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index a508f9be4f..74981dcb20 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1831,14 +1831,22 @@ defmodule Module.Types.Descr do
           :error ->
             list_new(list_type, last_type)
 
-          {bdd, last_type} ->
-            # It is safe to discard the negations for the tail because
-            # `list(term()) and not list(integer())` means a list
-            # of all terms except lists where all of them are integer,
-            # which means the head is still a term().
-            {list_type, _} =
+          {bdd, last_type_no_list} ->
+            # The argument last_type may include list types; in this case, we aim to add
+            # those to the main list type, only to keep the type of the final element (which may
+            # be either the empty list, or some non-list value).
+            # To do so, we go through the list types in last_type, but since those are stored
+            # as a bdd of list types, we take care to include the effect of negations on computing
+            # each last type.
+            # To see if a negation changes the last type or the list type, we just need to check
+            # 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)
+            {list_type, last_type} =
               list_get_pos(bdd)
-              |> Enum.reduce({list_type, last_type}, fn {head, tail}, {acc_head, acc_tail} ->
+              |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail},
+                                                                {acc_head, acc_tail} ->
+                tail = list_tail_unfold(tail)
                 {union(head, acc_head), union(tail, acc_tail)}
               end)
 
@@ -1854,7 +1862,13 @@ defmodule Module.Types.Descr do
             # empty_list()
             # maybe i should get tl on the bdd?
 
-            list_new(list_type, Map.delete(last_type, :list))
+            last_type =
+              case last_type do
+                :term -> @not_non_empty_list
+                other -> Map.delete(other, :list)
+              end
+
+            list_new(list_type, last_type)
         end
       end
 
@@ -1871,7 +1885,7 @@ defmodule Module.Types.Descr do
     {{list_type, last_type}, :bdd_top, :bdd_bot}
   end
 
-  # Takes all the paths from the root to the leaves finishing with a 1,
+  # 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_get(bdd), do: list_get([], {:term, :term}, [], bdd)
@@ -1890,31 +1904,48 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Takes all the paths from the root to the leaves finishing with a 1,
-  # and compile into tuples of positive and negative nodes. Keep only the non-empty positives.
-  defp list_get_pos(bdd), do: list_get_pos([], {:term, :term}, [], bdd)
+  # Takes all the lines from the root to the leaves finishing with a 1,
+  # and compile into tuples of positive and negative nodes. Keep only the non-empty positives,
+  # and include the impact of negations on the last type.
+  # To see if a negation changes the last type or the list type, we just need to check
+  # 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_get_pos(bdd), do: list_get_pos(:term, :term, bdd, [])
 
-  defp list_get_pos(acc, {list_acc, tail_acc} = pos, negs, bdd) do
+  defp list_get_pos(list_acc, last_acc, bdd, lines_acc) do
     case bdd do
       :bdd_bot ->
-        acc
+        lines_acc
 
       :bdd_top ->
-        if list_empty_line?(list_acc, tail_acc, negs) do
-          acc
+        [{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_get_pos(list_acc, last, right, lines_acc)
+          else
+            list_get_pos(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
-          [pos | acc]
+          list_get_pos(list_acc, last_acc, left, lines_acc)
         end
-
-      {{list, tail} = list_type, left, right} ->
-        new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)}
-        list_get_pos(list_get_pos(acc, new_pos, negs, left), pos, [list_type | negs], right)
     end
   end
 
-  # Takes all the paths from the root to the leaves finishing with a 1, computes the intersection
+  # Takes all the lines from the root to the leaves finishing with a 1, computes the intersection
   # of the positives, and calls the condition on the result. Checks it is true for all of them.
-  # As if calling Enum.all? on all the paths of the bdd.
+  # As if calling Enum.all? on all the lines of the bdd.
   defp list_all?(bdd, condition), do: list_all?({:term, :term}, [], bdd, condition)
 
   defp list_all?({list_acc, tail_acc} = pos, negs, bdd, condition) do
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 53b4362906..3c85a390f0 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2031,6 +2031,30 @@ defmodule Module.Types.ExprTest do
                )
              ) == dynamic(integer())
     end
+
+    # test "regressions – duplicate-key list pattern" do
+    #   assert typecheck!(
+    #            # HEAD PATTERN LIST
+    #            [
+    #              # first tuple
+    #              [
+    #                {key, _}
+    #                # second tuple + rest
+    #                | [{key, _} | _] = rest
+    #              ]
+    #            ],
+    #            # BODY – we just return the tail we captured
+    #            rest
+    #          ) ==
+    #            dynamic(
+    #              non_empty_list(
+    #                # every element is {term, term}
+    #                tuple([term(), term()]),
+    #                # the tail can be anything
+    #                term()
+    #              )
+    #            )
+    # end
   end
 
   describe "info" do

From 09a859948d22a30c67bb6bc00f61f46b3f1c7118 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 24 Jul 2025 16:54:24 +0200
Subject: [PATCH 3/9] Add test

---
 .../test/elixir/module/types/expr_test.exs    | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 3c85a390f0..5e1a7e7e57 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2055,6 +2055,25 @@ defmodule Module.Types.ExprTest do
     #              )
     #            )
     # end
+
+    test "Oban.Telemetry pattern matching does not time-out" do
+      assert typecheck!(fn
+               [:oban, :job, _event], _measure, _meta, _opts -> :ok
+               #  [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok
+               [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok
+               [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok
+               [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok
+               #  [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok
+               #  [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok
+               _event, _measure, _meta, _opts -> :ok
+             end)
+             |> equal?(
+               fun(
+                 [term(), term(), term(), term()],
+                 dynamic(atom([:ok]))
+               )
+             )
+    end
   end
 
   describe "info" do

From 5a6519090a55c3c4e07edca1f88c59a9e5d5946a Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Thu, 24 Jul 2025 17:10:48 +0200
Subject: [PATCH 4/9] Add test

---
 .../test/elixir/module/types/expr_test.exs    | 47 ++++++++++++-------
 1 file changed, 30 insertions(+), 17 deletions(-)

diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 5e1a7e7e57..4c24c59dec 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2056,23 +2056,36 @@ defmodule Module.Types.ExprTest do
     #            )
     # end
 
-    test "Oban.Telemetry pattern matching does not time-out" do
-      assert typecheck!(fn
-               [:oban, :job, _event], _measure, _meta, _opts -> :ok
-               #  [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok
-               [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok
-               [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok
-               [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok
-               #  [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok
-               #  [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok
-               _event, _measure, _meta, _opts -> :ok
-             end)
-             |> equal?(
-               fun(
-                 [term(), term(), term(), term()],
-                 dynamic(atom([:ok]))
-               )
-             )
+    test "typecheck! finishes within 200 ms for Oban-style pattern match" do
+      timeout_ms = 200
+
+      task =
+        Task.async(fn ->
+          typecheck!(fn
+            [:oban, :job, _event], _measure, _meta, _opts -> :ok
+            [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok
+            [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok
+            [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok
+            [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok
+            [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok
+            [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok
+            _event, _measure, _meta, _opts -> :ok
+          end)
+        end)
+
+      case Task.yield(task, timeout_ms) || Task.shutdown(task, :brutal_kill) do
+        {:ok, type} ->
+          assert type
+                 |> equal?(
+                   fun(
+                     [term(), term(), term(), term()],
+                     dynamic(atom([:ok]))
+                   )
+                 )
+
+        nil ->
+          flunk("typecheck! did not finish within #{timeout_ms} ms")
+      end
     end
   end
 

From b03ed2336477f0311e8791f0ed7da0df9945771b Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 29 Jul 2025 19:20:43 +0200
Subject: [PATCH 5/9] Functioning map BDDs

---
 lib/elixir/lib/module/types/descr.ex          | 943 ++++++++++++++----
 .../test/elixir/module/types/descr_test.exs   |  56 +-
 2 files changed, 780 insertions(+), 219 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 74981dcb20..ce9bb8ce1f 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -26,6 +26,9 @@ defmodule Module.Types.Descr do
   @bit_top (1 <<< 7) - 1
   @bit_number @bit_integer ||| @bit_float
 
+  defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot]}
+  defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot]}
+
   defmacrop domain_key(key), do: {:domain_key, key}
 
   @domain_key_types [
@@ -45,10 +48,10 @@ defmodule Module.Types.Descr do
 
   @fun_top :fun_top
   @atom_top {:negation, :sets.new(version: 2)}
-  @map_top [{:open, %{}, []}]
+  @map_top {{:open, %{}}, :bdd_top, :bdd_bot}
   @non_empty_list_top {{:term, :term}, :bdd_top, :bdd_bot}
   @tuple_top [{:open, []}]
-  @map_empty [{:closed, %{}, []}]
+  @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot}
 
   @none %{}
   @term %{
@@ -544,6 +547,52 @@ defmodule Module.Types.Descr do
   (bitmap, atom) are checked first for speed since, if they are present,
   the type is non-empty as we normalize then during construction.
   """
+
+  # defguardp is_descr(d)
+  #           when d == :term or
+  #                  (is_map(d) and
+  #                     (Map.has_key?(d, :atom) or Map.has_key?(d, :bitmap) or
+  #                        Map.has_key?(d, :list) or Map.has_key?(d, :map) or
+  #                        Map.has_key?(d, :tuple) or Map.has_key?(d, :fun)))
+
+  # defp bdd_size({{tag, fields = %{}}, l, r}) when tag in [:open, :closed] do
+  #   bdd_size(l) + bdd_size(r) + 1 + Enum.reduce(fields, 0, fn d, acc -> descr_size(d) + acc end)
+  # end
+
+  # defp bdd_size({{list = %{}, last = %{}}, l, r}) do
+  #   bdd_size(l) + bdd_size(r) + 1 + descr_or_domain_size(list) + descr_or_fields_size(last)
+  # end
+
+  defp bdd_size({lit, l, r}), do: bdd_size(l) + bdd_size(r) + 1
+
+  defp bdd_size(bdd), do: 0
+
+  defp dnf_structural_size(dnf) do
+    Enum.reduce(dnf, 0, fn {_tag, pos}, acc ->
+      1 + acc + length(pos)
+    end)
+  end
+
+  defp dnf_size(dnf) do
+    Enum.reduce(dnf, 0, fn {_tag, pos}, acc ->
+      1 + acc + Enum.reduce(pos, 0, fn d, acc -> descr_size(d) + acc end)
+    end)
+  end
+
+  def descr_size(:term), do: 1
+
+  def descr_size(%{} = descr) do
+    Enum.reduce(Map.to_list(descr), 0, fn {key, value}, acc ->
+      acc + descr_size(key, value)
+    end)
+  end
+
+  def descr_size(:tuple, dnf), do: dnf_size(dnf)
+  def descr_size(:fun, bdd), do: bdd_size(bdd)
+  def descr_size(:map, bdd), do: bdd_size(bdd)
+  def descr_size(:list, bdd), do: bdd_size(bdd)
+  def descr_size(_, _), do: 1
+
   def empty?(:term), do: false
 
   def empty?(%{} = descr) do
@@ -555,6 +604,46 @@ defmodule Module.Types.Descr do
         true
 
       descr ->
+        # IO.puts("Woooh")
+        d = descr_size(descr)
+
+        if d > 100 do
+          IO.puts("descr_size(descr): #{d}")
+          IO.puts("The decomposition is:")
+
+          if Map.has_key?(descr, :atom),
+            do: IO.puts("Atom size: #{descr_size(:atom, descr.atom)}")
+
+          if Map.has_key?(descr, :list) do
+            IO.puts("List size: #{descr_size(:list, descr.list)}")
+          else
+            IO.puts("List size: 0")
+          end
+
+          if Map.has_key?(descr, :map) do
+            IO.puts("Map size: #{descr_size(:map, descr.map)}")
+          else
+            IO.puts("Map size: 0")
+          end
+
+          if Map.has_key?(descr, :tuple) do
+            IO.puts("Tuple size: #{descr_size(:tuple, descr.tuple)}")
+            IO.puts("Tuple structural size: #{dnf_structural_size(descr.tuple)}")
+          else
+            IO.puts("Tuple size: 0")
+          end
+
+          if Map.has_key?(descr, :fun) do
+            IO.puts("Fun size: #{descr_size(:fun, descr.fun)}")
+          else
+            IO.puts("Fun size: 0")
+          end
+
+          # dbg(descr)
+        end
+
+        # dbg(descr, limit: :infinity, printable_limit: :infinity, width: :infinity)
+
         not Map.has_key?(descr, :atom) and
           not Map.has_key?(descr, :bitmap) and
           not Map.has_key?(descr, :optional) and
@@ -1979,38 +2068,54 @@ defmodule Module.Types.Descr do
   defp list_tail_unfold(:term), do: @not_non_empty_list
   defp list_tail_unfold(other), do: Map.delete(other, :list)
 
-  defp list_union(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_top, _} -> :bdd_top
-      {_, :bdd_top} -> :bdd_top
-      {:bdd_bot, bdd} -> bdd
-      {bdd, :bdd_bot} -> bdd
-      {{list, l1, r1}, {list, l2, r2}} -> {list, list_union(l1, l2), list_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
-      {{list, l, r}, bdd} -> {list, list_union(l, bdd), list_union(r, bdd)}
+  # Attempt a merge, if the union is between two single lists.
+  defp list_union(list_literal(list1, last1), list_literal(list2, last2)) do
+    cond do
+      subtype?(list1, list2) and subtype?(last1, last2) -> list_literal(list2, last2)
+      subtype?(list2, list1) and subtype?(last2, last1) -> list_literal(list1, last1)
+      equal?(list1, list2) -> list_literal(list1, union(last1, last2))
+      true -> list_union_recur(list_literal(list1, last1), list_literal(list2, last2))
     end
   end
 
-  defp list_intersection(bdd1, bdd2) do
+  defp list_union(bdd1, bdd2), do: list_union_recur(bdd1, bdd2)
+
+  defp list_union_recur(bdd1, bdd2) do
     case {bdd1, bdd2} do
-      {bdd, {{list, tail}, :bdd_top, :bdd_bot}} when is_tuple(bdd) ->
-        if list == :term and tail == :term do
-          bdd
-        else
-          list_intersection_recur(bdd1, bdd2)
-        end
+      {:bdd_top, _} ->
+        :bdd_top
 
-      {{{list, tail}, :bdd_top, :bdd_bot}, bdd} when is_tuple(bdd) ->
-        if list == :term and tail == :term do
-          bdd
-        else
-          list_intersection_recur(bdd1, bdd2)
-        end
+      {_, :bdd_top} ->
+        :bdd_top
 
-      _ ->
-        list_intersection_recur(bdd1, bdd2)
+      {:bdd_bot, bdd} ->
+        bdd
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {{list, l1, r1}, {list, l2, r2}} ->
+        {list, list_union(l1, l2), list_union(r1, r2)}
+
+      {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 ->
+        {list1, list_union(l1, bdd2), list_union(r1, bdd2)}
+
+      {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 ->
+        {list2, list_union(bdd1, l2), list_union(bdd1, r2)}
+    end
+  end
+
+  defp is_list_top?({{list, tail}, :bdd_top, :bdd_bot}) do
+    list == :term and tail == :term
+  end
+
+  defp is_list_top?(_), do: false
+
+  defp list_intersection(bdd1, bdd2) do
+    cond do
+      is_list_top?(bdd1) and is_tuple(bdd2) -> bdd2
+      is_list_top?(bdd2) and is_tuple(bdd1) -> bdd1
+      true -> list_intersection_recur(bdd1, bdd2)
     end
     |> case do
       {_, :bdd_bot, :bdd_bot} -> :bdd_bot
@@ -2039,24 +2144,38 @@ defmodule Module.Types.Descr do
       # whole bdd).
       # Note: instead of inserting the bdd at the root, we decided to intersect with
       # every atom in the bdd. If empty, then replace with the right tree.
-      {bdd, {list, :bdd_top, :bdd_bot}} ->
-        intersect_bdd_with_list(bdd, list)
+      # {bdd, {list, :bdd_top, :bdd_bot}} ->
+      #   intersect_bdd_with_list(bdd, list)
 
-      {bdd, {list, :bdd_bottom, :bdd_top}} ->
-        {list, :bdd_bottom, bdd}
+      # {bdd, {list, :bdd_bottom, :bdd_top}} ->
+      #   {list, :bdd_bottom, bdd}
 
-      {{list, :bdd_top, :bdd_bottom}, bdd} ->
-        intersect_bdd_with_list(bdd, list)
+      # {{list, :bdd_top, :bdd_bottom}, bdd} ->
+      #   intersect_bdd_with_list(bdd, list)
 
-      {{list, :bdd_bottom, :bdd_top}, bdd} ->
-        {list, :bdd_bottom, bdd}
+      # {{list, :bdd_bottom, :bdd_top}, bdd} ->
+      #   {list, :bdd_bottom, bdd}
+      {list_literal(list1, last1), list_literal(list2, last2)} ->
+        try do
+          list1 = non_empty_intersection!(list1, list2)
+          last1 = non_empty_intersection!(last1, last2)
+          list_literal(list1, last1)
+        catch
+          :empty -> :bdd_bot
+        end
 
       # General cases
       {{list, l1, r1}, {list, l2, r2}} ->
         {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)}
 
-      {{list, l, r}, bdd} ->
-        {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)}
+      {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 ->
+        {list1, list_intersection_recur(l1, bdd2), list_intersection_recur(r1, bdd2)}
+
+      {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 ->
+        {list2, list_intersection_recur(bdd1, l2), list_intersection_recur(bdd1, r2)}
+
+        # {{list, l, r}, bdd} ->
+        # {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)}
     end
   end
 
@@ -2093,12 +2212,29 @@ defmodule Module.Types.Descr do
   # The result may be larger than the initial bdd1, which is maintained in the accumulator.
   defp list_difference(bdd1, bdd2) do
     case {bdd1, bdd2} do
-      {:bdd_bot, _} -> :bdd_bot
-      {_, :bdd_top} -> :bdd_bot
-      {bdd, :bdd_bot} -> bdd
-      {:bdd_top, {lst, l, r}} -> {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)}
-      {{lst, l1, r1}, {lst, l2, r2}} -> {lst, list_difference(l1, l2), list_difference(r1, r2)}
-      {{lst, l, r}, bdd} -> {lst, list_difference(l, bdd), list_difference(r, bdd)}
+      {:bdd_bot, _} ->
+        :bdd_bot
+
+      {_, :bdd_top} ->
+        :bdd_bot
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {:bdd_top, {lst, l, r}} ->
+        {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)}
+
+      {{lst, l1, r1}, {lst, l2, r2}} ->
+        {lst, list_difference(l1, l2), list_difference(r1, r2)}
+
+      {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 < lst2 ->
+        {lst1, list_difference(l1, bdd2), list_difference(r1, bdd2)}
+
+      {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 > lst2 ->
+        {lst2, list_difference(bdd1, l2), list_difference(bdd1, r2)}
+
+        # {{lst, l, r}, bdd} ->
+        #   {lst, list_difference(l, bdd), list_difference(r, bdd)}
     end
     |> case do
       {_, :bdd_bot, :bdd_bot} -> :bdd_bot
@@ -2449,6 +2585,239 @@ defmodule Module.Types.Descr do
   # and other keys bound to any type. It will be represented using a map domain that maps
   # atom to `if_set(integer())`, and every other domain key to `term_or_optional()`.
 
+  # ## TESTING
+  # def map_merge(%{map: bdd1} = d1, %{map: bdd2} = d2) do
+  #   # Starting accumulator: the empty map type
+  #   res = %{map: :bdd_bot}
+
+  #   # Recursive auxiliary function
+  #   aux = fn aux, accu, bdd1, bdd2 ->
+  #     case {map_first_label(bdd1), map_first_label(bdd2)} do
+  #       {:dummy, :dummy} ->
+  #         {some1, none1} = map_empty_cases(bdd1)
+  #         {some2, none2} = map_empty_cases(bdd2)
+
+  #         some = some1 or some2
+  #         none = none1 and none2
+
+  #         # Approximation if some and not none
+  #         if some do
+  #           fields = :maps.from_list(accu)
+  #           map_union(res, %{map: map_new(:open, fields)})
+  #         else
+  #           res
+  #         end
+
+  #       {l1, l2} ->
+  #         l = min_label(l1, l2)
+
+  #         # Split along label l
+  #         split1 = map_split(bdd1, l)
+  #         split2 = map_split(bdd2, l)
+
+  #         Enum.reduce(split1, res, fn {t1, d1_next}, acc ->
+  #           Enum.reduce(split2, acc, fn {t2, d2_next}, acc2 ->
+  #             t =
+  #               if Map.has_key?(t2, :optional) and t2.optional do
+  #                 union(t1, remove_optional(t2))
+  #               else
+  #                 t2
+  #               end
+
+  #             aux.(aux, [{l, t} | accu], d1_next.map, d2_next.map)
+  #           end)
+  #         end)
+  #     end
+  #   end
+
+  #   aux.(aux, [], bdd1, bdd2)
+  # end
+
+  # defp map_first_label(:bdd_top), do: :dummy
+  # defp map_first_label(:bdd_bot), do: :dummy
+
+  # defp map_first_label({{tag, fields}, :bdd_top, :bdd_bot}) do
+  #   case :maps.next(:maps.iterator(fields)) do
+  #     :none -> :dummy
+  #     {key, _value, _iter} -> key
+  #   end
+  # end
+
+  # defp map_first_label({{_tag, _fields}, l, _r}), do: map_first_label(l)
+
+  # # Returns {some, none}
+  # defp map_empty_cases(bdd) do
+  #   map_bdd_get(bdd)
+  #   |> Enum.reduce({false, true}, fn
+  #     {:open, fields, _negs}, {some, none} ->
+  #       some = some or map_size(fields) > 0
+  #       none = none and map_size(fields) == 0
+  #       {some, none}
+
+  #     {:closed, fields, _negs}, {some, none} ->
+  #       some = some or map_size(fields) > 0
+  #       none = none and map_size(fields) == 0
+  #       {some, none}
+  #   end)
+  # end
+
+  # # Split a BDD into a list of {type_for_label, rest_of_map}
+  # defp map_split(bdd, label) do
+  #   map_bdd_get(bdd)
+  #   |> Enum.map(fn {tag, fields, negs} ->
+  #     case :maps.take(label, fields) do
+  #       {value, fields_rest} ->
+  #         {remove_optional(value), %{map: map_new(tag, fields_rest)}}
+
+  #       :error ->
+  #         # If absent
+  #         type_for_label =
+  #           case tag do
+  #             :open -> term_or_optional()
+  #             :closed -> not_set()
+  #             domains = %{} -> Map.get(domains, domain_key(:atom), not_set())
+  #           end
+
+  #         {type_for_label, %{map: map_new(tag, fields)}}
+  #     end
+  #   end)
+  # end
+
+  # defp min_label(:dummy, :dummy), do: :dummy
+  # defp min_label(:dummy, l), do: l
+  # defp min_label(l, :dummy), do: l
+  # defp min_label(l1, l2), do: if(l1 <= l2, do: l1, else: l2)
+
+  @doc """
+  Type-level merge for maps (like `Map.merge/2`).
+
+  Semantics per OCaml code:
+  - For each key `l`, if the right map's type for `l` **may be absent**,
+    the merged type for `l` is `left(l) ∪ present(right(l))`;
+    otherwise it is `right(l)` (right-biased override).
+  - Domains are merged with the same rule (component-wise).
+  - If either side is `:open`, the result is effectively open (via domains).
+
+  Returns `{:ok, merged_descr}` or `:badmap` if either input is not a (possibly dynamic) map type.
+  """
+  def map_merge(:term, _), do: :badmap
+  def map_merge(_, :term), do: :badmap
+
+  def map_merge(%{} = descr1, %{} = descr2) do
+    case {:maps.take(:dynamic, descr1), :maps.take(:dynamic, descr2)} do
+      {:error, :error} ->
+        with {:ok, m} <- map_merge_static(descr1, descr2) do
+          {:ok, m}
+        else
+          :badmap -> :badmap
+        end
+
+      {{dyn1, stat1}, :error} ->
+        with {:ok, stat_stat} <- map_merge_static(stat1, descr2),
+             {:ok, dyn_stat} <- map_merge_static(dynamic(dyn1), descr2) do
+          {:ok, union(stat_stat, dynamic(dyn_stat))}
+        else
+          :badmap -> :badmap
+        end
+
+      {:error, {dyn2, stat2}} ->
+        with {:ok, stat_stat} <- map_merge_static(descr1, stat2),
+             {:ok, stat_dyn} <- map_merge_static(descr1, dynamic(dyn2)) do
+          {:ok, union(stat_stat, dynamic(stat_dyn))}
+        else
+          :badmap -> :badmap
+        end
+
+      {{dyn1, stat1}, {dyn2, stat2}} ->
+        with {:ok, ss} <- map_merge_static(stat1, stat2),
+             {:ok, sd} <- map_merge_static(stat1, dynamic(dyn2)),
+             {:ok, ds} <- map_merge_static(dynamic(dyn1), stat2),
+             {:ok, dd} <- map_merge_static(dynamic(dyn1), dynamic(dyn2)) do
+          {:ok, union(ss, union(dynamic(sd), union(dynamic(ds), dynamic(dd))))}
+        else
+          :badmap -> :badmap
+        end
+    end
+  end
+
+  # --- Core static merger on the BDDs ---------------------------------------
+
+  defp map_merge_static(%{map: bdd1} = d1, %{map: bdd2} = d2) do
+    # both inputs must be exclusively map (no extra components)
+    if map_only?(d1) and map_only?(d2) do
+      # Build the result by taking the cross-product of positive literals
+      # (DNF lines) and unioning merged literals.
+      merged_bdd =
+        map_bdd_get(bdd1)
+        |> Enum.reduce(:bdd_bot, fn {tag1, fields1, _negs1}, acc1 ->
+          Enum.reduce(map_bdd_get(bdd2), acc1, fn {tag2, fields2, _negs2}, acc2 ->
+            {new_tag_or_domains, new_fields} =
+              map_literal_merge(tag1, fields1, tag2, fields2)
+
+            map_union(acc2, {{new_tag_or_domains, new_fields}, :bdd_top, :bdd_bot})
+          end)
+        end)
+
+      {:ok, %{map: merged_bdd}}
+    else
+      :badmap
+    end
+  end
+
+  defp map_merge_static(_, _), do: :badmap
+
+  # --- Literal / domain merge (right-biased with "optional means fallback") --
+
+  # Merge two map literals (tag-or-domains + fields) into one literal.
+  defp map_literal_merge(tag_or_domains1, fields1, tag_or_domains2, fields2) do
+    default1 = map_key_tag_to_type(tag_or_domains1)
+    default2 = map_key_tag_to_type(tag_or_domains2)
+
+    # Merge domains first (handles openness and all non-atom key domains)
+    new_tag_or_domains = map_domain_merge(tag_or_domains1, tag_or_domains2)
+
+    # For explicit atom keys: symmetrical merge with defaults for missing keys
+    new_fields =
+      symmetrical_merge(fields1, default1, fields2, default2, fn _key, v1, v2 ->
+        map_merge_value(v1, v2)
+      end)
+
+    {new_tag_or_domains, new_fields}
+  end
+
+  # Component-wise merge of domains. For every domain key dk in @domain_key_types:
+  # result(dk) = merge_value( domain1(dk), domain2(dk) ).
+  # If all resulting domain entries are empty/optional, collapse to :closed.
+  defp map_domain_merge(tag_or_domains1, tag_or_domains2) do
+    new_domains =
+      for domain_key(_) = dk <- @domain_key_types, reduce: %{} do
+        acc ->
+          v1 = map_domain_default(tag_or_domains1, dk)
+          v2 = map_domain_default(tag_or_domains2, dk)
+          v = map_merge_value(v1, v2)
+
+          if empty_or_optional?(v) do
+            acc
+          else
+            Map.put(acc, dk, v)
+          end
+      end
+
+    if map_size(new_domains) == 0, do: :closed, else: new_domains
+  end
+
+  # Default value for a domain when not explicitly present in the literal.
+  defp map_domain_default(:open, _dk), do: term_or_optional()
+  defp map_domain_default(:closed, _dk), do: not_set()
+  defp map_domain_default(domains = %{}, dk), do: Map.get(domains, dk, not_set())
+
+  # Merge the two value types for a key, per OCaml's rule:
+  # if right may be absent, use left ∪ present(right), else right.
+  defp map_merge_value(left, right) do
+    {optional?, right_present} = pop_optional_static(right)
+    if optional?, do: union(left, right_present), else: right
+  end
+
   defp map_descr(tag, pairs, default, force?) do
     {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false)
 
@@ -2513,25 +2882,73 @@ 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, []}]
+  defp map_new(tag, fields = %{}), do: {{tag, fields}, :bdd_top, :bdd_bot}
 
   defp map_only?(descr), do: empty?(Map.delete(descr, :map))
 
-  defp map_union(dnf1, dnf2) do
-    # Union is just concatenation, but we rely on some optimization strategies to
-    # avoid the list to grow when possible
+  defp map_union(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_top, _} ->
+        :bdd_top
 
-    # first pass trying to identify patterns where two maps can be fused as one
-    with [map1] <- dnf1,
-         [map2] <- dnf2,
-         optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do
-      [optimized]
-    else
-      # otherwise we just concatenate and remove structural duplicates
-      _ -> dnf1 ++ (dnf2 -- dnf1)
+      {_, :bdd_top} ->
+        :bdd_top
+
+      {:bdd_bot, bdd} ->
+        bdd
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {map_literal(tag1, fields1), map_literal(tag2, fields2)} ->
+        case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do
+          {tag, fields, []} ->
+            {{tag, fields}, :bdd_top, :bdd_bot}
+
+          nil ->
+            lit1 = {tag1, fields1}
+            lit2 = {tag2, fields2}
+
+            cond do
+              lit1 == lit2 -> {lit1, :bdd_top, :bdd_bot}
+              lit1 < lit2 -> {lit1, :bdd_top, {lit2, :bdd_top, :bdd_bot}}
+              lit1 > lit2 -> {lit2, :bdd_top, {lit1, :bdd_top, :bdd_bot}}
+            end
+        end
+
+      {{map, l1, r1}, {map, l2, r2}} ->
+        {map, map_union(l1, l2), map_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
+      {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 ->
+        {map1, map_union(l1, bdd2), map_union(r1, bdd2)}
+
+      {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 ->
+        {map2, map_union(bdd1, l2), map_union(bdd1, r2)}
+
+        # {{map, l, r}, bdd} ->
+        #   {map, map_union(l, bdd), map_union(r, bdd)}
     end
   end
 
+  # defp map_union(dnf1, dnf2) do
+  #   # Union is just concatenation, but we rely on some optimization strategies to
+  #   # avoid the list to grow when possible
+
+  #   # first pass trying to identify patterns where two maps can be fused as one
+  #   with [map1] <- dnf1,
+  #        [map2] <- dnf2,
+  #        optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do
+  #     [optimized]
+  #   else
+  #     # otherwise we just concatenate and remove structural duplicates
+  #     _ -> dnf1 ++ (dnf2 -- dnf1)
+  #   end
+  # end
+  # defp maybe_optimize_map_union(map, map), do: map
+
   defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do
     case map_union_optimization_strategy(tag1, pos1, tag2, pos2) do
       :all_equal ->
@@ -2555,7 +2972,8 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp maybe_optimize_map_union(_, _), do: nil
+  defp maybe_optimize_map_union(map1, map2),
+    do: raise("I should not be there: see inputs #{inspect(map1)} and #{inspect(map2)}")
 
   defp map_union_optimization_strategy(tag1, pos1, tag2, pos2)
   defp map_union_optimization_strategy(tag, pos, tag, pos), do: :all_equal
@@ -2627,21 +3045,111 @@ defmodule Module.Types.Descr do
     if subtype?(v2, v1), do: :right_subtype_of_left
   end
 
-  # Given two unions of maps, intersects each pair of maps.
-  defp map_intersection(dnf1, dnf2) do
-    for {tag1, pos1, negs1} <- dnf1,
-        {tag2, pos2, negs2} <- dnf2,
-        reduce: [] do
-      acc ->
+  defp is_map_top?({{tag, fields}, :bdd_top, :bdd_bot}) do
+    tag == :open and map_size(fields) == 0
+  end
+
+  defp is_map_top?(_), do: false
+
+  defp map_intersection(bdd1, bdd2) do
+    # If intersecting with the top map type, no-op
+    cond do
+      is_map_top?(bdd1) and is_tuple(bdd2) -> bdd2
+      is_map_top?(bdd2) and is_tuple(bdd1) -> bdd1
+      true -> map_intersection_recur(bdd1, bdd2)
+    end
+  end
+
+  defp map_intersection_recur(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
+
+      {map_literal(tag1, fields1), map_literal(tag2, fields2)} ->
         try do
-          {tag, fields} = map_literal_intersection(tag1, pos1, tag2, pos2)
-          prepend_to_map_dnf(tag, fields, negs1 ++ (negs2 -- negs1), acc)
+          map = map_literal_intersection(tag1, fields1, tag2, fields2)
+          {map, :bdd_top, :bdd_bot}
         catch
-          :empty -> acc
+          :empty -> :bdd_bot
         end
+
+      # 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).
+      # No: bc we want to have increasing order of literals.
+      # {bdd, {map, :bdd_top, :bdd_bot}} ->
+      #   {map, bdd, :bdd_bot}
+
+      # {bdd, {map, :bdd_bot, :bdd_top}} ->
+      #   {map, :bdd_bot, bdd}
+
+      # {{map, :bdd_top, :bdd_bot}, bdd} ->
+      #   {map, bdd, :bdd_bot}
+
+      # {{map, :bdd_bot, :bdd_top}, bdd} ->
+      #   {map, :bdd_bot, bdd}
+
+      # General cases
+      {{map, l1, r1}, {map, l2, r2}} ->
+        {map, map_intersection_recur(l1, l2), map_intersection_recur(r1, r2)}
+
+      {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 ->
+        {map1, map_intersection_recur(l1, bdd2), map_intersection_recur(r1, bdd2)}
+
+      {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 ->
+        {map2, map_intersection_recur(bdd1, l2), map_intersection_recur(bdd1, r2)}
+
+        # {{map, l, r}, bdd} ->
+        #   {map, map_intersection_recur(l, bdd), map_intersection_recur(r, bdd)}
     end
   end
 
+  defp map_difference(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_bot, _} ->
+        :bdd_bot
+
+      {_, :bdd_top} ->
+        :bdd_bot
+
+      {bdd, :bdd_bot} ->
+        bdd
+
+      {:bdd_top, {map, l, r}} ->
+        {map, map_difference(:bdd_top, l), map_difference(:bdd_top, r)}
+
+      {{map, l1, r1}, {map, l2, r2}} ->
+        {map, map_difference(l1, l2), map_difference(r1, r2)}
+
+      {{map1, l1, r1}, {map2, _l2, _r2}} when map1 < map2 ->
+        {map1, map_difference(l1, bdd2), map_difference(r1, bdd2)}
+
+      {{map1, _l1, _r1}, {map2, l2, r2}} when map1 > map2 ->
+        {map2, map_difference(bdd1, l2), map_difference(bdd1, r2)}
+
+        # {{map, l, r}, bdd} -> {map, map_difference(l, bdd), map_difference(r, bdd)}
+    end
+  end
+
+  # defp map_negation(bdd) do
+  #   case bdd do
+  #     :bdd_bot -> :bdd_top
+  #     :bdd_top -> :bdd_bot
+  #     {map, l, r} -> {map, map_negation(l), map_negation(r)}
+  #   end
+  # end
+
   # Intersects two map literals; throws if their intersection is empty.
   # Both open: the result is open.
   defp map_literal_intersection(:open, map1, :open, map2) do
@@ -2750,61 +3258,90 @@ defmodule Module.Types.Descr do
     if empty?(type), do: throw(:empty), else: type
   end
 
-  defp map_difference(_, dnf) when dnf == @map_top, do: []
-  defp map_difference(dnf, dnf), do: []
-
-  defp map_difference(dnf1, dnf2) do
-    Enum.reduce(dnf2, dnf1, fn
-      {:open, fields2, []}, current_dnf when map_size(fields2) == 1 ->
-        # Optimization: we are removing an open map with one field.
-        Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
-          {key, value, _rest} = :maps.next(:maps.iterator(fields2))
-          t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value)
+  # defp map_difference(_, dnf) when dnf == @map_top, do: []
+  # defp map_difference(dnf, dnf), do: []
+
+  # defp map_difference(dnf1, dnf2) do
+  #   Enum.reduce(dnf2, dnf1, fn
+  #     {:open, fields2, []}, current_dnf when map_size(fields2) == 1 ->
+  #       # Optimization: we are removing an open map with one field.
+  #       Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
+  #         {key, value, _rest} = :maps.next(:maps.iterator(fields2))
+  #         t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value)
+
+  #         if empty?(t_diff) do
+  #           acc
+  #         else
+  #           {tag, pos} = {tag1, Map.put(fields1, key, t_diff)}
+  #           entry = {tag, pos, negs1}
+
+  #           cond do
+  #             :lists.member({tag, pos}, negs1) -> acc
+  #             :lists.member(entry, acc) -> acc
+  #             true -> [entry | acc]
+  #           end
+  #         end
+  #       end)
+
+  #     {tag2, fields2, negs2}, current_dnf ->
+  #       Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
+  #         negs =
+  #           if :lists.member({tag2, fields2}, negs1) do
+  #             negs1
+  #           else
+  #             [{tag2, fields2} | negs1]
+  #           end
+
+  #         acc = prepend_to_map_dnf(tag1, fields1, negs, acc)
+
+  #         Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc ->
+  #           try do
+  #             {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2)
+  #             prepend_to_map_dnf(tag, fields, negs1, acc)
+  #           catch
+  #             :empty -> acc
+  #           end
+  #         end)
+  #       end)
+  #   end)
+  # end
+
+  # defp prepend_to_map_dnf(tag, fields, negs, acc) do
+  #   entry = {tag, fields, negs}
+
+  #   cond do
+  #     :lists.member({tag, fields}, negs) -> acc
+  #     :lists.member(entry, acc) -> acc
+  #     true -> [entry | acc]
+  #   end
+  # end
 
-          if empty?(t_diff) do
-            acc
-          else
-            {tag, pos} = {tag1, Map.put(fields1, key, t_diff)}
-            entry = {tag, pos, negs1}
-
-            cond do
-              :lists.member({tag, pos}, negs1) -> acc
-              :lists.member(entry, acc) -> acc
-              true -> [entry | acc]
-            end
-          end
-        end)
-
-      {tag2, fields2, negs2}, current_dnf ->
-        Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
-          negs =
-            if :lists.member({tag2, fields2}, negs1) do
-              negs1
-            else
-              [{tag2, fields2} | negs1]
-            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.
+  def map_bdd_get(bdd) do
+    # dbg(bdd)
+    map_bdd_get([], {:open, %{}}, [], bdd)
+  end
 
-          acc = prepend_to_map_dnf(tag1, fields1, negs, acc)
+  defp map_bdd_get(acc, {tag, fields} = map, negs, bdd) do
+    case bdd do
+      :bdd_bot ->
+        acc
 
-          Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc ->
-            try do
-              {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2)
-              prepend_to_map_dnf(tag, fields, negs1, acc)
-            catch
-              :empty -> acc
-            end
-          end)
-        end)
-    end)
-  end
+      :bdd_top ->
+        if map_empty?(tag, fields, negs), do: acc, else: [{tag, fields, negs} | acc]
 
-  defp prepend_to_map_dnf(tag, fields, negs, acc) do
-    entry = {tag, fields, negs}
+      {{next_tag, next_fields} = next_map, left, right} ->
+        acc =
+          try do
+            new_pos = map_literal_intersection(tag, fields, next_tag, next_fields)
+            map_bdd_get(acc, new_pos, negs, left)
+          catch
+            :empty -> acc
+          end
 
-    cond do
-      :lists.member({tag, fields}, negs) -> acc
-      :lists.member(entry, acc) -> acc
-      true -> [entry | acc]
+        map_bdd_get(acc, map, [next_map | negs], right)
     end
   end
 
@@ -2851,15 +3388,15 @@ 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, []}]}, key)
+  defp map_fetch_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key)
        when not is_map_key(fields, key) do
     map_key_tag_to_type(tag_or_domains) |> pop_optional_static()
   end
 
   # Takes a map dnf and returns the union of types it can take for a given key.
   # If the key may be undefined, it will contain the `not_set()` type.
-  defp map_fetch_static(%{map: dnf}, key) do
-    dnf
+  defp map_fetch_static(%{map: bdd}, key) do
+    map_bdd_get(bdd)
     |> Enum.reduce(none(), fn
       # Optimization: if there are no negatives and key exists, return its value
       {_tag, %{^key => value}, []}, acc ->
@@ -3022,28 +3559,20 @@ defmodule Module.Types.Descr do
     end
   end
 
-  def map_refresh_domain(%{map: [{tag, fields, []}]}, domain, type) do
-    %{map: [{map_refresh_tag(tag, domain, type), fields, []}]}
+  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}}
   end
 
-  def map_refresh_domain(%{map: dnf}, domain, type) do
-    Enum.map(dnf, fn
-      {tag, fields, []} ->
-        {map_refresh_tag(tag, domain, type), fields, []}
-
-      {tag, fields, negs} ->
-        # For negations, we count on the idea that a negation will not remove any
-        # type from a domain unless it completely cancels out the type.
-        # So for any non-empty map dnf, we just update the domain with the new type,
-        # as well as its negations to keep them accurate.
-        {map_refresh_tag(tag, domain, type), fields,
-         Enum.map(negs, fn {neg_tag, neg_fields} ->
-           {map_refresh_tag(neg_tag, domain, type), neg_fields}
-         end)}
-    end)
+  # TODO: TEST THIS (previous implem was wrong)
+  def map_refresh_domain(%{map: bdd}, domain, type) do
+    # For negations, we count on the idea that a negation will not remove any
+    # type from a domain unless it completely cancels out the type.
+    # So for any non-empty map dnf, we just update the domain with the new type,
+    # as well as its negations to keep them accurate.
+    %{map: bdd_map(bdd, fn {tag, fields} -> {map_refresh_tag(tag, domain, type), fields} end)}
   end
 
-  def map_refresh_atom(descr = %{map: dnf}, atom_key, type) do
+  def map_refresh_atom(descr = %{map: bdd}, atom_key, type) do
     case atom_key do
       {:union, keys} ->
         keys
@@ -3051,10 +3580,9 @@ defmodule Module.Types.Descr do
         |> Enum.reduce(descr, fn key, acc -> map_refresh_key(acc, key, type) end)
 
       {:negation, keys} ->
-        # 1) Fetch all the possible keys in the dnf
+        # 1) Fetch all the possible keys in the bdd
         # 2) Get them all, except the ones in neg_atoms
-        possible_keys = map_fetch_all_key_names(dnf)
-        considered_keys = :sets.subtract(possible_keys, keys)
+        considered_keys = map_fetch_all_key_names(bdd) |> :sets.subtract(keys)
 
         considered_keys
         |> :sets.to_list()
@@ -3078,20 +3606,22 @@ defmodule Module.Types.Descr do
   end
 
   # Directly inserts a key of a given type into every positive and negative map.
-  defp map_put_static(%{map: dnf} = descr, key, type) do
-    dnf =
-      Enum.map(dnf, fn {tag, fields, negs} ->
-        {tag, Map.put(fields, key, type),
-         Enum.map(negs, fn {neg_tag, neg_fields} ->
-           {neg_tag, Map.put(neg_fields, key, type)}
-         end)}
-      end)
+  defp map_put_static(%{map: bdd} = descr, key, type) do
+    bdd = bdd_map(bdd, fn {tag, fields} -> {tag, Map.put(fields, key, type)} end)
 
-    %{descr | map: dnf}
+    %{descr | map: bdd}
   end
 
   defp map_put_static(descr, _key, _type), do: descr
 
+  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
+
   @doc """
   Removes a key from a map type.
   """
@@ -3222,7 +3752,7 @@ defmodule Module.Types.Descr do
 
   defp unfold_domains(domains = %{}), do: domains
 
-  defp map_get_static(%{map: [{tag_or_domains, fields, []}]}, key_descr) do
+  defp map_get_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key_descr) do
     # For each non-empty kind of type in the key_descr, we add the corresponding key domain in a union.
     domains = unfold_domains(tag_or_domains)
 
@@ -3230,20 +3760,23 @@ defmodule Module.Types.Descr do
     |> covered_key_types()
     |> Enum.reduce(none(), fn
       # Note: we could stop if we reach term_or_optional()
-      {:atom, atom_type}, acc -> map_get_atom([{domains, fields, []}], atom_type) |> union(acc)
-      key_type, acc -> Map.get(domains, key_type, not_set()) |> union(acc)
+      {:atom, atom_type}, acc ->
+        map_get_atom(map_literal(domains, fields), atom_type) |> union(acc)
+
+      key_type, acc ->
+        Map.get(domains, key_type, not_set()) |> union(acc)
     end)
   end
 
-  defp map_get_static(%{map: dnf}, key_descr) do
+  defp map_get_static(%{map: bdd}, key_descr) do
     key_descr
     |> covered_key_types()
     |> Enum.reduce(none(), fn
       {:atom, atom_type}, acc ->
-        map_get_atom(dnf, atom_type) |> union(acc)
+        map_get_atom(bdd, atom_type) |> union(acc)
 
       domain_key, acc ->
-        map_get_domain(dnf, domain_key) |> union(acc)
+        map_get_domain(bdd, domain_key) |> union(acc)
     end)
   end
 
@@ -3264,13 +3797,13 @@ defmodule Module.Types.Descr do
   #   Fetching a key of type `atom() and not (:a)` from a map of type
   #   `%{a: atom(), b: float(), atom() => pid()}`
   #   would return either `nil` or `float()` (key `:b`) or `pid()` (key `atom()`), but not `atom()` (key `:a`).
-  defp map_get_atom(dnf, atom_type) do
+  defp map_get_atom(bdd, atom_type) do
     case atom_type do
       {:union, atoms} ->
         atoms
         |> :sets.to_list()
         |> Enum.reduce(none(), fn atom, acc ->
-          {static_optional?, type} = map_fetch_static(%{map: dnf}, atom)
+          {static_optional?, type} = map_fetch_static(%{map: bdd}, atom)
 
           if static_optional? do
             union(type, acc) |> nil_or_type() |> if_set()
@@ -3280,15 +3813,15 @@ defmodule Module.Types.Descr do
         end)
 
       {:negation, atoms} ->
-        # 1) Fetch all the possible keys in the dnf
+        # 1) Fetch all the possible keys in the bdd
         # 2) Get them all, except the ones in neg_atoms
-        possible_keys = map_fetch_all_key_names(dnf)
+        possible_keys = map_fetch_all_key_names(bdd)
         considered_keys = :sets.subtract(possible_keys, atoms)
 
         considered_keys
         |> :sets.to_list()
         |> Enum.reduce(none(), fn atom, acc ->
-          {static_optional?, type} = map_fetch_static(%{map: dnf}, atom)
+          {static_optional?, type} = map_fetch_static(%{map: bdd}, atom)
 
           if static_optional? do
             union(type, acc) |> nil_or_type() |> if_set()
@@ -3296,13 +3829,13 @@ defmodule Module.Types.Descr do
             union(type, acc)
           end
         end)
-        |> union(map_get_domain(dnf, domain_key(:atom)))
+        |> union(map_get_domain(bdd, domain_key(:atom)))
     end
   end
 
   # Fetch all present keys in a map dnf (including negated ones).
-  defp map_fetch_all_key_names(dnf) do
-    dnf
+  defp map_fetch_all_key_names(bdd) do
+    map_bdd_get(bdd)
     |> Enum.reduce(:sets.new(version: 2), fn {_tag, fields, negs}, acc ->
       keys = :sets.from_list(Map.keys(fields))
 
@@ -3316,8 +3849,8 @@ defmodule Module.Types.Descr do
   end
 
   # Take a map dnf and return the union of types for the given key domain.
-  defp map_get_domain(dnf, domain_key(_) = domain_key) do
-    dnf
+  defp map_get_domain(bdd, domain_key(_) = domain_key) do
+    map_bdd_get(bdd)
     |> Enum.reduce(none(), fn
       {tag, _fields, []}, acc when is_atom(tag) ->
         map_key_tag_to_type(tag) |> union(acc)
@@ -3368,7 +3901,8 @@ defmodule Module.Types.Descr do
     case :maps.take(:dynamic, descr) do
       :error ->
         if descr_key?(descr, :map) and map_only?(descr) do
-          {optional?, taken, result} = map_take_static(descr, key, initial)
+          {optional?, taken, result} =
+            map_take_static(descr, key, initial)
 
           cond do
             taken == nil -> {nil, updater.(result)}
@@ -3386,9 +3920,14 @@ defmodule Module.Types.Descr do
           result = union(dynamic(updater.(dynamic_result)), updater.(static_result))
 
           cond do
-            static_taken == nil and dynamic_taken == nil -> {nil, result}
-            static_optional? or empty?(dynamic_taken) -> :badkey
-            true -> {union(dynamic(dynamic_taken), static_taken), result}
+            static_taken == nil and dynamic_taken == nil ->
+              {nil, result}
+
+            static_optional? or empty?(dynamic_taken) ->
+              :badkey
+
+            true ->
+              {union(dynamic(dynamic_taken), static_taken), result}
           end
         else
           :badmap
@@ -3398,7 +3937,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, []}]} = descr, key, initial)
+  defp map_take_static(%{map: {{tag, fields}, :bdd_top, :bdd_bot}} = descr, key, initial)
        when not is_map_key(fields, key) do
     case tag do
       :open -> {true, maybe_union(initial, fn -> term() end), descr}
@@ -3406,9 +3945,10 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp map_take_static(%{map: dnf}, key, initial) do
+  defp map_take_static(%{map: bdd}, key, initial) do
     {value, map} =
-      Enum.reduce(dnf, {initial, none()}, fn
+      map_bdd_get(bdd)
+      |> Enum.reduce({initial, none()}, fn
         # Optimization: if there are no negatives, we can directly remove the key.
         {tag, fields, []}, {value, map} ->
           {fst, snd} = map_pop_key(tag, fields, key)
@@ -3447,9 +3987,7 @@ defmodule Module.Types.Descr do
   # Short-circuits if it finds a non-empty map literal in the union.
   # Since the algorithm is recursive, we implement the short-circuiting
   # as throw/catch.
-  defp map_empty?(dnf) do
-    Enum.all?(dnf, fn {tag, pos, negs} -> map_empty?(tag, pos, negs) end)
-  end
+  defp map_empty?(bdd), do: map_bdd_get(bdd) == []
 
   defp map_empty?(_, pos, []), do: Enum.any?(Map.to_list(pos), fn {_, v} -> empty?(v) end)
   defp map_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true
@@ -3460,7 +3998,7 @@ defmodule Module.Types.Descr do
       atom_default = map_key_tag_to_type(tag)
       neg_atom_default = map_key_tag_to_type(neg_tag)
 
-      (Enum.all?(neg_fields, fn {neg_key, neg_type} ->
+      (Enum.all?(Map.to_list(neg_fields), fn {neg_key, neg_type} ->
          cond do
            # Ignore keys present in both maps; will be handled below
            is_map_key(fields, neg_key) ->
@@ -3481,7 +4019,7 @@ defmodule Module.Types.Descr do
              empty?(diff) or map_empty?(tag, Map.put(fields, neg_key, diff), negs)
          end
        end) and
-         Enum.all?(fields, fn {key, type} ->
+         Enum.all?(Map.to_list(fields), fn {key, type} ->
            case neg_fields do
              %{^key => neg_type} ->
                diff = difference(type, neg_type)
@@ -3568,24 +4106,31 @@ defmodule Module.Types.Descr do
   end
 
   # Use heuristics to normalize a map dnf for pretty printing.
-  defp map_normalize(dnfs) do
-    for dnf <- dnfs, not map_empty?([dnf]) do
-      {tag, fields, negs} = dnf
-
+  defp map_normalize(bdd) do
+    for {tag, fields, negs} <- map_bdd_get(bdd) do
       {fields, negs} =
-        Enum.reduce(negs, {fields, []}, fn neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} ->
-          if map_empty_negation?(tag, acc_fields, neg) do
-            {acc_fields, acc_negs}
-          else
-            case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do
-              {:one, diff_key} ->
-                {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])),
-                 acc_negs}
+        Enum.reduce(negs, {fields, []}, fn
+          # Optimization: we are removing an open map with one field.
+          {:open, neg_fields}, {acc_fields, acc_negs} when map_size(neg_fields) == 1 ->
+            {key, value, _rest} = :maps.next(:maps.iterator(neg_fields))
+            t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value)
+
+            # If the difference was empty, then the whole line would be empty, which is not.
+            {Map.put(acc_fields, key, t_diff), acc_negs}
+
+          neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} ->
+            if non_intersecting_negation?(tag, acc_fields, neg) do
+              {acc_fields, acc_negs}
+            else
+              case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do
+                {:one, diff_key} ->
+                  {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])),
+                   acc_negs}
 
-              _ ->
-                {acc_fields, [neg | acc_negs]}
+                _ ->
+                  {acc_fields, [neg | acc_negs]}
+              end
             end
-          end
         end)
 
       {tag, fields, negs}
@@ -3619,11 +4164,10 @@ defmodule Module.Types.Descr do
   defp map_fuse_with_first_fusible(map, []), do: [map]
 
   defp map_fuse_with_first_fusible(map, [candidate | rest]) do
-    if fused = maybe_optimize_map_union(map, candidate) do
+    case maybe_optimize_map_union(map, candidate) do
+      nil -> [candidate | map_fuse_with_first_fusible(map, rest)]
       # we found a fusible candidate, we're done
-      [fused | rest]
-    else
-      [candidate | map_fuse_with_first_fusible(map, rest)]
+      fused -> [fused | rest]
     end
   end
 
@@ -3646,7 +4190,7 @@ defmodule Module.Types.Descr do
   end
 
   # Adapted from `map_empty?` to remove useless negations.
-  defp map_empty_negation?(tag, fields, {neg_tag, neg_fields}) do
+  defp non_intersecting_negation?(tag, fields, {neg_tag, neg_fields}) do
     (tag == :closed and
        Enum.any?(neg_fields, fn {neg_key, neg_type} ->
          not is_map_key(fields, neg_key) and not is_optional_static(neg_type)
@@ -3657,9 +4201,8 @@ defmodule Module.Types.Descr do
          end))
   end
 
-  defp map_to_quoted(dnf, opts) do
-    dnf
-    |> map_normalize()
+  defp map_to_quoted(bdd, opts) do
+    map_normalize(bdd)
     |> Enum.map(&map_each_to_quoted(&1, opts))
   end
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 17a6746c4d..f406adb296 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -129,10 +129,12 @@ defmodule Module.Types.DescrTest do
       assert union(empty_map(), open_map([{domain_key(:integer), atom()}]))
              |> equal?(open_map([{domain_key(:integer), atom()}]))
 
-      assert union(open_map(), open_map([{domain_key(:integer), atom()}])) == open_map()
+      assert union(open_map(), open_map([{domain_key(:integer), atom()}]))
+             |> equal?(open_map())
 
       # Test union of open map and map with domain key
-      assert union(open_map(), open_map([{domain_key(:integer), atom()}])) == open_map()
+      assert union(open_map(), open_map([{domain_key(:integer), atom()}]))
+             |> equal?(open_map())
     end
 
     test "list" do
@@ -161,7 +163,8 @@ defmodule Module.Types.DescrTest do
       assert union(
                open_map(a: float(), b: atom()),
                open_map(a: integer(), b: atom())
-             ) == open_map(a: union(float(), integer()), b: atom())
+             )
+             |> equal?(open_map(a: union(float(), integer()), b: atom()))
 
       assert union(
                closed_map(a: float(), b: atom()),
@@ -279,11 +282,11 @@ defmodule Module.Types.DescrTest do
                closed_map(a: integer())
              )
 
-      assert intersection(closed_map(a: integer()), open_map(b: not_set())) ==
-               closed_map(a: integer())
+      assert intersection(closed_map(a: integer()), open_map(b: not_set()))
+             |> equal?(closed_map(a: integer()))
 
-      assert intersection(closed_map(a: integer()), open_map(b: if_set(integer()))) ==
-               closed_map(a: integer())
+      assert intersection(closed_map(a: integer()), open_map(b: if_set(integer())))
+             |> equal?(closed_map(a: integer()))
 
       assert equal?(
                intersection(closed_map(a: integer()), closed_map(a: if_set(integer()))),
@@ -541,6 +544,7 @@ defmodule Module.Types.DescrTest do
       # Non-overlapping domain keys
       t1 = closed_map([{domain_key(:integer), atom()}])
       t2 = closed_map([{domain_key(:atom), binary()}])
+
       assert equal?(difference(t1, t2) |> union(empty_map()), t1)
       assert empty?(difference(t1, t1))
 
@@ -1724,15 +1728,21 @@ defmodule Module.Types.DescrTest do
       assert map_delete(term(), :a) == :badmap
       assert map_delete(integer(), :a) == :badmap
       assert map_delete(union(open_map(), integer()), :a) == :badmap
-      assert map_delete(closed_map(a: integer(), b: atom()), :a) == {:ok, closed_map(b: atom())}
-      assert map_delete(empty_map(), :a) == {:ok, empty_map()}
 
-      assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a) ==
-               {:ok, closed_map(b: atom())}
+      assert map_delete(closed_map(a: integer(), b: atom()), :a)
+             |> elem(1)
+             |> equal?(closed_map(b: atom()))
+
+      assert map_delete(empty_map(), :a) |> elem(1) |> equal?(empty_map())
+
+      assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a)
+             |> elem(1)
+             |> equal?(closed_map(b: atom()))
 
       # Deleting a non-existent key
-      assert map_delete(closed_map(a: integer(), b: atom()), :c) ==
-               {:ok, closed_map(a: integer(), b: atom())}
+      assert map_delete(closed_map(a: integer(), b: atom()), :c)
+             |> elem(1)
+             |> equal?(closed_map(a: integer(), b: atom()))
 
       # Deleting from a dynamic map
       assert map_delete(dynamic(), :a) == {:ok, dynamic(open_map(a: not_set()))}
@@ -1770,9 +1780,10 @@ defmodule Module.Types.DescrTest do
     end
 
     test "map_delete with atom fallback" do
-      assert closed_map([{:a, integer()}, {:b, atom()}, {domain_key(:atom), pid()}])
-             |> map_delete(:a) ==
-               {:ok, closed_map([{:a, not_set()}, {:b, atom()}, {domain_key(:atom), pid()}])}
+      assert closed_map(a: integer(), b: atom(), atom: pid())
+             |> map_delete(:a)
+             |> elem(1)
+             |> equal?(closed_map(a: not_set(), b: atom(), atom: pid()))
     end
 
     test "map_take" do
@@ -1780,8 +1791,8 @@ defmodule Module.Types.DescrTest do
       assert map_take(integer(), :a) == :badmap
       assert map_take(union(open_map(), integer()), :a) == :badmap
 
-      assert map_take(closed_map(a: integer(), b: atom()), :a) ==
-               {integer(), closed_map(b: atom())}
+      {took, rest} = map_take(closed_map(a: integer(), b: atom()), :a)
+      assert equal?(took, integer()) and equal?(rest, closed_map(b: atom()))
 
       # Deleting a non-existent key
       assert map_take(empty_map(), :a) == :badkey
@@ -1880,6 +1891,13 @@ defmodule Module.Types.DescrTest do
 
       # Put a key-value pair in a difference of maps
       {:ok, type} = difference(open_map(), closed_map(a: integer())) |> map_put(:b, atom())
+
+      type2 = difference(open_map(b: atom()), closed_map(a: integer()))
+      diff = difference(type, type2)
+      assert empty?(diff)
+      assert subtype?(type, type2)
+      assert subtype?(type2, type)
+
       assert equal?(type, difference(open_map(b: atom()), closed_map(a: integer())))
 
       # Put a new key-value pair with dynamic type
@@ -2034,7 +2052,7 @@ defmodule Module.Types.DescrTest do
              |> difference(list(integer()))
              |> difference(list(atom()))
              |> to_quoted_string() ==
-               "non_empty_list(term()) and not (non_empty_list(atom()) or non_empty_list(integer()))"
+               "non_empty_list(term()) and not (non_empty_list(integer()) or non_empty_list(atom()))"
 
       assert list(term(), integer()) |> to_quoted_string() ==
                "empty_list() or non_empty_list(term(), integer())"

From d6f0217f4c0042bf669afceff5069bb180ffb995 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Sun, 3 Aug 2025 20:52:03 +0200
Subject: [PATCH 6/9] Rewrite of every type as bdd

---
 lib/elixir/lib/module/types/descr.ex          | 1500 +++++++----------
 .../test/elixir/module/types/descr_test.exs   |   23 +-
 .../test/elixir/module/types/expr_test.exs    |   55 +-
 3 files changed, 684 insertions(+), 894 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index ce9bb8ce1f..09c0faa4ce 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -12,6 +12,7 @@ defmodule Module.Types.Descr do
   # Vocabulary:
   #
   # * DNF - disjunctive normal form which is a pair of unions and negations.
+  # * BDD - binary decision diagram which is a set-theoretic representation of types as a tree.
   #   In the case of maps, we augment each pair with the open/closed tag.
 
   import Bitwise
@@ -27,6 +28,7 @@ defmodule Module.Types.Descr do
   @bit_number @bit_integer ||| @bit_float
 
   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 domain_key(key), do: {:domain_key, key}
@@ -50,7 +52,7 @@ defmodule Module.Types.Descr do
   @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, []}]
+  @tuple_top {{:open, []}, :bdd_top, :bdd_bot}
   @map_empty {{:closed, %{}}, :bdd_top, :bdd_bot}
 
   @none %{}
@@ -176,15 +178,28 @@ defmodule Module.Types.Descr do
     Enum.reduce(funs, &intersection/2)
   end
 
+  # This is an insertion of an arrow {domain, return} into a list of non-overlapping arrows.
+  # If no arrow overlaps with the new arrow, it will be inserted at the end.
+  # For any arrow that overlaps, we split this arrow into two: one where the domains intersect,
+  # and one where the domains differ. Then we continue the recursion with the domain subtracted
+  # from the one of the overlapping arrow.
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
     common = intersection(domain, acc_domain)
 
     if empty?(common) do
       [{acc_domain, acc_return} | pivot_overlapping_clause(domain, return, acc)]
     else
-      [{common, union(return, acc_return)} | acc]
-      |> prepend_to_unless_empty(difference(domain, common), return)
-      |> prepend_to_unless_empty(difference(acc_domain, common), acc_return)
+      diff = difference(domain, acc_domain)
+
+      rest =
+        if empty?(diff) do
+          []
+        else
+          pivot_overlapping_clause(diff, return, acc)
+        end
+
+      [{common, union(return, acc_return)} | rest]
+      |> prepend_to_unless_empty(difference(acc_domain, domain), acc_return)
     end
   end
 
@@ -233,8 +248,8 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp unwrap_domain_tuple(%{tuple: dnf} = descr, transform) when map_size(descr) == 1 do
-    Enum.map(dnf, transform)
+  defp unwrap_domain_tuple(%{tuple: bdd} = descr, transform) when map_size(descr) == 1 do
+    tuple_bdd_to_dnf_no_negations(bdd) |> Enum.map(transform)
   end
 
   defp unwrap_domain_tuple(descr, _transform) when descr == %{}, do: []
@@ -456,9 +471,11 @@ defmodule Module.Types.Descr do
       {right_dynamic, right_static} = Map.pop(right, :dynamic, right)
       dynamic_part = difference_static(left_dynamic, right_static)
 
-      if empty?(dynamic_part),
-        do: none(),
-        else: Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part)
+      # This might be the worst place possible to check for emptiness.
+      # if empty?(dynamic_part),
+      # do: none(),
+      # else:
+      Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part)
     else
       difference_static(left, right)
     end
@@ -547,52 +564,6 @@ defmodule Module.Types.Descr do
   (bitmap, atom) are checked first for speed since, if they are present,
   the type is non-empty as we normalize then during construction.
   """
-
-  # defguardp is_descr(d)
-  #           when d == :term or
-  #                  (is_map(d) and
-  #                     (Map.has_key?(d, :atom) or Map.has_key?(d, :bitmap) or
-  #                        Map.has_key?(d, :list) or Map.has_key?(d, :map) or
-  #                        Map.has_key?(d, :tuple) or Map.has_key?(d, :fun)))
-
-  # defp bdd_size({{tag, fields = %{}}, l, r}) when tag in [:open, :closed] do
-  #   bdd_size(l) + bdd_size(r) + 1 + Enum.reduce(fields, 0, fn d, acc -> descr_size(d) + acc end)
-  # end
-
-  # defp bdd_size({{list = %{}, last = %{}}, l, r}) do
-  #   bdd_size(l) + bdd_size(r) + 1 + descr_or_domain_size(list) + descr_or_fields_size(last)
-  # end
-
-  defp bdd_size({lit, l, r}), do: bdd_size(l) + bdd_size(r) + 1
-
-  defp bdd_size(bdd), do: 0
-
-  defp dnf_structural_size(dnf) do
-    Enum.reduce(dnf, 0, fn {_tag, pos}, acc ->
-      1 + acc + length(pos)
-    end)
-  end
-
-  defp dnf_size(dnf) do
-    Enum.reduce(dnf, 0, fn {_tag, pos}, acc ->
-      1 + acc + Enum.reduce(pos, 0, fn d, acc -> descr_size(d) + acc end)
-    end)
-  end
-
-  def descr_size(:term), do: 1
-
-  def descr_size(%{} = descr) do
-    Enum.reduce(Map.to_list(descr), 0, fn {key, value}, acc ->
-      acc + descr_size(key, value)
-    end)
-  end
-
-  def descr_size(:tuple, dnf), do: dnf_size(dnf)
-  def descr_size(:fun, bdd), do: bdd_size(bdd)
-  def descr_size(:map, bdd), do: bdd_size(bdd)
-  def descr_size(:list, bdd), do: bdd_size(bdd)
-  def descr_size(_, _), do: 1
-
   def empty?(:term), do: false
 
   def empty?(%{} = descr) do
@@ -604,50 +575,10 @@ defmodule Module.Types.Descr do
         true
 
       descr ->
-        # IO.puts("Woooh")
-        d = descr_size(descr)
-
-        if d > 100 do
-          IO.puts("descr_size(descr): #{d}")
-          IO.puts("The decomposition is:")
-
-          if Map.has_key?(descr, :atom),
-            do: IO.puts("Atom size: #{descr_size(:atom, descr.atom)}")
-
-          if Map.has_key?(descr, :list) do
-            IO.puts("List size: #{descr_size(:list, descr.list)}")
-          else
-            IO.puts("List size: 0")
-          end
-
-          if Map.has_key?(descr, :map) do
-            IO.puts("Map size: #{descr_size(:map, descr.map)}")
-          else
-            IO.puts("Map size: 0")
-          end
-
-          if Map.has_key?(descr, :tuple) do
-            IO.puts("Tuple size: #{descr_size(:tuple, descr.tuple)}")
-            IO.puts("Tuple structural size: #{dnf_structural_size(descr.tuple)}")
-          else
-            IO.puts("Tuple size: 0")
-          end
-
-          if Map.has_key?(descr, :fun) do
-            IO.puts("Fun size: #{descr_size(:fun, descr.fun)}")
-          else
-            IO.puts("Fun size: 0")
-          end
-
-          # dbg(descr)
-        end
-
-        # dbg(descr, limit: :infinity, printable_limit: :infinity, width: :infinity)
-
         not Map.has_key?(descr, :atom) and
           not Map.has_key?(descr, :bitmap) and
           not Map.has_key?(descr, :optional) and
-          not Map.has_key?(descr, :tuple) and
+          (not Map.has_key?(descr, :tuple) or tuple_empty?(descr.tuple)) and
           (not Map.has_key?(descr, :map) or map_empty?(descr.map)) and
           (not Map.has_key?(descr, :list) or list_empty?(descr.list)) and
           (not Map.has_key?(descr, :fun) or fun_empty?(descr.fun))
@@ -661,6 +592,7 @@ defmodule Module.Types.Descr do
   defp empty_key?(:fun, value), do: fun_empty?(value)
   defp empty_key?(:map, value), do: map_empty?(value)
   defp empty_key?(:list, value), do: list_empty?(value)
+  defp empty_key?(:tuple, value), do: tuple_empty?(value)
   defp empty_key?(_, _value), do: false
 
   @doc """
@@ -732,9 +664,9 @@ defmodule Module.Types.Descr do
   defp to_quoted(:atom, val, _opts), do: atom_to_quoted(val)
   defp to_quoted(:bitmap, val, _opts), do: bitmap_to_quoted(val)
   defp to_quoted(:dynamic, descr, opts), do: dynamic_to_quoted(descr, opts)
-  defp to_quoted(:map, dnf, opts), do: map_to_quoted(dnf, opts)
-  defp to_quoted(:list, dnf, opts), do: list_to_quoted(dnf, false, opts)
-  defp to_quoted(:tuple, dnf, opts), do: tuple_to_quoted(dnf, opts)
+  defp to_quoted(:map, bdd, opts), do: map_to_quoted(bdd, opts)
+  defp to_quoted(:list, bdd, opts), do: list_to_quoted(bdd, false, opts)
+  defp to_quoted(:tuple, bdd, opts), do: tuple_to_quoted(bdd, opts)
   defp to_quoted(:fun, bdd, opts), do: fun_to_quoted(bdd, opts)
 
   @doc """
@@ -1417,7 +1349,22 @@ defmodule Module.Types.Descr do
     type_args = args_to_domain(arguments)
 
     Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
-      aux_apply(acc, type_args, term(), intersection_of_arrows)
+      {x, _cache} = aux_apply(acc, type_args, term(), intersection_of_arrows, %{})
+      x
+    end)
+  end
+
+  defp apply_disjoint(arguments, arrows) do
+    type_args = args_to_domain(arguments)
+
+    Enum.reduce(arrows, none(), fn {args, ret}, acc_return ->
+      dom = args_to_domain(args)
+
+      if empty?(intersection(dom, type_args)) do
+        acc_return
+      else
+        union(acc_return, ret)
+      end
     end)
   end
 
@@ -1435,39 +1382,67 @@ defmodule Module.Types.Descr do
   # - arrow_intersections: The list of function arrows to process
 
   # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
-  defp aux_apply(result, _input, rets_reached, []) do
-    if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
+  defp aux_apply(result, input, rets_reached, [], cache) do
+    cache_key = {result, input, rets_reached, []}
+    res = union(result, rets_reached)
+    {res, Map.put(cache, cache_key, res)}
   end
 
-  defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do
+  defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections], cache) do
     # Calculate the part of the input not covered by this arrow's domain
-    dom_subtract = difference(input, args_to_domain(args))
-
-    # Refine the return type by intersecting with this arrow's return type
-    ret_refine = intersection(returns_reached, ret)
-
-    # Phase 1: Domain partitioning
-    # If the input is not fully covered by the arrow's domain, then the result type should be
-    # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
-    # parts of the domain.
-    #
-    # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
-    # both atoms and pids in the result.
-    result =
-      if empty?(dom_subtract) do
-        result
-      else
-        aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
-      end
+    cache_key = {result, input, returns_reached, [{args, ret} | arrow_intersections]}
+
+    case cache do
+      %{^cache_key => value} ->
+        {value, cache}
+
+      _ ->
+        dom = args_to_domain(args)
+        no_intersection? = empty?(intersection(dom, input))
+
+        cond do
+          # First: is there any intersection between the input and the arrow's domain?
+          # If not, we skip this arrow.
+          no_intersection? ->
+            {result, cache} =
+              aux_apply(result, input, returns_reached, arrow_intersections, cache)
 
-    # 2. Return type refinement
-    # The result type is also refined (intersected) in the sense that, if several arrows match
-    # the same part of the input, then the result type is an intersection of the return types of
-    # those arrows.
+            cache = Map.put(cache, cache_key, result)
+            {result, cache}
 
-    # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
-    # should result in (atom() ∩ pid()), which is none().
-    aux_apply(result, input, ret_refine, arrow_intersections)
+          true ->
+            dom_subtract = difference(input, dom)
+
+            # Refine the return type by intersecting with this arrow's return type
+            ret_refine = intersection(returns_reached, ret)
+
+            # Phase 1: Domain partitioning
+            # If the input is not fully covered by the arrow's domain, then the result type should be
+            # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
+            # parts of the domain.
+            #
+            # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
+            # both atoms and pids in the result.
+
+            {result, cache} =
+              if empty?(dom_subtract) do
+                {result, cache}
+              else
+                aux_apply(result, dom_subtract, returns_reached, arrow_intersections, cache)
+              end
+
+            # 2. Return type refinement
+            # The result type is also refined (intersected) in the sense that, if several arrows match
+            # the same part of the input, then the result type is an intersection of the return types of
+            # those arrows.
+
+            # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
+            # should result in (atom() ∩ pid()), which is none().
+            {result, cache} = aux_apply(result, input, ret_refine, arrow_intersections, cache)
+            cache = Map.put(cache, cache_key, result)
+            {result, cache}
+        end
+    end
   end
 
   # Takes all the paths from the root to the leaves finishing with a 1,
@@ -1497,9 +1472,15 @@ defmodule Module.Types.Descr do
   # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty
   defp fun_empty?(bdd) do
     case bdd do
-      :fun_bottom -> true
-      :fun_top -> false
-      bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end)
+      :fun_bottom ->
+        true
+
+      :fun_top ->
+        false
+
+      bdd ->
+        fun_get(bdd)
+        |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end)
     end
   end
 
@@ -1536,8 +1517,10 @@ defmodule Module.Types.Descr do
           # Filter positives to only those with matching arity, then check if the negative
           # function's domain is a supertype of the positive domain and if the phi function
           # determines emptiness.
+          neg_dom = args_to_domain(neg_arguments)
+
           length(neg_arguments) == positive_arity and
-            subtype?(args_to_domain(neg_arguments), positive_domain) and
+            subtype?(neg_dom, positive_domain) and
             phi_starter(neg_arguments, neg_return, positives)
         end)
     end
@@ -1580,26 +1563,32 @@ defmodule Module.Types.Descr do
     # we can simplify the phi function check to a direct subtyping test.
     # This avoids the expensive recursive phi computation by checking only that applying the
     # input to the positive intersection yields a subtype of the return
-    if all_non_empty_domains?([{arguments, return} | positives]) do
-      fun_apply_static(arguments, [positives])
-      |> subtype?(return)
-    else
-      n = length(arguments)
-      # Arity mismatch: functions with different arities cannot be subtypes
-      # of the target function type (arguments -> return)
-      if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do
-        false
-      else
-        # Initialize memoization cache for the recursive phi computation
-        arguments = Enum.map(arguments, &{false, &1})
-        {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{})
-        result
-      end
+    case disjoint_non_empty_domains?({arguments, return}, positives) do
+      :disjoint_non_empty ->
+        apply_disjoint(arguments, positives) |> subtype?(return)
+
+      :non_empty ->
+        fun_apply_static(arguments, [positives]) |> subtype?(return)
+
+      _ ->
+        n = length(arguments)
+        # Arity mismatch: functions with different arities cannot be subtypes
+        # of the target function type (arguments -> return)
+        if Enum.any?(positives, fn {args, _ret} -> length(args) != n end) do
+          false
+        else
+          # Initialize memoization cache for the recursive phi computation
+          arguments = Enum.map(arguments, &{false, &1})
+          {result, _cache} = phi(arguments, {false, negation(return)}, positives, %{})
+          result
+        end
     end
   end
 
   defp phi(args, {b, t}, [], cache) do
-    {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache}
+    result = Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
+    {result, Map.put(cache, {args, {b, t}, []}, result)}
+    # {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache}
   end
 
   defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do
@@ -1640,12 +1629,49 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp disjoint_non_empty_domains?({arguments, return}, positives) do
+    b1 = all_disjoint_domains?(positives)
+    b2 = all_non_empty_domains?([{arguments, return} | positives])
+
+    cond do
+      b1 and b2 -> :disjoint_non_empty
+      b2 -> :non_empty
+      true -> nil
+    end
+  end
+
   defp all_non_empty_domains?(positives) do
     Enum.all?(positives, fn {args, _ret} ->
       Enum.all?(args, fn arg -> not empty?(arg) end)
     end)
   end
 
+  # For two arguments to be disjoint, we need at least one of their types to be disjoint.
+  defp disjoint_arguments?(args1, args2) do
+    Enum.reduce_while(Enum.zip(args1, args2), false, fn {t1, t2}, acc ->
+      t = intersection(t1, t2)
+
+      if empty?(t) do
+        {:halt, true}
+      else
+        {:cont, acc}
+      end
+    end)
+  end
+
+  # Test that all positives are two to two disjoint. We iterate on the list to do so.
+  defp all_disjoint_domains?([]), do: true
+
+  defp all_disjoint_domains?([{args, _} | rest]) do
+    Enum.reduce_while(rest, true, fn {args_rest, _}, _acc ->
+      if disjoint_arguments?(args, args_rest) do
+        {:cont, true}
+      else
+        {:halt, false}
+      end
+    end)
+  end
+
   defp fun_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
       {:fun_top, _} -> :fun_top
@@ -1895,15 +1921,15 @@ defmodule Module.Types.Descr do
 
   ## List
 
-  # Represents both list and improper list simultaneously using a pair
-  # `{list_type, last_type}`.
-  #
-  # We compute if it is a proper or improper list based if the last_type
-  # is an empty_list() or a list(). In particular, the last_type may be
-  # stored as `:term` for optimization purposes. This is ok because operations
-  # like `tl` effectively return the list itself plus the union of the tail
-  # (and if the tail includes the list itself, they are equivalent). And,
-  # for other operations like difference, we expand the tail_type back into
+  # Represents list and improper list simultaneously as a BDD with nodes of the form
+  # `{list_type, last_type}`, where `list_type` is the type of elements in the list,
+  # and `last_type` is the type of the last element (so `[]` if the list is proper,
+  # and anything else but a list if the list is improper).
+
+  # The last_type may be stored as `:term` for optimization purposes. This is ok
+  # because operations like `tl` effectively return the list itself plus the union of
+  # the tail (and if the tail includes the list itself, they are equivalent). And, for other
+  # operations like difference, we expand the tail_type back into
   # `not non_empty_list()` via `list_tail_unfold/1`. Overall, this simplifies
   # the code because we don't need to special case `not non_empty_list()`.
   #
@@ -2068,42 +2094,8 @@ defmodule Module.Types.Descr do
   defp list_tail_unfold(:term), do: @not_non_empty_list
   defp list_tail_unfold(other), do: Map.delete(other, :list)
 
-  # Attempt a merge, if the union is between two single lists.
-  defp list_union(list_literal(list1, last1), list_literal(list2, last2)) do
-    cond do
-      subtype?(list1, list2) and subtype?(last1, last2) -> list_literal(list2, last2)
-      subtype?(list2, list1) and subtype?(last2, last1) -> list_literal(list1, last1)
-      equal?(list1, list2) -> list_literal(list1, union(last1, last2))
-      true -> list_union_recur(list_literal(list1, last1), list_literal(list2, last2))
-    end
-  end
-
-  defp list_union(bdd1, bdd2), do: list_union_recur(bdd1, bdd2)
-
-  defp list_union_recur(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_top, _} ->
-        :bdd_top
-
-      {_, :bdd_top} ->
-        :bdd_top
-
-      {:bdd_bot, bdd} ->
-        bdd
-
-      {bdd, :bdd_bot} ->
-        bdd
-
-      {{list, l1, r1}, {list, l2, r2}} ->
-        {list, list_union(l1, l2), list_union(r1, r2)}
-
-      {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 ->
-        {list1, list_union(l1, bdd2), list_union(r1, bdd2)}
-
-      {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 ->
-        {list2, list_union(bdd1, l2), list_union(bdd1, r2)}
-    end
-  end
+  @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
@@ -2111,11 +2103,21 @@ defmodule Module.Types.Descr do
 
   defp is_list_top?(_), do: false
 
+  defp list_intersection(list_literal(list1, last1), list_literal(list2, last2)) do
+    try do
+      list = non_empty_intersection!(list1, list2)
+      last = non_empty_intersection!(last1, last2)
+      list_literal(list, last)
+    catch
+      :empty -> :bdd_bot
+    end
+  end
+
   defp list_intersection(bdd1, bdd2) do
     cond do
       is_list_top?(bdd1) and is_tuple(bdd2) -> bdd2
       is_list_top?(bdd2) and is_tuple(bdd1) -> bdd1
-      true -> list_intersection_recur(bdd1, bdd2)
+      true -> bdd_intersection(bdd1, bdd2)
     end
     |> case do
       {_, :bdd_bot, :bdd_bot} -> :bdd_bot
@@ -2123,84 +2125,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp list_intersection_recur(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).
-      # Note: instead of inserting the bdd at the root, we decided to intersect with
-      # every atom in the bdd. If empty, then replace with the right tree.
-      # {bdd, {list, :bdd_top, :bdd_bot}} ->
-      #   intersect_bdd_with_list(bdd, list)
-
-      # {bdd, {list, :bdd_bottom, :bdd_top}} ->
-      #   {list, :bdd_bottom, bdd}
-
-      # {{list, :bdd_top, :bdd_bottom}, bdd} ->
-      #   intersect_bdd_with_list(bdd, list)
-
-      # {{list, :bdd_bottom, :bdd_top}, bdd} ->
-      #   {list, :bdd_bottom, bdd}
-      {list_literal(list1, last1), list_literal(list2, last2)} ->
-        try do
-          list1 = non_empty_intersection!(list1, list2)
-          last1 = non_empty_intersection!(last1, last2)
-          list_literal(list1, last1)
-        catch
-          :empty -> :bdd_bot
-        end
-
-      # General cases
-      {{list, l1, r1}, {list, l2, r2}} ->
-        {list, list_intersection_recur(l1, l2), list_intersection_recur(r1, r2)}
-
-      {{list1, l1, r1}, {list2, l2, r2}} when list1 < list2 ->
-        {list1, list_intersection_recur(l1, bdd2), list_intersection_recur(r1, bdd2)}
-
-      {{list1, l1, r1}, {list2, l2, r2}} when list1 > list2 ->
-        {list2, list_intersection_recur(bdd1, l2), list_intersection_recur(bdd1, r2)}
-
-        # {{list, l, r}, bdd} ->
-        # {list, list_intersection_recur(l, bdd), list_intersection_recur(r, bdd)}
-    end
-  end
-
-  # We can only do this if the bdd has :bdd_bot as right child. Otherwise, if `a` is the root,
-  # it contains both formulas `a and left`, and `not a and right`. Thus, intersecting `not a`
-  # with a `{list, last}` is a wrong formula. Then, if the intersection is empty, the whole
-  # bdd is empty.
-  defp intersect_bdd_with_list(bdd, {list, last}) do
-    case bdd do
-      {{bdd_list, bdd_last}, left, :bdd_bot} ->
-        list = intersection(bdd_list, list)
-        last = intersection(bdd_last, last)
-
-        if empty?(list) or empty?(last) do
-          :bdd_bot
-        else
-          {{list, last}, left, :bdd_bot}
-        end
-
-      _ ->
-        # Otherwise, we simply put the positive list at the root.
-        {{list, last}, bdd, :bdd_bot}
-    end
-  end
-
   # Computes the difference between two BDD (Binary Decision Diagram) list types.
   # It progressively subtracts each type in bdd2 from all types in bdd1.
   # The algorithm handles three cases:
@@ -2210,32 +2134,24 @@ defmodule Module.Types.Descr do
   #    b) If only the last type differs, subtracts it
   # 3. Base case: adds bdd2 type to negations of bdd1 type
   # The result may be larger than the initial bdd1, which is maintained in the accumulator.
-  defp list_difference(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_bot, _} ->
-        :bdd_bot
+  defp list_difference(list_literal(list1, last1) = bdd1, list_literal(list2, last2) = bdd2) do
+    cond do
+      empty?(intersection(list1, list2)) or empty?(intersection(last1, last2)) ->
+        list_literal(list1, last1)
 
-      {_, :bdd_top} ->
+      subtype?(list1, list2) and subtype?(last1, last2) ->
         :bdd_bot
 
-      {bdd, :bdd_bot} ->
-        bdd
-
-      {:bdd_top, {lst, l, r}} ->
-        {lst, list_difference(:bdd_top, l), list_difference(:bdd_top, r)}
-
-      {{lst, l1, r1}, {lst, l2, r2}} ->
-        {lst, list_difference(l1, l2), list_difference(r1, r2)}
-
-      {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 < lst2 ->
-        {lst1, list_difference(l1, bdd2), list_difference(r1, bdd2)}
-
-      {{lst1, l1, r1}, {lst2, l2, r2}} when lst1 > lst2 ->
-        {lst2, list_difference(bdd1, l2), list_difference(bdd1, r2)}
+      equal?(list1, list2) ->
+        list_literal(list1, difference(last1, last2))
 
-        # {{lst, l, r}, bdd} ->
-        #   {lst, list_difference(l, bdd), list_difference(r, bdd)}
+      true ->
+        bdd_difference(bdd1, bdd2)
     end
+  end
+
+  defp list_difference(bdd1, bdd2) do
+    bdd_difference(bdd1, bdd2)
     |> case do
       {_, :bdd_bot, :bdd_bot} -> :bdd_bot
       bdd -> bdd
@@ -2247,13 +2163,23 @@ defmodule Module.Types.Descr do
 
   defp list_empty_line?(list_type, last_type, negs) do
     last_type = list_tail_unfold(last_type)
-
+    # To make a list {list, last} empty with some negative lists:
+    # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one.
+    # 2. Each of the list supertypes:
+    #     a. either completely covers the type, if its last type is a supertype of the positive one,
+    #     b. or it removes part of the last type.
     empty?(list_type) or empty?(last_type) or
       Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type ->
-        if subtype?(list_type, neg_type) and subtype?(acc_last_type, neg_last) do
-          {:halt, nil}
+        if subtype?(list_type, neg_type) do
+          d = difference(acc_last_type, neg_last)
+
+          if empty?(d) do
+            {:halt, nil}
+          else
+            {:cont, d}
+          end
         else
-          {:cont, difference(acc_last_type, neg_last)}
+          {:cont, acc_last_type}
         end
       end)
       |> is_nil()
@@ -2554,17 +2480,30 @@ defmodule Module.Types.Descr do
 
   ## Map
   #
-  # Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs
-  # `{map_literal, negated_literals}` where `map_literal` is a map type literal
-  # and `negated_literals` is a list of map type literals that are negated from it.
-  # Each pair is augmented with the :open or :closed tag.
+  # Maps are represented as BDDs, that is, a tree of pairs `{tag_or_domain, fields}`
+  # where `tag_or_domain` is either :closed or :open, or a map from domain keys
+  # (@domain_key_types) to types, and `fields` is a map of atom keys (:foo, :bar, ...)
+  # to types.
   #
   # For instance, the type `%{..., a: integer()} and not %{b: atom()}` can be represented
-  # by the DNF containing one pair of shape:
+  # by the BDD containing one pair of shape:
+  #
+  #     {{:open, %{:a => integer()}}, {{:closed, %{:b => atom()}}, :bdd_bot, :bdd_top}, :bdd_bot}
+  #
+  # which can be seen as:
+  #
+  #     └─ %{..., a: integer()}
+  #      ├─ %{b: atom()}
+  #      │  ├─ :bdd_bot
+  #      │  └─ :bdd_top
+  #      └─ :bdd_bot
   #
-  #     {:open, %{a => integer()}, [{:closed, %{b => atom()}}]}
+  # and is interpreted as the intersection of `%{..., a: integer()}` with
+  # `not %{b: atom()}`, since the only path from the root to the leaves which
+  # ends with `:bdd_top` is the one which takes the first (left) branch after
+  # `%{..., a: integer()}`, and the second (right) branch after `%{b: atom()}`.
   #
-  # The goal of keeping symbolic negations is to avoid distributing difference on
+  # This representation keeps negations symbolic, and avoids distributing difference on
   # every member of a union which creates a lot of map literals in the union and
   # requires emptiness checks to avoid creating empty maps.
   #
@@ -2573,7 +2512,7 @@ defmodule Module.Types.Descr do
   # `%{..., a: if_set(not atom()), b: integer()}`. For maps with more keys,
   # each key in a negated literal may create a new union when eliminated.
   #
-  # Instead of a tag :open or :closed, we can also use a map of domains which
+  # Instead of a tag :open or :closed, we can use a map of domains which
   # specifies for each defined key domain (@domain_key_types) the type associated with
   # those keys.
   #
@@ -2585,239 +2524,6 @@ defmodule Module.Types.Descr do
   # and other keys bound to any type. It will be represented using a map domain that maps
   # atom to `if_set(integer())`, and every other domain key to `term_or_optional()`.
 
-  # ## TESTING
-  # def map_merge(%{map: bdd1} = d1, %{map: bdd2} = d2) do
-  #   # Starting accumulator: the empty map type
-  #   res = %{map: :bdd_bot}
-
-  #   # Recursive auxiliary function
-  #   aux = fn aux, accu, bdd1, bdd2 ->
-  #     case {map_first_label(bdd1), map_first_label(bdd2)} do
-  #       {:dummy, :dummy} ->
-  #         {some1, none1} = map_empty_cases(bdd1)
-  #         {some2, none2} = map_empty_cases(bdd2)
-
-  #         some = some1 or some2
-  #         none = none1 and none2
-
-  #         # Approximation if some and not none
-  #         if some do
-  #           fields = :maps.from_list(accu)
-  #           map_union(res, %{map: map_new(:open, fields)})
-  #         else
-  #           res
-  #         end
-
-  #       {l1, l2} ->
-  #         l = min_label(l1, l2)
-
-  #         # Split along label l
-  #         split1 = map_split(bdd1, l)
-  #         split2 = map_split(bdd2, l)
-
-  #         Enum.reduce(split1, res, fn {t1, d1_next}, acc ->
-  #           Enum.reduce(split2, acc, fn {t2, d2_next}, acc2 ->
-  #             t =
-  #               if Map.has_key?(t2, :optional) and t2.optional do
-  #                 union(t1, remove_optional(t2))
-  #               else
-  #                 t2
-  #               end
-
-  #             aux.(aux, [{l, t} | accu], d1_next.map, d2_next.map)
-  #           end)
-  #         end)
-  #     end
-  #   end
-
-  #   aux.(aux, [], bdd1, bdd2)
-  # end
-
-  # defp map_first_label(:bdd_top), do: :dummy
-  # defp map_first_label(:bdd_bot), do: :dummy
-
-  # defp map_first_label({{tag, fields}, :bdd_top, :bdd_bot}) do
-  #   case :maps.next(:maps.iterator(fields)) do
-  #     :none -> :dummy
-  #     {key, _value, _iter} -> key
-  #   end
-  # end
-
-  # defp map_first_label({{_tag, _fields}, l, _r}), do: map_first_label(l)
-
-  # # Returns {some, none}
-  # defp map_empty_cases(bdd) do
-  #   map_bdd_get(bdd)
-  #   |> Enum.reduce({false, true}, fn
-  #     {:open, fields, _negs}, {some, none} ->
-  #       some = some or map_size(fields) > 0
-  #       none = none and map_size(fields) == 0
-  #       {some, none}
-
-  #     {:closed, fields, _negs}, {some, none} ->
-  #       some = some or map_size(fields) > 0
-  #       none = none and map_size(fields) == 0
-  #       {some, none}
-  #   end)
-  # end
-
-  # # Split a BDD into a list of {type_for_label, rest_of_map}
-  # defp map_split(bdd, label) do
-  #   map_bdd_get(bdd)
-  #   |> Enum.map(fn {tag, fields, negs} ->
-  #     case :maps.take(label, fields) do
-  #       {value, fields_rest} ->
-  #         {remove_optional(value), %{map: map_new(tag, fields_rest)}}
-
-  #       :error ->
-  #         # If absent
-  #         type_for_label =
-  #           case tag do
-  #             :open -> term_or_optional()
-  #             :closed -> not_set()
-  #             domains = %{} -> Map.get(domains, domain_key(:atom), not_set())
-  #           end
-
-  #         {type_for_label, %{map: map_new(tag, fields)}}
-  #     end
-  #   end)
-  # end
-
-  # defp min_label(:dummy, :dummy), do: :dummy
-  # defp min_label(:dummy, l), do: l
-  # defp min_label(l, :dummy), do: l
-  # defp min_label(l1, l2), do: if(l1 <= l2, do: l1, else: l2)
-
-  @doc """
-  Type-level merge for maps (like `Map.merge/2`).
-
-  Semantics per OCaml code:
-  - For each key `l`, if the right map's type for `l` **may be absent**,
-    the merged type for `l` is `left(l) ∪ present(right(l))`;
-    otherwise it is `right(l)` (right-biased override).
-  - Domains are merged with the same rule (component-wise).
-  - If either side is `:open`, the result is effectively open (via domains).
-
-  Returns `{:ok, merged_descr}` or `:badmap` if either input is not a (possibly dynamic) map type.
-  """
-  def map_merge(:term, _), do: :badmap
-  def map_merge(_, :term), do: :badmap
-
-  def map_merge(%{} = descr1, %{} = descr2) do
-    case {:maps.take(:dynamic, descr1), :maps.take(:dynamic, descr2)} do
-      {:error, :error} ->
-        with {:ok, m} <- map_merge_static(descr1, descr2) do
-          {:ok, m}
-        else
-          :badmap -> :badmap
-        end
-
-      {{dyn1, stat1}, :error} ->
-        with {:ok, stat_stat} <- map_merge_static(stat1, descr2),
-             {:ok, dyn_stat} <- map_merge_static(dynamic(dyn1), descr2) do
-          {:ok, union(stat_stat, dynamic(dyn_stat))}
-        else
-          :badmap -> :badmap
-        end
-
-      {:error, {dyn2, stat2}} ->
-        with {:ok, stat_stat} <- map_merge_static(descr1, stat2),
-             {:ok, stat_dyn} <- map_merge_static(descr1, dynamic(dyn2)) do
-          {:ok, union(stat_stat, dynamic(stat_dyn))}
-        else
-          :badmap -> :badmap
-        end
-
-      {{dyn1, stat1}, {dyn2, stat2}} ->
-        with {:ok, ss} <- map_merge_static(stat1, stat2),
-             {:ok, sd} <- map_merge_static(stat1, dynamic(dyn2)),
-             {:ok, ds} <- map_merge_static(dynamic(dyn1), stat2),
-             {:ok, dd} <- map_merge_static(dynamic(dyn1), dynamic(dyn2)) do
-          {:ok, union(ss, union(dynamic(sd), union(dynamic(ds), dynamic(dd))))}
-        else
-          :badmap -> :badmap
-        end
-    end
-  end
-
-  # --- Core static merger on the BDDs ---------------------------------------
-
-  defp map_merge_static(%{map: bdd1} = d1, %{map: bdd2} = d2) do
-    # both inputs must be exclusively map (no extra components)
-    if map_only?(d1) and map_only?(d2) do
-      # Build the result by taking the cross-product of positive literals
-      # (DNF lines) and unioning merged literals.
-      merged_bdd =
-        map_bdd_get(bdd1)
-        |> Enum.reduce(:bdd_bot, fn {tag1, fields1, _negs1}, acc1 ->
-          Enum.reduce(map_bdd_get(bdd2), acc1, fn {tag2, fields2, _negs2}, acc2 ->
-            {new_tag_or_domains, new_fields} =
-              map_literal_merge(tag1, fields1, tag2, fields2)
-
-            map_union(acc2, {{new_tag_or_domains, new_fields}, :bdd_top, :bdd_bot})
-          end)
-        end)
-
-      {:ok, %{map: merged_bdd}}
-    else
-      :badmap
-    end
-  end
-
-  defp map_merge_static(_, _), do: :badmap
-
-  # --- Literal / domain merge (right-biased with "optional means fallback") --
-
-  # Merge two map literals (tag-or-domains + fields) into one literal.
-  defp map_literal_merge(tag_or_domains1, fields1, tag_or_domains2, fields2) do
-    default1 = map_key_tag_to_type(tag_or_domains1)
-    default2 = map_key_tag_to_type(tag_or_domains2)
-
-    # Merge domains first (handles openness and all non-atom key domains)
-    new_tag_or_domains = map_domain_merge(tag_or_domains1, tag_or_domains2)
-
-    # For explicit atom keys: symmetrical merge with defaults for missing keys
-    new_fields =
-      symmetrical_merge(fields1, default1, fields2, default2, fn _key, v1, v2 ->
-        map_merge_value(v1, v2)
-      end)
-
-    {new_tag_or_domains, new_fields}
-  end
-
-  # Component-wise merge of domains. For every domain key dk in @domain_key_types:
-  # result(dk) = merge_value( domain1(dk), domain2(dk) ).
-  # If all resulting domain entries are empty/optional, collapse to :closed.
-  defp map_domain_merge(tag_or_domains1, tag_or_domains2) do
-    new_domains =
-      for domain_key(_) = dk <- @domain_key_types, reduce: %{} do
-        acc ->
-          v1 = map_domain_default(tag_or_domains1, dk)
-          v2 = map_domain_default(tag_or_domains2, dk)
-          v = map_merge_value(v1, v2)
-
-          if empty_or_optional?(v) do
-            acc
-          else
-            Map.put(acc, dk, v)
-          end
-      end
-
-    if map_size(new_domains) == 0, do: :closed, else: new_domains
-  end
-
-  # Default value for a domain when not explicitly present in the literal.
-  defp map_domain_default(:open, _dk), do: term_or_optional()
-  defp map_domain_default(:closed, _dk), do: not_set()
-  defp map_domain_default(domains = %{}, dk), do: Map.get(domains, dk, not_set())
-
-  # Merge the two value types for a key, per OCaml's rule:
-  # if right may be absent, use left ∪ present(right), else right.
-  defp map_merge_value(left, right) do
-    {optional?, right_present} = pop_optional_static(right)
-    if optional?, do: union(left, right_present), else: right
-  end
-
   defp map_descr(tag, pairs, default, force?) do
     {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false)
 
@@ -2886,68 +2592,21 @@ defmodule Module.Types.Descr do
 
   defp map_only?(descr), do: empty?(Map.delete(descr, :map))
 
-  defp map_union(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_top, _} ->
-        :bdd_top
-
-      {_, :bdd_top} ->
-        :bdd_top
-
-      {:bdd_bot, bdd} ->
-        bdd
-
-      {bdd, :bdd_bot} ->
-        bdd
-
-      {map_literal(tag1, fields1), map_literal(tag2, fields2)} ->
-        case maybe_optimize_map_union({tag1, fields1, []}, {tag2, fields2, []}) do
-          {tag, fields, []} ->
-            {{tag, fields}, :bdd_top, :bdd_bot}
-
-          nil ->
-            lit1 = {tag1, fields1}
-            lit2 = {tag2, fields2}
-
-            cond do
-              lit1 == lit2 -> {lit1, :bdd_top, :bdd_bot}
-              lit1 < lit2 -> {lit1, :bdd_top, {lit2, :bdd_top, :bdd_bot}}
-              lit1 > lit2 -> {lit2, :bdd_top, {lit1, :bdd_top, :bdd_bot}}
-            end
-        end
-
-      {{map, l1, r1}, {map, l2, r2}} ->
-        {map, map_union(l1, l2), map_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
-      {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 ->
-        {map1, map_union(l1, bdd2), map_union(r1, bdd2)}
-
-      {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 ->
-        {map2, map_union(bdd1, l2), map_union(bdd1, r2)}
-
-        # {{map, l, r}, bdd} ->
-        #   {map, map_union(l, bdd), map_union(r, bdd)}
+  defp non_empty_map_only?(descr) do
+    case :maps.take(:map, descr) do
+      :error -> false
+      {map_bdd, rest} -> empty?(rest) and not map_empty?(map_bdd)
     end
   end
 
-  # defp map_union(dnf1, dnf2) do
-  #   # Union is just concatenation, but we rely on some optimization strategies to
-  #   # avoid the list to grow when possible
+  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 -> {{tag1, fields1}, :bdd_top, {{tag2, fields2}, :bdd_top, :bdd_bot}}
+    end
+  end
 
-  #   # first pass trying to identify patterns where two maps can be fused as one
-  #   with [map1] <- dnf1,
-  #        [map2] <- dnf2,
-  #        optimized when optimized != nil <- maybe_optimize_map_union(map1, map2) do
-  #     [optimized]
-  #   else
-  #     # otherwise we just concatenate and remove structural duplicates
-  #     _ -> dnf1 ++ (dnf2 -- dnf1)
-  #   end
-  # end
-  # defp maybe_optimize_map_union(map, map), do: map
+  def 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
@@ -3045,110 +2704,52 @@ defmodule Module.Types.Descr do
     if subtype?(v2, v1), do: :right_subtype_of_left
   end
 
-  defp is_map_top?({{tag, fields}, :bdd_top, :bdd_bot}) do
-    tag == :open and map_size(fields) == 0
-  end
-
+  defp is_map_top?(map_literal(:open, fields)) when map_size(fields) == 0, do: true
   defp is_map_top?(_), do: false
 
+  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}
+    catch
+      :empty -> :bdd_bot
+    end
+  end
+
   defp map_intersection(bdd1, bdd2) do
     # If intersecting with the top map type, no-op
     cond do
       is_map_top?(bdd1) and is_tuple(bdd2) -> bdd2
       is_map_top?(bdd2) and is_tuple(bdd1) -> bdd1
-      true -> map_intersection_recur(bdd1, bdd2)
-    end
-  end
-
-  defp map_intersection_recur(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
-
-      {map_literal(tag1, fields1), map_literal(tag2, fields2)} ->
-        try do
-          map = map_literal_intersection(tag1, fields1, tag2, fields2)
-          {map, :bdd_top, :bdd_bot}
-        catch
-          :empty -> :bdd_bot
-        end
-
-      # 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).
-      # No: bc we want to have increasing order of literals.
-      # {bdd, {map, :bdd_top, :bdd_bot}} ->
-      #   {map, bdd, :bdd_bot}
-
-      # {bdd, {map, :bdd_bot, :bdd_top}} ->
-      #   {map, :bdd_bot, bdd}
-
-      # {{map, :bdd_top, :bdd_bot}, bdd} ->
-      #   {map, bdd, :bdd_bot}
-
-      # {{map, :bdd_bot, :bdd_top}, bdd} ->
-      #   {map, :bdd_bot, bdd}
-
-      # General cases
-      {{map, l1, r1}, {map, l2, r2}} ->
-        {map, map_intersection_recur(l1, l2), map_intersection_recur(r1, r2)}
-
-      {{map1, l1, r1}, {map2, l2, r2}} when map1 < map2 ->
-        {map1, map_intersection_recur(l1, bdd2), map_intersection_recur(r1, bdd2)}
-
-      {{map1, l1, r1}, {map2, l2, r2}} when map1 > map2 ->
-        {map2, map_intersection_recur(bdd1, l2), map_intersection_recur(bdd1, r2)}
-
-        # {{map, l, r}, bdd} ->
-        #   {map, map_intersection_recur(l, bdd), map_intersection_recur(r, bdd)}
+      true -> bdd_intersection(bdd1, bdd2)
     end
   end
 
-  defp map_difference(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_bot, _} ->
-        :bdd_bot
+  # Optimizations on single maps.
+  defp map_difference(map_literal(tag, fields) = map1, map_literal(neg_tag, neg_fields) = map2) do
+    # Case 1: we are removing an open map with one field. Just do the difference of that field.
+    if neg_tag == :open and map_size(neg_fields) == 1 do
+      {key, value, _rest} = :maps.next(:maps.iterator(neg_fields))
+      t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value)
 
-      {_, :bdd_top} ->
+      if empty?(t_diff) do
         :bdd_bot
+      else
+        map_literal(tag, Map.put(fields, key, t_diff))
+      end
+    else
+      # Case 2: the maps have all but one key in common. Do the difference of that key.
+      case map_all_but_one(tag, fields, neg_tag, neg_fields) do
+        {:one, diff_key} ->
+          map_literal(tag, Map.update!(fields, diff_key, &difference(&1, neg_fields[diff_key])))
 
-      {bdd, :bdd_bot} ->
-        bdd
-
-      {:bdd_top, {map, l, r}} ->
-        {map, map_difference(:bdd_top, l), map_difference(:bdd_top, r)}
-
-      {{map, l1, r1}, {map, l2, r2}} ->
-        {map, map_difference(l1, l2), map_difference(r1, r2)}
-
-      {{map1, l1, r1}, {map2, _l2, _r2}} when map1 < map2 ->
-        {map1, map_difference(l1, bdd2), map_difference(r1, bdd2)}
-
-      {{map1, _l1, _r1}, {map2, l2, r2}} when map1 > map2 ->
-        {map2, map_difference(bdd1, l2), map_difference(bdd1, r2)}
-
-        # {{map, l, r}, bdd} -> {map, map_difference(l, bdd), map_difference(r, bdd)}
+        _ ->
+          bdd_difference(map1, map2)
+      end
     end
   end
 
-  # defp map_negation(bdd) do
-  #   case bdd do
-  #     :bdd_bot -> :bdd_top
-  #     :bdd_top -> :bdd_bot
-  #     {map, l, r} -> {map, map_negation(l), map_negation(r)}
-  #   end
-  # end
+  defp map_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2)
 
   # Intersects two map literals; throws if their intersection is empty.
   # Both open: the result is open.
@@ -3258,71 +2859,10 @@ defmodule Module.Types.Descr do
     if empty?(type), do: throw(:empty), else: type
   end
 
-  # defp map_difference(_, dnf) when dnf == @map_top, do: []
-  # defp map_difference(dnf, dnf), do: []
-
-  # defp map_difference(dnf1, dnf2) do
-  #   Enum.reduce(dnf2, dnf1, fn
-  #     {:open, fields2, []}, current_dnf when map_size(fields2) == 1 ->
-  #       # Optimization: we are removing an open map with one field.
-  #       Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
-  #         {key, value, _rest} = :maps.next(:maps.iterator(fields2))
-  #         t_diff = difference(Map.get(fields1, key, map_key_tag_to_type(tag1)), value)
-
-  #         if empty?(t_diff) do
-  #           acc
-  #         else
-  #           {tag, pos} = {tag1, Map.put(fields1, key, t_diff)}
-  #           entry = {tag, pos, negs1}
-
-  #           cond do
-  #             :lists.member({tag, pos}, negs1) -> acc
-  #             :lists.member(entry, acc) -> acc
-  #             true -> [entry | acc]
-  #           end
-  #         end
-  #       end)
-
-  #     {tag2, fields2, negs2}, current_dnf ->
-  #       Enum.reduce(current_dnf, [], fn {tag1, fields1, negs1}, acc ->
-  #         negs =
-  #           if :lists.member({tag2, fields2}, negs1) do
-  #             negs1
-  #           else
-  #             [{tag2, fields2} | negs1]
-  #           end
-
-  #         acc = prepend_to_map_dnf(tag1, fields1, negs, acc)
-
-  #         Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc ->
-  #           try do
-  #             {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2)
-  #             prepend_to_map_dnf(tag, fields, negs1, acc)
-  #           catch
-  #             :empty -> acc
-  #           end
-  #         end)
-  #       end)
-  #   end)
-  # end
-
-  # defp prepend_to_map_dnf(tag, fields, negs, acc) do
-  #   entry = {tag, fields, negs}
-
-  #   cond do
-  #     :lists.member({tag, fields}, negs) -> acc
-  #     :lists.member(entry, acc) -> acc
-  #     true -> [entry | acc]
-  #   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.
-  def map_bdd_get(bdd) do
-    # dbg(bdd)
-    map_bdd_get([], {:open, %{}}, [], bdd)
-  end
+  def map_bdd_get(bdd), do: map_bdd_get([], {:open, %{}}, [], bdd)
 
   defp map_bdd_get(acc, {tag, fields} = map, negs, bdd) do
     case bdd do
@@ -3358,7 +2898,7 @@ defmodule Module.Types.Descr do
   def map_fetch(%{} = descr, key) when is_atom(key) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        if descr_key?(descr, :map) and map_only?(descr) do
+        if descr_key?(descr, :map) and non_empty_map_only?(descr) do
           {static_optional?, static_type} = map_fetch_static(descr, key)
 
           if static_optional? or empty?(static_type) do
@@ -3614,14 +3154,6 @@ defmodule Module.Types.Descr do
 
   defp map_put_static(descr, _key, _type), do: descr
 
-  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
-
   @doc """
   Removes a key from a map type.
   """
@@ -4107,35 +3639,50 @@ defmodule Module.Types.Descr do
 
   # Use heuristics to normalize a map dnf for pretty printing.
   defp map_normalize(bdd) do
-    for {tag, fields, negs} <- map_bdd_get(bdd) do
-      {fields, negs} =
-        Enum.reduce(negs, {fields, []}, fn
-          # Optimization: we are removing an open map with one field.
-          {:open, neg_fields}, {acc_fields, acc_negs} when map_size(neg_fields) == 1 ->
-            {key, value, _rest} = :maps.next(:maps.iterator(neg_fields))
-            t_diff = difference(Map.get(fields, key, map_key_tag_to_type(tag)), value)
-
-            # If the difference was empty, then the whole line would be empty, which is not.
-            {Map.put(acc_fields, key, t_diff), acc_negs}
-
-          neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} ->
-            if non_intersecting_negation?(tag, acc_fields, neg) do
-              {acc_fields, acc_negs}
-            else
-              case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do
-                {:one, diff_key} ->
-                  {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])),
-                   acc_negs}
-
-                _ ->
-                  {acc_fields, [neg | acc_negs]}
-              end
-            end
-        end)
+    map_bdd_get(bdd)
+    |> Enum.map(fn {tag, fields, negs} ->
+      map_eliminate_while_negs_decrease(tag, fields, negs)
+    end)
+    |> map_fusion()
+  end
 
+  # Continue to eliminate negations while length of list of negs decreases
+  defp map_eliminate_while_negs_decrease(tag, fields, []), do: {tag, fields, []}
+
+  defp map_eliminate_while_negs_decrease(tag, fields, negs) do
+    n = length(negs)
+    {fields, negs} = maybe_eliminate_map_negations(tag, fields, negs)
+
+    if length(negs) < n do
+      map_eliminate_while_negs_decrease(tag, fields, negs)
+    else
       {tag, fields, negs}
     end
-    |> map_fusion()
+  end
+
+  defp maybe_eliminate_map_negations(tag, fields, negs) do
+    Enum.reduce(negs, {fields, []}, fn neg = {neg_tag, neg_fields}, {acc_fields, acc_negs} ->
+      # If the intersection with the negative is empty, we can remove the negative.
+      empty_intersection? =
+        try do
+          _ = map_literal_intersection(tag, acc_fields, neg_tag, neg_fields)
+          false
+        catch
+          :empty -> true
+        end
+
+      if empty_intersection? do
+        {acc_fields, acc_negs}
+      else
+        case map_all_but_one(tag, acc_fields, neg_tag, neg_fields) do
+          {:one, diff_key} ->
+            {Map.update!(acc_fields, diff_key, &difference(&1, neg_fields[diff_key])), acc_negs}
+
+          _ ->
+            {acc_fields, [neg | acc_negs]}
+        end
+      end
+    end)
   end
 
   # Given a dnf, fuse maps when possible
@@ -4189,18 +3736,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Adapted from `map_empty?` to remove useless negations.
-  defp non_intersecting_negation?(tag, fields, {neg_tag, neg_fields}) do
-    (tag == :closed and
-       Enum.any?(neg_fields, fn {neg_key, neg_type} ->
-         not is_map_key(fields, neg_key) and not is_optional_static(neg_type)
-       end)) or
-      (neg_tag == :closed and
-         Enum.any?(fields, fn {key, type} ->
-           not is_map_key(neg_fields, key) and not is_optional_static(type)
-         end))
-  end
-
   defp map_to_quoted(bdd, opts) do
     map_normalize(bdd)
     |> Enum.map(&map_each_to_quoted(&1, opts))
@@ -4317,7 +3852,7 @@ defmodule Module.Types.Descr do
 
   ## Tuple
 
-  # Represents tuple types in two forms:
+  # Represents tuple types as a BDD with nodes of the following forms:
   # 1. Closed tuples: Fixed-length tuples with specific element types
   #    Example: {integer(), atom()}
   # 2. Open tuples: Variable-length tuples with a minimum set of element types
@@ -4374,28 +3909,17 @@ defmodule Module.Types.Descr do
     {acc, dynamic?}
   end
 
-  defp tuple_new(tag, elements), do: [{tag, elements}]
-
-  defp tuple_intersection(dnf1, dnf2) do
-    for {tag1, elements1} <- dnf1,
-        {tag2, elements2} <- dnf2,
-        reduce: [] do
-      acc ->
-        case tuple_literal_intersection(tag1, elements1, tag2, elements2) do
-          {tag, elements} ->
-            entry = {tag, elements}
-
-            case :lists.member(entry, acc) do
-              true -> acc
-              false -> [entry | acc]
-            end
+  defp tuple_new(tag, elements), do: tuple_literal(tag, elements)
 
-          :empty ->
-            acc
-        end
+  defp tuple_intersection(tuple_literal(tag1, elements1), tuple_literal(tag2, elements2)) do
+    case tuple_literal_intersection(tag1, elements1, tag2, elements2) do
+      {tag, elements} -> tuple_literal(tag, elements)
+      :empty -> :bdd_bot
     end
   end
 
+  defp tuple_intersection(bdd1, bdd2), do: bdd_intersection(bdd1, bdd2)
+
   defp tuple_literal_intersection(tag1, elements1, tag2, elements2) do
     n = length(elements1)
     m = length(elements2)
@@ -4428,19 +3952,108 @@ defmodule Module.Types.Descr do
     zip_non_empty_intersection!(rest1, rest2, [non_empty_intersection!(type1, type2) | acc])
   end
 
-  defp tuple_difference(_, dnf) when dnf == @tuple_top do
-    0
+  defp tuple_difference(bdd1, bdd2), do: bdd_difference(bdd1, bdd2)
+
+  defp tuple_empty?(bdd), do: tuple_bdd_to_dnf(bdd) == []
+
+  # No negations, so not empty unless there's an empty type
+  # Note: since the extraction from the BDD is done in a way that guarantees that
+  # the elements are non-empty, we can avoid checking for empty types there.
+  # Otherwise, tuple_empty?(_, elements, []) would be Enum.any?(elements, &empty?/1)
+  defp tuple_empty?(_, _, []), do: false
+  # Open empty negation makes it empty
+  defp tuple_empty?(_, _, [{:open, []} | _]), do: true
+  # Open positive can't be emptied by a single closed negative
+  defp tuple_empty?(:open, _pos, [{:closed, _}]), do: false
+
+  defp tuple_empty?(tag, elements, [{neg_tag, neg_elements} | negs]) do
+    n = length(elements)
+    m = length(neg_elements)
+
+    # Scenarios where the difference is guaranteed to be empty:
+    # 1. When removing larger tuples from a fixed-size positive tuple
+    # 2. When removing smaller tuples from larger tuples
+    if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do
+      tuple_empty?(tag, elements, negs)
+    else
+      case element_intersection(elements, neg_elements) do
+        :empty ->
+          tuple_empty?(tag, elements, negs)
+
+        _ ->
+          tuple_elements_empty?([], tag, elements, neg_elements, negs) and
+            tuple_compatibility(n, m, tag, elements, neg_tag, negs)
+      end
+    end
+  end
+
+  # Recursively check elements for emptiness
+  defp tuple_elements_empty?(_, _, _, [], _), do: true
+
+  defp tuple_elements_empty?(acc_meet, tag, elements, [neg_type | neg_elements], negs) do
+    # Handles the case where {tag, elements} is an open tuple, like {:open, []}
+    {ty, elements} = List.pop_at(elements, 0, term())
+    diff = difference(ty, neg_type)
+    meet = intersection(ty, neg_type)
+
+    # In this case, there is no intersection between the positive and this negative.
+    # So we should just "go next"
+    (empty?(diff) or tuple_empty?(tag, Enum.reverse(acc_meet, [diff | elements]), negs)) and
+      tuple_elements_empty?([meet | acc_meet], tag, elements, neg_elements, negs)
+  end
+
+  # Function that, given two tuples {tag1, elements1} and {tag2, elements2}, computes the
+  # intersection of all their elements (with default term() if one is open).
+  # If any intersection is empty, it return :empty. Else, it should return the list of them.
+  defp element_intersection(elements1, elements2) do
+    elements1 =
+      if length(elements1) < length(elements2),
+        do: tuple_fill(elements1, length(elements2)),
+        else: elements1
+
+    elements2 =
+      if length(elements1) > length(elements2),
+        do: tuple_fill(elements2, length(elements1)),
+        else: elements2
+
+    Enum.reduce_while(Enum.zip(elements1, elements2), [], fn {type1, type2}, acc ->
+      case intersection(type1, type2) do
+        :empty -> {:halt, :empty}
+        meet -> {:cont, [meet | acc]}
+      end
+    end)
+    |> case do
+      :empty -> :empty
+      list -> Enum.reverse(list)
+    end
   end
 
-  defp tuple_difference(dnf1, dnf2) do
-    Enum.reduce(dnf2, dnf1, fn {tag2, elements2}, dnf1 ->
-      Enum.reduce(dnf1, [], fn {tag1, elements1}, acc ->
-        tuple_eliminate_single_negation(tag1, elements1, {tag2, elements2})
-        |> tuple_union(acc)
+  # Determines if the set difference is empty when:
+  # - Positive tuple: {tag, elements} of size n
+  # - Negative tuple: open or closed tuples of size m
+  defp tuple_compatibility(n, m, tag, elements, neg_tag, negs) do
+    # The tuples to consider are all those of size n to m - 1, and if the negative tuple is
+    # closed, we also need to consider tuples of size greater than m + 1.
+    tag == :closed or
+      (Enum.all?(n..(m - 1)//1, &tuple_empty?(:closed, tuple_fill(elements, &1), negs)) and
+         (neg_tag == :open or tuple_empty?(:open, tuple_fill(elements, m + 1), negs)))
+  end
+
+  defp tuple_eliminate_negations(tag, elements, negs) do
+    Enum.reduce(negs, [{tag, elements}], fn {neg_tag, neg_elements}, acc ->
+      Enum.flat_map(acc, fn {tag, elements} ->
+        tuple_eliminate_single_negation(tag, elements, {neg_tag, neg_elements})
       end)
     end)
   end
 
+  defp empty_element_intersection?(elements1, elements2) do
+    Enum.any?(Enum.zip(elements1, elements2), fn {type1, type2} ->
+      empty?(intersection(type1, type2))
+    end)
+  end
+
+  # Important: this generates DISJOINT tuples.
   defp tuple_eliminate_single_negation(tag, elements, {neg_tag, neg_elements}) do
     n = length(elements)
     m = length(neg_elements)
@@ -4448,34 +4061,67 @@ defmodule Module.Types.Descr do
     # Scenarios where the difference is guaranteed to be empty:
     # 1. When removing larger tuples from a fixed-size positive tuple
     # 2. When removing smaller tuples from larger tuples
-    if (tag == :closed and n < m) or (neg_tag == :closed and n > m) do
+    # 3. When there is no intersection between the elements of the two tuples
+    if (tag == :closed and n < m) or (neg_tag == :closed and n > m) or
+         empty_element_intersection?(elements, neg_elements) do
       [{tag, elements}]
     else
-      tuple_union(
+      tuple_dnf_union(
         tuple_elim_content([], tag, elements, neg_elements),
         tuple_elim_size(n, m, tag, elements, neg_tag)
       )
     end
   end
 
-  # Eliminates negations according to tuple content.
-  defp tuple_elim_content(_acc, _tag, _elements, []), do: []
-
-  # Subtracts each element of a negative tuple to build a new tuple with the difference.
-  # Example: {number(), atom()} and not {float(), :foo} contains types {integer(), :foo}
-  # as well as {float(), atom() and not :foo}
-  # Same process as tuple_elements_empty?
+  # Build a disjoint disjunction for {t1,...,tn} ∧ not {u1,...,un}
+  # by splitting on the *earliest* index where they differ.
+  #
+  # Invariant:
+  # - `acc` holds the prefix we've already forced to *match* the negative tuple,
+  #   stored in reverse order (so we can `Enum.reverse/2` at the end when we emit).
+  # - `elements` are the yet-unprocessed positive tuple element types.
+  # - `neg_elements` are the corresponding negative tuple element types.
+  #
+  # For position i:
+  #   - One branch mismatches here:  (ti \ ui), with earlier positions fixed to intersection(tj, uj).
+  #   - The other recursive path forces match here: intersection(ti, ui) and continues to i+1.
+  #
+  # This yields disjoint branches like:
+  #   {t1∧¬u1, t2, t3, ...} OR {t1∧u1, t2∧¬u2, t3, ...} OR {t1∧u1, t2∧u2, t3∧¬u3, ...} ...
   defp tuple_elim_content(acc, tag, elements, [neg_type | neg_elements]) do
-    {ty, elements} = List.pop_at(elements, 0, term())
+    # If `elements` is shorter, default to top type `term()` (as in your example).
+    {ty, rest} = List.pop_at(elements, 0, term())
+
+    # ti \ ui  (i.e., ti ∧ ¬ui)
     diff = difference(ty, neg_type)
+    # ti ∧ ui
+    meet = intersection(ty, neg_type)
+
+    # Branch where the earliest difference is *here*.
+    # Earlier positions are the accumulated matches in `acc`;
+    # later positions remain unconstrained (`rest` as-is).
+    here_branch =
+      if empty?(diff) do
+        []
+      else
+        [{tag, Enum.reverse(acc, [diff | rest])}]
+      end
 
-    res = tuple_elim_content([ty | acc], tag, elements, neg_elements)
+    # Branches where we force equality here and defer the first difference to later positions.
+    later_branches =
+      if empty?(meet) do
+        []
+      else
+        tuple_elim_content([meet | acc], tag, rest, neg_elements)
+      end
 
-    if empty?(diff) do
-      res
-    else
-      [{tag, Enum.reverse(acc, [diff | elements])} | res]
-    end
+    here_branch ++ later_branches
+  end
+
+  # No more negative elements to process: there is no “all-equal” branch to add,
+  # because we’re constructing {t} ∧ ¬{u}, which must differ somewhere.
+  defp tuple_elim_content(_acc, _tag, _elements, []) do
+    []
   end
 
   # Eliminates negations according to size
@@ -4498,8 +4144,8 @@ defmodule Module.Types.Descr do
     )
   end
 
-  defp tuple_union(dnf1, dnf2) do
-    # Union is just concatenation, but we rely on some optimization strategies to
+  defp tuple_dnf_union(dnf1, dnf2) do
+    # Union of tuple DNFs is just concatenation, but we rely on some optimization strategies to
     # avoid the list to grow when possible
 
     # first pass trying to identify patterns where two maps can be fused as one
@@ -4513,6 +4159,18 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp tuple_union(
+         tuple_literal(tag1, elements1) = tuple1,
+         tuple_literal(tag2, elements2) = tuple2
+       ) do
+    case maybe_optimize_tuple_union({tag1, elements1}, {tag2, elements2}) do
+      {tag, elements} -> tuple_literal(tag, elements)
+      nil -> bdd_union(tuple1, tuple2)
+    end
+  end
+
+  defp tuple_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
+
   defp maybe_optimize_tuple_union({tag1, pos1} = tuple1, {tag2, pos2} = tuple2) do
     case tuple_union_optimization_strategy(tag1, pos1, tag2, pos2) do
       :all_equal ->
@@ -4599,22 +4257,57 @@ defmodule Module.Types.Descr do
     if subtype?(v2, v1), do: :right_subtype_of_left
   end
 
-  defp tuple_to_quoted(dnf, opts) do
-    dnf
+  defp tuple_to_quoted(bdd, opts) do
+    tuple_bdd_to_dnf_no_negations(bdd)
     |> tuple_fusion()
     |> Enum.map(&tuple_literal_to_quoted(&1, opts))
   end
 
-  # Given a dnf of tuples, fuses the tuple unions when possible,
+  # Transforms a bdd into a dnf (union of tuples with negations)
+  def tuple_bdd_to_dnf(bdd),
+    do: tuple_bdd_get([], {:open, []}, [], bdd, &{&1, &2, &3}, &[&1 | &2])
+
+  # Transforms a bdd into a positive normal form (union of tuples with no negations)
+  # Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates
+  defp tuple_bdd_to_dnf_no_negations(bdd),
+    do: tuple_bdd_get([], {:open, []}, [], bdd, &tuple_eliminate_negations/3, &tuple_dnf_union/2)
+
+  defp tuple_bdd_get(acc, {tag, elements} = tuple, negs, bdd, transform, compose) do
+    case bdd do
+      :bdd_bot ->
+        acc
+
+      :bdd_top ->
+        if tuple_empty?(tag, elements, negs) do
+          acc
+        else
+          compose.(transform.(tag, elements, negs), acc)
+        end
+
+      {{next_tag, next_elements} = next_tuple, left, right} ->
+        acc =
+          case tuple_literal_intersection(tag, elements, next_tag, next_elements) do
+            :empty ->
+              acc
+
+            new_tuple ->
+              tuple_bdd_get(acc, new_tuple, negs, left, transform, compose)
+          end
+
+        tuple_bdd_get(acc, tuple, [next_tuple | negs], right, transform, compose)
+    end
+  end
+
+  # Given a union of tuples, fuses the tuple unions when possible,
   # e.g. {integer(), atom()} or {float(), atom()} into {number(), atom()}
   # The negations of two fused tuples are just concatenated.
-  defp tuple_fusion(dnf) do
+  defp tuple_fusion(dnf_no_negations) do
     # Steps:
     # 1. Consider tuples without negations apart from those with
     # 2. Group tuples by size and tag
     # 3. Try fusions for each group until no fusion is found
     # 4. Merge the groups back into a dnf
-    dnf
+    dnf_no_negations
     |> Enum.group_by(fn {tag, elems} -> {tag, length(elems)} end)
     |> Enum.flat_map(fn {_, tuples} -> tuple_non_negated_fuse(tuples) end)
   end
@@ -4688,7 +4381,7 @@ defmodule Module.Types.Descr do
   def tuple_fetch(%{} = descr, key) when is_integer(key) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        if descr_key?(descr, :tuple) and tuple_only?(descr) do
+        if descr_key?(descr, :tuple) and non_empty_tuple_only?(descr) do
           {static_optional?, static_type} = tuple_fetch_static(descr, key)
 
           # If I access a static tuple at a "open position", we have two options:
@@ -4732,6 +4425,13 @@ defmodule Module.Types.Descr do
 
   defp tuple_only?(descr), do: empty?(Map.delete(descr, :tuple))
 
+  defp non_empty_tuple_only?(descr) do
+    case :maps.take(:tuple, descr) do
+      :error -> false
+      {tuple_bdd, rest} -> empty?(rest) and not tuple_empty?(tuple_bdd)
+    end
+  end
+
   defp tuple_fetch_static(descr, index) when is_integer(index) do
     case descr do
       :term -> {true, term()}
@@ -4740,8 +4440,9 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp tuple_get(dnf, index) do
-    Enum.reduce(dnf, none(), fn
+  defp tuple_get(bdd, index) do
+    tuple_bdd_to_dnf_no_negations(bdd)
+    |> Enum.reduce(none(), fn
       {tag, elements}, acc -> Enum.at(elements, index, tuple_tag_to_type(tag)) |> union(acc)
     end)
   end
@@ -4755,23 +4456,24 @@ defmodule Module.Types.Descr do
     case :maps.take(:dynamic, descr) do
       :error ->
         if tuple_only?(descr) do
-          process_tuples_values(Map.get(descr, :tuple, []))
+          process_tuples_values(Map.get(descr, :tuple, :bdd_bot))
         else
           :badtuple
         end
 
       {dynamic, static} ->
         if tuple_only?(static) and descr_key?(dynamic, :tuple) do
-          dynamic(process_tuples_values(Map.get(dynamic, :tuple, [])))
-          |> union(process_tuples_values(Map.get(static, :tuple, [])))
+          dynamic(process_tuples_values(Map.get(dynamic, :tuple, :bdd_bot)))
+          |> union(process_tuples_values(Map.get(static, :tuple, :bdd_bot)))
         else
           :badtuple
         end
     end
   end
 
-  defp process_tuples_values(dnf) do
-    Enum.reduce(dnf, none(), fn {tag, elements}, acc ->
+  defp process_tuples_values(bdd) do
+    tuple_bdd_to_dnf_no_negations(bdd)
+    |> Enum.reduce(none(), fn {tag, elements}, acc ->
       cond do
         Enum.any?(elements, &empty?/1) -> none()
         tag == :open -> term()
@@ -4830,8 +4532,8 @@ defmodule Module.Types.Descr do
   def tuple_delete_at(_, _), do: :badindex
 
   # Takes a static map type and removes an index from it.
-  defp tuple_delete_static(%{tuple: dnf}, index) do
-    %{tuple: Enum.map(dnf, fn {tag, elements} -> {tag, List.delete_at(elements, index)} end)}
+  defp tuple_delete_static(%{tuple: bdd}, index) do
+    %{tuple: bdd_map(bdd, fn {tag, elements} -> {tag, List.delete_at(elements, index)} end)}
   end
 
   # If there is no map part to this static type, there is nothing to delete.
@@ -4894,8 +4596,8 @@ defmodule Module.Types.Descr do
   defp tuple_insert_static(descr, _, _) when descr == @none, do: none()
 
   defp tuple_insert_static(descr, index, type) do
-    Map.update!(descr, :tuple, fn dnf ->
-      Enum.map(dnf, fn {tag, elements} ->
+    Map.update!(descr, :tuple, fn bdd ->
+      bdd_map(bdd, fn {tag, elements} ->
         {tag, List.insert_at(elements, index, type)}
       end)
     end)
@@ -4907,16 +4609,98 @@ defmodule Module.Types.Descr do
 
   defp tuple_of_size_at_least_static?(descr, index) do
     case descr do
-      %{tuple: dnf} ->
-        Enum.all?(dnf, fn
-          {_, elements} -> length(elements) >= index
-        end)
+      %{tuple: bdd} ->
+        tuple_bdd_to_dnf_no_negations(bdd)
+        |> Enum.all?(fn {_, elements} -> length(elements) >= index end)
 
       %{} ->
         true
     end
   end
 
+  ## BDD helpers
+
+  # 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(bdd1, bdd2) do
+    case {bdd1, bdd2} do
+      {:bdd_bot, _} ->
+        :bdd_bot
+
+      {other, :bdd_bot} ->
+        other
+
+      {:bdd_top, {lit, l, r}} ->
+        {lit, bdd_difference(:bdd_top, l), bdd_difference(:bdd_top, r)}
+
+      {_, :bdd_top} ->
+        :bdd_bot
+
+      {{lit, l1, r1}, {lit, l2, r2}} ->
+        {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)}
+
+      {{lit1, l1, r1}, {lit2, _, _} = bdd2} when lit1 < lit2 ->
+        {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)}
+
+      {{lit1, _, _} = bdd1, {lit2, l2, r2}} when lit1 > lit2 ->
+        {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)}
+    end
+  end
+
+  # 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
+
   ## 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 f406adb296..0383a2a17d 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -637,13 +637,14 @@ defmodule Module.Types.DescrTest do
              )
 
       # Nested lists with last element
+      # "lists of (lists of integers), ending with atom"
+      # minus
+      # "lists of (lists of numbers), ending with boolean"
+      # gives:
+      # "non empty lists of (lists of integers), ending with (atom and not boolean)"
+
       assert difference(list(list(integer()), atom()), list(list(number()), boolean()))
-             |> equal?(
-               union(
-                 non_empty_list(list(integer()), difference(atom(), boolean())),
-                 non_empty_list(difference(list(integer()), list(number())), atom())
-               )
-             )
+             |> equal?(non_empty_list(list(integer()), difference(atom(), boolean())))
 
       # Union types in last element
       assert difference(list(integer(), union(atom(), binary())), list(number(), atom()))
@@ -1538,11 +1539,12 @@ defmodule Module.Types.DescrTest do
     test "map_fetch" do
       assert map_fetch(term(), :a) == :badmap
       assert map_fetch(union(open_map(), integer()), :a) == :badmap
+      assert map_fetch(difference(open_map(), open_map()), :a) == :badmap
+      assert map_fetch(difference(closed_map(a: integer()), closed_map(a: term())), :a) == :badmap
 
       assert map_fetch(open_map(), :a) == :badkey
       assert map_fetch(open_map(a: not_set()), :a) == :badkey
       assert map_fetch(union(closed_map(a: integer()), closed_map(b: atom())), :a) == :badkey
-      assert map_fetch(difference(closed_map(a: integer()), closed_map(a: term())), :a) == :badkey
 
       assert map_fetch(closed_map(a: integer()), :a) == {false, integer()}
 
@@ -2361,7 +2363,7 @@ defmodule Module.Types.DescrTest do
              )
              |> union(difference(open_map(x: atom()), open_map(x: boolean())))
              |> to_quoted_string() ==
-               "%{..., a: integer(), b: atom(), c: boolean()} or %{..., x: atom() and not boolean()}"
+               "%{..., a: integer(), b: atom(), c: boolean()} or\n  (%{..., x: atom() and not boolean()} and not %{..., a: integer(), b: atom(), c: boolean()})"
 
       assert closed_map(a: number(), b: atom(), c: pid())
              |> difference(closed_map(a: integer(), b: atom(), c: pid()))
@@ -2375,6 +2377,11 @@ defmodule Module.Types.DescrTest do
 
       # Remark: this simplification is order dependent. Having the first difference
       # after the second gives a different result.
+      assert open_map(a: number(), b: atom(), c: union(pid(), port()))
+             |> difference(open_map(a: integer(), b: atom(), c: union(pid(), port())))
+             |> difference(open_map(a: float(), b: atom(), c: pid()))
+             |> to_quoted_string() == "%{..., a: float(), b: atom(), c: port()}"
+
       assert open_map(a: number(), b: atom(), c: union(pid(), port()))
              |> difference(open_map(a: float(), b: atom(), c: pid()))
              |> difference(open_map(a: integer(), b: atom(), c: union(pid(), port())))
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 4c24c59dec..6ace937319 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2056,36 +2056,35 @@ defmodule Module.Types.ExprTest do
     #            )
     # end
 
-    test "typecheck! finishes within 200 ms for Oban-style pattern match" do
-      timeout_ms = 200
-
-      task =
-        Task.async(fn ->
-          typecheck!(fn
-            [:oban, :job, _event], _measure, _meta, _opts -> :ok
-            [:oban, :notifier, :switch], _measure, %{status: _status}, _opts -> :ok
-            [:oban, :peer, :election, :stop], _measure, _meta, _opts -> :ok
-            [:oban, :plugin, :exception], _measure, _meta, _opts -> :ok
-            [:oban, :plugin, :stop], _measure, _meta, _opts -> :ok
-            [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts -> :ok
-            [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts -> :ok
-            _event, _measure, _meta, _opts -> :ok
-          end)
-        end)
+    test "typecheck! must finish fast for large pattern match" do
+      type =
+        typecheck!(fn
+          [:oban, :job, _event], _measure, _meta, _opts ->
+            :ok
 
-      case Task.yield(task, timeout_ms) || Task.shutdown(task, :brutal_kill) do
-        {:ok, type} ->
-          assert type
-                 |> equal?(
-                   fun(
-                     [term(), term(), term(), term()],
-                     dynamic(atom([:ok]))
-                   )
-                 )
+          [:oban, :notifier, :switch], _measure, %{status: _status}, _opts ->
+            :ok
+
+          [:oban, :peer, :election, :stop], _measure, _meta, _opts ->
+            :ok
+
+          [:oban, :plugin, :exception], _measure, _meta, _opts ->
+            :ok
+
+          [:oban, :plugin, :stop], _measure, _meta, _opts ->
+            :ok
+
+          [:oban, :queue, :shutdown], _measure, %{orphaned: [_ | _]}, _opts ->
+            :ok
+
+          [:oban, :stager, :switch], _measure, %{mode: _mode}, _opts ->
+            :ok
+
+          _event, _measure, _meta, _opts ->
+            :ok
+        end)
 
-        nil ->
-          flunk("typecheck! did not finish within #{timeout_ms} ms")
-      end
+      assert subtype?(type, fun([term(), term(), term(), term()], atom([:ok])))
     end
   end
 

From 415a3a2ecf6eb525f854901c4058de708294ba38 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 4 Aug 2025 18:13:27 +0200
Subject: [PATCH 7/9] Cleanup

---
 lib/elixir/lib/module/types/descr.ex          | 453 +++++++-----------
 .../test/elixir/module/types/expr_test.exs    |  34 +-
 2 files changed, 188 insertions(+), 299 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 09c0faa4ce..3e335b01e7 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -48,7 +48,7 @@ defmodule Module.Types.Descr do
     {:domain_key, :list}
   ]
 
-  @fun_top :fun_top
+  @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}
@@ -178,11 +178,25 @@ defmodule Module.Types.Descr do
     Enum.reduce(funs, &intersection/2)
   end
 
-  # This is an insertion of an arrow {domain, return} into a list of non-overlapping arrows.
-  # If no arrow overlaps with the new arrow, it will be inserted at the end.
-  # For any arrow that overlaps, we split this arrow into two: one where the domains intersect,
-  # and one where the domains differ. Then we continue the recursion with the domain subtracted
-  # from the one of the overlapping arrow.
+  # Inserts a new arrow `{domain, return}` into `acc`, a list whose arrows
+  # have disjoint domains.
+  #
+  # To preserve that invariant we compare the new arrow with every function in
+  # the accumulator, `{acc_domain, acc_return}`:
+  #
+  #   * If `intersection(domain, acc_domain)` is empty, the arrows do not overlap.
+  #     We keep the current arrow and recurse on the tail.
+  #
+  #   * Otherwise, the domains overlap. We partition them into:
+  #
+  #       common = intersection(domain, acc_domain)   # shared part
+  #       diff   = difference(domain, acc_domain)     # only in new arrow
+  #       left   = difference(acc_domain, domain)     # only in existing arrow
+  #
+  #     We emit `{common, union(return, acc_return)}` for the shared part,
+  #     keep `{left, acc_return}` (if any), and continue inserting `diff`
+  #     into the remainder of the list to handle further overlaps.
+
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
     common = intersection(domain, acc_domain)
 
@@ -449,7 +463,7 @@ defmodule Module.Types.Descr do
 
   defp intersection(:fun, v1, v2) do
     bdd = fun_intersection(v1, v2)
-    if bdd == :fun_bottom, do: 0, else: bdd
+    if bdd == :bdd_bot, do: 0, else: bdd
   end
 
   defp intersection(:dynamic, v1, v2) do
@@ -471,10 +485,6 @@ defmodule Module.Types.Descr do
       {right_dynamic, right_static} = Map.pop(right, :dynamic, right)
       dynamic_part = difference_static(left_dynamic, right_static)
 
-      # This might be the worst place possible to check for emptiness.
-      # if empty?(dynamic_part),
-      # do: none(),
-      # else:
       Map.put(difference_static(left_static, right_dynamic), :dynamic, dynamic_part)
     else
       difference_static(left, right)
@@ -547,7 +557,7 @@ defmodule Module.Types.Descr do
 
   defp difference(:fun, v1, v2) do
     bdd = fun_difference(v1, v2)
-    if bdd == :fun_bottom, do: 0, else: bdd
+    if bdd == :bdd_bot, do: 0, else: bdd
   end
 
   @doc """
@@ -1078,8 +1088,8 @@ defmodule Module.Types.Descr do
 
   ### Key concepts:
 
-  # * BDD structure: A tree with function nodes and :fun_top/:fun_bottom leaves.
-  #   Paths to :fun_top represent valid function types. Nodes are positive when
+  # * BDD structure: A tree with function nodes and :bdd_top/:bdd_bot leaves.
+  #   Paths to :bdd_top represent valid function types. Nodes are positive when
   #   following a left branch (e.g. (int, float -> bool) and negative otherwise.
 
   # * Function variance:
@@ -1098,7 +1108,7 @@ 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}, :fun_top, :fun_bottom}
+  defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot}
 
   # Creates a function type from a list of inputs and an output
   # where the inputs and/or output may be dynamic.
@@ -1349,8 +1359,7 @@ defmodule Module.Types.Descr do
     type_args = args_to_domain(arguments)
 
     Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
-      {x, _cache} = aux_apply(acc, type_args, term(), intersection_of_arrows, %{})
-      x
+      aux_apply(acc, type_args, term(), intersection_of_arrows)
     end)
   end
 
@@ -1382,67 +1391,39 @@ defmodule Module.Types.Descr do
   # - arrow_intersections: The list of function arrows to process
 
   # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
-  defp aux_apply(result, input, rets_reached, [], cache) do
-    cache_key = {result, input, rets_reached, []}
-    res = union(result, rets_reached)
-    {res, Map.put(cache, cache_key, res)}
+  defp aux_apply(result, _input, rets_reached, []) do
+    if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
   end
 
-  defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections], cache) do
+  defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do
     # Calculate the part of the input not covered by this arrow's domain
-    cache_key = {result, input, returns_reached, [{args, ret} | arrow_intersections]}
-
-    case cache do
-      %{^cache_key => value} ->
-        {value, cache}
-
-      _ ->
-        dom = args_to_domain(args)
-        no_intersection? = empty?(intersection(dom, input))
-
-        cond do
-          # First: is there any intersection between the input and the arrow's domain?
-          # If not, we skip this arrow.
-          no_intersection? ->
-            {result, cache} =
-              aux_apply(result, input, returns_reached, arrow_intersections, cache)
-
-            cache = Map.put(cache, cache_key, result)
-            {result, cache}
-
-          true ->
-            dom_subtract = difference(input, dom)
-
-            # Refine the return type by intersecting with this arrow's return type
-            ret_refine = intersection(returns_reached, ret)
-
-            # Phase 1: Domain partitioning
-            # If the input is not fully covered by the arrow's domain, then the result type should be
-            # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
-            # parts of the domain.
-            #
-            # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
-            # both atoms and pids in the result.
+    dom_subtract = difference(input, args_to_domain(args))
+
+    # Phase 1: Domain partitioning
+    # If the input is not fully covered by the arrow's domain, then the result type should be
+    # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
+    # parts of the domain.
+    #
+    # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
+    # both atoms and pids in the result.
+    result =
+      if empty?(dom_subtract) do
+        result
+      else
+        aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
+      end
 
-            {result, cache} =
-              if empty?(dom_subtract) do
-                {result, cache}
-              else
-                aux_apply(result, dom_subtract, returns_reached, arrow_intersections, cache)
-              end
+    # 2. Return type refinement
+    # The result type is also refined (intersected) in the sense that, if several arrows match
+    # the same part of the input, then the result type is an intersection of the return types of
+    # those arrows.
 
-            # 2. Return type refinement
-            # The result type is also refined (intersected) in the sense that, if several arrows match
-            # the same part of the input, then the result type is an intersection of the return types of
-            # those arrows.
+    # Refine the return type by intersecting with this arrow's return type
+    ret_refine = intersection(returns_reached, ret)
 
-            # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
-            # should result in (atom() ∩ pid()), which is none().
-            {result, cache} = aux_apply(result, input, ret_refine, arrow_intersections, cache)
-            cache = Map.put(cache, cache_key, result)
-            {result, cache}
-        end
-    end
+    # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
+    # should result in (atom() ∩ pid()), which is none().
+    aux_apply(result, input, ret_refine, arrow_intersections)
   end
 
   # Takes all the paths from the root to the leaves finishing with a 1,
@@ -1452,8 +1433,8 @@ defmodule Module.Types.Descr do
 
   defp fun_get(acc, pos, neg, bdd) do
     case bdd do
-      :fun_bottom -> acc
-      :fun_top -> [{pos, neg} | acc]
+      :bdd_bot -> acc
+      :bdd_top -> [{pos, neg} | acc]
       {fun, left, right} -> fun_get(fun_get(acc, [fun | pos], neg, left), pos, [fun | neg], right)
     end
   end
@@ -1472,15 +1453,9 @@ defmodule Module.Types.Descr do
   # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty
   defp fun_empty?(bdd) do
     case bdd do
-      :fun_bottom ->
-        true
-
-      :fun_top ->
-        false
-
-      bdd ->
-        fun_get(bdd)
-        |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end)
+      :bdd_bot -> true
+      :bdd_top -> false
+      bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end)
     end
   end
 
@@ -1517,10 +1492,8 @@ defmodule Module.Types.Descr do
           # Filter positives to only those with matching arity, then check if the negative
           # function's domain is a supertype of the positive domain and if the phi function
           # determines emptiness.
-          neg_dom = args_to_domain(neg_arguments)
-
           length(neg_arguments) == positive_arity and
-            subtype?(neg_dom, positive_domain) and
+            subtype?(args_to_domain(neg_arguments), positive_domain) and
             phi_starter(neg_arguments, neg_return, positives)
         end)
     end
@@ -1588,7 +1561,6 @@ defmodule Module.Types.Descr do
   defp phi(args, {b, t}, [], cache) do
     result = Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t))
     {result, Map.put(cache, {args, {b, t}, []}, result)}
-    # {Enum.any?(args, fn {bool, typ} -> bool and empty?(typ) end) or (b and empty?(t)), cache}
   end
 
   defp phi(args, {b, ret}, [{arguments, return} | rest_positive], cache) do
@@ -1630,8 +1602,8 @@ defmodule Module.Types.Descr do
   end
 
   defp disjoint_non_empty_domains?({arguments, return}, positives) do
-    b1 = all_disjoint_domains?(positives)
-    b2 = all_non_empty_domains?([{arguments, return} | positives])
+    b1 = all_disjoint_arguments?(positives)
+    b2 = all_non_empty_arguments?([{arguments, return} | positives])
 
     cond do
       b1 and b2 -> :disjoint_non_empty
@@ -1640,44 +1612,30 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp all_non_empty_domains?(positives) do
+  defp all_non_empty_arguments?(positives) do
     Enum.all?(positives, fn {args, _ret} ->
       Enum.all?(args, fn arg -> not empty?(arg) end)
     end)
   end
 
-  # For two arguments to be disjoint, we need at least one of their types to be disjoint.
+  # For two arguments to be disjoint, one of their types must be disjoint.
   defp disjoint_arguments?(args1, args2) do
-    Enum.reduce_while(Enum.zip(args1, args2), false, fn {t1, t2}, acc ->
-      t = intersection(t1, t2)
-
-      if empty?(t) do
-        {:halt, true}
-      else
-        {:cont, acc}
-      end
-    end)
+    Enum.any?(Enum.zip(args1, args2), fn {t1, t2} -> disjoint?(t1, t2) end)
   end
 
-  # Test that all positives are two to two disjoint. We iterate on the list to do so.
-  defp all_disjoint_domains?([]), do: true
+  defp all_disjoint_arguments?([]), do: true
 
-  defp all_disjoint_domains?([{args, _} | rest]) do
-    Enum.reduce_while(rest, true, fn {args_rest, _}, _acc ->
-      if disjoint_arguments?(args, args_rest) do
-        {:cont, true}
-      else
-        {:halt, false}
-      end
-    end)
+  defp all_disjoint_arguments?([{args, _} | rest]) do
+    Enum.all?(rest, fn {args_rest, _} -> disjoint_arguments?(args, args_rest) end) and
+      all_disjoint_arguments?(rest)
   end
 
   defp fun_union(bdd1, bdd2) do
     case {bdd1, bdd2} do
-      {:fun_top, _} -> :fun_top
-      {_, :fun_top} -> :fun_top
-      {:fun_bottom, bdd} -> bdd
-      {bdd, :fun_bottom} -> bdd
+      {: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.
@@ -1686,93 +1644,76 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp fun_intersection(bdd1, bdd2) do
-    # If intersecting with the top type for that arity, no-op
-    case {bdd1, bdd2} do
-      {bdd, {{args, return} = fun, :fun_top, :fun_bottom}} when is_tuple(bdd) ->
-        if return == :term and Enum.all?(args, &(&1 == %{})) and
-             matching_arity_left?(bdd, length(args)) do
-          bdd
-        else
-          {fun, bdd, :fun_bottom}
-        end
-
-      {{{args, return} = fun, :fun_top, :fun_bottom}, bdd} when is_tuple(bdd) ->
-        if return == :term and Enum.all?(args, &(&1 == %{})) and
-             matching_arity_left?(bdd, length(args)) do
-          bdd
-        else
-          {fun, bdd, :fun_bottom}
-        end
-
-      _ ->
-        fun_intersection_recur(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 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 matching_arity_left?(_, _arity), do: true
+  defp is_fun_top?(_, _), do: false
 
-  defp matching_arity_right?({_, l, r}, arity) do
-    matching_arity_left?(l, arity) and matching_arity_right?(r, arity)
+  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
+      true -> fun_bdd_intersection(bdd1, bdd2)
+    end
   end
 
-  defp matching_arity_right?(_, _arity), do: true
-
-  defp fun_intersection_recur(bdd1, bdd2) do
+  defp fun_bdd_intersection(bdd1, bdd2) do
     case {bdd1, bdd2} do
       # Base cases
-      {_, :fun_bottom} ->
-        :fun_bottom
+      {_, :bdd_bot} ->
+        :bdd_bot
 
-      {:fun_bottom, _} ->
-        :fun_bottom
+      {:bdd_bot, _} ->
+        :bdd_bot
 
-      {:fun_top, bdd} ->
+      {:bdd_top, bdd} ->
         bdd
 
-      {bdd, :fun_top} ->
+      {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, :fun_top, :fun_bottom}} ->
-        {fun, bdd, :fun_bottom}
+      {bdd, {fun, :bdd_top, :bdd_bot}} ->
+        {fun, bdd, :bdd_bot}
 
-      {bdd, {fun, :fun_bottom, :fun_top}} ->
-        {fun, :fun_bottom, bdd}
+      {bdd, {fun, :bdd_bot, :bdd_top}} ->
+        {fun, :bdd_bot, bdd}
 
-      {{fun, :fun_top, :fun_bottom}, bdd} ->
-        {fun, bdd, :fun_bottom}
+      {{fun, :bdd_top, :bdd_bot}, bdd} ->
+        {fun, bdd, :bdd_bot}
 
-      {{fun, :fun_bottom, :fun_top}, bdd} ->
-        {fun, :fun_bottom, bdd}
+      {{fun, :bdd_bot, :bdd_top}, bdd} ->
+        {fun, :bdd_bot, bdd}
 
       # General cases
       {{fun, l1, r1}, {fun, l2, r2}} ->
-        {fun, fun_intersection_recur(l1, l2), fun_intersection_recur(r1, r2)}
+        {fun, fun_bdd_intersection(l1, l2), fun_bdd_intersection(r1, r2)}
 
       {{fun, l, r}, bdd} ->
-        {fun, fun_intersection_recur(l, bdd), fun_intersection_recur(r, bdd)}
+        {fun, fun_bdd_intersection(l, bdd), fun_bdd_intersection(r, bdd)}
     end
   end
 
-  defp fun_difference(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:fun_bottom, _} -> :fun_bottom
-      {_, :fun_top} -> :fun_bottom
-      {bdd, :fun_bottom} -> bdd
-      {:fun_top, {fun, l, r}} -> {fun, fun_difference(:fun_top, l), fun_difference(:fun_top, r)}
-      {{fun, l1, r1}, {fun, l2, r2}} -> {fun, fun_difference(l1, l2), fun_difference(r1, r2)}
-      {{fun, l, r}, bdd} -> {fun, fun_difference(l, bdd), fun_difference(r, bdd)}
-    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)
+  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)
   end
 
+  defp matching_arity_right?(_, _arity), do: true
+
+  defp fun_difference(bdd1, bdd2), do: 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
@@ -1947,16 +1888,16 @@ defmodule Module.Types.Descr do
             list_new(list_type, last_type)
 
           {bdd, last_type_no_list} ->
-            # The argument last_type may include list types; in this case, we aim to add
-            # those to the main list type, only to keep the type of the final element (which may
-            # be either the empty list, or some non-list value).
-            # To do so, we go through the list types in last_type, but since those are stored
-            # as a bdd of list types, we take care to include the effect of negations on computing
-            # each last type.
-            # To see if a negation changes the last type or the list type, we just need to check
-            # 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)
+            # `last_type` may itself represent one or more list types.
+            # Our goal is to fold those list types into `list_type` while retaining the
+            # possible type of the final element (which can be `[]` or any non-list value).
+            #
+            # The list types inside `last_type` are stored in a BDD that includes possible
+            # negations, so we must evaluate each node with its sign taken into account.
+            #
+            # A negation only matters when the negated list type is a supertype of the
+            # corresponding positive list type; in that case we subtract the negated
+            # variant from the positive one.
             {list_type, last_type} =
               list_get_pos(bdd)
               |> Enum.reduce({list_type, last_type_no_list}, fn {head, tail},
@@ -1965,24 +1906,6 @@ defmodule Module.Types.Descr do
                 {union(head, acc_head), union(tail, acc_tail)}
               end)
 
-            # So for instance if i give term() and `term() and not (list(term())`
-            # what happens?
-            # list_type starts with term() and does not change
-            # last_type starts with everything but :list and []
-            # then we iterate over the bdd, which contains... what? it contains
-            # {:term, :term} and not {:term, %{bitmap: 2}}
-            # what is bitmap: 2? it is empty_list()
-            # we only add the positive {:term, :term} to both things
-            # so we get {:term, :term} lol... that seems wrong, i should not add back the
-            # empty_list()
-            # maybe i should get tl on the bdd?
-
-            last_type =
-              case last_type do
-                :term -> @not_non_empty_list
-                other -> Map.delete(other, :list)
-              end
-
             list_new(list_type, last_type)
         end
       end
@@ -2011,7 +1934,7 @@ defmodule Module.Types.Descr do
         acc
 
       :bdd_top ->
-        [{pos, negs} | acc]
+        if list_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc]
 
       {{list, tail} = list_type, left, right} ->
         new_pos = {intersection(list_acc, list), intersection(tail_acc, tail)}
@@ -2135,18 +2058,14 @@ defmodule Module.Types.Descr do
   # 3. Base case: adds bdd2 type to negations of bdd1 type
   # The result may be larger than the initial bdd1, which is maintained in the accumulator.
   defp list_difference(list_literal(list1, last1) = bdd1, list_literal(list2, last2) = bdd2) do
-    cond do
-      empty?(intersection(list1, list2)) or empty?(intersection(last1, last2)) ->
-        list_literal(list1, last1)
-
-      subtype?(list1, list2) and subtype?(last1, last2) ->
-        :bdd_bot
-
-      equal?(list1, list2) ->
-        list_literal(list1, difference(last1, last2))
+    list = intersection(list1, list2)
+    last = intersection(last1, last2)
 
-      true ->
-        bdd_difference(bdd1, bdd2)
+    cond do
+      empty?(list) or empty?(last) -> list_literal(list1, last1)
+      subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot
+      equal?(list1, list2) -> list_literal(list1, difference(last1, last2))
+      true -> bdd_difference(bdd1, bdd2)
     end
   end
 
@@ -2159,9 +2078,9 @@ defmodule Module.Types.Descr do
   end
 
   defp list_empty?(@non_empty_list_top), do: false
-  defp list_empty?(bdd), do: list_all?(bdd, &list_empty_line?/3)
+  defp list_empty?(bdd), do: list_all?(bdd, &list_empty?/3)
 
-  defp list_empty_line?(list_type, last_type, negs) do
+  defp list_empty?(list_type, last_type, negs) do
     last_type = list_tail_unfold(last_type)
     # To make a list {list, last} empty with some negative lists:
     # 1. Ignore negative lists which do not have a list type that is a supertype of the positive one.
@@ -2172,12 +2091,7 @@ defmodule Module.Types.Descr do
       Enum.reduce_while(negs, last_type, fn {neg_type, neg_last}, acc_last_type ->
         if subtype?(list_type, neg_type) do
           d = difference(acc_last_type, neg_last)
-
-          if empty?(d) do
-            {:halt, nil}
-          else
-            {:cont, d}
-          end
+          if empty?(d), do: {:halt, nil}, else: {:cont, d}
         else
           {:cont, acc_last_type}
         end
@@ -2340,27 +2254,23 @@ defmodule Module.Types.Descr do
   defp list_normalize(bdd) do
     list_get(bdd)
     |> Enum.reduce([], fn {{list, last}, negs}, acc ->
-      if list_empty_line?(list, last, negs) do
-        acc
-      else
-        # First, try to eliminate the negations from the existing type.
-        {list, last, negs} =
-          Enum.uniq(negs)
-          |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} ->
-            last = list_tail_unfold(last)
-            new_list = intersection(list, nlist)
-            new_last = intersection(last, nlast)
-
-            cond do
-              # No intersection between the list and the negative
-              empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs}
-              subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs}
-              true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]}
-            end
-          end)
+      # First, try to eliminate the negations from the existing type.
+      {list, last, negs} =
+        Enum.uniq(negs)
+        |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} ->
+          last = list_tail_unfold(last)
+          new_list = intersection(list, nlist)
+          new_last = intersection(last, nlast)
 
-        add_to_list_normalize(acc, list, last, negs |> Enum.reverse())
-      end
+          cond do
+            # No intersection between the list and the negative
+            empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs}
+            subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs}
+            true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]}
+          end
+        end)
+
+      add_to_list_normalize(acc, list, last, negs |> Enum.reverse())
     end)
   end
 
@@ -2631,9 +2541,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp maybe_optimize_map_union(map1, map2),
-    do: raise("I should not be there: see inputs #{inspect(map1)} and #{inspect(map2)}")
-
   defp map_union_optimization_strategy(tag1, pos1, tag2, pos2)
   defp map_union_optimization_strategy(tag, pos, tag, pos), do: :all_equal
   defp map_union_optimization_strategy(:open, empty, _, _) when empty == %{}, do: :any_map
@@ -3103,7 +3010,6 @@ defmodule Module.Types.Descr do
     %{map: {{map_refresh_tag(tag, domain, type), fields}, :bdd_top, :bdd_bot}}
   end
 
-  # TODO: TEST THIS (previous implem was wrong)
   def map_refresh_domain(%{map: bdd}, domain, type) do
     # For negations, we count on the idea that a negation will not remove any
     # type from a domain unless it completely cancels out the type.
@@ -4073,7 +3979,7 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Build a disjoint disjunction for {t1,...,tn} ∧ not {u1,...,un}
+  # Build a disjoint disjunction for {t1,...,tn} /\ not {u1,...,un}
   # by splitting on the *earliest* index where they differ.
   #
   # Invariant:
@@ -4087,14 +3993,14 @@ defmodule Module.Types.Descr do
   #   - The other recursive path forces match here: intersection(ti, ui) and continues to i+1.
   #
   # This yields disjoint branches like:
-  #   {t1∧¬u1, t2, t3, ...} OR {t1∧u1, t2∧¬u2, t3, ...} OR {t1∧u1, t2∧u2, t3∧¬u3, ...} ...
+  #   {t1 /\ not u1, t2, t3, ...} OR {t1 /\ u1, t2 /\ not u2, t3, ...} OR {t1/\u1, t2/\u2, t3/\ not u3, ...} ...
   defp tuple_elim_content(acc, tag, elements, [neg_type | neg_elements]) do
     # If `elements` is shorter, default to top type `term()` (as in your example).
     {ty, rest} = List.pop_at(elements, 0, term())
 
-    # ti \ ui  (i.e., ti ∧ ¬ui)
+    # ti \ ui  (i.e., ti and not ui)
     diff = difference(ty, neg_type)
-    # ti ∧ ui
+    # ti /\ ui
     meet = intersection(ty, neg_type)
 
     # Branch where the earliest difference is *here*.
@@ -4119,7 +4025,7 @@ defmodule Module.Types.Descr do
   end
 
   # No more negative elements to process: there is no “all-equal” branch to add,
-  # because we’re constructing {t} ∧ ¬{u}, which must differ somewhere.
+  # because we’re constructing {t} ant not {u}, which must differ somewhere.
   defp tuple_elim_content(_acc, _tag, _elements, []) do
     []
   end
@@ -4637,48 +4543,23 @@ defmodule Module.Types.Descr do
   defp bdd_intersection({lit1, _, _} = bdd1, {lit2, l2, r2}) when lit1 > lit2,
     do: {lit2, bdd_intersection(bdd1, l2), bdd_intersection(bdd1, r2)}
 
-  defp bdd_difference(bdd1, bdd2) do
-    case {bdd1, bdd2} do
-      {:bdd_bot, _} ->
-        :bdd_bot
-
-      {other, :bdd_bot} ->
-        other
-
-      {:bdd_top, {lit, l, r}} ->
-        {lit, bdd_difference(:bdd_top, l), bdd_difference(:bdd_top, r)}
-
-      {_, :bdd_top} ->
-        :bdd_bot
-
-      {{lit, l1, r1}, {lit, l2, r2}} ->
-        {lit, bdd_difference(l1, l2), bdd_difference(r1, r2)}
-
-      {{lit1, l1, r1}, {lit2, _, _} = bdd2} when lit1 < lit2 ->
-        {lit1, bdd_difference(l1, bdd2), bdd_difference(r1, bdd2)}
-
-      {{lit1, _, _} = bdd1, {lit2, l2, r2}} when lit1 > lit2 ->
-        {lit2, bdd_difference(bdd1, l2), bdd_difference(bdd1, r2)}
-    end
-  end
-
-  # 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(: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({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, 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_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_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
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 6ace937319..26c9610736 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2033,19 +2033,26 @@ defmodule Module.Types.ExprTest do
     end
 
     # test "regressions – duplicate-key list pattern" do
-    #   assert typecheck!(
-    #            # HEAD PATTERN LIST
-    #            [
-    #              # first tuple
-    #              [
-    #                {key, _}
-    #                # second tuple + rest
-    #                | [{key, _} | _] = rest
-    #              ]
-    #            ],
-    #            # BODY – we just return the tail we captured
-    #            rest
-    #          ) ==
+    #   x =
+    #     typecheck!(
+    #       # HEAD PATTERN LIST
+    #       [
+    #         # first tuple
+    #         [
+    #           {key, _}
+    #           # second tuple + rest
+    #           | [{key, _} | _] = rest
+    #         ]
+    #       ],
+    #       # BODY – we just return the tail we captured
+    #       rest
+    #     )
+
+    #   IO.puts("x: #{to_quoted_string(x)}")
+    #   IO.puts("x: #{inspect(x)}")
+
+    #   assert x
+    #          |> equal?(
     #            dynamic(
     #              non_empty_list(
     #                # every element is {term, term}
@@ -2054,6 +2061,7 @@ defmodule Module.Types.ExprTest do
     #                term()
     #              )
     #            )
+    #          )
     # end
 
     test "typecheck! must finish fast for large pattern match" do

From ec5906ba8ccc0740ba548686b45b285e27bea511 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 4 Aug 2025 18:26:07 +0200
Subject: [PATCH 8/9]  Updated the handling of positive and negative functions
 in `fun_normalize` and `fun_get`

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

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 3e335b01e7..400d4cb72f 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -196,7 +196,6 @@ defmodule Module.Types.Descr do
   #     We emit `{common, union(return, acc_return)}` for the shared part,
   #     keep `{left, acc_return}` (if any), and continue inserting `diff`
   #     into the remainder of the list to handle further overlaps.
-
   defp pivot_overlapping_clause(domain, return, [{acc_domain, acc_return} | acc]) do
     common = intersection(domain, acc_domain)
 
@@ -1314,7 +1313,7 @@ defmodule Module.Types.Descr do
   defp fun_normalize(%{fun: bdd}, arity, mode) do
     {domain, arrows, bad_arities} =
       Enum.reduce(fun_get(bdd), {term(), [], []}, fn
-        {pos_funs, neg_funs}, {domain, arrows, bad_arities} ->
+        {pos_funs, _neg_funs}, {domain, arrows, bad_arities} ->
           arrow_arity =
             case pos_funs do
               [{args, _} | _] -> length(args)
@@ -1325,9 +1324,6 @@ defmodule Module.Types.Descr do
             arrow_arity != arity ->
               {domain, arrows, [arrow_arity | bad_arities]}
 
-            fun_empty?(pos_funs, neg_funs) ->
-              {domain, arrows, bad_arities}
-
             true ->
               # Calculate domain from all positive functions
               path_domain =
@@ -1363,13 +1359,13 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  defp apply_disjoint(arguments, arrows) do
-    type_args = args_to_domain(arguments)
+  # A fast way to do function application when the arguments of the function are disjoint.
+  # Just build the union of all the return types of arrows that match the input.
+  defp apply_disjoint(input_arguments, arrows) do
+    type_input = args_to_domain(input_arguments)
 
     Enum.reduce(arrows, none(), fn {args, ret}, acc_return ->
-      dom = args_to_domain(args)
-
-      if empty?(intersection(dom, type_args)) do
+      if empty?(intersection(args_to_domain(args), type_input)) do
         acc_return
       else
         union(acc_return, ret)
@@ -1399,6 +1395,9 @@ defmodule Module.Types.Descr do
     # Calculate the part of the input not covered by this arrow's domain
     dom_subtract = difference(input, args_to_domain(args))
 
+    # Refine the return type by intersecting with this arrow's return type
+    ret_refine = intersection(returns_reached, ret)
+
     # Phase 1: Domain partitioning
     # If the input is not fully covered by the arrow's domain, then the result type should be
     # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
@@ -1418,9 +1417,6 @@ defmodule Module.Types.Descr do
     # the same part of the input, then the result type is an intersection of the return types of
     # those arrows.
 
-    # Refine the return type by intersecting with this arrow's return type
-    ret_refine = intersection(returns_reached, ret)
-
     # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
     # should result in (atom() ∩ pid()), which is none().
     aux_apply(result, input, ret_refine, arrow_intersections)
@@ -1434,7 +1430,7 @@ defmodule Module.Types.Descr do
   defp fun_get(acc, pos, neg, bdd) do
     case bdd do
       :bdd_bot -> acc
-      :bdd_top -> [{pos, neg} | acc]
+      :bdd_top -> if fun_empty?(pos, neg), do: acc, else: [{pos, neg} | acc]
       {fun, left, right} -> fun_get(fun_get(acc, [fun | pos], neg, left), pos, [fun | neg], right)
     end
   end
@@ -1451,13 +1447,7 @@ defmodule Module.Types.Descr do
   # - `fun(1) and not fun(1)` is empty
   # - `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
-    case bdd do
-      :bdd_bot -> true
-      :bdd_top -> false
-      bdd -> fun_get(bdd) |> Enum.all?(fn {posits, negats} -> fun_empty?(posits, negats) end)
-    end
-  end
+  defp fun_empty?(bdd), do: fun_get(bdd) == []
 
   # Checks if a function type represented by positive and negative function literals is empty.
 
@@ -1660,6 +1650,8 @@ defmodule Module.Types.Descr do
     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
@@ -1817,7 +1809,7 @@ defmodule Module.Types.Descr do
   end
 
   defp fun_get_pos(bdd) do
-    for {pos, negs} <- fun_get(bdd), not fun_empty?(pos, negs) do
+    for {pos, _negs} <- fun_get(bdd) do
       fun_filter_subset(pos, [])
     end
   end

From f933a16843d932f61057f7975d04dacf949134ee Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 4 Aug 2025 18:38:38 +0200
Subject: [PATCH 9/9] Remove commented-out  test

---
 .../test/elixir/module/types/expr_test.exs    | 32 -------------------
 1 file changed, 32 deletions(-)

diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 26c9610736..7d19fbb73a 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -2032,38 +2032,6 @@ defmodule Module.Types.ExprTest do
              ) == dynamic(integer())
     end
 
-    # test "regressions – duplicate-key list pattern" do
-    #   x =
-    #     typecheck!(
-    #       # HEAD PATTERN LIST
-    #       [
-    #         # first tuple
-    #         [
-    #           {key, _}
-    #           # second tuple + rest
-    #           | [{key, _} | _] = rest
-    #         ]
-    #       ],
-    #       # BODY – we just return the tail we captured
-    #       rest
-    #     )
-
-    #   IO.puts("x: #{to_quoted_string(x)}")
-    #   IO.puts("x: #{inspect(x)}")
-
-    #   assert x
-    #          |> equal?(
-    #            dynamic(
-    #              non_empty_list(
-    #                # every element is {term, term}
-    #                tuple([term(), term()]),
-    #                # the tail can be anything
-    #                term()
-    #              )
-    #            )
-    #          )
-    # end
-
     test "typecheck! must finish fast for large pattern match" do
       type =
         typecheck!(fn