From 8bbf824c58603dbe34fe85c3cf1c86c8299490a7 Mon Sep 17 00:00:00 2001
From: Lukasz Samson <lukaszsamson@gmail.com>
Date: Tue, 23 Jun 2026 09:53:10 +0200
Subject: [PATCH] Split tuple_insert_static into two paths

- bdd_map on pure positive disjunction
- expand to the exact negation-free positive DNF, insert and union on negations and/or implicit :bdd_top

Fixes #15517
---
 lib/elixir/lib/module/types/descr.ex          | 56 ++++++++++++++-----
 .../test/elixir/module/types/descr_test.exs   | 12 ++++
 2 files changed, 54 insertions(+), 14 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 8198124a56..37bda5e8bb 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -5317,23 +5317,51 @@ defmodule Module.Types.Descr do
 
   defp tuple_insert_static(descr, index, type) do
     Map.update!(descr, :tuple, fn bdd ->
-      bdd_map(bdd, fn bdd_leaf(tag, elements) ->
-        # 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`).
-        elements =
-          if tag == :open and length(elements) < index do
-            tuple_fill(elements, index)
-          else
-            elements
-          end
-
-        bdd_leaf_new(tag, List.insert_at(elements, index, type))
-      end)
+      if tuple_bdd_positive?(bdd) do
+        # A pure disjunction of leaves: the insert distributes over the union, so
+        # we rewrite each leaf in place (preserving the structure callers assert on).
+        bdd_map(bdd, fn bdd_leaf(tag, elements) ->
+          tuple_insert_leaf(tag, elements, index, type)
+        end)
+      else
+        # The bdd carries negations and/or implicit `:bdd_top` positive paths
+        # (e.g. from `tuple_difference(open_tuple([]), _) -> bdd_negation`).
+        # `bdd_map` rewrites only explicit leaves, so it would skip the implicit
+        # top (losing the insert) and wrongly transform negated leaves. Expand to
+        # the exact negation-free positive DNF first, then insert into each leaf.
+        bdd
+        |> tuple_bdd_to_dnf_no_negations()
+        |> Enum.reduce(:bdd_bot, fn {tag, elements}, acc ->
+          tuple_union(tuple_insert_leaf(tag, elements, index, type), acc)
+        end)
+      end
     end)
   end
 
+  # Inserts `type` at `index` into a single tuple literal. If the tuple is open,
+  # `List.insert_at` needs the tuple filled with `term()` up to `index` first.
+  # Closed tuples of an incorrect size are cancelled before reaching here (the
+  # input is intersected/guarded with `tuple_of_size_at_least`).
+  defp tuple_insert_leaf(tag, elements, index, type) do
+    elements =
+      if tag == :open and length(elements) < index do
+        tuple_fill(elements, index)
+      else
+        elements
+      end
+
+    bdd_leaf_new(tag, List.insert_at(elements, index, type))
+  end
+
+  # `bdd_map` rewrites a tuple insert exactly only on a pure positive disjunction
+  # of leaves (every node keeps its literal on the constrained-top branch with no
+  # dual branch). Any dual branch (or implicit `:bdd_top` in negated position)
+  # would be transformed incorrectly or skipped.
+  defp tuple_bdd_positive?(:bdd_bot), do: true
+  defp tuple_bdd_positive?(bdd_leaf(_, _)), do: true
+  defp tuple_bdd_positive?({_, _lit, :bdd_top, u, :bdd_bot}), do: tuple_bdd_positive?(u)
+  defp tuple_bdd_positive?(_), do: false
+
   @doc """
   Replace an element in the tuple at the given (0-based) index.
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index ce65063fbb..6eee49062c 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -2035,6 +2035,18 @@ defmodule Module.Types.DescrTest do
              |> tuple_insert_at(1, float())
              |> equal?(tuple([integer(), float(), atom(), boolean()]))
 
+      # Inserting must be a congruence wrt equal?, even when the positive side is
+      # the implicit top (a negation with :bdd_top branches) rather than an
+      # explicit open leaf. Here t2 == open_tuple([term(), term()]).
+      t2 = opt_difference(open_tuple([]), opt_union(tuple([]), tuple([term()])))
+      assert equal?(t2, open_tuple([term(), term()]))
+
+      assert tuple_insert_at(t2, 2, float())
+             |> equal?(tuple_insert_at(open_tuple([term(), term()]), 2, float()))
+
+      # The inserted index is actually constrained to float().
+      refute subtype?(tuple([integer(), integer(), atom()]), tuple_insert_at(t2, 2, float()))
+
       # Test inserting into a complex union involving dynamic
       assert opt_union(tuple([integer(), atom()]), dynamic(tuple([float(), binary()])))
              |> tuple_insert_at(1, boolean())