Tentative fix for invalid rewrite of negated BDD in map_update_put_domains

lib/elixir/lib/module/types/descr.ex

@@ -3784,14 +3784,59 @@ defmodule Module.Types.Descr do
   defp map_update_put_domains(bdd, [], _type_fun, _force?), do: %{map: bdd}
 
   defp map_update_put_domains(bdd, domain_keys, type_fun, force?) do
+    put = fn tag -> map_update_put_domain(tag, domain_keys, type_fun, force?) end
+
     bdd =
-      bdd_map(bdd, fn bdd_leaf(tag, fields) ->
-        bdd_leaf_new(map_update_put_domain(tag, domain_keys, type_fun, force?), fields)
-      end)
+      cond do
+        # A pure disjunction of leaves: the domain-put distributes over the
+        # union, so we can rewrite each leaf in place (and keep the structure
+        # that callers may assert on).
+        map_bdd_positive?(bdd) ->
+          bdd_map(bdd, fn bdd_leaf(tag, fields) -> bdd_leaf_new(put.(tag), fields) end)
+
+        # A non-forced put only changes a leaf that already carries one of the put
+        # domains. When none do, the put is a genuine no-op, so the type
+        # (negations included) is returned unchanged. Unlike a tag-equality check
+        # this is sound: a leaf that *does* carry the domain may broaden to the
+        # same tag yet still move maps across a negation boundary.
+        not force? and not map_bdd_has_domain?(bdd, domain_keys) ->
+          bdd
+
+        # Otherwise the bdd has negated leaves. `bdd_map` would rewrite a negated
+        # leaf, turning `not N` into `not put(N)`, which enlarges the negated set
+        # and wrongly excludes maps the put can actually produce. Over-approximate
+        # soundly instead: the image of `A \ B` is contained in the image of `A`,
+        # so we apply the put to the positive part of each non-empty DNF line and
+        # drop the negations. Empty lines are dropped by
+        # `map_bdd_to_dnf_remove_empty`.
+        true ->
+          bdd
+          |> map_bdd_to_dnf_remove_empty()
+          |> Enum.reduce(:bdd_bot, fn {tag, fields, _negs}, acc ->
+            map_union(bdd_leaf_new(put.(tag), fields), acc)
+          end)
+      end
 
     %{map: bdd}
   end
 
+  # `bdd_map` rewrites a domain-put exactly only on a pure positive disjunction
+  # of leaves (every node keeps its literal on the constrained-top branch with no
+  # dual branch), where the rewrite distributes over the union. Any dual (negated)
+  # branch means a leaf appears negated, where the rewrite is not sound.
+  defp map_bdd_positive?(:bdd_bot), do: true
+  defp map_bdd_positive?(:bdd_top), do: true
+  defp map_bdd_positive?(bdd_leaf(_, _)), do: true
+  defp map_bdd_positive?({_, _lit, :bdd_top, u, :bdd_bot}), do: map_bdd_positive?(u)
+  defp map_bdd_positive?({_, _, _, _, _}), do: false
+
+  # True when some leaf of the bdd carries one of the given domain keys.
+  defp map_bdd_has_domain?(bdd, domain_keys) do
+    bdd_reduce(bdd, false, fn bdd_leaf(tag, _fields), acc ->
+      acc or (is_list(tag) and Enum.any?(domain_keys, &(fields_find(&1, tag) != :error)))
+    end)
+  end
+
   defp map_update_put_domain(tag_or_domains, domain_keys, type_fun, force?) do
     case tag_or_domains do
       :open ->

lib/elixir/test/elixir/module/types/descr_test.exs

@@ -2741,6 +2741,40 @@ defmodule Module.Types.DescrTest do
                {open_map(), open_map(k: binary(), x: term()), []}
     end
 
+    test "domain put on a negated map does not exclude achievable values" do
+      # Putting a domain key must not rewrite negated leaves: `not N` -> `not put(N)`
+      # would enlarge the negation and drop maps the put can produce. The result
+      # must stay disjoint from nothing it can reach, i.e. (X \ Y) and Y disjoint,
+      # and a <= c => (a \ b) \ c is empty.
+
+      # (a) negated closed leaf: %{a: :x} is Map.put(%{a: term()}, :a, :x), in `d`.
+      d = opt_difference(open_map(), empty_map())
+      {:ok, res} = map_put(d, atom(), atom([:x]))
+      assert subtype?(closed_map(a: atom([:x])), res)
+
+      # (b) negated domains-list leaf: %{1 => :y} is Map.put(%{1 => :z}, 1, :y).
+      d2 =
+        opt_difference(
+          open_map([{domain_key(:integer), atom()}]),
+          closed_map([{domain_key(:integer), atom([:y])}])
+        )
+
+      {:ok, res2} = map_put(d2, integer(), atom([:y]))
+      x = opt_difference(closed_map([{domain_key(:integer), atom([:y])}]), empty_map())
+      refute empty?(opt_intersection(x, res2))
+
+      # via map_update/5 (the call Map.put uses) and the dynamic paths
+      {_, resu, _} = map_update(d, atom(), atom([:x]), false, true)
+      assert subtype?(closed_map(a: atom([:x])), resu)
+      {:ok, resd} = map_put(dynamic(d), atom(), atom([:x]))
+      assert subtype?(dynamic(closed_map(a: atom([:x]))), resd)
+      {_, resud, _} = map_update(dynamic(d), atom(), atom([:x]), false, true)
+      assert subtype?(dynamic(closed_map(a: atom([:x]))), resud)
+
+      # A non-forced put whose domain is absent stays an exact no-op.
+      assert map_update(d, binary(), integer(), false, false) == {none(), d, []}
+    end
+
     test "with non-empty open maps does not call the callback with none from absent branches" do
       # This is a test of the map_update_fun/5 with forced?: false parameter.
       # We check that it does not call its typed_fun argument with `none()`