diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index 9755a6fbae..66505570e1 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -1290,7 +1290,7 @@ defmodule Module.Types.Apply do
         _ -> args_types
       end
 
-    case map_update(map, key, none(), true, true, false) do
+    case map_update(map, key, none(), true, true, false, :keep) do
       {value, descr, _errors} ->
         value = opt_union(value, default)
         {:ok, return(tuple([value, descr]), args_types, stack)}
@@ -1306,7 +1306,7 @@ defmodule Module.Types.Apply do
   defp remote_apply(Map, :pop_lazy, _info, [map, key, fun] = args_types, stack) do
     case fun_apply(fun, []) do
       {:ok, default} ->
-        case map_update(map, key, none(), true, true, false) do
+        case map_update(map, key, none(), true, true, false, :keep) do
           {value, descr, _errors} ->
             value = opt_union(value, default)
             {:ok, return(tuple([value, descr]), args_types, stack)}
@@ -1340,9 +1340,7 @@ defmodule Module.Types.Apply do
   end
 
   defp remote_apply(Map, :replace, _info, [map, key, value] = args_types, stack) do
-    fun = fn _value, optional? -> {value, optional?} end
-
-    case map_update_fun(map, key, fun, false, false) do
+    case map_update(map, key, upper_bound(value), false, false, false, :keep) do
       {_value, descr, _errors} -> {:ok, return(descr, args_types, stack)}
       :badmap -> {:error, badremote(Map, :replace, args_types)}
       {:error, _errors} -> {:error, {:badkeydomain, map, key, "do nothing"}}
@@ -1350,9 +1348,7 @@ defmodule Module.Types.Apply do
   end
 
   defp remote_apply(Map, :replace!, _info, [map, key, value] = args_types, stack) do
-    fun = fn _value, optional? -> {value, optional?} end
-
-    case map_update_fun(map, key, fun, false, false) do
+    case map_update(map, key, upper_bound(value), false, false) do
       {_value, descr, _errors} -> {:ok, return(descr, args_types, stack)}
       :badmap -> {:error, badremote(Map, :replace!, args_types)}
       {:error, _errors} -> {:error, {:badkeydomain, map, key, "raise"}}
@@ -1377,18 +1373,20 @@ defmodule Module.Types.Apply do
           _ -> map
         end
 
+      # `fun` is the inferred function type; this adapter computes its return type.
       fun_apply = fn arg_type, optional? ->
         if empty?(arg_type) do
           {default, false}
         else
-          case fun_apply(fun, [arg_type]) do
-            {:ok, res} -> {if(optional?, do: opt_union(res, default), else: res), false}
+          case fun_apply_or_none(fun, [arg_type]) do
+            {:ok, res, _status} -> {if(optional?, do: opt_union(res, default), else: res), false}
             reason -> throw({:badapply, reason, [arg_type]})
           end
         end
       end
 
-      map_update_fun(map, key, fun_apply, false, true)
+      map_update_fun(map, key, fun_apply, true, true)
+      |> map_update_check_callback(fun, gradual?(map))
     catch
       {:badapply, reason, args_types} ->
         {:error, {:badapply, fun, args_types, reason}}
@@ -1509,9 +1507,7 @@ defmodule Module.Types.Apply do
   end
 
   defp remote_apply(:maps, :update, _info, [key, value, map] = args_types, stack) do
-    fun = fn _value, optional? -> {value, optional?} end
-
-    case map_update_fun(map, key, fun, false, false) do
+    case map_update(map, key, upper_bound(value), false, false) do
       {_value, descr, _errors} -> {:ok, return(descr, args_types, stack)}
       :badmap -> {:error, badremote(:maps, :update, args_types)}
       {:error, _errors} -> {:error, {:badkeydomain, map, key, "raise"}}
@@ -1894,15 +1890,22 @@ defmodule Module.Types.Apply do
   ## Map helpers
 
   defp map_put_new(map, key, value, name, args_types, stack) do
-    fun = fn
-      type, true -> {opt_union(type, value), false}
-      type, false -> {if(empty?(type), do: value, else: type), false}
-    end
+    # No update is needed when every possible key is already required.
+    with {:finite, [_ | _] = keys} <- atom_fetch(upper_bound(key)),
+         true <- Enum.all?(keys, &match?({false, _}, map_fetch_key(map, &1))) do
+      {:ok, return(map, args_types, stack)}
+    else
+      _ ->
+        fun = fn
+          type, true -> {opt_union(type, value), false}
+          type, false -> {if(empty?(type), do: value, else: type), false}
+        end
 
-    case map_update_fun(map, key, fun, false, true) do
-      {_value, descr, _errors} -> {:ok, return(descr, args_types, stack)}
-      :badmap -> {:error, badremote(Map, name, args_types)}
-      {:error, _errors} -> {:ok, map}
+        case map_update_fun(map, key, fun, false, true) do
+          {_value, descr, _errors} -> {:ok, return(descr, args_types, stack)}
+          :badmap -> {:error, badremote(Map, name, args_types)}
+          {:error, _errors} -> {:ok, map}
+        end
     end
   end
 
@@ -1914,14 +1917,18 @@ defmodule Module.Types.Apply do
           _ -> map
         end
 
+      # Apply the inferred function type to each old field type, without executing it.
       fun_apply = fn arg_type, optional? ->
-        case fun_apply(fun, [arg_type]) do
-          {:ok, res} -> {res, optional?}
+        case fun_apply_or_none(fun, [arg_type]) do
+          {:ok, res, _status} -> {res, optional?}
           reason -> throw({:badapply, reason, [arg_type]})
         end
       end
 
-      map_update_fun(map, key, fun_apply, false, false)
+      on_missing = if name == :replace_lazy, do: :keep, else: :reject
+
+      map_update_fun(map, key, fun_apply, true, false, on_missing)
+      |> map_update_check_callback(fun, gradual?(map))
     catch
       {:badapply, reason, args_types} ->
         {:error, {:badapply, fun, args_types, reason}}
@@ -1934,6 +1941,23 @@ defmodule Module.Types.Apply do
 
   ## Application helpers
 
+  # Check all old values together: a single unmatched fragment must not reject the update.
+  defp map_update_check_callback({old_values, _descr, _errors} = result, fun, gradual?) do
+    unless empty?(old_values) do
+      arguments = [if(gradual?, do: dynamic(old_values), else: old_values)]
+
+      case fun_apply_or_none(fun, arguments) do
+        {:ok, _result, :ok} -> :ok
+        {:ok, _result, reason} -> throw({:badapply, reason, arguments})
+        reason -> throw({:badapply, reason, arguments})
+      end
+    end
+
+    result
+  end
+
+  defp map_update_check_callback(result, _fun, _gradual?), do: result
+
   defp domain(nil, [{domain, _}]), do: domain
   defp domain(domain, _clauses), do: domain
 
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e0f4174161..8e0a1f6653 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -47,10 +47,10 @@ defmodule Module.Types.Descr do
   # Remark: those are explicit BDD constructors. The functional constructors are `bdd_new/1` and `bdd_new/3`.
   @fun_top {:negation, %{}}
   @atom_top {:negation, :sets.new(version: 2)}
-  @map_top {:erlang.phash2([:open | @fields_new]), :open, @fields_new}
+  @map_top {2 * :erlang.phash2([:open | @fields_new]), :open, @fields_new}
   @non_empty_list_top {:erlang.phash2([:term | :term]), :term, :term}
   @tuple_top {:erlang.phash2([:open | []]), :open, []}
-  @map_empty {-:erlang.phash2(@fields_new), :closed, @fields_new}
+  @map_empty {-2 * :erlang.phash2(@fields_new), :closed, @fields_new}
 
   defmacrop bdd_leaf(arg1, arg2) do
     quote do
@@ -572,7 +572,7 @@ defmodule Module.Types.Descr do
 
   defp numberize(:map, bdd) do
     bdd_map(bdd, fn bdd_leaf(tag, fields) ->
-      bdd_leaf_new(
+      map_new(
         tag,
         fields_map(fn _key, {value, optional?} -> {numberize(value), optional?} end, fields)
       )
@@ -1403,6 +1403,41 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # Variant of fun_apply for map callbacks: incompatible fields contribute none().
+  def fun_apply_or_none(:term, [_argument]), do: :badfun
+
+  def fun_apply_or_none(fun, [argument]) do
+    {fun_dynamic, fun_static} =
+      case :maps.take(:dynamic, fun) do
+        :error -> {nil, fun}
+        pair -> pair
+      end
+
+    fun_static = if empty?(fun_static), do: none(), else: fun_static
+    fun = if fun_dynamic, do: Map.put(fun_static, :dynamic, fun_dynamic), else: fun_static
+
+    with true <- fun_only?(fun_static) or :badfun,
+         {:ok, domain, static_arrows, dynamic_arrows} <-
+           fun_normalize_both(fun_static, fun_dynamic, 1) do
+      # Match fields against the callback's known input domain.
+      # For a gradual callback, discard the dynamic() fallback that would accept any input.
+      domain =
+        if static_arrows == [] and
+             Enum.any?(dynamic_arrows, &(not empty?(fetch_domain(&1)))),
+           do: lower_bound(domain),
+           else: upper_bound(domain)
+
+      [domain] = if domain == :term, do: [term()], else: domain_to_flat_args(domain, 1)
+      matching = bare_intersection(upper_bound(argument), domain)
+
+      if empty?(matching) do
+        {:ok, none(), {:badarg, [domain], empty?(argument)}}
+      else
+        with {:ok, result} <- fun_apply(fun, [matching]), do: {:ok, result, :ok}
+      end
+    end
+  end
+
   defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
   defp dynamic_fun_top?(:term), do: true
   defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
@@ -2914,17 +2949,105 @@ defmodule Module.Types.Descr do
     fields_get(domain, key, none())
   end
 
-  defp map_new(tag, fields), do: bdd_leaf_new(tag, fields)
+  # Map leaf ids reserve their lowest bit for a conservative
+  # emptiness cache: 0 is non-empty and 1 is unknown. Definitely empty
+  # literals are normalized to :bdd_bot.
+  # This allows cheap `map_leaf_empty?` checks.
+  defp map_new(tag, fields) do
+    case Enum.reduce_while(fields, 0, fn
+           {_key, {_type, true}}, state ->
+             {:cont, state}
+
+           {_key, {type, false}}, state ->
+             case descr_emptiness(type) do
+               :empty -> {:halt, :empty}
+               :non_empty -> {:cont, state}
+               :unknown -> {:cont, 1}
+             end
+         end) do
+      :empty ->
+        :bdd_bot
+
+      state ->
+        {id, _, _} = leaf = bdd_leaf_new(tag, fields)
+        put_elem(leaf, 0, id * 2 + state)
+    end
+  end
+
+  defp descr_emptiness(:term), do: :non_empty
 
-  defp map_only?(descr), do: empty?(Map.delete(descr, :map))
+  defp descr_emptiness(descr) when is_map(descr) do
+    Enum.reduce_while(descr, :empty, fn {component, value}, acc ->
+      case component_emptiness(component, value) do
+        :non_empty -> {:halt, :non_empty}
+        :unknown -> {:cont, :unknown}
+        :empty -> {:cont, acc}
+      end
+    end)
+  end
 
-  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, %{})
+  defp descr_emptiness(_descr), do: :unknown
+
+  defp component_emptiness(:bitmap, bitmap) when bitmap != 0,
+    do: :non_empty
+
+  defp component_emptiness(:atom, {atom_type, atom_set}) do
+    if atom_type == :negation or not :sets.is_empty(atom_set) do
+      :non_empty
+    else
+      :unknown
+    end
+  end
+
+  defp component_emptiness(:tuple, {id, tag, elements})
+       when is_integer(id) and tag in [:open, :closed] do
+    Enum.reduce_while(elements, :non_empty, fn element, _acc ->
+      case descr_emptiness(element) do
+        :non_empty -> {:cont, :non_empty}
+        state -> {:halt, state}
+      end
+    end)
+  end
+
+  defp component_emptiness(:list, {id, head, tail}) when is_integer(id) do
+    case {descr_emptiness(head), descr_emptiness(tail)} do
+      {:empty, _} -> :empty
+      {_, :empty} -> :empty
+      {:non_empty, :non_empty} -> :non_empty
+      _ -> :unknown
+    end
+  end
+
+  defp component_emptiness(:fun, {:negation, _}), do: :non_empty
+
+  defp component_emptiness(:fun, {:union, arities}) do
+    if Enum.any?(Map.values(arities), &match?(bdd_leaf(_, _), &1)) do
+      :non_empty
+    else
+      :unknown
+    end
+  end
+
+  defp component_emptiness(:map, :bdd_bot), do: :empty
+
+  defp component_emptiness(:map, {id, _tag, _fields}) do
+    case id &&& 1 do
+      0 -> :non_empty
+      _ -> :unknown
+    end
+  end
+
+  defp component_emptiness(_component, _value), do: :unknown
+
+  defp map_leaf_empty?({id, tag, fields}) do
+    case id &&& 1 do
+      0 -> false
+      _ -> init_map_line_empty?(tag, fields, [])
     end
   end
 
+  defp map_only?(descr), do: empty?(Map.delete(descr, :map))
+
   defp map_union(bdd_leaf(:open, []) = leaf, _), do: leaf
   defp map_union(_, bdd_leaf(:open, []) = leaf), do: leaf
   defp map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
@@ -3196,22 +3319,22 @@ defmodule Module.Types.Descr do
   def map_fetch_key(%{} = descr, key) when is_atom(key) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        if descr_key?(descr, :map) and non_empty_map_only?(descr) do
-          {static_type, static_optional?} = map_fetch_key_static(descr, key)
-
+        with true <- descr_key?(descr, :map) and map_only?(descr),
+             {static_type, static_optional?} <- map_fetch_key_static(descr, key, true) do
           if static_optional? or empty?(static_type) do
             :badkey
           else
             {false, static_type}
           end
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
 
       {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
-          {dynamic_type, dynamic_optional?} = map_fetch_key_static(dynamic, key)
-          {static_type, static_optional?} = map_fetch_key_static(static, key)
+        with true <- descr_key?(dynamic, :map) and map_only?(static),
+             {dynamic_type, dynamic_optional?} <- map_fetch_key_static(dynamic, key, true) do
+          {static_type, static_optional?} = map_fetch_key_static(static, key, false)
 
           if static_optional? or empty?(dynamic_type) do
             :badkey
@@ -3219,37 +3342,55 @@ defmodule Module.Types.Descr do
             {dynamic_optional?, opt_union(dynamic(dynamic_type), static_type)}
           end
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
     end
   end
 
   # Optimization for bdd leafs
-  defp map_fetch_key_static(%{map: bdd_leaf(tag, fields)}, key) do
-    case fields_find(key, fields) do
-      {:ok, field} -> field
-      :error -> map_key_tag_to_field(tag)
+  defp map_fetch_key_static(%{map: bdd_leaf(tag, fields) = leaf}, key, badmap_when_empty?) do
+    if map_leaf_empty?(leaf) do
+      if badmap_when_empty?, do: :badmap, else: {none(), false}
+    else
+      case fields_find(key, fields) do
+        {:ok, field} -> field
+        :error -> map_key_tag_to_field(tag)
+      end
     end
   end
 
-  defp map_fetch_key_static(%{map: bdd}, key) do
-    bdd |> map_bdd_to_dnf_with_empty() |> map_dnf_fetch_static(key)
+  defp map_fetch_key_static(%{map: bdd}, key, badmap_when_empty?) do
+    case map_bdd_to_dnf_remove_empty(bdd) do
+      [] -> if badmap_when_empty?, do: :badmap, else: {none(), false}
+      dnf -> map_dnf_fetch_static(dnf, key)
+    end
   end
 
-  defp map_fetch_key_static(%{}, _key), do: {none(), false}
-  defp map_fetch_key_static(:term, _key), do: {term(), true}
+  defp map_fetch_key_static(%{}, _key, _badmap_when_empty?), do: {none(), false}
+  defp map_fetch_key_static(:term, _key, _badmap_when_empty?), do: {term(), true}
 
-  # Takes a map DNF and returns the union of present-value types a key can take
-  # and whether the key is optional.
+  # Takes a map DNF with non-empty lines and returns the union of
+  # present-value types a key can take and whether the key is optional.
   defp map_dnf_fetch_static(dnf, key) do
-    Enum.reduce(dnf, {none(), false}, fn
-      {tag, fields, negs}, acc ->
-        {field, bdd} = map_pop_key_bdd(tag, fields, key)
-
-        # First: if a map has a none() field, then fetching from it is none() too
-        # Then: if there is a negative open_map(), map type is empty
-        with false <- map_empty?(bdd, %{}),
-             negative when negative != :empty <- map_split_negative_pairs_key(negs, key) do
+    Enum.reduce(dnf, {none(), false}, fn {tag, fields, negs}, acc ->
+      case map_split_key_line(tag, fields, negs, key, acc) do
+        {acc, _field, _bdd, _negative} -> acc
+        :empty -> acc
+      end
+    end)
+  end
+
+  # Add the possible old field to acc, and keep the split for updating the map.
+  defp map_split_key_line(tag, fields, negs, key, acc) do
+    {field, bdd} = map_pop_key_bdd(tag, fields, key)
+
+    case map_split_negative_pairs_key(negs, key) do
+      :empty ->
+        :empty
+
+      negative ->
+        acc =
           if map_pair_projection_keeps_full_fst?(negative, bdd) do
             field_opt_union(field, acc, %{})
           else
@@ -3259,10 +3400,9 @@ defmodule Module.Types.Descr do
               field_opt_union(field, acc, %{})
             end)
           end
-        else
-          _ -> acc
-        end
-    end)
+
+        {acc, field, bdd, negative}
+    end
   end
 
   defp map_split_negative_pairs_key(negs, key) do
@@ -3473,43 +3613,52 @@ defmodule Module.Types.Descr do
   The `return_type?` flag is used for optimizations purposes. If set to false,
   the returned `type` should not be used, as it will be imprecise.
 
+  With the default `on_missing` policy:
   If `force?` is false, the key is expected to exist. When true, it forces
   the key into existence.
+
+  `on_missing` says what to do when the key is absent: `:apply` applies the update,
+  `:keep` leaves the map unchanged, and `:reject` excludes that case from the result.
+  Error reporting is handled separately. The default is `:apply` when `force?` is
+  true, and `:reject` otherwise.
   """
-  def map_update(descr, key_descr, type, optional?, return_type? \\ true, force? \\ false)
+  def map_update(
+        descr,
+        key_descr,
+        type,
+        optional?,
+        return_type? \\ true,
+        force? \\ false,
+        on_missing \\ :default
+      )
       when is_boolean(optional?) do
-    case type do
-      :term ->
-        map_update_unchecked(
-          descr,
-          key_descr,
-          fn _, _ -> {:term, optional?} end,
-          return_type?,
-          force?
-        )
-
-      %{dynamic: dynamic} ->
-        fun = fn _, _ -> {dynamic, optional?} end
-        map_update_unchecked(dynamic(descr), key_descr, fun, return_type?, force?)
+    {descr, type} =
+      case type do
+        %{dynamic: dynamic} -> {dynamic(descr), dynamic}
+        _ -> {descr, type}
+      end
 
-      %{} ->
-        fun = fn _, _ -> {type, optional?} end
-        map_update_unchecked(descr, key_descr, fun, return_type?, force?)
-    end
+    operation = {{:constant, {type, optional?}}, map_update_on_missing(on_missing, force?)}
+    map_update_unchecked(descr, key_descr, operation, return_type?, force?)
   end
 
   @doc """
-  Updates `key_descr` in `descr` with `type`.
-
-  `key_descr` is split into optional and required keys and tracked accordingly.
-  The gradual aspect of `key_descr` does not impact the return type.
+  Updates `key_descr` in `descr` with `type_fun`.
 
-  This is a more general version of `map_update/6` and has the same return values.
-  However, the third argument is an anonymous function that receives the current
-  value and whether it is optional. Note the value returned by `type_fun` cannot
-  hold dynamic. Any dynamic conversion must happen before invoking this function.
+  This is a more general version of `map_update/7`: the third argument is an
+  anonymous function that receives the current value and whether it is optional.
+  For a gradual map, the value passed to the callback is gradual too. A returned
+  dynamic wrapper is removed before rebuilding the map; the map's gradual component
+  is handled by the update itself.
   """
-  def map_update_fun(descr, key_descr, type_fun, return_type? \\ true, force? \\ false) do
+  def map_update_fun(
+        descr,
+        key_descr,
+        type_fun,
+        return_type? \\ true,
+        force? \\ false,
+        on_missing \\ :default
+      ) do
     gradual? = gradual?(descr)
 
     type_fun = fn value, optional? ->
@@ -3521,36 +3670,43 @@ defmodule Module.Types.Descr do
       {new_value, new_optional?}
     end
 
-    map_update_unchecked(descr, key_descr, type_fun, return_type?, force?)
+    operation = {{:callback, type_fun}, map_update_on_missing(on_missing, force?)}
+    map_update_unchecked(descr, key_descr, operation, return_type?, force?)
   end
 
-  def map_update_unchecked(:term, _key_descr, _type_fun, _return_type?, _force?), do: :badmap
+  defp map_update_on_missing(:default, true), do: :apply
+  defp map_update_on_missing(:default, false), do: :reject
+  defp map_update_on_missing(mode, _) when mode in [:apply, :keep, :reject], do: mode
 
-  def map_update_unchecked(descr, key_descr, type_fun, return_type?, force?) do
+  defp map_update_unchecked(:term, _key_descr, _operation, _return_type?, _force?), do: :badmap
+
+  defp map_update_unchecked(descr, key_descr, operation, return_type?, force?) do
     split_keys = map_split_keys_and_domains(key_descr)
 
     case :maps.take(:dynamic, descr) do
       :error ->
-        if descr_key?(descr, :map) and map_only?(descr) do
-          {type, descr, errors, found?} =
-            map_update_static(descr, split_keys, type_fun, return_type?, force?, true)
-
+        with true <- descr_key?(descr, :map) and map_only?(descr),
+             {type, descr, errors, found?} <-
+               map_update_static(descr, split_keys, operation, return_type?, force?, true) do
           if found? do
             {type, descr, errors}
           else
             {:error, errors}
           end
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
 
       {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
+        with true <- descr_key?(dynamic, :map) and map_only?(static),
+             {dynamic_value, dynamic_descr, dynamic_errors, dynamic_found?} <-
+               map_update_static(dynamic, split_keys, operation, return_type?, force?, false) do
           {static_value, static_descr, static_errors, _static_found?} =
-            map_update_static(static, split_keys, type_fun, return_type?, force?, true)
-
-          {dynamic_value, dynamic_descr, dynamic_errors, dynamic_found?} =
-            map_update_static(dynamic, split_keys, type_fun, return_type?, force?, false)
+            case map_update_static(static, split_keys, operation, return_type?, force?, true) do
+              :badmap -> {none(), none(), [], false}
+              result -> result
+            end
 
           # We can exceptionally check for none() here because
           # we already check for empty downstream
@@ -3561,38 +3717,68 @@ defmodule Module.Types.Descr do
             {:error, static_errors ++ dynamic_errors}
           end
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
     end
   end
 
-  defp map_update_static(%{map: bdd}, split_keys, type_fun, return_type?, force?, static?) do
+  # Update leaf case
+  defp map_update_static(
+         %{map: bdd_leaf(tag, fields) = leaf},
+         split_keys,
+         operation,
+         return_type?,
+         force?,
+         static?
+       ) do
+    if map_leaf_empty?(leaf) do
+      :badmap
+    else
+      map_update_static_dnf(
+        leaf,
+        [{tag, fields, []}],
+        split_keys,
+        operation,
+        return_type?,
+        force?,
+        static?
+      )
+    end
+  end
+
+  defp map_update_static(%{map: bdd}, split_keys, operation, return_type?, force?, static?) do
+    case map_bdd_to_dnf_remove_empty(bdd) do
+      [] -> :badmap
+      dnf -> map_update_static_dnf(bdd, dnf, split_keys, operation, return_type?, force?, static?)
+    end
+  end
+
+  defp map_update_static(%{}, _split_keys, _operation, _return_type?, _force?, _static?) do
+    {none(), none(), [], false}
+  end
+
+  defp map_update_static(:term, split_keys, operation, return_type?, force?, static?) do
+    map_update_static(%{map: @map_top}, split_keys, operation, return_type?, force?, static?)
+  end
+
+  defp map_update_static_dnf(bdd, dnf, split_keys, operation, return_type?, force?, static?) do
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
+    accepts_missing? = elem(operation, 1) != :reject
+
     optional_keys =
       ((map_keys_from_negated_set(maybe_negated_set, bdd) -- optional_keys) -- required_keys) ++
         optional_keys
 
-    dnf = map_bdd_to_dnf_with_empty(bdd)
-
     {found?, value, domains, errors} =
       if force? and not return_type? do
         {false, none(), required_domains ++ optional_domains, []}
       else
-        callback =
-          if return_type? do
-            fn -> map_update_merge_atom_key(bdd, dnf) end
-          else
-            fn ->
-              # If we have required keys, we can assume domain_atom always work
-              if required_keys != [] or map_update_any_atom_key?(bdd, dnf) do
-                term()
-              else
-                none()
-              end
-            end
-          end
+        callback = fn ->
+          map_update_named_key_type(dnf, required_keys ++ optional_keys, return_type?)
+        end
 
         # Required domains must be found
         {found_required?, matched_required_domains, missing_domains, value} =
@@ -3605,82 +3791,86 @@ defmodule Module.Types.Descr do
         errors = Enum.map(missing_domains, &{:baddomain, domain_key_to_descr(&1)})
 
         domains =
-          if force?,
+          if accepts_missing?,
             do: required_domains ++ optional_domains,
             else: matched_required_domains ++ matched_optional_domains
 
         {found_required? or found_optional?, value, domains, errors}
       end
 
+    # Named-key updates below always union into this using the original bdd/dnf
     acc =
-      if found? or (force? and domains != []) do
-        # If any of required or optional domains are satisfied, then we compute the
-        # initial return type. `map_update_keys_static` will then union into the
-        # computed type below, using the original bdd/dnf, not the one with updated domains.
-        descr = map_update_put_domains(bdd, domains, type_fun, force?)
-        {value, descr, errors, true}
-      else
-        {value, none(), errors, false}
-      end
+      cond do
+        domains != [] and (found? or accepts_missing?) ->
+          atom_keys =
+            if maybe_negated_set,
+              do: :lists.usort(optional_keys ++ :sets.to_list(maybe_negated_set)),
+              else: []
 
-    map_update_keys_static(dnf, required_keys, optional_keys, type_fun, force?, static?, acc)
-  end
+          descr = map_update_domains(dnf, domains, operation, atom_keys)
+          {value, descr, errors, found? or force?}
 
-  defp map_update_static(%{}, _split_keys, _type_fun, _return_type?, _force?, _static?) do
-    {none(), none(), [], false}
-  end
+        found? ->
+          # Hit named atom keys only; there is no domain association to rewrite
+          {value, none(), errors, true}
 
-  defp map_update_static(:term, split_keys, type_fun, _return_type?, force?, static?) do
-    # Since it is an open map, we don't need to check the domains.
-    # The negated set will also be empty, because there are no fields.
-    # Finally, merged required_keys into optional_keys.
-    {required_keys, optional_keys, _maybe_negated_set, required_domains, optional_domains} =
-      split_keys
+        true ->
+          {value, none(), errors, false}
+      end
 
-    if required_domains != [] or optional_domains != [] do
-      {term(), open_map(), [], true}
-    else
-      acc = {none(), none(), [], false}
-      dnf = map_bdd_to_dnf_with_empty(@map_top)
-      map_update_keys_static(dnf, required_keys, optional_keys, type_fun, force?, static?, acc)
-    end
+    map_update_keys_static(dnf, required_keys, optional_keys, operation, force?, static?, acc)
   end
 
-  defp map_update_keys_static(dnf, required, optional, type_fun, force?, static?, acc) do
-    acc = map_update_keys(dnf, required, type_fun, true, force?, static?, acc)
-    acc = map_update_keys(dnf, optional, type_fun, false, force?, static?, acc)
+  defp map_update_keys_static(dnf, required, optional, operation, force?, static?, acc) do
+    acc = map_update_named_keys(dnf, required, operation, true, force?, static?, acc)
+    acc = map_update_named_keys(dnf, optional, operation, false, force?, static?, acc)
     acc
   end
 
-  defp map_update_keys(dnf, keys, type_fun, required_key?, force?, static?, acc) do
+  # For each possible key, starting from the original map:
+  # 1. Collect its old values and whether it may be absent. Split the positive
+  #    and negative maps into {field, rest_of_map}.
+  # 2. Remove the negations. Constants already replace the field.
+  # 3. For callbacks, apply it.
+  # 4. Rebuild maps with the new field and union them into the result.
+  # 5. Accumulate the old values and handle missing-key errors.
+  defp map_update_named_keys(dnf, keys, operation, required_key?, force?, static?, acc) do
     Enum.reduce(keys, acc, fn key, {acc_value, acc_descr, acc_errors, acc_found?} ->
-      {{value, optional?}, descr} =
+      {pairs, {value, optional?}} =
         case dnf do
-          # Optimization: avoid creating term types when updating open maps
+          # Optimization: for one open map with no exclusions, read the field and rest directly
           [{:open, fields, []}] ->
-            if fields_is_key(key, fields) do
-              map_dnf_pop_key_static(dnf, key, {none(), false})
-            else
-              {{term(), true}, %{map: map_new(:open, fields)}}
-            end
+            {field, rest} = map_pop_key_bdd(:open, fields, key)
+            {map_update_prepare_pairs([], field, rest, operation), field}
 
           _ ->
-            map_dnf_pop_key_static(dnf, key, {none(), false})
+            Enum.flat_map_reduce(dnf, {none(), false}, fn {tag, fields, negs}, acc ->
+              case map_split_key_line(tag, fields, negs, key, acc) do
+                :empty ->
+                  {[], acc}
+
+                {acc, field, rest, negatives} ->
+                  {map_update_prepare_pairs(negatives, field, rest, operation), acc}
+              end
+            end)
         end
 
+      # If callback, then apply it.
+      # Then rebuild the maps with the new field.
+      descr =
+        pairs
+        |> map_update_maybe_apply_callback(operation)
+        |> Enum.reduce(none(), fn {{new_type, new_optional?}, rest}, acc ->
+          opt_union(map_put_key_static(%{map: rest}, key, new_type, new_optional?), acc)
+        end)
+
+      acc_descr = opt_union(descr, acc_descr)
+
       if not force? and empty?(value) do
         acc_errors = if required_key?, do: [{:badkey, key} | acc_errors], else: acc_errors
         {acc_value, acc_descr, acc_errors, acc_found?}
       else
         acc_value = opt_union(value, acc_value)
-
-        {new_value, new_optional?} = type_fun.(value, optional?)
-
-        acc_descr =
-          opt_union(map_put_key_static(descr, key, new_value, new_optional?), acc_descr)
-
-        # The field will be missing if we are not forcing,
-        # we are in static mode and the value is optional.
         missing? = not force? and static? and optional?
 
         if required_key? and missing? do
@@ -3692,15 +3882,113 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  # Each pair links a key's field {value_type, optional?} to the rest of its map.
+  # Constant updates return pairs with the NEW field already attached.
+  # Callbacks return OLD fields; map_update_maybe_apply_callback applies the callback later.
+  defp map_update_prepare_pairs(negative, field, rest, {{:constant, new}, mode}) do
+    case mode do
+      :apply ->
+        # Update both present and absent keys.
+        map_update_project_pair(negative, field, rest, new)
+
+      :reject ->
+        # Only maps where the key is present can produce a result.
+        map_update_project_pair(negative, field, rest, new, false)
+
+      :keep ->
+        # Update present keys; keep maps with an absent key unchanged.
+        map_update_project_pair(negative, field, rest, new, true)
+    end
+  end
+
+  defp map_update_prepare_pairs(negative, field, rest, {{:callback, _fun}, _mode}) do
+    map_remove_negative(negative, field, rest)
+  end
+
+  # Find which remaining maps survive the exclusions, then put the new field.
+  defp map_update_project_pair(negative, field, rest, new) do
+    cond do
+      field_empty?(field) or field_empty?(new) ->
+        []
+
+      map_pair_projection_keeps_full_snd?(negative, field) ->
+        # Some old value, or absence, avoids all exclusions; every map in rest survives.
+        [{new, rest}]
+
+      true ->
+        negative
+        |> map_remove_negative(field, rest)
+        |> Enum.map(fn {_old, rest} -> {new, rest} end)
+    end
+  end
+
+  # Update present keys, preserving absent keys only when keep_absent? is true.
+  defp map_update_project_pair(negative, field, rest, new, keep_absent?) do
+    {old_type, optional?} = field
+    old_type = if field_empty?(new), do: none(), else: old_type
+    optional? = keep_absent? and optional?
+
+    # Emit each shortcut's result and remove that case from further processing.
+    {old_type, pairs} =
+      if not empty?(old_type) and
+           map_pair_projection_keeps_full_snd?(negative, {old_type, false}) do
+        {none(), [{new, rest}]}
+      else
+        {old_type, []}
+      end
+
+    {optional?, pairs} =
+      if optional? and map_pair_projection_keeps_full_snd?(negative, {none(), true}) do
+        {false, [{{none(), true}, rest} | pairs]}
+      else
+        {optional?, pairs}
+      end
+
+    # Eliminate negatives once for the cases neither shortcut handled.
+    field = {old_type, optional?}
+
+    if field_empty?(field) do
+      pairs
+    else
+      negative
+      |> map_remove_negative(field, rest)
+      |> Enum.reduce(pairs, fn {{old_type, optional?}, rest}, acc ->
+        acc = if empty?(old_type), do: acc, else: [{new, rest} | acc]
+        if optional?, do: [{{none(), true}, rest} | acc], else: acc
+      end)
+    end
+  end
+
+  # Constant updates already attached the new fields in map_update_prepare_pairs
+  defp map_update_maybe_apply_callback(pairs, {{:constant, _new}, _mode}), do: pairs
+
+  defp map_update_maybe_apply_callback(pairs, {{:callback, fun}, mode}) do
+    # Apply the callback to each pair separately
+    pairs
+    |> Enum.flat_map(fn {{old_type, optional?}, rest} ->
+      present = if empty?(old_type), do: {none(), false}, else: fun.(old_type, false)
+
+      absent =
+        case {optional?, mode} do
+          {true, :apply} -> fun.(none(), true)
+          {true, :keep} -> {none(), true}
+          _ -> {none(), false}
+        end
+
+      new = field_opt_union(present, absent, %{})
+      if field_empty?(new), do: [], else: [{new, rest}]
+    end)
+  end
+
   # Directly inserts a key of a given type into every positive and negative map.
   defp map_put_key_static(%{map: bdd} = descr, key, value, optional?) do
     bdd =
       bdd_map(bdd, fn
         bdd_leaf(:closed, fields) when optional? and value == @none ->
-          bdd_leaf_new(:closed, fields)
+          map_new(:closed, fields)
 
         bdd_leaf(tag, fields) ->
-          bdd_leaf_new(tag, fields_store(key, {value, optional?}, fields))
+          map_new(tag, fields_store(key, {value, optional?}, fields))
       end)
 
     %{descr | map: bdd}
@@ -3768,36 +4056,14 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp map_update_merge_atom_key(bdd, dnf) do
-    {_seen, acc} =
-      bdd_reduce(bdd, {%{}, none()}, fn bdd_leaf(_tag, fields), seen_acc ->
-        fields_fold(fields, seen_acc, fn key, {_type, _optional?}, {seen, acc} ->
-          if Map.has_key?(seen, key) do
-            {seen, acc}
-          else
-            {value, _optional?} = map_dnf_fetch_static(dnf, key)
-            {Map.put(seen, key, []), opt_union(acc, value)}
-          end
-        end)
-      end)
-
-    acc
-  end
+  defp map_update_named_key_type(dnf, keys, return_type?) do
+    Enum.reduce_while(keys, none(), fn key, acc ->
+      {value, _optional?} = map_dnf_fetch_static(dnf, key)
 
-  defp map_update_any_atom_key?(bdd, dnf) do
-    bdd_reduce(bdd, %{}, fn bdd_leaf(_tag, fields), acc ->
-      fields_fold(fields, acc, fn key, {_type, _optional?}, acc ->
-        if Map.has_key?(acc, key) do
-          acc
-        else
-          {value, _optional?} = map_dnf_fetch_static(dnf, key)
-          not empty?(value) and throw(:found_key)
-          Map.put(acc, key, [])
-        end
-      end)
+      if not return_type? and not empty?(value),
+        do: {:halt, term()},
+        else: {:cont, opt_union(value, acc)}
     end)
-  catch
-    :found_key -> true
   end
 
   # For each domain key, check if it exists in the map DNF and classify it
@@ -3841,75 +4107,99 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  # 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 bdd, we just update the domain with the new type,
-  # as well as its negations to keep them accurate.
-  #
-  # Note we store all domain_keys at once. Therefore, this operation:
-  #
-  #    map = %{integer() => if_set(:foo), float() => if_set(:bar)}
-  #    Map.put(map, integer() or float(), pid())
-  #
-  # will return:
-  #
-  #    %{integer() => if_set(:foo or pid()), float() => if_set(:bar or pid())}
-  #
-  # We could instead have returned:
-  #
-  #    %{integer() => if_set(:foo or pid()), float() => if_set(:bar)} or
-  #      %{integer() => if_set(:foo), float() => if_set(:bar or pid())}
-  #
-  # But that would not be helpful, as we can't distinguish between these two
-  # in Elixir code. It only makes sense to build the union for domain keys
-  # that do not exist.
-  defp map_update_put_domains(bdd, [], _type_fun, _force?), do: %{map: bdd}
+  # For each possible key domain, starting from the original map:
+  # 1. Split the positive and negative maps into {field, rest_of_map} for this domain.
+  # 2. Remove pairs excluded by the negative maps. Constants attach the new field now.
+  # 3. For callbacks, update each remaining pair's field, handling absent keys as requested.
+  # 4. Rebuild maps with the updated domain and union them into the result.
+  defp map_update_domains(dnf, domain_keys, operation, atom_keys) do
+    Enum.reduce(:lists.usort(domain_keys), none(), fn domain, acc ->
+      pairs =
+        Enum.flat_map(dnf, fn {tag, fields, negs} ->
+          {old_field, rest} = map_pop_domain_bdd(tag, fields, domain)
+
+          case map_split_negative_pairs_domain(negs, domain) do
+            :empty -> []
+            negative -> map_update_prepare_pairs(negative, old_field, rest, operation)
+          end
+        end)
 
-  defp map_update_put_domains(bdd, domain_keys, type_fun, force?) do
-    bdd =
-      bdd_map(bdd, fn bdd_leaf(tag, fields) ->
-        bdd_leaf_new(map_update_put_domain(tag, domain_keys, type_fun, force?), fields)
+      map_update_maybe_apply_callback(pairs, operation)
+      |> Enum.reduce(acc, fn {new_field, rest}, acc ->
+        opt_union(map_rejoin_domain(rest, domain, new_field, atom_keys), acc)
       end)
+    end)
+  end
 
-    %{map: bdd}
+  defp map_split_negative_pairs_domain(negs, domain_key) do
+    Enum.reduce_while(negs, [], fn
+      bdd_leaf(:open, []), _acc -> {:halt, :empty}
+      bdd_leaf(tag, fields), acc -> {:cont, [map_pop_domain_bdd(tag, fields, domain_key) | acc]}
+    end)
   end
 
-  defp map_update_put_domain(tag_or_domains, domain_keys, type_fun, force?) do
-    case tag_or_domains do
-      :open ->
-        :open
+  # Rebuild maps by adding the updated field to the remaining map:
+  # 1. If optional?, include the remaining map unchanged.
+  # 2. For each alternative in rest, allow old_type or new_type in the domain.
+  #    Keep named keys and other domains unchanged.
+  # 3. Add values in new_type but not old_type to each negative's domain, then
+  #    subtract it to preserve its restrictions on the remaining entries.
+  # 4. Exclude the empty map after inserting a value.
+  # 5. Union the rebuilt maps with the unchanged map alternatives from step 1.
+  defp map_rejoin_domain(rest, domain, {new_type, optional?}, atom_keys) do
+    acc = if optional?, do: %{map: rest}, else: none()
 
-      :closed ->
-        # Non-forced updates must not invoke the callback on absent branches:
-        # the callback may itself typecheck a function application, and
-        # applying it to `none()` will raise undue warnings.
-        if force?,
-          do: fields_from_keys(domain_keys, elem(type_fun.(none(), true), 0)),
-          else: :closed
-
-      # Note: domain_keys may contain duplicates, so we cannot
-      # do a side-by-side traversal here.
-      domains when is_list(domains) ->
-        Enum.reduce(domain_keys, domains, fn domain_key, acc ->
-          case fields_find(domain_key, acc) do
-            {:ok, value} ->
-              fields_store(
-                domain_key,
-                opt_union(value, elem(type_fun.(value, true), 0)),
-                acc
-              )
+    if empty?(new_type) do
+      acc
+    else
+      rest
+      |> map_bdd_to_dnf_remove_empty()
+      |> Enum.reduce(acc, fn {tag, fields, negs}, acc ->
+        fields = map_domain_protect_fields(tag, fields, domain, atom_keys)
+        old_type = map_domain_tag_to_type(tag, domain)
+        added_type = bare_difference(new_type, old_type)
+        output_type = opt_union(old_type, new_type)
+        output = map_new(map_replace_domain(tag, domain, output_type), fields)
+
+        output =
+          Enum.reduce(negs, output, fn bdd_leaf(neg_tag, neg_fields), output ->
+            neg_fields = map_domain_protect_fields(neg_tag, neg_fields, domain, atom_keys)
+            neg_type = opt_union(map_domain_tag_to_type(neg_tag, domain), added_type)
+            negative = map_new(map_replace_domain(neg_tag, domain, neg_type), neg_fields)
+            map_difference(output, negative)
+          end)
 
-            :error ->
-              # Likewise, only forced updates may synthesize missing domain keys.
-              if force?,
-                do: fields_store(domain_key, elem(type_fun.(none(), true), 0), acc),
-                else: acc
-          end
-        end)
+        opt_union(opt_difference(%{map: output}, empty_map()), acc)
+      end)
     end
   end
 
+  defp map_domain_protect_fields(tag, fields, :atom, atom_keys) do
+    Enum.reduce(atom_keys, fields, fn key, fields ->
+      if fields_is_key(key, fields),
+        do: fields,
+        else: fields_store(key, map_key_tag_to_field(tag), fields)
+    end)
+  end
+
+  defp map_domain_protect_fields(_tag, fields, _domain, _atom_keys), do: fields
+
+  defp map_replace_domain(:open, _domain_key, :term), do: :open
+
+  defp map_replace_domain(:open, domain_key, type) do
+    fields_store(domain_key, type, fields_from_keys(@domain_key_types, term()))
+  end
+
+  defp map_replace_domain(:closed, domain_key, type) do
+    if type == @none, do: :closed, else: fields_from_keys([domain_key], type)
+  end
+
+  defp map_replace_domain(domains, domain_key, type) when is_list(domains) do
+    if type == @none,
+      do: :orddict.erase(domain_key, domains),
+      else: fields_store(domain_key, type, domains)
+  end
+
   @doc """
   Puts a static key into `descr`.
 
@@ -3932,12 +4222,28 @@ defmodule Module.Types.Descr do
 
   def map_put(descr, key_descr, type) do
     if key_descr in [:term, %{dynamic: :term}] and type in [:term, %{dynamic: :term}] do
-      {:ok, if(gradual?(type) or gradual?(descr), do: dynamic(open_map()), else: open_map())}
+      cond do
+        not map_descr_only?(descr) or empty?(descr) ->
+          :badmap
+
+        gradual?(type) or gradual?(descr) ->
+          {:ok, dynamic(opt_difference(open_map(), empty_map()))}
+
+        true ->
+          {:ok, opt_difference(open_map(), empty_map())}
+      end
     else
       map_put_shared(descr, map_split_keys_and_domains(key_descr), type)
     end
   end
 
+  defp map_descr_only?(descr) do
+    case :maps.take(:dynamic, descr) do
+      :error -> descr_key?(descr, :map) and map_only?(descr)
+      {dynamic, static} -> descr_key?(dynamic, :map) and map_only?(static)
+    end
+  end
+
   defp map_put_shared(%{} = descr, split_keys, :term),
     do: map_put_static_value(descr, split_keys, :term)
 
@@ -3951,24 +4257,53 @@ defmodule Module.Types.Descr do
   defp map_put_static_value(descr, split_keys, type) do
     case :maps.take(:dynamic, descr) do
       :error ->
-        if non_empty_map_only?(descr) do
-          {:ok, map_put_static(descr, split_keys, type)}
+        if descr_key?(descr, :map) and map_only?(descr) do
+          map_put_static(descr, split_keys, type)
         else
           :badmap
         end
 
       {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
-          static_descr = map_put_static(static, split_keys, type)
-          dynamic_descr = map_put_static(dynamic, split_keys, type)
+        with true <- descr_key?(dynamic, :map) and map_only?(static),
+             {:ok, dynamic_descr} <- map_put_static(dynamic, split_keys, type) do
+          static_descr =
+            case map_put_static(static, split_keys, type) do
+              :badmap -> none()
+              {:ok, descr} -> descr
+            end
+
           {:ok, opt_union(static_descr, dynamic(dynamic_descr))}
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
     end
   end
 
+  defp map_put_static(%{map: bdd_leaf(tag, fields) = leaf}, split_keys, type) do
+    if map_leaf_empty?(leaf) do
+      :badmap
+    else
+      {:ok, map_put_static_dnf(leaf, [{tag, fields, []}], split_keys, type)}
+    end
+  end
+
   defp map_put_static(%{map: bdd}, split_keys, type) do
+    case map_bdd_to_dnf_remove_empty(bdd) do
+      [] -> :badmap
+      dnf -> {:ok, map_put_static_dnf(bdd, dnf, split_keys, type)}
+    end
+  end
+
+  defp map_put_static(%{}, _split_keys, _type) do
+    {:ok, none()}
+  end
+
+  defp map_put_static(:term, split_keys, type) do
+    map_put_static(%{map: @map_top}, split_keys, type)
+  end
+
+  defp map_put_static_dnf(bdd, dnf, split_keys, type) do
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
@@ -3976,35 +4311,26 @@ defmodule Module.Types.Descr do
       ((map_keys_from_negated_set(maybe_negated_set, bdd) -- optional_keys) -- required_keys) ++
         optional_keys
 
-    type_fun = fn _, _ -> {type, false} end
-
     descr =
       case required_domains ++ optional_domains do
-        [] -> none()
-        domains -> map_update_put_domains(bdd, domains, type_fun, true)
+        [] ->
+          none()
+
+        domains ->
+          atom_keys =
+            if maybe_negated_set,
+              do: :lists.usort(optional_keys ++ :sets.to_list(maybe_negated_set)),
+              else: []
+
+          map_put_domains(dnf, domains, type, atom_keys)
       end
 
-    dnf = map_bdd_to_dnf_with_empty(bdd)
     map_put_keys_static(dnf, required_keys ++ optional_keys, type, false, descr)
   end
 
-  defp map_put_static(%{}, _split_keys, _type) do
-    none()
-  end
-
-  defp map_put_static(:term, split_keys, type) do
-    # Since it is an open map, we don't need to check the domains.
-    # The negated set will also be empty, because there are no fields.
-    # Finally, merged required_keys into optional_keys.
-    {required_keys, optional_keys, _maybe_negated_set, required_domains, optional_domains} =
-      split_keys
-
-    if required_domains != [] or optional_domains != [] do
-      open_map()
-    else
-      dnf = map_bdd_to_dnf_with_empty(@map_top)
-      map_put_keys_static(dnf, required_keys ++ optional_keys, type, false, none())
-    end
+  defp map_put_domains(dnf, domain_keys, type, atom_keys) do
+    operation = {{:constant, {type, false}}, :apply}
+    map_update_domains(dnf, domain_keys, operation, atom_keys)
   end
 
   defp map_put_keys_static(dnf, keys, value, optional?, acc) do
@@ -4030,40 +4356,57 @@ defmodule Module.Types.Descr do
 
     case :maps.take(:dynamic, descr) do
       :error ->
-        if descr_key?(descr, :map) and map_only?(descr) do
-          type_selected = map_get_static(descr, split_keys)
-
-          if empty?(type_selected) do
-            :error
-          else
-            {:ok, type_selected}
-          end
+        with true <- descr_key?(descr, :map) and map_only?(descr),
+             {:ok, type_selected} <- map_get_static(descr, split_keys) do
+          if empty?(type_selected),
+            do: :error,
+            else: {:ok, type_selected}
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
 
       {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
-          static_type = map_get_static(static, split_keys)
-          dynamic_type = map_get_static(dynamic, split_keys)
+        with true <- descr_key?(dynamic, :map) and map_only?(static),
+             {:ok, dynamic_type} <- map_get_static(dynamic, split_keys) do
+          static_type =
+            case map_get_static(static, split_keys) do
+              :badmap -> none()
+              {:ok, type} -> type
+            end
 
-          if empty?(dynamic_type) do
-            :error
-          else
-            {:ok, opt_union(dynamic(dynamic_type), static_type)}
-          end
+          if empty?(dynamic_type),
+            do: :error,
+            else: {:ok, opt_union(dynamic(dynamic_type), static_type)}
         else
-          :badmap
+          false -> :badmap
+          :badmap -> :badmap
         end
     end
   end
 
+  defp map_get_static(%{map: bdd_leaf(tag, fields) = leaf}, split_keys) do
+    if map_leaf_empty?(leaf) do
+      :badmap
+    else
+      {:ok, map_get_static_dnf(leaf, [{tag, fields, []}], split_keys)}
+    end
+  end
+
   defp map_get_static(%{map: bdd}, split_keys) do
+    case map_bdd_to_dnf_remove_empty(bdd) do
+      [] -> :badmap
+      dnf -> {:ok, map_get_static_dnf(bdd, dnf, split_keys)}
+    end
+  end
+
+  defp map_get_static(%{}, _split_keys), do: {:ok, none()}
+  defp map_get_static(:term, _split_keys), do: {:ok, term()}
+
+  defp map_get_static_dnf(bdd, dnf, split_keys) do
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
-    dnf = map_bdd_to_dnf_with_empty(bdd)
-
     acc = none()
     acc = map_get_keys(dnf, required_keys, acc)
     acc = map_get_keys(dnf, optional_keys, acc)
@@ -4073,9 +4416,6 @@ defmodule Module.Types.Descr do
     acc
   end
 
-  defp map_get_static(%{}, _split_keys), do: none()
-  defp map_get_static(:term, _split_keys), do: term()
-
   defp map_get_keys(dnf, keys, acc) do
     Enum.reduce(keys, acc, fn atom, acc ->
       {value, _optional?} = map_dnf_fetch_static(dnf, atom)
@@ -4083,19 +4423,11 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  # Take a map BDD and return the union of present-value types for the given key domain.
+  # The DNF lines are already nonempty, so every value allowed by their domain
+  # can occur at a fresh key, even when the line has negatives.
   defp map_get_domain(dnf, domain_key, acc) when is_atom(domain_key) do
-    Enum.reduce(dnf, acc, fn
-      # Optimization: if there are no negatives, get the domain tag directly
-      {tag, _fields, []}, acc ->
-        map_domain_tag_to_type(tag, domain_key) |> opt_union(acc)
-
-      {tag_or_domains, fields, negs}, acc ->
-        if init_map_line_empty?(tag_or_domains, fields, negs) do
-          acc
-        else
-          map_domain_tag_to_type(tag_or_domains, domain_key) |> opt_union(acc)
-        end
+    Enum.reduce(dnf, acc, fn {tag_or_domains, _fields, _negs}, acc ->
+      map_domain_tag_to_type(tag_or_domains, domain_key) |> opt_union(acc)
     end)
   end
 
@@ -4112,6 +4444,8 @@ defmodule Module.Types.Descr do
   end
 
   # Compute which keys are optional, which ones are required, as well as domain keys
+  defp map_split_keys_and_domains(:term), do: map_split_keys_and_domains(unfolded_term())
+
   defp map_split_keys_and_domains(%{dynamic: dynamic} = static) do
     {required_keys, optional_keys, maybe_negated_set} =
       case {static, unfold(dynamic)} do
@@ -4459,6 +4793,13 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  # Split out the residual domain field without removing its domain association.
+  # A map literal constrains every key in a residual domain uniformly and cannot
+  # require such a key to exist.
+  defp map_pop_domain_bdd(tag, fields, domain_key) do
+    {{map_domain_tag_to_type(tag, domain_key), true}, map_new(tag, fields)}
+  end
+
   defp map_to_quoted(bdd, opts) do
     bdd
     |> map_bdd_to_dnf_with_empty()
@@ -6164,7 +6505,19 @@ defmodule Module.Types.Descr do
         fun.(leaf)
 
       {_, leaf, left, union, right} ->
-        bdd_node_new(fun.(leaf), bdd_map(left, fun), bdd_map(union, fun), bdd_map(right, fun))
+        case fun.(leaf) do
+          :bdd_bot ->
+            # (false and left) or union or (not false and right)
+            bdd_union(bdd_map(union, fun), bdd_map(right, fun))
+
+          mapped_leaf ->
+            bdd_node_new(
+              mapped_leaf,
+              bdd_map(left, fun),
+              bdd_map(union, fun),
+              bdd_map(right, fun)
+            )
+        end
     end
   end
 
@@ -6476,7 +6829,7 @@ defmodule Module.Types.Descr do
 
       {:ok, seen} ->
         case opt_map_union(tag1, fields1, tag2, fields2, seen) do
-          {tag, fields} -> bdd_leaf_new(tag, fields)
+          {tag, fields} -> map_new(tag, fields)
           nil -> bdd_union(bdd1, bdd2)
         end
     end
@@ -6672,7 +7025,7 @@ defmodule Module.Types.Descr do
           %{}
         )
 
-      bdd_leaf_new(tag, fields)
+      map_new(tag, fields)
     catch
       :empty -> :bdd_bot
     end
@@ -6766,7 +7119,7 @@ defmodule Module.Types.Descr do
     if field_empty?(field_diff) do
       :subtype
     else
-      a_diff = bdd_leaf_new(tag, fields_store(key, field_diff, fields))
+      a_diff = map_new(tag, fields_store(key, field_diff, fields))
 
       a_type =
         case type do
@@ -6774,14 +7127,14 @@ defmodule Module.Types.Descr do
             :bdd_bot
 
           :union ->
-            bdd_leaf_new(tag, fields_store(key, field_opt_union(field1, field2, seen), fields))
+            map_new(tag, fields_store(key, field_opt_union(field1, field2, seen), fields))
 
           :intersection ->
             field_int = field_opt_intersection(field1, field2, seen)
 
             if field_empty?(field_int),
               do: :bdd_bot,
-              else: bdd_leaf_new(tag, fields_store(key, field_int, fields))
+              else: map_new(tag, fields_store(key, field_int, fields))
         end
 
       {:one_key_difference, a_diff, a_type}
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 1c73a3a8ae..92b7f4aef6 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -2832,12 +2832,19 @@ defmodule Module.Types.DescrTest do
 
       # Removing all maps with tuple keys
       t_no_tuple = opt_difference(all_domains, closed_map([{domain_key(:tuple), float()}]))
-      t_really_no_tuple = opt_difference(all_domains, open_map([{domain_key(:tuple), float()}]))
+
+      maps_with_tuple_keys =
+        opt_difference(open_map(), open_map([{domain_key(:tuple), none()}]))
+
+      t_really_no_tuple = opt_difference(all_domains, maps_with_tuple_keys)
       assert subtype?(all_domains, open_map())
       # It's only closed maps, so it should not change
       assert map_get(t_no_tuple, tuple()) == {:ok, float()}
-      # This time we actually removed all tuple to float keys
+      # Exclude maps with at least one tuple key, retaining the other domains.
+      refute empty?(t_really_no_tuple)
       assert map_get(t_really_no_tuple, tuple()) == :error
+      assert map_get(t_really_no_tuple, atom([:bar])) == {:ok, atom([:ok])}
+      assert map_get(t_really_no_tuple, integer()) == {:ok, atom([:int])}
 
       t1 = closed_map([{domain_key(:tuple), integer()}])
       t2 = closed_map([{domain_key(:tuple), float()}])
@@ -3082,15 +3089,15 @@ defmodule Module.Types.DescrTest do
                   )
                 ), []}
 
-      # A "none" map
+      # A semantically empty map reports an invalid operand, not a missing key.
       assert open_map()
              |> opt_difference(open_map(a: {term(), true}, c: {term(), true}))
-             |> map_update(atom([:b]), integer(), false) == {:error, [badkey: :b]}
+             |> map_update(atom([:b]), integer(), false) == :badmap
 
-      # ... even when forcing
+      # ... even when forcing.
       assert open_map()
              |> opt_difference(open_map(a: {term(), true}, c: {term(), true}))
-             |> map_update(atom([:b]), integer(), false, true, true) == {none(), none(), []}
+             |> map_update(atom([:b]), integer(), false, true, true) == :badmap
     end
 
     # Times out without a projection-aware map_update path
@@ -3103,15 +3110,98 @@ defmodule Module.Types.DescrTest 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()`
       # due to the key being absent in the map.
-      type = dynamic(opt_difference(open_map(), empty_map()))
+      static_type = opt_difference(open_map(), empty_map())
+      type = dynamic(static_type)
 
       fun = fn value, _optional? ->
-        send(self(), :callback_invoked)
+        if empty?(value), do: send(self(), :callback_invoked_with_none)
         {value, false}
       end
 
-      assert map_update_fun(type, binary(), fun, false, false) == {dynamic(none()), type, []}
-      refute_received :callback_invoked
+      assert {value, result, []} = map_update_fun(type, binary(), fun, false, false)
+      assert equal?(value, dynamic(none()))
+      assert equal?(result, type)
+      refute_received :callback_invoked_with_none
+    end
+
+    test "popping a binary key drops invalidated negative map constraints" do
+      non_empty_map = opt_difference(open_map(), empty_map())
+
+      assert {value, rest, []} = map_update(non_empty_map, binary(), none(), true)
+      assert value == term()
+      assert equal?(rest, open_map())
+    end
+
+    test "popping a binary key preserves constraints on disjoint key domains" do
+      no_integer_keys = open_map([{domain_key(:integer), none()}])
+      has_integer_key = opt_difference(open_map(), no_integer_keys)
+
+      assert {value, rest, []} = map_update(has_integer_key, binary(), none(), true)
+      assert value == term()
+      assert equal?(rest, has_integer_key)
+    end
+
+    test "domain callbacks distinguish absence from an empty required field" do
+      type = opt_difference(open_map(), empty_map())
+
+      for {optional?, expected} <- [{true, open_map()}, {false, none()}] do
+        fun = fn _value, _optional? -> {none(), optional?} end
+        assert {:term, rest, []} = map_update_fun(type, binary(), fun, true, false)
+        assert equal?(rest, expected)
+      end
+    end
+
+    test "required-empty callback output does not drop unrelated negative domains" do
+      type =
+        opt_difference(
+          open_map([{domain_key(:float), binary()}, {domain_key(:integer), atom()}]),
+          open_map([{domain_key(:integer), atom([:excluded])}])
+        )
+
+      # A partial relation: binary values return a PID; atom values do not return.
+      fun = fn value, _optional? ->
+        {if(disjoint?(value, binary()), do: none(), else: pid()), false}
+      end
+
+      assert {_value, only_float, []} = map_update_fun(type, float(), fun, true, false)
+
+      assert {_value, both, []} =
+               map_update_fun(type, opt_union(integer(), float()), fun, true, false)
+
+      assert equal?(only_float, both)
+
+      int_pid = open_map([{domain_key(:integer), pid()}, {domain_key(:float), pid()}])
+      assert empty?(opt_intersection(both, int_pid))
+    end
+
+    test "non-forced domain updates on a union do not write missing domains" do
+      int_map = closed_map([{domain_key(:integer), atom([:a])}])
+      float_map = closed_map([{domain_key(:float), atom([:b])}])
+      type = opt_union(int_map, float_map)
+
+      fun = fn value, optional? ->
+        refute empty?(value)
+        {pid(), optional?}
+      end
+
+      int_result =
+        closed_map([{domain_key(:integer), opt_union(atom([:a]), pid())}])
+        |> opt_difference(empty_map())
+
+      float_result =
+        closed_map([{domain_key(:float), opt_union(atom([:b]), pid())}])
+        |> opt_difference(empty_map())
+
+      assert {_value, rest, []} = map_update_fun(type, integer(), fun, true, false)
+      assert equal?(rest, int_result)
+      refute subtype?(float_map, rest)
+
+      required = fn value, _optional? -> fun.(value, false) end
+
+      assert {_value, rest, []} =
+               map_update_fun(type, opt_union(integer(), float()), required, true, false)
+
+      assert equal?(rest, opt_union(int_result, float_result))
     end
 
     test "with dynamic atom keys" do
@@ -3124,7 +3214,7 @@ defmodule Module.Types.DescrTest do
                )
 
       assert equal?(type, atom([:value]))
-      assert equal?(descr, closed_map(key: {atom([:value, :new_value]), false}))
+      assert equal?(descr, closed_map(key: {atom([:new_value]), false}))
       assert errors == []
 
       assert {type, descr, errors} =
@@ -3136,7 +3226,7 @@ defmodule Module.Types.DescrTest do
                )
 
       assert equal?(type, dynamic(atom([:value])))
-      assert equal?(descr, dynamic(closed_map(key: {atom([:value, :new_value]), false})))
+      assert equal?(descr, dynamic(closed_map(key: {atom([:new_value]), false})))
       assert errors == []
 
       # Check struct fields
@@ -3149,6 +3239,7 @@ defmodule Module.Types.DescrTest do
                )
 
       assert type == term()
+
       assert equal?(descr, open_map(__struct__: {term(), false}))
       assert errors == []
 
@@ -3217,39 +3308,44 @@ defmodule Module.Types.DescrTest do
     end
 
     test "with domain keys" do
-      map =
+      fields = [
+        {domain_key(:integer), binary()},
+        {domain_key(:pid), binary()},
+        {domain_key(:port), binary()}
+      ]
+
+      map = closed_map(fields)
+
+      integer_result =
         closed_map([
-          {domain_key(:integer), binary()},
+          {domain_key(:integer), opt_union(integer(), binary())},
           {domain_key(:pid), binary()},
           {domain_key(:port), binary()}
         ])
+        |> opt_difference(empty_map())
 
-      assert map_update(map, none(), integer(), false) ==
-               {:error, []}
+      pid_result =
+        closed_map([
+          {domain_key(:integer), binary()},
+          {domain_key(:pid), opt_union(integer(), binary())},
+          {domain_key(:port), binary()}
+        ])
+        |> opt_difference(empty_map())
+
+      reference_result =
+        closed_map([{domain_key(:reference), integer()} | fields]) |> opt_difference(empty_map())
 
-      assert map_update(map, integer(), integer(), false) ==
-               {binary(),
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), binary()},
-                  {domain_key(:port), binary()}
-                ]), []}
+      binary_result =
+        closed_map([{domain_key(:binary), integer()} | fields]) |> opt_difference(empty_map())
+
+      assert map_update(map, none(), integer(), false) == {:error, []}
+      assert map_update(map, integer(), integer(), false) == {binary(), integer_result, []}
 
       assert map_update(map, opt_union(pid(), integer()), integer(), false) ==
-               {binary(),
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()}
-                ]), []}
+               {binary(), opt_union(pid_result, integer_result), []}
 
       assert map_update(map, opt_union(pid(), reference()), integer(), false) ==
-               {binary(),
-                closed_map([
-                  {domain_key(:integer), binary()},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()}
-                ]), [baddomain: reference()]}
+               {binary(), pid_result, [baddomain: reference()]}
 
       assert map_update(
                map,
@@ -3257,12 +3353,7 @@ defmodule Module.Types.DescrTest do
                integer(),
                false
              ) ==
-               {binary(),
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()}
-                ]), []}
+               {binary(), opt_union(pid_result, integer_result), []}
 
       assert map_update(
                map,
@@ -3270,17 +3361,12 @@ defmodule Module.Types.DescrTest do
                integer(),
                false
              ) ==
-               {binary(),
-                closed_map([
-                  {domain_key(:integer), binary()},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()}
-                ]), []}
+               {binary(), pid_result, []}
 
       assert map_update(map, dynamic(opt_union(reference(), binary())), integer(), false) ==
                {:error, []}
 
-      # ... unless forcing
+      # Forcing admits absent domains, still as alternative key choices.
       assert map_update(
                map,
                dynamic(opt_union(reference(), binary())),
@@ -3289,14 +3375,7 @@ defmodule Module.Types.DescrTest do
                true,
                true
              ) ==
-               {none(),
-                closed_map([
-                  {domain_key(:integer), binary()},
-                  {domain_key(:pid), binary()},
-                  {domain_key(:port), binary()},
-                  {domain_key(:binary), integer()},
-                  {domain_key(:reference), integer()}
-                ]), []}
+               {none(), opt_union(reference_result, binary_result), []}
 
       # Putting dynamic atom over record keys
       assert {type, descr, errors} =
@@ -3313,32 +3392,32 @@ defmodule Module.Types.DescrTest do
                descr,
                opt_union(
                  closed_map(key1: {binary(), false}, key2: {integer(), false}),
-                 closed_map(key1: {opt_union(integer(), binary()), false}, key2: {pid(), false})
+                 closed_map(key1: {integer(), false}, key2: {pid(), false})
                )
              )
 
       assert errors == [baddomain: atom()]
 
       # ... unless forcing
-      assert map_update(
-               closed_map(key1: {binary(), false}, key2: {pid(), false}),
-               atom(),
-               integer(),
-               false,
-               true,
-               true
-             ) ==
-               {opt_union(binary(), pid()),
-                [
-                  closed_map([
-                    {domain_key(:atom), integer()},
-                    key1: {binary(), false},
-                    key2: {pid(), false}
-                  ]),
-                  closed_map(key1: {integer(), false}, key2: {pid(), false}),
-                  closed_map(key1: {binary(), false}, key2: {integer(), false})
-                ]
-                |> Enum.reduce(&opt_union/2), [baddomain: atom()]}
+      map = closed_map(key1: {binary(), false}, key2: {pid(), false})
+
+      assert {type, descr, errors} = map_update(map, atom(), integer(), false, true, true)
+      assert equal?(type, opt_union(binary(), pid()))
+
+      expected =
+        [
+          closed_map([
+            {domain_key(:atom), integer()},
+            key1: {binary(), false},
+            key2: {pid(), false}
+          ]),
+          closed_map(key1: {integer(), false}, key2: {pid(), false}),
+          closed_map(key1: {binary(), false}, key2: {integer(), false})
+        ]
+        |> Enum.reduce(&opt_union/2)
+
+      assert equal?(descr, expected)
+      assert errors == [baddomain: atom()]
 
       assert {type, descr, errors} =
                map_update(
@@ -3354,35 +3433,39 @@ defmodule Module.Types.DescrTest do
                descr,
                opt_union(
                  closed_map(key1: {binary(), false}, key2: {integer(), false}),
-                 closed_map(key1: {opt_union(integer(), binary()), false}, key2: {pid(), false})
+                 closed_map(key1: {integer(), false}, key2: {pid(), false})
                )
              )
 
       assert errors == []
 
-      # A "none()" map
-      assert open_map()
-             |> opt_difference(open_map(a: {term(), true}, c: {term(), true}))
-             |> map_update(binary(), integer(), false) == {:error, [baddomain: binary()]}
-
-      # ... even when forcing
-      {type, descr, errors} =
-        open_map()
-        |> opt_difference(open_map(a: {term(), true}, c: {term(), true}))
-        |> map_update(binary(), integer(), false, true, true)
+      # A non-empty map with no binary keys reports a missing domain.
+      map = closed_map(a: {integer(), false})
+      refute empty?(map)
+      assert map_update(map, binary(), integer(), false) == {:error, [baddomain: binary()]}
 
+      # Forcing a required none() value has no old value and no possible result,
+      # but must still report the missing domain.
+      assert {type, descr, errors} = map_update(map, binary(), none(), false, true, true)
       assert empty?(type)
       assert empty?(descr)
       assert errors == [baddomain: binary()]
     end
 
     test "with mixed keys" do
-      assert map_update(dynamic(), opt_union(atom([:key]), binary()), integer(), false) ==
-               {dynamic(), dynamic(open_map()), []}
+      expected = opt_difference(open_map(), empty_map())
+
+      assert {value, result, []} =
+               map_update(dynamic(), opt_union(atom([:key]), binary()), integer(), false)
+
+      assert equal?(value, dynamic())
+      assert equal?(result, dynamic(expected))
 
       # When precise dynamic keys are given, at least one must succeed
+      map = closed_map([{:key, {atom(), false}}, {domain_key(:integer), binary()}])
+
       assert map_update(
-               closed_map([{:key, {atom(), false}}, {domain_key(:integer), binary()}]),
+               map,
                dynamic(opt_union(atom([:key]), integer())),
                integer(),
                false
@@ -3394,6 +3477,7 @@ defmodule Module.Types.DescrTest do
                     {:key, {atom(), false}},
                     {domain_key(:integer), opt_union(binary(), integer())}
                   ])
+                  |> opt_difference(empty_map())
                 ), []}
 
       # Negated keys
@@ -3409,16 +3493,19 @@ defmodule Module.Types.DescrTest do
 
       assert equal?(
                descr,
-               closed_map(key1: {binary(), false}, key2: {opt_union(integer(), binary()), false})
+               closed_map(key1: {binary(), false}, key2: {integer(), false})
              )
 
       assert errors == [baddomain: atom()]
 
+      map_with_atom_domain =
+        closed_map(
+          [key1: {binary(), false}, key2: {binary(), false}] ++
+            [{domain_key(:atom), pid()}]
+        )
+
       assert map_update(
-               closed_map(
-                 [key1: {binary(), false}, key2: {binary(), false}] ++
-                   [{domain_key(:atom), pid()}]
-               ),
+               map_with_atom_domain,
                opt_difference(atom(), atom([:key1])),
                integer(),
                false
@@ -3435,6 +3522,7 @@ defmodule Module.Types.DescrTest do
                     key1: {binary(), false},
                     key2: {binary(), false}
                   ])
+                  |> opt_difference(empty_map())
                 ), []}
 
       # Missing keys
@@ -3460,7 +3548,8 @@ defmodule Module.Types.DescrTest do
                     {:key, {atom(), false}},
                     {domain_key(:integer), binary()},
                     {domain_key(:pid), integer()}
-                  ]),
+                  ])
+                  |> opt_difference(empty_map()),
                   closed_map([
                     {:key, {atom(), false}},
                     {:other_key, {integer(), false}},
@@ -3476,8 +3565,150 @@ defmodule Module.Types.DescrTest do
     end
   end
 
+  describe "map update witnesses" do
+    test "does not call a non-forced callback for an absent explicit key" do
+      input =
+        dynamic(
+          opt_union(
+            closed_map(a: {integer(), false}, tag: {atom([:left]), false}),
+            closed_map(tag: {atom([:right]), false})
+          )
+        )
+
+      fun = fn value, optional? ->
+        refute empty?(value)
+        refute optional?
+        {value, false}
+      end
+
+      assert {_, _, []} = map_update_fun(input, atom([:a]), fun)
+    end
+
+    test "keeping absence preserves its remainder without invoking the callback" do
+      input =
+        dynamic(opt_union(closed_map(a: {integer(), false}), closed_map(b: {binary(), false})))
+
+      fun = fn value, optional? ->
+        refute empty?(value)
+        refute optional?
+        {pid(), false}
+      end
+
+      assert {_, result, []} = map_update_fun(input, atom([:a]), fun, false, false, :keep)
+
+      expected =
+        dynamic(opt_union(closed_map(a: {pid(), false}), closed_map(b: {binary(), false})))
+
+      assert equal?(result, expected)
+
+      assert {_, kept, []} = map_update(input, atom([:a]), none(), true, true, false, :keep)
+      assert {_, rejected, []} = map_update(input, atom([:a]), none(), true, true, false)
+      assert equal?(kept, dynamic(opt_union(empty_map(), closed_map(b: {binary(), false}))))
+      assert equal?(rejected, dynamic(empty_map()))
+    end
+
+    test "excluded atoms are not counted as old values or successful keys" do
+      key = opt_difference(atom(), atom([:a]))
+      input = closed_map(a: {integer(), false}, b: {binary(), false})
+      assert {value, result, _errors} = map_update(input, key, pid(), false)
+      assert value == binary()
+      assert equal?(result, closed_map(a: {integer(), false}, b: {pid(), false}))
+      assert {:error, _} = map_update(closed_map(a: {integer(), false}), key, pid(), false)
+    end
+
+    test "atom-domain updates include redundant named fields" do
+      input = closed_map([{domain_key(:atom), integer()}, a: {integer(), true}])
+      expected = closed_map(a: {pid(), false})
+
+      assert {:ok, put} = map_put(input, atom(), pid())
+      assert subtype?(expected, put)
+
+      assert {_, updated, []} = map_update(input, atom(), pid(), false)
+      assert subtype?(expected, updated)
+    end
+
+    test "domain overwrites preserve unrelated exclusions and equivalent inputs" do
+      input =
+        closed_map([{domain_key(:integer), atom()}, tag: {atom([:old, :new]), false}])
+        |> opt_difference(
+          closed_map([{domain_key(:integer), atom()}, tag: {atom([:old]), false}])
+        )
+
+      simplified = closed_map([{domain_key(:integer), atom()}, tag: {atom([:new]), false}])
+      assert equal?(input, simplified)
+
+      assert {:ok, put} = map_put(input, integer(), pid())
+      assert {:ok, simple_put} = map_put(simplified, integer(), pid())
+      assert map_fetch_key(put, :tag) == {false, atom([:new])}
+      assert equal?(put, simple_put)
+
+      assert {_, update, []} = map_update(input, integer(), pid(), false)
+      assert {_, simple_update, []} = map_update(simplified, integer(), pid(), false)
+      assert equal?(update, simple_update)
+      assert map_fetch_key(update, :tag) == {false, atom([:new])}
+    end
+
+    test "named atoms in negative leaves are protected during residual writes" do
+      input =
+        closed_map([{domain_key(:atom), atom([:old])}])
+        |> opt_difference(closed_map(a: {atom([:old]), false}))
+
+      partition = closed_map(a: {atom([:old]), false})
+      equivalent = opt_union(opt_intersection(input, partition), opt_difference(input, partition))
+      assert equal?(input, equivalent)
+      key = opt_difference(atom(), atom([:a]))
+      assert {:ok, left} = map_put(input, key, pid())
+      assert {:ok, right} = map_put(equivalent, key, pid())
+      assert equal?(left, right)
+      refute subtype?(closed_map(a: {pid(), false}), left)
+    end
+
+    test "pop preserves the remaining existence required by two negative literals" do
+      positive = closed_map([{domain_key(:binary), opt_union(atom(), pid())}])
+
+      input =
+        positive
+        |> opt_difference(closed_map([{domain_key(:binary), atom()}]))
+        |> opt_difference(closed_map([{domain_key(:binary), pid()}]))
+
+      assert {_, result, []} = map_update(input, binary(), none(), true)
+      assert equal?(result, opt_difference(positive, empty_map()))
+    end
+  end
+
+  describe "map domain updates with negated BDDs" do
+    test "map_put and map_update with a negated closed leaf" do
+      type = opt_difference(open_map(), empty_map())
+      target = closed_map(a: {atom([:x]), false})
+
+      for {type, target} <- [{type, target}, {dynamic(type), dynamic(target)}] do
+        assert {:ok, put} = map_put(type, atom(), atom([:x]))
+        assert {_, update, []} = map_update(type, atom(), atom([:x]), false, true)
+        assert subtype?(target, put)
+        assert subtype?(target, update)
+      end
+    end
+
+    test "map_put with a negated domain or empty map" do
+      only_y = closed_map([{domain_key(:integer), atom([:y])}])
+      target = opt_difference(only_y, empty_map())
+
+      for type <- [
+            opt_difference(open_map([{domain_key(:integer), atom()}]), only_y),
+            opt_difference(closed_map([{domain_key(:integer), atom([:z])}]), empty_map())
+          ] do
+        assert {:ok, result} = map_put(type, integer(), atom([:y]))
+        refute empty?(opt_intersection(result, target))
+      end
+    end
+  end
+
   describe "map_put" do
     test "with static atom keys" do
+      # with a domain key produces non-empty maps"
+      assert {:ok, result} = map_put(empty_map(), integer(), integer())
+      assert subtype?(result, opt_difference(open_map(), empty_map()))
+
       assert map_put(open_map(key: {binary(), false}), atom([:key]), integer()) ==
                {:ok, open_map(key: {integer(), false})}
 
@@ -3539,19 +3770,29 @@ defmodule Module.Types.DescrTest do
 
     test "with dynamic/term as key-value" do
       assert map_put(closed_map(key: {atom([:value]), false}), dynamic(), dynamic()) ==
-               {:ok, dynamic(open_map())}
+               {:ok, dynamic(opt_difference(open_map(), empty_map()))}
 
       assert map_put(closed_map(key: {atom([:value]), false}), dynamic(), term()) ==
-               {:ok, open_map()}
+               {:ok, opt_difference(open_map(), empty_map())}
 
       assert map_put(closed_map(key: {atom([:value]), false}), term(), dynamic()) ==
-               {:ok, dynamic(open_map())}
+               {:ok, dynamic(opt_difference(open_map(), empty_map()))}
 
       assert map_put(closed_map(key: {atom([:value]), false}), term(), term()) ==
-               {:ok, open_map()}
+               {:ok, opt_difference(open_map(), empty_map())}
 
       assert map_put(dynamic(closed_map(key: {atom([:value]), false})), term(), term()) ==
-               {:ok, dynamic(open_map())}
+               {:ok, dynamic(opt_difference(open_map(), empty_map()))}
+    end
+
+    test "with term key can update an explicit atom key" do
+      map = closed_map(a: {integer(), false})
+
+      assert {:ok, result} = map_put(map, term(), binary())
+      assert {:ok, expected} = map_put(map, unfold(term()), binary())
+      assert equal?(result, expected)
+      assert subtype?(closed_map(a: {binary(), false}), result)
+      assert subtype?(closed_map(a: {integer(), false}, b: {binary(), false}), result)
     end
 
     test "with dynamic atom keys" do
@@ -3591,83 +3832,81 @@ defmodule Module.Types.DescrTest do
     end
 
     test "with domain keys" do
-      map =
+      fields = [
+        {domain_key(:integer), binary()},
+        {domain_key(:pid), binary()},
+        {domain_key(:port), binary()}
+      ]
+
+      map = closed_map(fields)
+
+      integer_result =
         closed_map([
-          {domain_key(:integer), binary()},
+          {domain_key(:integer), opt_union(integer(), binary())},
           {domain_key(:pid), binary()},
           {domain_key(:port), binary()}
         ])
+        |> opt_difference(empty_map())
 
-      assert map_put(map, integer(), integer()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), binary()},
-                  {domain_key(:port), binary()}
-                ])}
+      pid_result =
+        closed_map([
+          {domain_key(:integer), binary()},
+          {domain_key(:pid), opt_union(integer(), binary())},
+          {domain_key(:port), binary()}
+        ])
+        |> opt_difference(empty_map())
+
+      reference_result =
+        closed_map([{domain_key(:reference), integer()} | fields]) |> opt_difference(empty_map())
+
+      binary_result =
+        closed_map([{domain_key(:binary), integer()} | fields]) |> opt_difference(empty_map())
+
+      assert map_put(map, integer(), integer()) == {:ok, integer_result}
 
       assert map_put(map, opt_union(pid(), integer()), integer()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()}
-                ])}
+               {:ok, opt_union(pid_result, integer_result)}
 
       assert map_put(map, opt_union(pid(), reference()), integer()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), binary()},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()},
-                  {domain_key(:reference), integer()}
-                ])}
+               {:ok, opt_union(pid_result, reference_result)}
 
       assert map_put(map, opt_union(pid(), dynamic(opt_union(reference(), integer()))), integer()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), opt_union(integer(), binary())},
-                  {domain_key(:pid), opt_union(integer(), binary())},
-                  {domain_key(:port), binary()},
-                  {domain_key(:reference), integer()}
-                ])}
+               {:ok, opt_union(pid_result, opt_union(reference_result, integer_result))}
 
       assert map_put(map, dynamic(opt_union(reference(), binary())), integer()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), binary()},
-                  {domain_key(:pid), binary()},
-                  {domain_key(:port), binary()},
-                  {domain_key(:reference), integer()},
-                  {domain_key(:binary), integer()}
-                ])}
+               {:ok, opt_union(reference_result, binary_result)}
 
       # Putting dynamic atom over record keys
-      assert map_put(
-               closed_map(key1: {binary(), false}, key2: {binary(), false}),
-               atom(),
-               integer()
-             ) ==
-               {:ok,
-                [
-                  closed_map(key1: {binary(), false}, key2: {integer(), false}),
-                  closed_map(key1: {integer(), false}, key2: {binary(), false}),
-                  closed_map([
-                    {domain_key(:atom), integer()},
-                    key1: {binary(), false},
-                    key2: {binary(), false}
-                  ])
-                ]
-                |> Enum.reduce(&opt_union/2)}
+      record_map = closed_map(key1: {binary(), false}, key2: {binary(), false})
+
+      assert {:ok, result} = map_put(record_map, atom(), integer())
+
+      expected =
+        [
+          closed_map(key1: {binary(), false}, key2: {integer(), false}),
+          closed_map(key1: {integer(), false}, key2: {binary(), false}),
+          closed_map([
+            {domain_key(:atom), integer()},
+            key1: {binary(), false},
+            key2: {binary(), false}
+          ])
+        ]
+        |> Enum.reduce(&opt_union/2)
+
+      assert equal?(result, expected)
     end
 
     test "with mixed keys" do
-      assert map_put(dynamic(), opt_union(atom([:key]), binary()), integer()) ==
-               {:ok, dynamic(open_map())}
+      expected = opt_difference(open_map(), empty_map())
+
+      assert {:ok, result} = map_put(dynamic(), opt_union(atom([:key]), binary()), integer())
+      assert equal?(result, dynamic(expected))
 
       # When precise dynamic keys are given, at least one must succeed
+      map = closed_map([{:key, {atom(), false}}, {domain_key(:integer), binary()}])
+
       assert map_put(
-               closed_map([{:key, {atom(), false}}, {domain_key(:integer), binary()}]),
+               map,
                dynamic(opt_union(atom([:key]), integer())),
                integer()
              ) ==
@@ -3678,10 +3917,11 @@ defmodule Module.Types.DescrTest do
                     {:key, {atom(), false}},
                     {domain_key(:integer), opt_union(binary(), integer())}
                   ])
+                  |> opt_difference(empty_map())
                 )}
 
       assert map_put(
-               closed_map([{:key, {atom(), false}}, {domain_key(:integer), binary()}]),
+               map,
                dynamic(opt_union(atom([:other_key]), pid())),
                integer()
              ) ==
@@ -3697,29 +3937,35 @@ defmodule Module.Types.DescrTest do
                     {domain_key(:integer), binary()},
                     {domain_key(:pid), integer()}
                   ])
+                  |> opt_difference(empty_map())
                 )}
 
       # Negated keys
-      assert map_put(
-               closed_map(key1: {binary(), false}, key2: {binary(), false}),
-               opt_difference(atom(), atom([:key1])),
-               integer()
-             ) ==
-               {:ok,
-                opt_union(
-                  closed_map(key1: {binary(), false}, key2: {integer(), false}),
-                  closed_map([
-                    {domain_key(:atom), integer()},
-                    key1: {binary(), false},
-                    key2: {binary(), false}
-                  ])
-                )}
+      record_map = closed_map(key1: {binary(), false}, key2: {binary(), false})
+
+      assert {:ok, result} =
+               map_put(record_map, opt_difference(atom(), atom([:key1])), integer())
+
+      expected =
+        opt_union(
+          closed_map(key1: {binary(), false}, key2: {integer(), false}),
+          closed_map([
+            {domain_key(:atom), integer()},
+            key1: {binary(), false},
+            key2: {binary(), false}
+          ])
+        )
+
+      assert equal?(result, expected)
+
+      map_with_atom_domain =
+        closed_map(
+          [key1: {binary(), false}, key2: {binary(), false}] ++
+            [{domain_key(:atom), pid()}]
+        )
 
       assert map_put(
-               closed_map(
-                 [key1: {binary(), false}, key2: {binary(), false}] ++
-                   [{domain_key(:atom), pid()}]
-               ),
+               map_with_atom_domain,
                opt_difference(atom(), atom([:key1])),
                integer()
              ) ==
@@ -3735,6 +3981,7 @@ defmodule Module.Types.DescrTest do
                     key1: {binary(), false},
                     key2: {binary(), false}
                   ])
+                  |> opt_difference(empty_map())
                 )}
     end
 
@@ -3745,6 +3992,27 @@ defmodule Module.Types.DescrTest do
       assert map_put(map, atom([:k]), binary()) ==
                {:ok, open_map(k: {binary(), false}, x: {term(), false})}
 
+      for {module, name} <- [{Map, :replace}, {Map, :replace!}, {Map, :put_new}, {:maps, :update}] do
+        args =
+          if module == Map, do: [map, atom([:k]), binary()], else: [atom([:k]), binary(), map]
+
+        assert {result, _context} =
+                 Module.Types.Apply.remote_apply(
+                   nil,
+                   module,
+                   name,
+                   args,
+                   {{:., [], [module, name]}, [], []},
+                   %{mode: :static},
+                   %{}
+                 )
+
+        expected =
+          if name == :put_new, do: map, else: open_map(k: {binary(), false}, x: {term(), false})
+
+        assert equal?(result, expected)
+      end
+
       map =
         opt_difference(
           open_map(k: {integer(), false}, x: {term(), false}),
@@ -3772,6 +4040,33 @@ defmodule Module.Types.DescrTest do
                {:ok, open_map(k: {binary(), false}, x: {term(), false})}
     end
 
+    test "is consistent across equivalent representations" do
+      a =
+        closed_map(
+          a:
+            {opt_negation(
+               open_map([
+                 {domain_key(:port), float()},
+                 {:a,
+                  {closed_map([
+                     {domain_key(:reference), boolean()},
+                     b: {boolean(), false},
+                     a: {boolean(), false}
+                   ]), false}},
+                 b: {opt_difference(fun(1), tuple()), false}
+               ])
+             ), false}
+        )
+
+      knife = closed_map([{domain_key(:map), opt_negation(open_tuple([fun(1)]))}])
+      a2 = opt_union(opt_intersection(a, knife), opt_difference(a, knife))
+      assert equal?(a, a2)
+
+      assert {:ok, r1} = map_put(a, atom(), knife)
+      assert {:ok, r2} = map_put(a2, atom(), knife)
+      assert equal?(r1, r2)
+    end
+
     test "is consistent across representations of an empty type" do
       # An empty map component that survives syntactically (open_map(c: none())
       # is a non-normalized empty, equal to none()) must report :badmap like
@@ -3783,6 +4078,87 @@ defmodule Module.Types.DescrTest do
     end
   end
 
+  describe "map operations with empty record lines" do
+    test "map_update ignores an empty static component beside a required key" do
+      canonical = closed_map(b: {term(), false})
+      polluted = opt_union(canonical, closed_map(a: {none(), false}))
+
+      assert equal?(polluted, canonical)
+
+      assert map_update(canonical, atom([:b]), atom([:x]), false) ==
+               {term(), closed_map(b: {atom([:x]), false}), []}
+
+      assert map_update(polluted, atom([:b]), atom([:x]), false) ==
+               map_update(canonical, atom([:b]), atom([:x]), false)
+    end
+
+    test "an empty open component does not provide a missing key domain" do
+      polluted = opt_union(empty_map(), open_map(a: {none(), false}))
+
+      assert equal?(polluted, empty_map())
+
+      assert map_update(empty_map(), integer(), atom([:x]), false) ==
+               {:error, [baddomain: integer()]}
+
+      assert map_update(polluted, integer(), atom([:x]), false) ==
+               map_update(empty_map(), integer(), atom([:x]), false)
+    end
+
+    test "map_update ignores an empty static component beside a gradual map" do
+      canonical = dynamic(open_map(key: {binary(), false}))
+      polluted = opt_union(canonical, closed_map(a: {none(), false}))
+
+      assert map_update(polluted, atom([:key]), integer(), false) ==
+               map_update(canonical, atom([:key]), integer(), false)
+    end
+
+    test "map operations reject an empty map component" do
+      empty_map_component = closed_map(a: {none(), false})
+      gradual_empty_map_component = dynamic(empty_map_component)
+
+      assert %{map: :bdd_bot} = empty_map_component
+      assert %{map: :bdd_bot} = closed_map(a: {empty_map_component, false})
+
+      excluded_maps =
+        opt_union(
+          closed_map(y: {integer(), false}),
+          closed_map(z: {integer(), false})
+        )
+
+      negative_map = opt_difference(open_map(), excluded_maps)
+      assert {:ok, %{map: :bdd_bot}} = map_put(negative_map, atom([:a]), none())
+
+      assert equal?(empty_map_component, none())
+      assert map_get(empty_map_component, atom([:a])) == map_get(none(), atom([:a]))
+      assert map_get(gradual_empty_map_component, atom([:a])) == :badmap
+
+      assert map_put(empty_map_component, atom([:a]), atom([:x])) == :badmap
+      assert map_put(none(), atom([:a]), atom([:x])) == :badmap
+      assert map_update(empty_map_component, atom([:a]), atom([:x]), false) == :badmap
+      assert map_update(none(), atom([:a]), atom([:x]), false) == :badmap
+      assert map_update(gradual_empty_map_component, atom([:a]), atom([:x]), false) == :badmap
+      assert map_fetch_key(empty_map_component, :a) == :badmap
+      assert map_fetch_key(gradual_empty_map_component, :a) == :badmap
+      assert map_fetch_key(none(), :a) == :badmap
+
+      # map_put
+      assert map_put(empty_map_component, atom(), dynamic()) == :badmap
+      assert map_put(dynamic(empty_map_component), atom(), dynamic()) == :badmap
+      assert map_put(none(), atom(), dynamic()) == :badmap
+      assert map_put(none(), term(), term()) == :badmap
+    end
+
+    test "map_put rejects an empty open component with static or gradual values" do
+      empty = open_map(a: {none(), false})
+      assert equal?(empty, none())
+
+      for value <- [integer(), dynamic()] do
+        assert map_put(none(), atom(), value) == :badmap
+        assert map_put(empty, atom(), value) == :badmap
+      end
+    end
+  end
+
   describe "disjoint" do
     test "map" do
       refute disjoint?(open_map(), open_map(a: {integer(), false}))
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index b97984f347..971c274432 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -1337,7 +1337,7 @@ defmodule Module.Types.ExprTest do
                  x = %{foo: :bar}
                  %{x | key => :baz}
                )
-             ) == closed_map(foo: {atom([:bar, :baz]), false})
+             ) == closed_map(foo: {atom([:baz]), false})
 
       # Override based on position
       assert typecheck!(
@@ -1406,6 +1406,8 @@ defmodule Module.Types.ExprTest do
     end
 
     test "updating maps with mixed record/dictionary keys" do
+      expected = dynamic(tuple([opt_difference(open_map(), empty_map()), open_map()]))
+
       # Static keys
       assert typecheck!(
                [map],
@@ -1413,12 +1415,12 @@ defmodule Module.Types.ExprTest do
                  key = if :rand.uniform() > 0.5, do: "key", else: :key
                  {%{map | key => :value}, map}
                )
-             ) ==
-               dynamic(tuple([open_map(), open_map()]))
+             )
+             |> equal?(expected)
 
       # Dynamic keys
-      assert typecheck!([map, key], key in ["key", :key], {%{map | key => :value}, map}) ==
-               dynamic(tuple([open_map(), open_map()]))
+      assert typecheck!([map, key], key in ["key", :key], {%{map | key => :value}, map})
+             |> equal?(expected)
     end
 
     test "inferred maps" do
diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs
index 7bf825dc10..3f051cd462 100644
--- a/lib/elixir/test/elixir/module/types/integration_test.exs
+++ b/lib/elixir/test/elixir/module/types/integration_test.exs
@@ -216,6 +216,30 @@ defmodule Module.Types.IntegrationTest do
   end
 
   describe "type checking" do
+    test "Map.update callback with a struct field selected through a map lookup" do
+      files = %{
+        "map_update_struct.ex" => """
+        defmodule MapUpdateStruct do
+          defstruct users: %{}, groups: %{}
+
+          @field %{user: :users, group: :groups}
+
+          def put(%__MODULE__{} = state, kind, id, %{} = value)
+              when is_map_key(@field, kind) and is_binary(id) do
+            Map.update(state, @field[kind], %{id => value}, &Map.put(&1, id, value))
+          end
+
+          def put2(%__MODULE__{} = state, kind, id, %{} = value)
+              when kind in [:user, :group] and is_binary(id) do
+            Map.update(state, @field[kind], %{id => value}, &Map.put(&1, id, value))
+          end
+        end
+        """
+      }
+
+      assert_no_warnings(files)
+    end
+
     test "inferred remote calls" do
       files = %{
         "a.ex" => """
diff --git a/lib/elixir/test/elixir/module/types/map_test.exs b/lib/elixir/test/elixir/module/types/map_test.exs
index 753c55ff77..5149387ed8 100644
--- a/lib/elixir/test/elixir/module/types/map_test.exs
+++ b/lib/elixir/test/elixir/module/types/map_test.exs
@@ -11,6 +11,46 @@ defmodule Module.Types.MapTest do
   import Module.Types.Descr
   defmacro domain_key(arg) when is_atom(arg), do: [arg]
 
+  describe "empty map operands" do
+    test "updates report an empty argument instead of a missing key" do
+      # A required field whose value never returns makes the entire map empty.
+      assert %{map: _} = map = typecheck!(%{a: raise("oops")})
+      assert empty?(map)
+
+      assert typeerror!(Map.replace!(%{a: raise("oops")}, :b, 1)) |> strip_ansi() == """
+             incompatible types given to Map.replace!/3:
+
+                 Map.replace!(%{a: raise(RuntimeError.exception("oops"))}, :b, 1)
+
+             given types:
+
+                 none(), :b, integer()
+
+             the 1st argument is empty (often represented as none()), \
+             most likely because it is the result of an expression that \
+             always fails, such as a `raise` or a previous invalid call. \
+             This causes any function called with this value to fail
+             """
+    end
+
+    test "forced updates also report an empty argument" do
+      assert typeerror!(Map.put_new(%{a: raise("oops")}, :b, 1)) |> strip_ansi() == """
+             incompatible types given to Map.put_new/3:
+
+                 Map.put_new(%{a: raise(RuntimeError.exception("oops"))}, :b, 1)
+
+             given types:
+
+                 none(), :b, integer()
+
+             the 1st argument is empty (often represented as none()), \
+             most likely because it is the result of an expression that \
+             always fails, such as a `raise` or a previous invalid call. \
+             This causes any function called with this value to fail
+             """
+    end
+  end
+
   describe "inferred" do
     test "Map.new/0" do
       assert typecheck!(Map.new()) == dynamic(empty_map())
@@ -132,8 +172,8 @@ defmodule Module.Types.MapTest do
       assert typecheck!([x], x |> Map.delete(:key) |> Map.put(:key, "123")) ==
                dynamic(open_map(key: {binary(), false}))
 
-      assert typecheck!([x, y], x |> Map.delete(:key) |> Map.put(String.to_unsafe_atom(y), "123")) ==
-               dynamic(open_map(key: {binary(), true}))
+      assert typecheck!([x, y], x |> Map.delete(:key) |> Map.put(String.to_unsafe_atom(y), "123"))
+             |> equal?(dynamic(opt_difference(open_map(key: {binary(), true}), empty_map())))
     end
   end
 
@@ -568,6 +608,13 @@ defmodule Module.Types.MapTest do
   end
 
   describe "Map.pop/2" do
+    test "preserves the map when an arbitrary atom key is absent" do
+      assert equal?(
+               typecheck!([key], Map.pop(%{foo: 1}, String.to_unsafe_atom(key))),
+               tuple([opt_union(integer(), atom([nil])), closed_map(foo: {integer(), true})])
+             )
+    end
+
     test "checking" do
       assert typecheck!(Map.pop(%{key: 123}, :key)) ==
                tuple([opt_union(integer(), atom([nil])), empty_map()])
@@ -808,6 +855,17 @@ defmodule Module.Types.MapTest do
                  x
                )
              ) == dynamic(open_map(key: {term(), false}))
+
+      # rest of a non-empty map may be empty
+      assert typecheck!(
+               [map],
+               map_size(map) > 0,
+               (
+                 {_value, rest} = Map.pop!(map, "some_key")
+                 rest
+               )
+             )
+             |> equal?(dynamic(open_map()))
     end
 
     test "errors" do
@@ -856,7 +914,8 @@ defmodule Module.Types.MapTest do
                  closed_map(foo: {integer(), false}, bar: {binary(), false})
                )
 
-      assert typecheck!([x], Map.put(x, 123, 456)) == dynamic(open_map())
+      assert typecheck!([x], Map.put(x, 123, 456)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
     end
 
     test "inference" do
@@ -912,10 +971,16 @@ defmodule Module.Types.MapTest do
                  closed_map(foo: {integer(), false}, bar: {binary(), false})
                )
 
-      assert typecheck!([], Map.put_new_lazy(%{789 => "binary"}, 123, fn -> 456 end)) ==
-               closed_map([{domain_key(:integer), opt_union(binary(), integer())}])
+      assert typecheck!([], Map.put_new_lazy(%{789 => "binary"}, 123, fn -> 456 end))
+             |> equal?(
+               opt_difference(
+                 closed_map([{domain_key(:integer), opt_union(binary(), integer())}]),
+                 empty_map()
+               )
+             )
 
-      assert typecheck!([x], Map.put_new_lazy(x, 123, fn -> 456 end)) == dynamic(open_map())
+      assert typecheck!([x], Map.put_new_lazy(x, 123, fn -> 456 end)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
     end
 
     test "inference" do
@@ -978,10 +1043,16 @@ defmodule Module.Types.MapTest do
                  closed_map(foo: {integer(), false}, bar: {binary(), false})
                )
 
-      assert typecheck!([], Map.put_new(%{789 => "binary"}, 123, 456)) ==
-               closed_map([{domain_key(:integer), opt_union(binary(), integer())}])
+      assert typecheck!([], Map.put_new(%{789 => "binary"}, 123, 456))
+             |> equal?(
+               opt_difference(
+                 closed_map([{domain_key(:integer), opt_union(binary(), integer())}]),
+                 empty_map()
+               )
+             )
 
-      assert typecheck!([x], Map.put_new(x, 123, 456)) == dynamic(open_map())
+      assert typecheck!([x], Map.put_new(x, 123, 456)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
     end
 
     test "inference" do
@@ -1024,7 +1095,7 @@ defmodule Module.Types.MapTest do
       assert typecheck!(
                [condition?],
                Map.replace(%{foo: 123}, if(condition?, do: :foo, else: :bar), "123")
-             ) == closed_map(foo: {binary(), false})
+             ) == closed_map(foo: {opt_union(integer(), binary()), false})
 
       assert typecheck!([x], Map.replace(x, 123, 456)) == dynamic(open_map())
     end
@@ -1073,7 +1144,7 @@ defmodule Module.Types.MapTest do
                Map.replace_lazy(%{foo: 123}, if(condition?, do: :foo, else: :bar), fn _ ->
                  "123"
                end)
-             ) == dynamic(closed_map(foo: {binary(), false}))
+             ) == dynamic(closed_map(foo: {opt_union(integer(), binary()), false}))
 
       # Both succeed but different clauses
       assert typecheck!(
@@ -1096,8 +1167,12 @@ defmodule Module.Types.MapTest do
 
       assert typecheck!([x], Map.replace_lazy(x, 123, fn _ -> 456 end)) == dynamic(open_map())
 
-      assert typecheck!([], Map.replace_lazy(%{123 => 456}, 123, fn x -> x * 1.0 end)) ==
+      result = typecheck!([], Map.replace_lazy(%{123 => 456}, 123, fn x -> x * 1.0 end))
+
+      assert equal?(
+               result,
                dynamic(closed_map([{domain_key(:integer), opt_union(integer(), float())}]))
+             )
     end
 
     test "inference" do
@@ -1163,7 +1238,8 @@ defmodule Module.Types.MapTest do
                Map.replace!(%{foo: 123}, if(condition?, do: :foo, else: :bar), "123")
              ) == closed_map(foo: {binary(), false})
 
-      assert typecheck!([x], Map.replace!(x, 123, 456)) == dynamic(open_map())
+      assert typecheck!([x], Map.replace!(x, 123, 456)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
     end
 
     test "inference" do
@@ -1255,7 +1331,7 @@ defmodule Module.Types.MapTest do
 
   describe "Map.update/4" do
     test "checking" do
-      assert typecheck!(Map.update(%{}, :key, :default, fn _ -> :value end)) ==
+      assert typecheck!(Map.update(%{}, :key, :default, fn :bar -> :value end)) ==
                dynamic(closed_map(key: {atom([:default]), false}))
 
       assert typecheck!(Map.update(%{key: 123}, :key, :default, fn _ -> :value end)) ==
@@ -1298,20 +1374,21 @@ defmodule Module.Types.MapTest do
                  )
                )
 
-      assert typecheck!([x], Map.update(x, 123, :default, fn _ -> 456 end)) == dynamic(open_map())
+      assert typecheck!([x], Map.update(x, 123, :default, fn _ -> 456 end)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
 
-      integer_to_integer_float_atom =
-        dynamic(
-          closed_map([
-            {domain_key(:integer), integer() |> opt_union(float()) |> opt_union(atom([:default]))}
-          ])
-        )
+      updated_value = integer() |> opt_union(float()) |> opt_union(atom([:default]))
 
-      assert typecheck!([], Map.update(%{123 => 456}, 123, :default, fn x -> x * 1.0 end)) ==
-               integer_to_integer_float_atom
+      integer_update_result =
+        closed_map([{domain_key(:integer), updated_value}])
+        |> opt_difference(empty_map())
+        |> dynamic()
 
-      assert typecheck!([], Map.update(%{123 => 456}, 456, :default, fn x -> x * 1.0 end)) ==
-               integer_to_integer_float_atom
+      assert typecheck!([], Map.update(%{123 => 456}, 123, :default, fn x -> x * 1.0 end))
+             |> equal?(integer_update_result)
+
+      assert typecheck!([], Map.update(%{123 => 456}, 456, :default, fn x -> x * 1.0 end))
+             |> equal?(integer_update_result)
     end
 
     test "inference" do
@@ -1344,6 +1421,71 @@ defmodule Module.Types.MapTest do
   end
 
   describe "Map.update!/3" do
+    test "callback diagnostics do not depend on equivalent map partitions" do
+      callback = typecheck!(fn x when is_integer(x) -> x + 1 end)
+
+      for {input, cut, key} <- [
+            {closed_map(value: {opt_union(integer(), float()), false}),
+             closed_map(value: {integer(), false}), atom([:value])},
+            {closed_map([{domain_key(:integer), opt_union(integer(), float())}]),
+             closed_map([{domain_key(:integer), integer()}]), integer()},
+            {closed_map([{domain_key(:atom), opt_union(integer(), float())}]),
+             closed_map(a: {integer(), false}), atom()}
+          ] do
+        partitioned = opt_union(opt_intersection(input, cut), opt_difference(input, cut))
+        assert equal?(input, partitioned)
+
+        apply = fn map ->
+          Module.Types.Apply.map_update_or_replace_lazy(
+            :update!,
+            [dynamic(map), key, callback],
+            %{mode: :static},
+            "raise"
+          )
+        end
+
+        assert {:ok, left} = apply.(input)
+        assert {:ok, right} = apply.(partitioned)
+        assert equal?(left, right)
+      end
+    end
+
+    test "ignores an incompatible callback alternative" do
+      assert typecheck!(
+               [condition?],
+               Map.update!(
+                 if(condition?, do: %{value: 1, kind: :good}, else: %{value: 1.0, kind: :bad}),
+                 :value,
+                 fn x when is_integer(x) -> x + 1 end
+               )
+             ) == dynamic(closed_map(value: {integer(), false}, kind: {atom([:good]), false}))
+    end
+
+    test "preserves correlations when applying an inferred multi-clause function" do
+      result =
+        typecheck!(
+          [condition?],
+          Map.update!(
+            if(condition?, do: %{value: :x, kind: :x}, else: %{value: :y, kind: :y}),
+            :value,
+            fn
+              :x -> 123
+              :y -> self()
+            end
+          )
+        )
+
+      assert equal?(
+               result,
+               dynamic(
+                 opt_union(
+                   closed_map(value: {integer(), false}, kind: {atom([:x]), false}),
+                   closed_map(value: {pid(), false}, kind: {atom([:y]), false})
+                 )
+               )
+             )
+    end
+
     test "checking" do
       assert typecheck!(Map.update!(%{key: 123}, :key, fn _ -> :value end)) ==
                dynamic(closed_map(key: {atom([:value]), false}))
@@ -1372,13 +1514,19 @@ defmodule Module.Types.MapTest do
                  )
                )
 
-      assert typecheck!([x], Map.update!(x, 123, fn _ -> 456 end)) == dynamic(open_map())
+      assert typecheck!([x], Map.update!(x, 123, fn _ -> 456 end)) ==
+               dynamic(opt_difference(open_map(), empty_map()))
+
+      integer_update_result =
+        closed_map([{domain_key(:integer), opt_union(integer(), float())}])
+        |> opt_difference(empty_map())
+        |> dynamic()
 
       assert typecheck!([], Map.update!(%{123 => 456}, 123, fn x -> x * 1.0 end)) ==
-               dynamic(closed_map([{domain_key(:integer), opt_union(integer(), float())}]))
+               integer_update_result
 
       assert typecheck!([], Map.update!(%{123 => 456}, 456, fn x -> x * 1.0 end)) ==
-               dynamic(closed_map([{domain_key(:integer), opt_union(integer(), float())}]))
+               integer_update_result
     end
 
     test "inference" do
@@ -1423,6 +1571,9 @@ defmodule Module.Types.MapTest do
 
                    (:bar -> dynamic(:value))
                """
+
+      assert typeerror!(Map.update!(%{key: 1}, :key, fn x, y -> {x, y} end)) =~
+               "expected a 1-arity function"
     end
 
     test "with unknown function type" do
diff --git a/lib/elixir/test/elixir/module/types/recursive_test.exs b/lib/elixir/test/elixir/module/types/recursive_test.exs
index 5914d12d70..1c7c4a7768 100644
--- a/lib/elixir/test/elixir/module/types/recursive_test.exs
+++ b/lib/elixir/test/elixir/module/types/recursive_test.exs
@@ -628,6 +628,18 @@ defmodule Module.Types.RecursiveTest do
       |> unfold()
     end
 
+    test "required recursive map fields defer emptiness checks" do
+      map =
+        recursive(%{
+          M: fn recur -> closed_map(a: {recur.(:M), false}) end
+        })
+        |> Map.fetch!(:M)
+        |> unfold()
+
+      assert empty?(map)
+      assert map_fetch_key(dynamic(map), :a) == :badmap
+    end
+
     # X = {integer(), Y} | nil and Y = {boolean(), X} | nil
     defp mutual_tuples() do
       %{X: nx, Y: ny} =