From b0126fbb83606bf2dde417e68a1c0f58b12105d6 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 01:05:46 +0200 Subject: [PATCH 1/7] Fix tuple_insert_at bug. --- lib/elixir/lib/module/types/descr.ex | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index fb130f9dd6..c343caf22c 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -5749,6 +5749,17 @@ defmodule Module.Types.Descr do defp tuple_insert_static(descr, index, type) do Map.update!(descr, :tuple, fn bdd -> bdd_map(bdd, fn {tag, elements} -> + # Iff the tuple is open, then we want List.insert_at to put the new element at the correct + # index, which requires filling the tuple with `term()` values first. + # Closed tuples of an incorrect size will be ignored (they are cancelled by the earlier + # intersection with `tuple_of_size_at_least`). + elements = + if tag == :open and length(elements) < index do + tuple_fill(elements, index) + else + elements + end + {tag, List.insert_at(elements, index, type)} end) end) From 2e4b5da13aae7c18c8751ee5be018ff33b33b30e Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 01:15:34 +0200 Subject: [PATCH 2/7] Much improved bdd_negation op. --- lib/elixir/lib/module/types/descr.ex | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index c343caf22c..30317a2365 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -6196,7 +6196,18 @@ defmodule Module.Types.Descr do def bdd_negation({_, _} = pair), do: {pair, :bdd_bot, :bdd_bot, :bdd_top} def bdd_negation({lit, c, u, d}) do - {lit, bdd_negation(bdd_union(c, u)), :bdd_bot, bdd_negation(bdd_union(d, u))} + inner = + {lit, bdd_negation(c), :bdd_bot, bdd_negation(d)} + + case u do + :bdd_bot -> inner + _ -> bdd_intersection(inner, bdd_negation(u)) + end + |> case do + # Full simplification necessary for e.g. formatter.ex compilation + {lit, c, u, c} -> bdd_union(u, c) + x -> x + end end def bdd_to_dnf(bdd), do: bdd_to_dnf([], [], [], bdd) From 8ce5957909a26ea53807be511ae93dc637d258b5 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 01:16:00 +0200 Subject: [PATCH 3/7] Add comment --- lib/elixir/lib/module/types/descr.ex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 30317a2365..d7658d094a 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -6190,7 +6190,8 @@ defmodule Module.Types.Descr do end end - # Lazy negation: eliminate the union, then perform normal negation (switching leaves) + # {lit, c, u, d} = (lit and c) or u or (not lit and d), so + # its negation is ((lit and not c) or (not lit and not d)) and not u. def bdd_negation(:bdd_top), do: :bdd_bot def bdd_negation(:bdd_bot), do: :bdd_top def bdd_negation({_, _} = pair), do: {pair, :bdd_bot, :bdd_bot, :bdd_top} From 37192d015b30181a10d562567ebe6e8c1a149aa3 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 14:04:13 +0200 Subject: [PATCH 4/7] Add bdd_negation_union to avoid union blow-up (fixes macro.ex 4s slowdown) --- lib/elixir/lib/module/types/descr.ex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index d7658d094a..bd81abb206 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -5879,7 +5879,7 @@ defmodule Module.Types.Descr do end {:eq, _, {lit, c2, u2, _d2}} -> - {lit, bdd_negation(bdd_union(c2, u2)), :bdd_bot, :bdd_bot} + {lit, bdd_negation_union(c2, u2), :bdd_bot, :bdd_bot} {:eq, {lit, _c1, u1, d1}, _} -> {lit, :bdd_bot, :bdd_bot, bdd_union(d1, u1)} @@ -5901,6 +5901,10 @@ defmodule Module.Types.Descr do defp bdd_difference_union(i, u1, u2), do: bdd_difference(i, bdd_union(u1, u2)) + defp bdd_negation_union(u1, u2) do + bdd_intersection(bdd_negation(u1), bdd_negation(u2)) + end + ## Optimize differences defp bdd_difference(bdd_leaf(_, _) = a1, bdd_leaf(_, _) = a2, leaf_compare) do From 201f3eff30eb635e2c30627a68309c247561d364 Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 14:04:47 +0200 Subject: [PATCH 5/7] Fix warning --- lib/elixir/lib/module/types/descr.ex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index bd81abb206..667f72c00d 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -6210,7 +6210,7 @@ defmodule Module.Types.Descr do end |> case do # Full simplification necessary for e.g. formatter.ex compilation - {lit, c, u, c} -> bdd_union(u, c) + {_lit, c, u, c} -> bdd_union(u, c) x -> x end end From 59dfd3d7a291219589752a5ed2950c4e8d2457dc Mon Sep 17 00:00:00 2001 From: Guillaume Duboc Date: Fri, 17 Apr 2026 16:35:40 +0200 Subject: [PATCH 6/7] Fix typo in comment for tuple_insert_static function --- lib/elixir/lib/module/types/descr.ex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 667f72c00d..0886f93c48 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -5749,7 +5749,7 @@ defmodule Module.Types.Descr do defp tuple_insert_static(descr, index, type) do Map.update!(descr, :tuple, fn bdd -> bdd_map(bdd, fn {tag, elements} -> - # Iff the tuple is open, then we want List.insert_at to put the new element at the correct + # If the tuple is open, then we want List.insert_at to put the new element at the correct # index, which requires filling the tuple with `term()` values first. # Closed tuples of an incorrect size will be ignored (they are cancelled by the earlier # intersection with `tuple_of_size_at_least`). From e2ecdb78ff2dc3c79098b439b513b7b0c3945753 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Fri, 17 Apr 2026 17:24:12 +0200 Subject: [PATCH 7/7] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: José Valim --- lib/elixir/lib/module/types/descr.ex | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex index 0886f93c48..0cead28194 100644 --- a/lib/elixir/lib/module/types/descr.ex +++ b/lib/elixir/lib/module/types/descr.ex @@ -5901,6 +5901,8 @@ defmodule Module.Types.Descr do defp bdd_difference_union(i, u1, u2), do: bdd_difference(i, bdd_union(u1, u2)) + # We avoid unions because they are lazy and we prune + # intersections more actively. defp bdd_negation_union(u1, u2) do bdd_intersection(bdd_negation(u1), bdd_negation(u2)) end @@ -6204,11 +6206,7 @@ defmodule Module.Types.Descr do inner = {lit, bdd_negation(c), :bdd_bot, bdd_negation(d)} - case u do - :bdd_bot -> inner - _ -> bdd_intersection(inner, bdd_negation(u)) - end - |> case do + case bdd_intersection(inner, bdd_negation(u)) do # Full simplification necessary for e.g. formatter.ex compilation {_lit, c, u, c} -> bdd_union(u, c) x -> x