From 880b4796e50c106d2d93caaa864379ea0f70a83d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Mon, 3 Nov 2025 19:54:59 +0100
Subject: [PATCH 1/9] WIP

---
 lib/elixir/lib/module/types/descr.ex          | 409 ++++++++----------
 lib/elixir/lib/module/types/expr.ex           |  79 ++--
 lib/elixir/lib/module/types/of.ex             |  67 ++-
 .../test/elixir/module/types/descr_test.exs   |  64 +--
 4 files changed, 240 insertions(+), 379 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 0bb3ea069f9..4992184ea8b 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -11,9 +11,8 @@ defmodule Module.Types.Descr do
 
   # Vocabulary:
   #
-  # * DNF - disjunctive normal form which is a pair of unions and negations.
-  # * BDD - binary decision diagram which is a set-theoretic representation of types as a tree.
-  #   In the case of maps, we augment each pair with the open/closed tag.
+  # * DNF - disjunctive normal form which is a pair of unions and negations
+  # * BDD - binary decision diagram which is a set-theoretic representation of types as a tree
 
   import Bitwise
 
@@ -2274,50 +2273,48 @@ defmodule Module.Types.Descr do
   # (@domain_key_types) to types, and `fields` is a map of atom keys (:foo, :bar, ...)
   # to types.
   #
-  # For instance, the type `%{..., a: integer()} and not %{b: atom()}` can be represented
-  # by the BDD containing one pair of shape:
-  #
-  #     {{:open, %{:a => integer()}}, {{:closed, %{:b => atom()}}, :bdd_bot, :bdd_top}, :bdd_bot}
-  #
-  # which can be seen as:
-  #
-  #     └─ %{..., a: integer()}
-  #      ├─ %{b: atom()}
-  #      │  ├─ :bdd_bot
-  #      │  └─ :bdd_top
-  #      └─ :bdd_bot
-  #
-  # and is interpreted as the intersection of `%{..., a: integer()}` with
-  # `not %{b: atom()}`, since the only path from the root to the leaves which
-  # ends with `:bdd_top` is the one which takes the first (left) branch after
-  # `%{..., a: integer()}`, and the second (right) branch after `%{b: atom()}`.
-  #
-  # This representation keeps negations symbolic, and avoids distributing difference on
-  # every member of a union which creates a lot of map literals in the union and
-  # requires emptiness checks to avoid creating empty maps.
-  #
-  # For instance, the difference between `%{...}` and `%{a: atom(), b: integer()}`
-  # is the union of `%{..., a: atom(), b: if_set(not integer())}` and
-  # `%{..., a: if_set(not atom()), b: integer()}`. For maps with more keys,
-  # each key in a negated literal may create a new union when eliminated.
-  #
-  # Instead of a tag :open or :closed, we can use a map of domains which
-  # specifies for each defined key domain (@domain_key_types) the type associated with
-  # those keys.
-  #
   # For instance, the type `%{atom() => if_set(integer())}` is the type of maps where atom keys
   # map to integers, without any non-atom keys. It is represented using the map literal
-  # `{%{atom: if_set(integer())}, [], []}`, with no defined keys or negations.
+  # `{%{atom: if_set(integer())}, %{}}`, with no defined keys.
   #
   # The type `%{..., atom() => integer()}` represents maps with atom keys bound to integers,
   # and other keys bound to any type. It will be represented using a map domain that maps
   # atom to `if_set(integer())`, and every other domain key to `term_or_optional()`.
 
-  defp map_descr(tag, pairs, default, force?) do
+  @doc """
+  Converts a type into domain keys.
+  """
+  def to_domain_keys(:term), do: @domain_key_types
+
+  def to_domain_keys(%{dynamic: dynamic}), do: to_domain_keys(dynamic)
+
+  def to_domain_keys(key_descr) do
+    for {type_kind, type} <- key_descr, reduce: [] do
+      acc ->
+        cond do
+          type_kind == :bitmap -> bitmap_to_domain_keys(type, acc)
+          not empty?(%{type_kind => type}) -> [domain_key(type_kind) | acc]
+          true -> acc
+        end
+    end
+  end
+
+  defp bitmap_to_domain_keys(bitmap, acc) do
+    acc = if (bitmap &&& @bit_binary) != 0, do: [domain_key(:binary) | acc], else: acc
+    acc = if (bitmap &&& @bit_empty_list) != 0, do: [domain_key(:empty_list) | acc], else: acc
+    acc = if (bitmap &&& @bit_integer) != 0, do: [domain_key(:integer) | acc], else: acc
+    acc = if (bitmap &&& @bit_float) != 0, do: [domain_key(:float) | acc], else: acc
+    acc = if (bitmap &&& @bit_pid) != 0, do: [domain_key(:pid) | acc], else: acc
+    acc = if (bitmap &&& @bit_port) != 0, do: [domain_key(:port) | acc], else: acc
+    acc = if (bitmap &&& @bit_reference) != 0, do: [domain_key(:reference) | acc], else: acc
+    acc
+  end
+
+  defp map_descr(tag, pairs, default, force_domains?) do
     {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false)
 
     map_new =
-      if domains != %{} or force? do
+      if domains != %{} or force_domains? do
         domains =
           if tag == :open do
             Enum.reduce(@domain_key_types, domains, &Map.put_new(&2, &1, default))
@@ -2336,10 +2333,15 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # TODO: Double check if we indeed want the union here
-  # when we start using domain types from Elixir itself
-  defp map_put_domain(domain, key, value) do
-    Map.update(domain, key, if_set(value), &union(&1, value))
+  # TODO: Unwrap domain keys when storing them, use a list wrapping instead
+  defp map_put_domain(domain, domain_keys, value) when is_list(domain_keys) do
+    Enum.reduce(domain_keys, domain, fn key, acc ->
+      Map.update(acc, key, if_set(value), &union(&1, value))
+    end)
+  end
+
+  defp map_put_domain(domain, domain_key(_) = domain_key, value) do
+    Map.update(domain, domain_key, if_set(value), &union(&1, value))
   end
 
   defp map_descr_pairs([{key, :term} | rest], fields, domain, dynamic?) do
@@ -2751,174 +2753,135 @@ defmodule Module.Types.Descr do
   end
 
   @doc """
-  Fetches and puts a `key` of a given type, assuming that the descr is exclusively
+  Fetches and puts a `key_or_domains`, assuming that the descr is exclusively
   a map (or dynamic).
+
+  This is a counter-part to `map_put/3` but one that assumes the `key_or_domains` exist.
   """
-  def map_fetch_and_put(:term, _key, _type), do: :badmap
+  def map_put_existing(:term, _key_or_domains, _type), do: :badmap
 
-  def map_fetch_and_put(descr, key, :term) when is_atom(key),
-    do: map_fetch_and_put_shared(descr, key, :term)
+  def map_put_existing(descr, key_or_domains, :term),
+    do: map_put_existing_shared(descr, key_or_domains, :term)
 
-  def map_fetch_and_put(descr, key, type) when is_atom(key) do
+  def map_put_existing(descr, key_or_domains, type) do
     case :maps.take(:dynamic, type) do
-      :error -> map_fetch_and_put_shared(descr, key, type)
-      {dynamic, _static} -> map_fetch_and_put_shared(dynamic(descr), key, dynamic)
+      :error -> map_put_existing_shared(descr, key_or_domains, type)
+      {dynamic, _static} -> map_put_existing_shared(dynamic(descr), key_or_domains, dynamic)
     end
   end
 
-  defp map_fetch_and_put_shared(descr, key, type) do
-    map_take(descr, key, none(), &map_put_static(&1, key, type))
-  end
-
-  @doc """
-  Puts a `key` of a given type, assuming that the descr is exclusively
-  a map (or dynamic).
-  """
-  def map_put(:term, _key, _type), do: :badmap
-  def map_put(descr, key, :term) when is_atom(key), do: map_put_shared(descr, key, :term)
-
-  def map_put(descr, key, type) when is_atom(key) do
-    case :maps.take(:dynamic, type) do
-      :error -> map_put_shared(descr, key, type)
-      {dynamic, _static} -> map_put_shared(dynamic(descr), key, dynamic)
+  defp map_put_existing_shared(descr, key, type) when is_atom(key) do
+    with {_, type} <- map_take(descr, key, none(), &map_put_static(&1, key, type)) do
+      {:ok, type}
     end
   end
 
-  @doc """
-  Refreshes the type of map after assuming some type was given to a key of a given type.
-  Assuming that the descr is exclusively a map (or dynamic).
-  """
-  # TODO: Figure out how this operation will be used from Elixir
-  def map_refresh(:term, _key, _type), do: :badmap
-
-  def map_refresh(descr, key_descr, type) do
-    {dynamic_descr, static_descr} = Map.pop(descr, :dynamic)
-    key_descr = unfold(key_descr)
-    type = unfold(type)
-
-    cond do
-      # Either 1) static part is a map, or 2) static part is empty and dynamic part contains maps
-      not map_only?(static_descr) ->
-        :badmap
-
-      empty?(static_descr) and not (not is_nil(dynamic_descr) and descr_key?(dynamic_descr, :map)) ->
-        :badmap
+  # TODO: If both descr and domain_keys are static,
+  # this should only succeed if ALL domain keys are present.
+  defp map_put_existing_shared(descr, domain_keys, type) when is_list(domain_keys) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if descr_key?(descr, :map) and map_only?(descr) do
+          case map_existing_domains(descr, domain_keys) do
+            [] -> :badkey
+            domain_keys -> {:ok, map_update_domains(descr, domain_keys, type)}
+          end
+        else
+          :badmap
+        end
 
-      # Either of those three types could be dynamic.
-      not (not is_nil(dynamic_descr) or Map.has_key?(key_descr, :dynamic) or
-               Map.has_key?(type, :dynamic)) ->
-        map_refresh_static(descr, key_descr, type)
+      {dynamic, static} ->
+        if descr_key?(dynamic, :map) and map_only?(static) do
+          case map_existing_domains(dynamic, domain_keys) do
+            [] ->
+              :badkey
 
-      true ->
-        # If one of those is dynamic, we just compute the union
-        {descr_dynamic, descr_static} = Map.pop(descr, :dynamic, descr)
-        {key_dynamic, key_static} = Map.pop(key_descr, :dynamic, key_descr)
-        {type_dynamic, type_static} = Map.pop(type, :dynamic, type)
-
-        with {:ok, new_static} <- map_refresh_static(descr_static, key_static, type_static),
-             {:ok, new_dynamic} <- map_refresh_static(descr_dynamic, key_dynamic, type_dynamic) do
-          {:ok, union(new_static, dynamic(new_dynamic))}
+            domain_keys ->
+              {:ok,
+               union(
+                 dynamic(map_update_domains(dynamic, domain_keys, type)),
+                 map_update_domains(static, domain_keys, type)
+               )}
+          end
+        else
+          :badmap
         end
     end
   end
 
-  def map_refresh_static(%{map: _} = descr, key_descr = %{}, type) do
-    # Check if descr is a valid map,
-    case atom_fetch(key_descr) do
-      # If the key_descr is a singleton, we directly put the type into the map.
-      {:finite, [single_key]} ->
-        map_put(descr, single_key, type)
+  defp map_existing_domains(%{map: bdd}, domain_keys) do
+    dnf = map_bdd_to_dnf(bdd)
 
-      # In this case, we iterate on key_descr to add type to each key type it covers.
-      # Since we do not know which key will be used, we do the union with previous types.
-      _ ->
-        new_descr =
-          key_descr
-          |> covered_key_types()
-          |> Enum.reduce(descr, fn
-            {:atom, atom_key}, acc ->
-              map_refresh_atom(acc, atom_key, type)
-
-            domain_key, acc ->
-              map_refresh_domain(acc, domain_key, type)
-          end)
+    Enum.filter(domain_keys, fn domain_key ->
+      Enum.any?(dnf, fn
+        {:open, _fields, []} ->
+          true
 
-        {:ok, new_descr}
-    end
-  end
+        {:closed, _fields, []} ->
+          false
 
-  def map_refresh_static(:term, _key_descr, _type), do: {:ok, open_map()}
-  def map_refresh_static(_, _, _), do: {:ok, none()}
+        {domains, _fields, []} ->
+          case domains do
+            %{^domain_key => type} -> not empty_or_optional?(type)
+            %{} -> false
+          end
 
-  @doc """
-  Updates a key in a map type by fetching its current type, unioning it with a
-  `new_additional_type`, and then putting the resulting union type back.
-
-  Returns:
-    - `{:ok, new_map_descr}`: If successful.
-    - `:badmap`: If the input `descr` is not a valid map type.
-    - `:badkey`: If the key is considered invalid during the take operation (e.g.,
-      an optional key that resolves to an empty type).
-  """
-  # TODO: Figure out how this operation will be used from Elixir
-  def map_refresh_key(descr, key, new_additional_type) when is_atom(key) do
-    case map_fetch(descr, key) do
-      :badmap ->
-        :badmap
-
-      # Key is not present: we just add the new one and make it optional.
-      :badkey ->
-        with {:ok, descr} <- map_put(descr, key, if_set(new_additional_type)) do
-          descr
-        end
+        {tag_or_domains, fields, negs} ->
+          {fst, snd} = map_pop_domain(tag_or_domains, fields, domain_key)
 
-      {_optional?, current_key_type} ->
-        type_to_put = union(current_key_type, new_additional_type)
+          case map_split_negative_domain(negs, domain_key) do
+            :empty ->
+              false
 
-        case map_fetch_and_put(descr, key, type_to_put) do
-          {_taken_type, new_map_descr} -> new_map_descr
-          # Propagates :badmap or :badkey from map_fetch_and_put
-          error -> error
-        end
-    end
-  end
+            negative ->
+              type =
+                negative
+                |> pair_make_disjoint()
+                |> pair_eliminate_negations_fst(fst, snd)
 
-  def map_refresh_domain(%{map: bdd_leaf(tag, fields)}, domain, type) do
-    %{map: bdd_leaf(map_refresh_tag(tag, domain, type), fields)}
+              not empty_or_optional?(type)
+          end
+      end)
+    end)
   end
 
-  def map_refresh_domain(%{map: bdd}, domain, type) do
+  defp map_update_domains(%{map: bdd}, domain_keys, type) do
     # For negations, we count on the idea that a negation will not remove any
     # type from a domain unless it completely cancels out the type.
     # So for any non-empty map bdd, we just update the domain with the new type,
     # as well as its negations to keep them accurate.
-    %{map: bdd_map(bdd, fn {tag, fields} -> {map_refresh_tag(tag, domain, type), fields} end)}
+    %{
+      map:
+        bdd_map(bdd, fn {tag, fields} -> {map_update_domain(tag, domain_keys, type), fields} end)
+    }
   end
 
-  def map_refresh_atom(descr = %{map: bdd}, atom_key, type) do
-    case atom_key do
-      {:union, keys} ->
-        keys
-        |> :sets.to_list()
-        |> Enum.reduce(descr, fn key, acc -> map_refresh_key(acc, key, type) end)
+  defp map_update_domain(tag_or_domains, domain_keys, type) do
+    case tag_or_domains do
+      :open ->
+        :open
 
-      {:negation, keys} ->
-        # 1) Fetch all the possible keys in the bdd
-        # 2) Get them all, except the ones in neg_atoms
-        considered_keys = map_bdd_to_dnf(bdd) |> map_fetch_all_key_names() |> :sets.subtract(keys)
+      :closed ->
+        Map.from_keys(domain_keys, if_set(type))
 
-        considered_keys
-        |> :sets.to_list()
-        |> Enum.reduce(descr, fn key, acc -> map_refresh_key(acc, key, type) end)
-        |> map_refresh_domain(domain_key(:atom), type)
+      domains = %{} ->
+        Enum.reduce(domain_keys, domains, fn domain_key, acc ->
+          Map.update(acc, domain_key, if_set(type), &union(&1, type))
+        end)
     end
   end
 
-  def map_refresh_tag(tag_or_domains, domain_key, type) do
-    case tag_or_domains do
-      :open -> :open
-      :closed -> %{domain_key => if_set(type)}
-      domains = %{} -> Map.update(domains, domain_key, if_set(type), &union(&1, type))
+  @doc """
+  Puts a `key` of a given type, assuming that the descr is exclusively
+  a map (or dynamic).
+  """
+  def map_put(:term, _key, _type), do: :badmap
+  def map_put(descr, key, :term) when is_atom(key), do: map_put_shared(descr, key, :term)
+
+  def map_put(descr, key, type) when is_atom(key) do
+    case :maps.take(:dynamic, type) do
+      :error -> map_put_shared(descr, key, type)
+      {dynamic, _static} -> map_put_shared(dynamic(descr), key, dynamic)
     end
   end
 
@@ -3028,56 +2991,25 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Returns the list of key types that are covered by the key_descr.
-  # E.g., for `{atom([:ok]), term} or integer()` it returns `[:tuple, :integer]`.
-  # We treat bitmap types as a separate key type.
-  defp covered_key_types(:term), do: @domain_key_types
-
-  defp covered_key_types(key_descr) do
-    for {type_kind, type} <- key_descr, reduce: [] do
-      acc ->
-        cond do
-          type_kind == :atom -> [{:atom, type} | acc]
-          type_kind == :bitmap -> bitmap_to_domain_keys(type) ++ acc
-          not empty?(%{type_kind => type}) -> [domain_key(type_kind) | acc]
-          true -> acc
-        end
-    end
-  end
-
-  defp bitmap_to_domain_keys(bitmap) do
-    [
-      if((bitmap &&& @bit_binary) != 0, do: domain_key(:binary)),
-      if((bitmap &&& @bit_empty_list) != 0, do: domain_key(:empty_list)),
-      if((bitmap &&& @bit_integer) != 0, do: domain_key(:integer)),
-      if((bitmap &&& @bit_float) != 0, do: domain_key(:float)),
-      if((bitmap &&& @bit_pid) != 0, do: domain_key(:pid)),
-      if((bitmap &&& @bit_port) != 0, do: domain_key(:port)),
-      if((bitmap &&& @bit_reference) != 0, do: domain_key(:reference))
-    ]
-    |> Enum.reject(&is_nil/1)
-  end
-
   defp nil_or_type(type), do: union(type, atom([nil]))
 
+  defp unfold_domains(:open), do: Map.from_keys(@domain_key_types, @term_or_optional)
   defp unfold_domains(:closed), do: %{}
-
-  defp unfold_domains(:open),
-    do: Map.new(@domain_key_types, fn domain_key -> {domain_key, @term_or_optional} end)
-
   defp unfold_domains(domains = %{}), do: domains
 
   defp map_get_static(%{map: bdd_leaf(tag_or_domains, fields)}, key_descr) do
     # For each non-empty kind of type in the key_descr, we add the corresponding key domain in a union.
     domains = unfold_domains(tag_or_domains)
 
-    key_descr
-    |> covered_key_types()
-    |> Enum.reduce(none(), fn
-      # Note: we could stop if we reach term_or_optional()
-      {:atom, atom_type}, acc ->
-        map_get_atom([{domains, fields, []}], atom_type) |> union(acc)
+    {key_descr, acc} =
+      case :maps.take(:atom, key_descr) do
+        {atom, key_descr} -> {key_descr, map_get_atom([{domains, fields, []}], atom)}
+        :error -> {key_descr, none()}
+      end
 
+    key_descr
+    |> to_domain_keys()
+    |> Enum.reduce(acc, fn
       key_type, acc ->
         Map.get(domains, key_type, not_set()) |> union(acc)
     end)
@@ -3086,14 +3018,16 @@ defmodule Module.Types.Descr do
   defp map_get_static(%{map: bdd}, key_descr) do
     dnf = map_bdd_to_dnf(bdd)
 
-    key_descr
-    |> covered_key_types()
-    |> Enum.reduce(none(), fn
-      {:atom, atom_type}, acc ->
-        map_get_atom(dnf, atom_type) |> union(acc)
+    {key_descr, acc} =
+      case :maps.take(:atom, key_descr) do
+        {atom, key_descr} -> {key_descr, map_get_atom(dnf, atom)}
+        :error -> {key_descr, none()}
+      end
 
-      domain_key, acc ->
-        map_get_domain(dnf, domain_key) |> union(acc)
+    key_descr
+    |> to_domain_keys()
+    |> Enum.reduce(acc, fn domain_key, acc ->
+      map_get_domain(dnf, domain_key) |> union(acc)
     end)
   end
 
@@ -3132,35 +3066,30 @@ defmodule Module.Types.Descr do
       {:negation, atoms} ->
         # 1) Fetch all the possible keys in the bdd
         # 2) Get them all, except the ones in neg_atoms
-        possible_keys = map_fetch_all_key_names(dnf)
-        considered_keys = :sets.subtract(possible_keys, atoms)
+        all_fields = map_merge_all_fields(dnf)
+        acc = map_get_domain(dnf, domain_key(:atom))
 
-        considered_keys
-        |> :sets.to_list()
-        |> Enum.reduce(none(), fn atom, acc ->
-          {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
+        for {atom, _} <- all_fields, not :sets.is_element(atom, atoms), reduce: acc do
+          acc ->
+            {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
 
-          if static_optional? do
-            union(type, acc) |> nil_or_type() |> if_set()
-          else
-            union(type, acc)
-          end
-        end)
-        |> union(map_get_domain(dnf, domain_key(:atom)))
+            if static_optional? do
+              union(type, acc) |> nil_or_type() |> if_set()
+            else
+              union(type, acc)
+            end
+        end
     end
   end
 
   # Fetch all present keys in a map dnf (including negated ones).
-  defp map_fetch_all_key_names(dnf) do
-    Enum.reduce(dnf, :sets.new(version: 2), fn {_tag, fields, negs}, acc ->
-      keys = :sets.from_list(Map.keys(fields))
-
+  defp map_merge_all_fields(dnf) do
+    Enum.reduce(dnf, %{}, fn {_tag, fields, negs}, acc ->
       # Add all the negative keys
       # Example: %{...} and not %{a: not_set()} makes key :a present in the map
-      Enum.reduce(negs, keys, fn {_tag, neg_fields}, acc ->
-        :sets.from_list(Map.keys(neg_fields)) |> :sets.union(acc)
+      Enum.reduce(negs, Map.merge(acc, fields), fn {_tag, neg_fields}, acc ->
+        Map.merge(acc, neg_fields)
       end)
-      |> :sets.union(acc)
     end)
   end
 
@@ -3209,7 +3138,7 @@ defmodule Module.Types.Descr do
     map_take(descr, key, none(), &intersection_static(&1, open_map([{key, not_set()}])))
   end
 
-  @compile {:inline, map_take: 4}
+  # If initial is nil, note we don't compute the value.
   defp map_take(:term, _key, _initial, _updater), do: :badmap
 
   defp map_take(descr, key, initial, updater) when is_atom(key) do
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 63599357376..0cd092fba80 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -172,58 +172,53 @@ defmodule Module.Types.Expr do
     # allow variables defined on the left side of | to be available
     # on the right side, this is safe.
     {pairs_types, context} =
-      Of.pairs(args, expected, stack, context, &of_expr(&1, &2, expr, &3, &4))
+      Enum.map_reduce(args, context, fn {key, value}, context ->
+        {key_tagged_type, dynamic_key?, context} =
+          Of.map_key_type(key, stack, context, &of_expr(&1, &2, expr, &3, &4))
+
+        {value_type, context} = of_expr(value, term(), expr, stack, context)
+        {{key_tagged_type, dynamic_key? or gradual?(value_type), value_type}, context}
+      end)
 
     expected =
       if stack.mode == :traversal do
         expected
       else
-        # TODO: Once we introduce domain keys, if we ever find a domain
-        # that overlaps atoms, we can only assume optional(atom()) => term(),
-        # which is what the `open_map()` below falls back into anyway.
-        Enum.reduce_while(pairs_types, expected, fn
-          {_, [key], _}, acc ->
-            case map_fetch_and_put(acc, key, term()) do
-              {_value, acc} -> {:cont, acc}
-              _ -> {:halt, open_map()}
-            end
+        # The only information we can attach to the expected types is that
+        # certain keys are expected.
+        #
+        # * If we have a single key, that's straight-forward
+        #
+        # * If we have multiple keys, it may be one or the other,
+        #   so we would need to generate unions, therefore we abort
+        #
+        # * If it is a domain key, then we could say such key is expected,
+        #   but it wouldn't effectively add any new information, so we skip it
+        expected_pairs =
+          Enum.reduce_while(pairs_types, [], fn
+            {{:domain, _}, _, _}, acc -> {:cont, acc}
+            {{:keys, [key]}, _, _}, acc -> {:cont, [{key, term()} | acc]}
+            {_, _, _}, _acc -> {:halt, []}
+          end)
 
-          _, _ ->
-            {:halt, open_map()}
-        end)
+        intersection(expected, open_map(expected_pairs))
       end
 
     {map_type, context} = of_expr(map, expected, expr, stack, context)
 
     try do
-      Of.permutate_map(pairs_types, stack, fn fallback, keys_to_assert, pairs ->
-        # Ensure all keys to assert and all type pairs exist in map
-        keys_to_assert = Enum.map(pairs, &elem(&1, 0)) ++ keys_to_assert
-
-        Enum.each(Enum.map(pairs, &elem(&1, 0)) ++ keys_to_assert, fn key ->
-          case map_fetch(map_type, key) do
-            {_, _} -> :ok
-            :badkey -> throw({:badkey, map_type, key, update, context})
-            :badmap -> throw({:badmap, map_type, update, context})
-          end
-        end)
-
-        # If all keys are known is no fallback (i.e. we know all keys being updated),
-        # we can update the existing map.
-        if fallback == none() do
-          Enum.reduce(pairs, map_type, fn {key, type}, acc ->
-            case map_fetch_and_put(acc, key, type) do
-              {_value, descr} -> descr
-              :badkey -> throw({:badkey, map_type, key, update, context})
+      Of.permutate_map(pairs_types, stack, fn pairs ->
+        Enum.reduce(pairs, map_type, fn {key_or_domains, type}, acc ->
+          if is_atom(key_or_domains) do
+            case map_put_existing(acc, key_or_domains, type) do
+              {:ok, descr} -> descr
+              :badkey -> throw({:badkey, map_type, key_or_domains, update, context})
               :badmap -> throw({:badmap, map_type, update, context})
             end
-          end)
-        else
-          # TODO: Use the fallback type to actually indicate if open or closed.
-          # The fallback must be unioned with the result of map_values with all
-          # `keys` deleted.
-          dynamic(open_map(pairs))
-        end
+          else
+            acc
+          end
+        end)
       end)
     catch
       error -> {error_type(), error(__MODULE__, error, meta, stack, context)}
@@ -240,6 +235,8 @@ defmodule Module.Types.Expr do
         stack,
         context
       ) do
+    # We pass the expected type as `term()` because the struct update
+    # operator already expects it to be a map at this point.
     {map_type, context} = of_expr(map, term(), struct, stack, context)
 
     context =
@@ -259,8 +256,8 @@ defmodule Module.Types.Expr do
       # TODO: Once we support typed structs, we need to type check them here
       {type, context} = of_expr(value, term(), expr, stack, context)
 
-      case map_fetch_and_put(acc, key, type) do
-        {_value, acc} -> {acc, context}
+      case map_put_existing(acc, key, type) do
+        {:ok, acc} -> {acc, context}
         _ -> {acc, context}
       end
     end)
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index be8d23e2d15..ae3cdc1f0d8 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -179,9 +179,8 @@ defmodule Module.Types.Of do
     {pairs_types, context} = pairs(pairs, expected, stack, context, of_fun)
 
     map =
-      permutate_map(pairs_types, stack, fn fallback, _keys, pairs ->
-        # TODO: Use the fallback type to actually indicate if open or closed.
-        if fallback == none(), do: closed_map(pairs), else: dynamic(open_map(pairs))
+      permutate_map(pairs_types, stack, fn pairs ->
+        closed_map(pairs)
       end)
 
     {map, context}
@@ -194,36 +193,40 @@ defmodule Module.Types.Of do
     Enum.map_reduce(pairs, context, fn {key, value}, context ->
       {_key_type, context} = of_fun.(key, term(), stack, context)
       {value_type, context} = of_fun.(value, term(), stack, context)
-      {{true, :none, value_type}, context}
+      {{{:domain, to_domain_keys(:term)}, true, value_type}, context}
     end)
   end
 
   def pairs(pairs, expected, stack, context, of_fun) do
     Enum.map_reduce(pairs, context, fn {key, value}, context ->
-      {dynamic_key?, keys, context} = finite_key_type(key, stack, context, of_fun)
+      {key_tagged_type, dynamic_key?, context} = map_key_type(key, stack, context, of_fun)
 
       expected_value_type =
-        with [key] <- keys, {_, expected_value_type} <- map_fetch(expected, key) do
+        with {:keys, [key]} <- key_tagged_type,
+             {_, expected_value_type} <- map_fetch(expected, key) do
           expected_value_type
         else
           _ -> term()
         end
 
       {value_type, context} = of_fun.(value, expected_value_type, stack, context)
-      {{dynamic_key? or gradual?(value_type), keys, value_type}, context}
+      {{key_tagged_type, dynamic_key? or gradual?(value_type), value_type}, context}
     end)
   end
 
-  defp finite_key_type(key, _stack, context, _of_fun) when is_atom(key) do
-    {false, [key], context}
+  @doc """
+  Returns the type of a map key.
+  """
+  def map_key_type(key, _stack, context, _of_fun) when is_atom(key) do
+    {{:keys, [key]}, false, context}
   end
 
-  defp finite_key_type(key, stack, context, of_fun) do
+  def map_key_type(key, stack, context, of_fun) do
     {key_type, context} = of_fun.(key, term(), stack, context)
 
     case atom_fetch(key_type) do
-      {:finite, list} -> {gradual?(key_type), list, context}
-      _ -> {gradual?(key_type), :none, context}
+      {:finite, list} -> {{:keys, list}, gradual?(key_type), context}
+      _ -> {{:domain, to_domain_keys(key_type)}, gradual?(key_type), context}
     end
   end
 
@@ -235,45 +238,35 @@ defmodule Module.Types.Of do
   end
 
   def permutate_map(pairs_types, _stack, of_map) do
-    {dynamic?, fallback, single, multiple, assert} =
-      Enum.reduce(pairs_types, {false, none(), [], [], []}, fn
-        {dynamic_pair?, keys, value_type}, {dynamic?, fallback, single, multiple, assert} ->
+    {dynamic?, domain, single, multiple} =
+      Enum.reduce(pairs_types, {false, [], [], []}, fn
+        {key_tagged_type, dynamic_pair?, value_type}, {dynamic?, domain, single, multiple} ->
           dynamic? = dynamic? or dynamic_pair?
 
-          case keys do
-            :none ->
-              fallback = union(fallback, value_type)
-
-              {fallback, assert} =
-                Enum.reduce(single, {fallback, assert}, fn {key, type}, {fallback, assert} ->
-                  {union(fallback, type), [key | assert]}
-                end)
-
-              {fallback, assert} =
-                Enum.reduce(multiple, {fallback, assert}, fn {keys, type}, {fallback, assert} ->
-                  {union(fallback, type), keys ++ assert}
-                end)
-
-              {dynamic?, fallback, [], [], assert}
-
+          case key_tagged_type do
             # Because a multiple key may override single keys, we can only
             # collect single keys while there are no multiples.
-            [key] when multiple == [] ->
-              {dynamic?, fallback, [{key, value_type} | single], multiple, assert}
+            {:keys, [key]} when multiple == [] ->
+              {dynamic?, domain, [{key, value_type} | single], multiple}
 
-            keys ->
-              {dynamic?, fallback, single, [{keys, value_type} | multiple], assert}
+            {:keys, keys} ->
+              {dynamic?, domain, single, [{keys, value_type} | multiple]}
+
+            {:domain, keys} ->
+              {dynamic?, [{keys, value_type} | domain], single, multiple}
           end
       end)
 
+    non_multiple = Enum.reverse(single, domain)
+
     map =
       case Enum.reverse(multiple) do
         [] ->
-          of_map.(fallback, Enum.uniq(assert), Enum.reverse(single))
+          of_map.(non_multiple)
 
         [{keys, type} | tail] ->
           for key <- keys, t <- cartesian_map(tail) do
-            of_map.(fallback, Enum.uniq(assert), Enum.reverse(single, [{key, type} | t]))
+            of_map.(non_multiple ++ [{key, type} | t])
           end
           |> Enum.reduce(&union/2)
       end
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 49925d9e8bd..aa7ad871aef 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1835,9 +1835,9 @@ defmodule Module.Types.DescrTest do
       assert equal?(type, open_map(a: not_set()))
     end
 
-    test "map_fetch_and_put" do
-      assert map_fetch_and_put(term(), :a, integer()) == :badmap
-      assert map_fetch_and_put(open_map(), :a, integer()) == :badkey
+    test "map_put_existing" do
+      assert map_put_existing(term(), :a, integer()) == :badmap
+      assert map_put_existing(open_map(), :a, integer()) == :badkey
     end
 
     test "map_put" do
@@ -1908,64 +1908,6 @@ defmodule Module.Types.DescrTest do
       {false, type} = map_fetch(map, :a)
       assert equal?(type, atom())
     end
-
-    test "map_put with domain keys" do
-      # Using a literal key or an expression of that singleton key is the same
-      assert map_refresh(empty_map(), atom([:a]), integer()) == {:ok, closed_map(a: integer())}
-
-      # Several keys
-      assert map_refresh(empty_map(), atom([:a, :b]), integer()) ==
-               {:ok, closed_map(a: if_set(integer()), b: if_set(integer()))}
-
-      assert map_refresh(empty_map(), integer(), integer()) ==
-               {:ok, closed_map([{domain_key(:integer), integer()}])}
-
-      assert map_refresh(closed_map([{domain_key(:integer), integer()}]), integer(), float()) ==
-               {:ok, closed_map([{domain_key(:integer), number()}])}
-
-      assert map_refresh(open_map(), integer(), integer()) == {:ok, open_map()}
-
-      # TODO: Revisit this
-      # {:ok, type} = map_refresh(empty_map(), integer(), dynamic())
-      # assert equal?(type, dynamic(closed_map([{domain_key(:integer), term()}])))
-
-      # Adding a key of type float to a dynamic only guarantees that we have a map
-      # as we cannot express "has at least one key of type float => float"
-      {:ok, type} = map_refresh(dynamic(), float(), float())
-      assert equal?(type, dynamic(open_map()))
-
-      assert closed_map([{domain_key(:integer), integer()}])
-             |> difference(open_map())
-             |> empty?()
-
-      assert closed_map([{domain_key(:integer), integer()}])
-             |> difference(open_map())
-             |> map_refresh(integer(), float()) == :badmap
-
-      assert map_refresh(empty_map(), number(), float()) ==
-               {:ok,
-                closed_map([
-                  {domain_key(:integer), float()},
-                  {domain_key(:float), float()}
-                ])}
-
-      # Tricky cases with atoms:
-      # We add one atom fields that maps to an integer, which is not :a. So we do not touch
-      # :a, add integer to :b, and add a domain field.
-      assert map_refresh(
-               closed_map(a: pid(), b: pid()),
-               atom() |> difference(atom([:a])),
-               integer()
-             ) ==
-               {:ok,
-                closed_map([
-                  {:a, pid()},
-                  {:b, union(pid(), integer())},
-                  {domain_key(:atom), integer()}
-                ])}
-
-      assert map_refresh(empty_map(), term(), integer()) == {:ok, map_with_default(integer())}
-    end
   end
 
   describe "disjoint" do

From ae51b34441b194a255949e143872a5aad2d44648 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Mon, 3 Nov 2025 20:17:07 +0100
Subject: [PATCH 2/9] Fix

---
 lib/elixir/lib/module/types/descr.ex | 39 +++++++---------------------
 1 file changed, 10 insertions(+), 29 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 4992184ea8b..814e854c45a 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -90,7 +90,7 @@ defmodule Module.Types.Descr do
   def atom(as), do: %{atom: atom_new(as)}
   def atom(), do: %{atom: @atom_top}
   def binary(), do: %{bitmap: @bit_binary}
-  def closed_map(pairs), do: map_descr(:closed, pairs, @term_or_optional, false)
+  def closed_map(pairs), do: map_descr(:closed, pairs, term_or_optional(), false)
   def empty_list(), do: %{bitmap: @bit_empty_list}
   def empty_map(), do: %{map: @map_empty}
   def integer(), do: %{bitmap: @bit_integer}
@@ -98,7 +98,7 @@ defmodule Module.Types.Descr do
   def list(type), do: list_descr(type, @empty_list, true)
   def non_empty_list(type, tail \\ @empty_list), do: list_descr(type, tail, false)
   def open_map(), do: %{map: @map_top}
-  def open_map(pairs), do: map_descr(:open, pairs, @term_or_optional, false)
+  def open_map(pairs), do: map_descr(:open, pairs, term_or_optional(), false)
   def open_map(pairs, default), do: map_descr(:open, pairs, if_set(default), true)
   def open_tuple(elements, _fallback \\ term()), do: tuple_descr(:open, elements)
   def pid(), do: %{bitmap: @bit_pid}
@@ -2993,28 +2993,6 @@ defmodule Module.Types.Descr do
 
   defp nil_or_type(type), do: union(type, atom([nil]))
 
-  defp unfold_domains(:open), do: Map.from_keys(@domain_key_types, @term_or_optional)
-  defp unfold_domains(:closed), do: %{}
-  defp unfold_domains(domains = %{}), do: domains
-
-  defp map_get_static(%{map: bdd_leaf(tag_or_domains, fields)}, key_descr) do
-    # For each non-empty kind of type in the key_descr, we add the corresponding key domain in a union.
-    domains = unfold_domains(tag_or_domains)
-
-    {key_descr, acc} =
-      case :maps.take(:atom, key_descr) do
-        {atom, key_descr} -> {key_descr, map_get_atom([{domains, fields, []}], atom)}
-        :error -> {key_descr, none()}
-      end
-
-    key_descr
-    |> to_domain_keys()
-    |> Enum.reduce(acc, fn
-      key_type, acc ->
-        Map.get(domains, key_type, not_set()) |> union(acc)
-    end)
-  end
-
   defp map_get_static(%{map: bdd}, key_descr) do
     dnf = map_bdd_to_dnf(bdd)
 
@@ -3096,16 +3074,19 @@ defmodule Module.Types.Descr do
   # Take a map bdd and return the union of types for the given key domain.
   defp map_get_domain(dnf, domain_key(_) = domain_key) do
     Enum.reduce(dnf, none(), fn
-      {tag, _fields, []}, acc when is_atom(tag) ->
-        map_key_tag_to_type(tag) |> union(acc)
+      {:open, _fields, []}, acc ->
+        union(term_or_optional(), acc)
+
+      {:closed, _fields, []}, acc ->
+        acc
 
       # Optimization: if there are no negatives and domains exists, return its value
       {%{^domain_key => value}, _fields, []}, acc ->
         value |> union(acc)
 
-      # Optimization: if there are no negatives and the key does not exist, return the default type.
-      {domains = %{}, _fields, []}, acc ->
-        map_key_tag_to_type(domains) |> union(acc)
+      # Optimization: if there are no negatives and the key does not exist, skip it
+      {_domains, _fields, []}, acc ->
+        acc
 
       {tag_or_domains, fields, negs}, acc ->
         {fst, snd} = map_pop_domain(tag_or_domains, fields, domain_key)

From 368306e5f924ff993e6981edbd63a1d6a69f308e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Mon, 3 Nov 2025 22:02:58 +0100
Subject: [PATCH 3/9] Rename and reorder

---
 lib/elixir/lib/module/types/apply.ex          |   2 +-
 lib/elixir/lib/module/types/descr.ex          | 313 +++++++++---------
 lib/elixir/lib/module/types/expr.ex           |   4 +-
 lib/elixir/lib/module/types/of.ex             |   6 +-
 lib/elixir/lib/module/types/pattern.ex        |   2 +-
 .../test/elixir/module/types/descr_test.exs   | 126 +++----
 6 files changed, 227 insertions(+), 226 deletions(-)

diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index 147189fa36c..ad82db3831d 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -437,7 +437,7 @@ defmodule Module.Types.Apply do
         empty?(common) and not (number_type?(left) and number_type?(right)) ->
           {:error, :mismatched_comparison}
 
-        match?({false, _}, map_fetch(dynamic(common), :__struct__)) ->
+        match?({false, _}, map_fetch_key(dynamic(common), :__struct__)) ->
           {:error, :struct_comparison}
 
         true ->
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 814e854c45a..2613e99570d 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2668,6 +2668,8 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  ## Map key functions
+
   @doc """
   Fetches the type of the value returned by accessing `key` on `map`
   with the assumption that the descr is exclusively a map (or dynamic).
@@ -2676,13 +2678,13 @@ defmodule Module.Types.Descr do
   if the type is dynamically optional or not, the second element is
   the type. In static mode, optional keys are not allowed.
   """
-  def map_fetch(:term, _key), do: :badmap
+  def map_fetch_key(:term, _key), do: :badmap
 
-  def map_fetch(%{} = descr, key) when is_atom(key) 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_optional?, static_type} = map_fetch_static(descr, key)
+          {static_optional?, static_type} = map_fetch_key_static(descr, key)
 
           if static_optional? or empty?(static_type) do
             :badkey
@@ -2695,8 +2697,8 @@ defmodule Module.Types.Descr do
 
       {dynamic, static} ->
         if descr_key?(dynamic, :map) and map_only?(static) do
-          {dynamic_optional?, dynamic_type} = map_fetch_static(dynamic, key)
-          {static_optional?, static_type} = map_fetch_static(static, key)
+          {dynamic_optional?, dynamic_type} = map_fetch_key_static(dynamic, key)
+          {static_optional?, static_type} = map_fetch_key_static(static, key)
 
           if static_optional? or empty?(dynamic_type) do
             :badkey
@@ -2711,17 +2713,17 @@ defmodule Module.Types.Descr do
 
   # Optimization: if the key does not exist in the map, avoid building
   # if_set/not_set pairs and return the popped value directly.
-  defp map_fetch_static(%{map: bdd_leaf(tag_or_domains, fields)}, key)
+  defp map_fetch_key_static(%{map: bdd_leaf(tag_or_domains, fields)}, key)
        when not is_map_key(fields, key) do
     map_key_tag_to_type(tag_or_domains) |> pop_optional_static()
   end
 
-  defp map_fetch_static(%{map: bdd}, key) do
+  defp map_fetch_key_static(%{map: bdd}, key) do
     map_bdd_to_dnf(bdd) |> map_dnf_fetch_static(key)
   end
 
-  defp map_fetch_static(%{}, _key), do: {false, none()}
-  defp map_fetch_static(:term, _key), do: {true, term()}
+  defp map_fetch_key_static(%{}, _key), do: {false, none()}
+  defp map_fetch_key_static(:term, _key), do: {true, term()}
 
   # Takes a map DNF and returns the union of types it can take for a given key.
   # If the key may be undefined, it will contain the `not_set()` type.
@@ -2752,6 +2754,150 @@ defmodule Module.Types.Descr do
     |> pop_optional_static()
   end
 
+  @doc """
+  Puts a `key` of a given type, assuming that the descr is exclusively
+  a map (or dynamic).
+  """
+  def map_put_key(:term, _key, _type), do: :badmap
+  def map_put_key(descr, key, :term) when is_atom(key), do: map_put_key_shared(descr, key, :term)
+
+  def map_put_key(descr, key, type) when is_atom(key) do
+    case :maps.take(:dynamic, type) do
+      :error -> map_put_key_shared(descr, key, type)
+      {dynamic, _static} -> map_put_key_shared(dynamic(descr), key, dynamic)
+    end
+  end
+
+  defp map_put_key_shared(descr, key, type) do
+    with {nil, descr} <- map_take(descr, key, nil, &map_put_key_static(&1, key, type)) do
+      {:ok, descr}
+    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, type) do
+    bdd = bdd_map(bdd, fn {tag, fields} -> {tag, Map.put(fields, key, type)} end)
+    %{descr | map: bdd}
+  end
+
+  defp map_put_key_static(descr, _key, _type), do: descr
+
+  @doc """
+  Removes a key from a map type.
+  """
+  def map_delete(descr, key) do
+    # We pass nil as the initial value so we can avoid computing the unions.
+    with {nil, descr} <-
+           map_take(descr, key, nil, &intersection_static(&1, open_map([{key, not_set()}]))) do
+      {:ok, descr}
+    end
+  end
+
+  @doc """
+  Removes a key from a map type and return its type.
+
+  ## Algorithm
+
+  1. Split the map type based on the presence of the key.
+  2. Take the second part of the split, which represents the union of all
+     record types where the key has been explicitly removed.
+  3. Intersect this with an open record type where the key is explicitly absent.
+     This step eliminates the key from open record types where it was implicitly present.
+  """
+  def map_take(descr, key) do
+    map_take(descr, key, none(), &intersection_static(&1, open_map([{key, not_set()}])))
+  end
+
+  # If initial is nil, note we don't compute the value.
+  defp map_take(:term, _key, _initial, _updater), do: :badmap
+
+  defp map_take(descr, key, initial, updater) when is_atom(key) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if descr_key?(descr, :map) and map_only?(descr) do
+          {optional?, taken, result} =
+            map_take_static(descr, key, initial)
+
+          cond do
+            taken == nil -> {nil, updater.(result)}
+            optional? or empty?(taken) -> :badkey
+            true -> {taken, updater.(result)}
+          end
+        else
+          :badmap
+        end
+
+      {dynamic, static} ->
+        if descr_key?(dynamic, :map) and map_only?(static) do
+          {_, dynamic_taken, dynamic_result} = map_take_static(dynamic, key, initial)
+          {static_optional?, static_taken, static_result} = map_take_static(static, key, initial)
+          result = union(dynamic(updater.(dynamic_result)), updater.(static_result))
+
+          cond do
+            static_taken == nil and dynamic_taken == nil ->
+              {nil, result}
+
+            static_optional? or empty?(dynamic_taken) ->
+              :badkey
+
+            true ->
+              {union(dynamic(dynamic_taken), static_taken), result}
+          end
+        else
+          :badmap
+        end
+    end
+  end
+
+  # Takes a static map type and removes a key from it.
+  # This allows the key to be put or deleted later on.
+  defp map_take_static(%{map: bdd_leaf(tag, fields)} = descr, key, initial)
+       when not is_map_key(fields, key) do
+    case tag do
+      :open -> {true, maybe_union(initial, fn -> term() end), descr}
+      :closed -> {true, initial, descr}
+    end
+  end
+
+  defp map_take_static(%{map: bdd}, key, initial) do
+    {value, map} =
+      map_bdd_to_dnf(bdd)
+      |> Enum.reduce({initial, none()}, fn
+        # Optimization: if there are no negatives, we can directly remove the key.
+        {tag, fields, []}, {value, map} ->
+          {fst, snd} = map_pop_key(tag, fields, key)
+          {maybe_union(value, fn -> fst end), union(map, snd)}
+
+        {tag, fields, negs}, {value, map} ->
+          {fst, snd} = map_pop_key(tag, fields, key)
+
+          case map_split_negative(negs, key) do
+            :empty ->
+              {value, map}
+
+            negative ->
+              disjoint = pair_make_disjoint(negative)
+
+              {maybe_union(value, fn -> pair_eliminate_negations_fst(disjoint, fst, snd) end),
+               disjoint |> pair_eliminate_negations_snd(fst, snd) |> union(map)}
+          end
+      end)
+
+    if value == nil do
+      {false, value, map}
+    else
+      {optional?, value} = pop_optional_static(value)
+      {optional?, value, map}
+    end
+  end
+
+  # If there is no map part to this static type, there is nothing to delete.
+  defp map_take_static(%{}, _key, initial), do: {false, initial, none()}
+
+  defp map_take_static(:term, _key, initial) do
+    {true, maybe_union(initial, fn -> term() end), open_map()}
+  end
+
   @doc """
   Fetches and puts a `key_or_domains`, assuming that the descr is exclusively
   a map (or dynamic).
@@ -2771,7 +2917,7 @@ defmodule Module.Types.Descr do
   end
 
   defp map_put_existing_shared(descr, key, type) when is_atom(key) do
-    with {_, type} <- map_take(descr, key, none(), &map_put_static(&1, key, type)) do
+    with {_, type} <- map_take(descr, key, none(), &map_put_key_static(&1, key, type)) do
       {:ok, type}
     end
   end
@@ -2871,50 +3017,10 @@ defmodule Module.Types.Descr do
     end
   end
 
-  @doc """
-  Puts a `key` of a given type, assuming that the descr is exclusively
-  a map (or dynamic).
-  """
-  def map_put(:term, _key, _type), do: :badmap
-  def map_put(descr, key, :term) when is_atom(key), do: map_put_shared(descr, key, :term)
-
-  def map_put(descr, key, type) when is_atom(key) do
-    case :maps.take(:dynamic, type) do
-      :error -> map_put_shared(descr, key, type)
-      {dynamic, _static} -> map_put_shared(dynamic(descr), key, dynamic)
-    end
-  end
-
-  defp map_put_shared(descr, key, type) do
-    with {nil, descr} <- map_take(descr, key, nil, &map_put_static(&1, key, type)) do
-      {:ok, descr}
-    end
-  end
-
-  # Directly inserts a key of a given type into every positive and negative map.
-  defp map_put_static(%{map: bdd} = descr, key, type) do
-    bdd = bdd_map(bdd, fn {tag, fields} -> {tag, Map.put(fields, key, type)} end)
-
-    %{descr | map: bdd}
-  end
-
-  defp map_put_static(descr, _key, _type), do: descr
-
-  @doc """
-  Removes a key from a map type.
-  """
-  def map_delete(descr, key) do
-    # We pass nil as the initial value so we can avoid computing the unions.
-    with {nil, descr} <-
-           map_take(descr, key, nil, &intersection_static(&1, open_map([{key, not_set()}]))) do
-      {:ok, descr}
-    end
-  end
-
   @doc """
   Computes the union of types for keys matching `key_type` within the `map_type`.
 
-  This generalizes `map_fetch/2` (which operates on a single literal key) to
+  This generalizes `map_fetch_key/2` (which operates on a single literal key) to
   work with a key type (e.g., `atom()`, `integer()`, `:a or :b`). It's based
   on the map-selection operator t.[t'] described in Section 4.2 of "Typing Records,
   Maps, and Structs" (Castagna et al., ICFP 2023).
@@ -3104,111 +3210,6 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  @doc """
-  Removes a key from a map type and return its type.
-
-  ## Algorithm
-
-  1. Split the map type based on the presence of the key.
-  2. Take the second part of the split, which represents the union of all
-     record types where the key has been explicitly removed.
-  3. Intersect this with an open record type where the key is explicitly absent.
-     This step eliminates the key from open record types where it was implicitly present.
-  """
-  def map_take(descr, key) do
-    map_take(descr, key, none(), &intersection_static(&1, open_map([{key, not_set()}])))
-  end
-
-  # If initial is nil, note we don't compute the value.
-  defp map_take(:term, _key, _initial, _updater), do: :badmap
-
-  defp map_take(descr, key, initial, updater) when is_atom(key) do
-    case :maps.take(:dynamic, descr) do
-      :error ->
-        if descr_key?(descr, :map) and map_only?(descr) do
-          {optional?, taken, result} =
-            map_take_static(descr, key, initial)
-
-          cond do
-            taken == nil -> {nil, updater.(result)}
-            optional? or empty?(taken) -> :badkey
-            true -> {taken, updater.(result)}
-          end
-        else
-          :badmap
-        end
-
-      {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
-          {_, dynamic_taken, dynamic_result} = map_take_static(dynamic, key, initial)
-          {static_optional?, static_taken, static_result} = map_take_static(static, key, initial)
-          result = union(dynamic(updater.(dynamic_result)), updater.(static_result))
-
-          cond do
-            static_taken == nil and dynamic_taken == nil ->
-              {nil, result}
-
-            static_optional? or empty?(dynamic_taken) ->
-              :badkey
-
-            true ->
-              {union(dynamic(dynamic_taken), static_taken), result}
-          end
-        else
-          :badmap
-        end
-    end
-  end
-
-  # Takes a static map type and removes a key from it.
-  # This allows the key to be put or deleted later on.
-  defp map_take_static(%{map: bdd_leaf(tag, fields)} = descr, key, initial)
-       when not is_map_key(fields, key) do
-    case tag do
-      :open -> {true, maybe_union(initial, fn -> term() end), descr}
-      :closed -> {true, initial, descr}
-    end
-  end
-
-  defp map_take_static(%{map: bdd}, key, initial) do
-    {value, map} =
-      map_bdd_to_dnf(bdd)
-      |> Enum.reduce({initial, none()}, fn
-        # Optimization: if there are no negatives, we can directly remove the key.
-        {tag, fields, []}, {value, map} ->
-          {fst, snd} = map_pop_key(tag, fields, key)
-          {maybe_union(value, fn -> fst end), union(map, snd)}
-
-        {tag, fields, negs}, {value, map} ->
-          {fst, snd} = map_pop_key(tag, fields, key)
-
-          case map_split_negative(negs, key) do
-            :empty ->
-              {value, map}
-
-            negative ->
-              disjoint = pair_make_disjoint(negative)
-
-              {maybe_union(value, fn -> pair_eliminate_negations_fst(disjoint, fst, snd) end),
-               disjoint |> pair_eliminate_negations_snd(fst, snd) |> union(map)}
-          end
-      end)
-
-    if value == nil do
-      {false, value, map}
-    else
-      {optional?, value} = pop_optional_static(value)
-      {optional?, value, map}
-    end
-  end
-
-  # If there is no map part to this static type, there is nothing to delete.
-  defp map_take_static(%{}, _key, initial), do: {false, initial, none()}
-
-  defp map_take_static(:term, _key, initial) do
-    {true, maybe_union(initial, fn -> term() end), open_map()}
-  end
-
   defp non_empty_map_literals_intersection(maps) do
     try do
       Enum.reduce(maps, {:open, %{}}, fn {next_tag, next_fields}, {tag, fields} ->
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 0cd092fba80..e0d2e91c850 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -243,7 +243,7 @@ defmodule Module.Types.Expr do
       if stack.mode == :traversal do
         context
       else
-        with {false, struct_key_type} <- map_fetch(map_type, :__struct__),
+        with {false, struct_key_type} <- map_fetch_key(map_type, :__struct__),
              {:finite, [^module]} <- atom_fetch(struct_key_type) do
           context
         else
@@ -256,7 +256,7 @@ defmodule Module.Types.Expr do
       # TODO: Once we support typed structs, we need to type check them here
       {type, context} = of_expr(value, term(), expr, stack, context)
 
-      case map_put_existing(acc, key, type) do
+      case map_put_key(acc, key, type) do
         {:ok, acc} -> {acc, context}
         _ -> {acc, context}
       end
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index ae3cdc1f0d8..82cab17519e 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -163,7 +163,7 @@ defmodule Module.Types.Of do
   Handles fetching a map key.
   """
   def map_fetch(expr, type, field, stack, context) when is_atom(field) do
-    case map_fetch(type, field) do
+    case map_fetch_key(type, field) do
       {_optional?, value_type} ->
         {value_type, context}
 
@@ -203,7 +203,7 @@ defmodule Module.Types.Of do
 
       expected_value_type =
         with {:keys, [key]} <- key_tagged_type,
-             {_, expected_value_type} <- map_fetch(expected, key) do
+             {_, expected_value_type} <- map_fetch_key(expected, key) do
           expected_value_type
         else
           _ -> term()
@@ -297,7 +297,7 @@ defmodule Module.Types.Of do
       Enum.map_reduce(args, context, fn {key, value}, context when is_atom(key) ->
         value_type =
           with true <- mode != :traversal,
-               {_, expected_value_type} <- map_fetch(expected, key) do
+               {_, expected_value_type} <- map_fetch_key(expected, key) do
             expected_value_type
           else
             _ -> term()
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 5cbedfb17bd..792b41921be 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -292,7 +292,7 @@ defmodule Module.Types.Pattern do
 
   defp of_pattern_var([{:key, field} | rest], type, reachable_var?, info, context)
        when is_atom(field) do
-    case map_fetch(type, field) do
+    case map_fetch_key(type, field) do
       {_optional?, type} -> of_pattern_var(rest, type, reachable_var?, info, context)
       _reason -> :error
     end
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index aa7ad871aef..0c73642dcd1 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -580,11 +580,11 @@ defmodule Module.Types.DescrTest do
       t_diff = difference(a_number, atom_to_float)
 
       # Removing atom keys that map to float, make the :a key point to integer only.
-      assert map_fetch(t_diff, :a) == {false, integer()}
+      assert map_fetch_key(t_diff, :a) == {false, integer()}
       # %{a => number, atom => pid} and not %{atom => float} gives numbers on :a
-      assert map_fetch(difference(a_number_and_pids, atom_to_float), :a) == {false, number()}
+      assert map_fetch_key(difference(a_number_and_pids, atom_to_float), :a) == {false, number()}
 
-      assert map_fetch(t_diff, :foo) == :badkey
+      assert map_fetch_key(t_diff, :foo) == :badkey
 
       assert subtype?(a_number, atom_to_term)
       refute subtype?(a_number, atom_to_float)
@@ -1529,53 +1529,55 @@ defmodule Module.Types.DescrTest do
       end)
     end
 
-    test "map_fetch" do
-      assert map_fetch(term(), :a) == :badmap
-      assert map_fetch(union(open_map(), integer()), :a) == :badmap
-      assert map_fetch(difference(open_map(), open_map()), :a) == :badmap
-      assert map_fetch(difference(closed_map(a: integer()), closed_map(a: term())), :a) == :badmap
+    test "map_fetch_key" do
+      assert map_fetch_key(term(), :a) == :badmap
+      assert map_fetch_key(union(open_map(), integer()), :a) == :badmap
+      assert map_fetch_key(difference(open_map(), open_map()), :a) == :badmap
 
-      assert map_fetch(open_map(), :a) == :badkey
-      assert map_fetch(open_map(a: not_set()), :a) == :badkey
-      assert map_fetch(union(closed_map(a: integer()), closed_map(b: atom())), :a) == :badkey
+      assert map_fetch_key(difference(closed_map(a: integer()), closed_map(a: term())), :a) ==
+               :badmap
 
-      assert map_fetch(closed_map(a: integer()), :a) == {false, integer()}
+      assert map_fetch_key(open_map(), :a) == :badkey
+      assert map_fetch_key(open_map(a: not_set()), :a) == :badkey
+      assert map_fetch_key(union(closed_map(a: integer()), closed_map(b: atom())), :a) == :badkey
 
-      assert map_fetch(union(closed_map(a: integer()), closed_map(a: atom())), :a) ==
+      assert map_fetch_key(closed_map(a: integer()), :a) == {false, integer()}
+
+      assert map_fetch_key(union(closed_map(a: integer()), closed_map(a: atom())), :a) ==
                {false, union(integer(), atom())}
 
       {false, value_type} =
         open_map(my_map: open_map(foo: integer()))
         |> intersection(open_map(my_map: open_map(bar: boolean())))
-        |> map_fetch(:my_map)
+        |> map_fetch_key(:my_map)
 
       assert equal?(value_type, open_map(foo: integer(), bar: boolean()))
 
       {false, value_type} =
         closed_map(a: union(integer(), atom()))
         |> difference(open_map(a: integer()))
-        |> map_fetch(:a)
+        |> map_fetch_key(:a)
 
       assert equal?(value_type, atom())
 
       {false, value_type} =
         closed_map(a: integer(), b: atom())
         |> difference(closed_map(a: integer(), b: atom([:foo])))
-        |> map_fetch(:a)
+        |> map_fetch_key(:a)
 
       assert equal?(value_type, integer())
 
       {false, value_type} =
         closed_map(a: integer())
         |> difference(closed_map(a: atom()))
-        |> map_fetch(:a)
+        |> map_fetch_key(:a)
 
       assert equal?(value_type, integer())
 
       {false, value_type} =
         open_map(a: integer(), b: atom())
         |> union(closed_map(a: tuple()))
-        |> map_fetch(:a)
+        |> map_fetch_key(:a)
 
       assert equal?(value_type, union(integer(), tuple()))
 
@@ -1583,47 +1585,48 @@ defmodule Module.Types.DescrTest do
         closed_map(a: atom())
         |> difference(closed_map(a: atom([:foo, :bar])))
         |> difference(closed_map(a: atom([:bar])))
-        |> map_fetch(:a)
+        |> map_fetch_key(:a)
 
       assert equal?(value_type, intersection(atom(), negation(atom([:foo, :bar]))))
 
       assert closed_map(a: union(atom([:ok]), pid()), b: integer(), c: tuple())
              |> difference(open_map(a: atom([:ok]), b: integer()))
              |> difference(open_map(a: atom(), c: tuple()))
-             |> map_fetch(:a) == {false, pid()}
+             |> map_fetch_key(:a) == {false, pid()}
 
       assert closed_map(a: union(atom([:foo]), pid()), b: integer(), c: tuple())
              |> difference(open_map(a: atom([:foo]), b: integer()))
              |> difference(open_map(a: atom(), c: tuple()))
-             |> map_fetch(:a) == {false, pid()}
+             |> map_fetch_key(:a) == {false, pid()}
 
       assert closed_map(a: union(atom([:foo, :bar, :baz]), integer()))
              |> difference(open_map(a: atom([:foo, :bar])))
              |> difference(open_map(a: atom([:foo, :baz])))
-             |> map_fetch(:a) == {false, integer()}
+             |> map_fetch_key(:a) == {false, integer()}
     end
 
-    test "map_fetch with dynamic" do
-      assert map_fetch(dynamic(), :a) == {true, dynamic()}
-      assert map_fetch(union(dynamic(), integer()), :a) == :badmap
-      assert map_fetch(union(dynamic(open_map(a: integer())), integer()), :a) == :badmap
-      assert map_fetch(union(dynamic(integer()), integer()), :a) == :badmap
+    test "map_fetch_key with dynamic" do
+      assert map_fetch_key(dynamic(), :a) == {true, dynamic()}
+      assert map_fetch_key(union(dynamic(), integer()), :a) == :badmap
+      assert map_fetch_key(union(dynamic(open_map(a: integer())), integer()), :a) == :badmap
+      assert map_fetch_key(union(dynamic(integer()), integer()), :a) == :badmap
 
       assert intersection(dynamic(), open_map(a: integer()))
-             |> map_fetch(:a) == {false, intersection(integer(), dynamic())}
+             |> map_fetch_key(:a) == {false, intersection(integer(), dynamic())}
 
-      {false, type} = union(dynamic(integer()), open_map(a: integer())) |> map_fetch(:a)
+      {false, type} = union(dynamic(integer()), open_map(a: integer())) |> map_fetch_key(:a)
       assert equal?(type, integer())
 
-      assert union(dynamic(integer()), open_map(a: if_set(integer()))) |> map_fetch(:a) == :badkey
+      assert union(dynamic(integer()), open_map(a: if_set(integer()))) |> map_fetch_key(:a) ==
+               :badkey
 
       assert union(dynamic(open_map(a: atom())), open_map(a: integer()))
-             |> map_fetch(:a) == {false, union(dynamic(atom()), integer())}
+             |> map_fetch_key(:a) == {false, union(dynamic(atom()), integer())}
     end
 
-    test "map_fetch with domain keys" do
+    test "map_fetch_key with domain keys" do
       integer_to_atom = open_map([{domain_key(:integer), atom()}])
-      assert map_fetch(integer_to_atom, :foo) == :badkey
+      assert map_fetch_key(integer_to_atom, :foo) == :badkey
 
       # the key :a is for sure of type pid and exists in type
       # %{atom() => pid()} and not %{:a => not_set()}
@@ -1632,24 +1635,24 @@ defmodule Module.Types.DescrTest do
       t3 = open_map(a: not_set())
 
       # Indeed, t2 is equivalent to the empty map
-      assert map_fetch(difference(t1, t2), :a) == :badkey
-      assert map_fetch(difference(t1, t3), :a) == {false, pid()}
+      assert map_fetch_key(difference(t1, t2), :a) == :badkey
+      assert map_fetch_key(difference(t1, t3), :a) == {false, pid()}
 
       t4 = closed_map([{domain_key(:pid), atom()}])
-      assert map_fetch(difference(t1, t4) |> difference(t3), :a) == {false, pid()}
+      assert map_fetch_key(difference(t1, t4) |> difference(t3), :a) == {false, pid()}
 
-      assert map_fetch(closed_map([{domain_key(:atom), pid()}]), :a) == :badkey
+      assert map_fetch_key(closed_map([{domain_key(:atom), pid()}]), :a) == :badkey
 
-      assert map_fetch(dynamic(closed_map([{domain_key(:atom), pid()}])), :a) ==
+      assert map_fetch_key(dynamic(closed_map([{domain_key(:atom), pid()}])), :a) ==
                {true, dynamic(pid())}
 
       assert closed_map([{domain_key(:atom), number()}])
              |> difference(open_map(a: if_set(integer())))
-             |> map_fetch(:a) == {false, float()}
+             |> map_fetch_key(:a) == {false, float()}
 
       assert closed_map([{domain_key(:atom), number()}])
              |> difference(closed_map(b: if_set(integer())))
-             |> map_fetch(:a) == :badkey
+             |> map_fetch_key(:a) == :badkey
     end
 
     test "map_get with domain keys" do
@@ -1719,6 +1722,7 @@ defmodule Module.Types.DescrTest do
                {:ok, union(atom([:b]), pid() |> nil_or_type())}
     end
 
+    # TODO: needs to be rewritten to key types
     test "map_delete" do
       assert map_delete(term(), :a) == :badmap
       assert map_delete(integer(), :a) == :badmap
@@ -1781,6 +1785,7 @@ defmodule Module.Types.DescrTest do
              |> equal?(closed_map(a: not_set(), b: atom(), atom: pid()))
     end
 
+    # TODO: needs to be rewritten to key types
     test "map_take" do
       assert map_take(term(), :a) == :badmap
       assert map_take(integer(), :a) == :badmap
@@ -1835,36 +1840,31 @@ defmodule Module.Types.DescrTest do
       assert equal?(type, open_map(a: not_set()))
     end
 
-    test "map_put_existing" do
-      assert map_put_existing(term(), :a, integer()) == :badmap
-      assert map_put_existing(open_map(), :a, integer()) == :badkey
-    end
-
-    test "map_put" do
-      assert map_put(term(), :a, integer()) == :badmap
-      assert map_put(integer(), :a, integer()) == :badmap
-      assert map_put(dynamic(integer()), :a, atom()) == :badmap
-      assert map_put(union(integer(), dynamic()), :a, atom()) == :badmap
-      assert map_put(empty_map(), :a, integer()) == {:ok, closed_map(a: integer())}
+    test "map_put_key" do
+      assert map_put_key(term(), :a, integer()) == :badmap
+      assert map_put_key(integer(), :a, integer()) == :badmap
+      assert map_put_key(dynamic(integer()), :a, atom()) == :badmap
+      assert map_put_key(union(integer(), dynamic()), :a, atom()) == :badmap
+      assert map_put_key(empty_map(), :a, integer()) == {:ok, closed_map(a: integer())}
 
       # Replace an existing key in a closed map
-      assert map_put(closed_map(a: integer()), :a, atom()) == {:ok, closed_map(a: atom())}
+      assert map_put_key(closed_map(a: integer()), :a, atom()) == {:ok, closed_map(a: atom())}
 
       # Add a new key to a closed map
-      assert map_put(closed_map(a: integer()), :b, atom()) ==
+      assert map_put_key(closed_map(a: integer()), :b, atom()) ==
                {:ok, closed_map(a: integer(), b: atom())}
 
       # Replace an existing key in an open map
-      assert map_put(open_map(a: integer()), :a, atom()) ==
+      assert map_put_key(open_map(a: integer()), :a, atom()) ==
                {:ok, open_map(a: atom())}
 
       # Add a new key to an open map
-      assert map_put(open_map(a: integer()), :b, atom()) ==
+      assert map_put_key(open_map(a: integer()), :b, atom()) ==
                {:ok, open_map(a: integer(), b: atom())}
 
       # Put a key-value pair in a union of maps
       {:ok, type} =
-        union(closed_map(a: integer()), closed_map(b: atom())) |> map_put(:c, boolean())
+        union(closed_map(a: integer()), closed_map(b: atom())) |> map_put_key(:c, boolean())
 
       assert equal?(
                type,
@@ -1875,17 +1875,17 @@ defmodule Module.Types.DescrTest do
              )
 
       # Put a key-value pair in a dynamic map
-      assert map_put(dynamic(open_map()), :a, integer()) ==
+      assert map_put_key(dynamic(open_map()), :a, integer()) ==
                {:ok, dynamic(open_map(a: integer()))}
 
       # Put a key-value pair in an intersection of maps
       {:ok, type} =
-        intersection(open_map(a: integer()), open_map(b: atom())) |> map_put(:c, boolean())
+        intersection(open_map(a: integer()), open_map(b: atom())) |> map_put_key(:c, boolean())
 
       assert equal?(type, open_map(a: integer(), b: atom(), c: boolean()))
 
       # Put a key-value pair in a difference of maps
-      {:ok, type} = difference(open_map(), closed_map(a: integer())) |> map_put(:b, atom())
+      {:ok, type} = difference(open_map(), closed_map(a: integer())) |> map_put_key(:b, atom())
 
       type2 = difference(open_map(b: atom()), closed_map(a: integer()))
       diff = difference(type, type2)
@@ -1897,15 +1897,15 @@ defmodule Module.Types.DescrTest do
 
       # Put a new key-value pair with dynamic type
       # Note: setting a field to a dynamic type makes the whole map become dynamic.
-      assert map_put(open_map(), :a, dynamic()) == {:ok, dynamic(open_map(a: term()))}
+      assert map_put_key(open_map(), :a, dynamic()) == {:ok, dynamic(open_map(a: term()))}
 
       # Put a key-value pair in a map with optional fields
-      {:ok, type} = closed_map(a: if_set(integer())) |> map_put(:b, atom())
+      {:ok, type} = closed_map(a: if_set(integer())) |> map_put_key(:b, atom())
       assert equal?(type, closed_map(a: if_set(integer()), b: atom()))
 
       # Fetching on a key-value pair that was put to a given type returns {false, type}
-      {:ok, map} = map_put(union(dynamic(), empty_map()), :a, atom())
-      {false, type} = map_fetch(map, :a)
+      {:ok, map} = map_put_key(union(dynamic(), empty_map()), :a, atom())
+      {false, type} = map_fetch_key(map, :a)
       assert equal?(type, atom())
     end
   end

From f0cc63fac1566ddc74e052509dd4447d841eb17d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 11:03:13 +0100
Subject: [PATCH 4/9] WIP

---
 lib/elixir/lib/module/types/descr.ex | 335 +++++++++++++++++----------
 1 file changed, 213 insertions(+), 122 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 2613e99570d..73879ab3d03 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2292,6 +2292,7 @@ defmodule Module.Types.Descr do
     for {type_kind, type} <- key_descr, reduce: [] do
       acc ->
         cond do
+          type_kind == :atom and match?({:union, _}, type) -> acc
           type_kind == :bitmap -> bitmap_to_domain_keys(type, acc)
           not empty?(%{type_kind => type}) -> [domain_key(type_kind) | acc]
           true -> acc
@@ -2851,18 +2852,22 @@ defmodule Module.Types.Descr do
 
   # Takes a static map type and removes a key from it.
   # This allows the key to be put or deleted later on.
-  defp map_take_static(%{map: bdd_leaf(tag, fields)} = descr, key, initial)
-       when not is_map_key(fields, key) do
-    case tag do
-      :open -> {true, maybe_union(initial, fn -> term() end), descr}
-      :closed -> {true, initial, descr}
-    end
+  defp map_take_static(%{map: bdd}, key, initial) do
+    map_dnf_take_static(map_bdd_to_dnf(bdd), key, initial)
   end
 
-  defp map_take_static(%{map: bdd}, key, initial) do
-    {value, map} =
-      map_bdd_to_dnf(bdd)
-      |> Enum.reduce({initial, none()}, fn
+  # If there is no map part to this static type, there is nothing to delete.
+  defp map_take_static(%{}, _key, initial) do
+    {false, initial, none()}
+  end
+
+  defp map_take_static(:term, _key, initial) do
+    {true, maybe_union(initial, fn -> term() end), open_map()}
+  end
+
+  defp map_dnf_take_static(dnf, key, initial) do
+    {value, descr} =
+      Enum.reduce(dnf, {initial, none()}, fn
         # Optimization: if there are no negatives, we can directly remove the key.
         {tag, fields, []}, {value, map} ->
           {fst, snd} = map_pop_key(tag, fields, key)
@@ -2884,20 +2889,14 @@ defmodule Module.Types.Descr do
       end)
 
     if value == nil do
-      {false, value, map}
+      # The boolean is unused when value is nil
+      {true, value, descr}
     else
       {optional?, value} = pop_optional_static(value)
-      {optional?, value, map}
+      {optional?, value, descr}
     end
   end
 
-  # If there is no map part to this static type, there is nothing to delete.
-  defp map_take_static(%{}, _key, initial), do: {false, initial, none()}
-
-  defp map_take_static(:term, _key, initial) do
-    {true, maybe_union(initial, fn -> term() end), open_map()}
-  end
-
   @doc """
   Fetches and puts a `key_or_domains`, assuming that the descr is exclusively
   a map (or dynamic).
@@ -2922,38 +2921,99 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # TODO: If both descr and domain_keys are static,
-  # this should only succeed if ALL domain keys are present.
-  defp map_put_existing_shared(descr, domain_keys, type) when is_list(domain_keys) do
-    case :maps.take(:dynamic, descr) do
-      :error ->
-        if descr_key?(descr, :map) and map_only?(descr) do
-          case map_existing_domains(descr, domain_keys) do
-            [] -> :badkey
-            domain_keys -> {:ok, map_update_domains(descr, domain_keys, type)}
-          end
-        else
-          :badmap
-        end
-
-      {dynamic, static} ->
-        if descr_key?(dynamic, :map) and map_only?(static) do
-          case map_existing_domains(dynamic, domain_keys) do
-            [] ->
-              :badkey
-
-            domain_keys ->
-              {:ok,
-               union(
-                 dynamic(map_update_domains(dynamic, domain_keys, type)),
-                 map_update_domains(static, domain_keys, type)
-               )}
-          end
-        else
-          :badmap
-        end
-    end
-  end
+  # def map_update(:term, key_descr, _type), do: :badmap
+
+  # def map_update(descr, key_descr, :term),
+  #   do: map_update_shared(descr, key_descr, :term)
+
+  # def map_update(descr, key_descr, type) do
+  #   case :maps.take(:dynamic, type) do
+  #     :error -> map_update_shared(descr, key_descr, type)
+  #     {dynamic, _static} -> map_update_shared(dynamic(descr), key_descr, dynamic)
+  #   end
+  # end
+
+  # defp map_update_shared(descr, key_descr, type) do
+  #   key_descr = upper_bound(key_descr)
+
+  #   case :maps.take(:dynamic, descr) do
+  #     :error ->
+  #       if descr_key?(descr, :map) and map_only?(descr) do
+  #         case map_existing_domains(descr, domain_keys) do
+  #           [] -> :badkey
+  #           domain_keys -> {:ok, map_update_domains(descr, domain_keys, type)}
+  #         end
+  #       else
+  #         :badmap
+  #       end
+
+  #     {dynamic, static} ->
+  #       if descr_key?(dynamic, :map) and map_only?(static) do
+  #         case map_existing_domains(dynamic, domain_keys) do
+  #           [] ->
+  #             :badkey
+
+  #           domain_keys ->
+  #             {:ok,
+  #              union(
+  #                dynamic(map_update_domains(dynamic, domain_keys, type)),
+  #                map_update_domains(static, domain_keys, type)
+  #              )}
+  #         end
+  #       else
+  #         :badmap
+  #       end
+  #   end
+  # end
+
+  # defp map_update_static(%{map: bdd}, key_descr, type) do
+  #   dnf = map_bdd_to_dnf(bdd)
+  #   {keys, key_descr} = map_split_keys(key_descr, bdd)
+  #   {optional, value, descr} = map_update_keys(dnf, keys, type)
+
+  #   key_descr
+  #   |> to_domain_keys()
+  #   |> Enum.reduce({optional, value, descr}, fn domain_key, acc ->
+  #     map_update_domain(dnf, domain_key) |> union(acc)
+  #   end)
+  # end
+
+  # defp map_update_static(%{}, _key_descr, _type) do
+  #   # No optional keys, no returned value, none is returned
+  #   {none(), none(), none()}
+  # end
+
+  # defp map_update_static(:term, key_descr, _type) do
+  #   # The whole key_descr is optional, returned value is term, open map is returned
+  #   {key_descr, term(), open_map()}
+  # end
+
+  # defp map_update_keys(dnf, keys, type) do
+  #   Enum.reduce(keys, {none(), none(), none()}, fn atom, {optional, value, acc} ->
+  #     {optional?, value, descr} = map_dnf_take_static(dnf, atom, value)
+  #     optional = if optional?, do: union(optional, atom([atom])), else: optional
+  #     descr = union(map_put_key_static(descr, atom, type), acc)
+  #     {optional, value, descr}
+  #   end)
+  # end
+
+  # defp map_update_atom_negation(%{atom: {:negation, atoms}} = descr, type) do
+  #   # 1) Fetch all the possible keys in the bdd
+  #   # 2) Get them all, except the ones in neg_atoms
+  #   all_fields = map_merge_all_fields(dnf)
+  #   acc = map_get_domain(dnf, domain_key(:atom))
+
+  #   for {atom, _} <- all_fields, not :sets.is_element(atom, atoms), reduce: acc do
+  #     acc ->
+  #       {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
+
+  #       if static_optional? do
+  #         union(type, acc) |> nil_or_type() |> if_set()
+  #       else
+  #         union(type, acc)
+  #       end
+  #   end
+  # end
 
   defp map_existing_domains(%{map: bdd}, domain_keys) do
     dnf = map_bdd_to_dnf(bdd)
@@ -3062,10 +3122,12 @@ defmodule Module.Types.Descr do
   def map_get(:term, _key_descr), do: :badmap
 
   def map_get(%{} = descr, key_descr) do
+    split_keys = map_split_keys(key_descr)
+
     case :maps.take(:dynamic, descr) do
       :error ->
         if descr_key?(descr, :map) and map_only?(descr) do
-          {optional?, type_selected} = map_get_static(descr, key_descr) |> pop_optional_static()
+          {optional?, type_selected} = map_get_static(descr, split_keys) |> pop_optional_static()
 
           cond do
             empty?(type_selected) -> {:ok_absent, atom([nil])}
@@ -3079,10 +3141,10 @@ defmodule Module.Types.Descr do
       {dynamic, static} ->
         if descr_key?(dynamic, :map) and map_only?(static) do
           {optional_dynamic?, dynamic_type} =
-            map_get_static(dynamic, key_descr) |> pop_optional_static()
+            map_get_static(dynamic, split_keys) |> pop_optional_static()
 
           {optional_static?, static_type} =
-            map_get_static(static, key_descr) |> pop_optional_static()
+            map_get_static(static, split_keys) |> pop_optional_static()
 
           type_selected = union(dynamic(dynamic_type), static_type)
 
@@ -3099,87 +3161,39 @@ defmodule Module.Types.Descr do
 
   defp nil_or_type(type), do: union(type, atom([nil]))
 
-  defp map_get_static(%{map: bdd}, key_descr) do
+  defp map_get_static(%{map: bdd}, split_keys) do
     dnf = map_bdd_to_dnf(bdd)
 
-    {key_descr, acc} =
-      case :maps.take(:atom, key_descr) do
-        {atom, key_descr} -> {key_descr, map_get_atom(dnf, atom)}
-        :error -> {key_descr, none()}
-      end
+    {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
+      split_keys
 
-    key_descr
-    |> to_domain_keys()
-    |> Enum.reduce(acc, fn domain_key, acc ->
-      map_get_domain(dnf, domain_key) |> union(acc)
-    end)
+    acc = none()
+    acc = map_get_keys(dnf, required_keys, acc)
+    acc = map_get_keys(dnf, optional_keys, acc)
+    acc = map_get_keys(dnf, map_materialize_negated_set(maybe_negated_set, bdd), acc)
+    acc = Enum.reduce(required_domains, acc, &map_get_domain(dnf, &1, &2))
+    acc = Enum.reduce(optional_domains, acc, &map_get_domain(dnf, &1, &2))
+    acc
   end
 
   defp map_get_static(%{}, _key), do: not_set()
   defp map_get_static(:term, _key), do: term_or_optional()
 
-  # Given a map dnf return the union of types for a given atom type. Handles two cases:
-  # 1. A union of atoms (e.g., `{:union, atoms}`):
-  #    - Iterates through each atom in the union.
-  #    - Fetches the type for each atom and combines them into a union.
-  #
-  # 2. A negation of atoms (e.g., `{:negation, atoms}`):
-  #    - Fetches all possible keys in the map's DNF.
-  #    - Excludes the negated atoms from the considered keys.
-  #    - Includes the domain of all atoms in the map's DNF.
-  #
-  # Example:
-  #   Fetching a key of type `atom() and not (:a)` from a map of type
-  #   `%{a: atom(), b: float(), atom() => pid()}`
-  #   would return either `nil` or `float()` (key `:b`) or `pid()` (key `atom()`), but not `atom()` (key `:a`).
-  defp map_get_atom(dnf, atom_type) do
-    case atom_type do
-      {:union, atoms} ->
-        atoms
-        |> :sets.to_list()
-        |> Enum.reduce(none(), fn atom, acc ->
-          {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
+  defp map_get_keys(dnf, keys, acc) do
+    Enum.reduce(keys, acc, fn atom, acc ->
+      {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
 
-          if static_optional? do
-            union(type, acc) |> nil_or_type() |> if_set()
-          else
-            union(type, acc)
-          end
-        end)
-
-      {:negation, atoms} ->
-        # 1) Fetch all the possible keys in the bdd
-        # 2) Get them all, except the ones in neg_atoms
-        all_fields = map_merge_all_fields(dnf)
-        acc = map_get_domain(dnf, domain_key(:atom))
-
-        for {atom, _} <- all_fields, not :sets.is_element(atom, atoms), reduce: acc do
-          acc ->
-            {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
-
-            if static_optional? do
-              union(type, acc) |> nil_or_type() |> if_set()
-            else
-              union(type, acc)
-            end
-        end
-    end
-  end
-
-  # Fetch all present keys in a map dnf (including negated ones).
-  defp map_merge_all_fields(dnf) do
-    Enum.reduce(dnf, %{}, fn {_tag, fields, negs}, acc ->
-      # Add all the negative keys
-      # Example: %{...} and not %{a: not_set()} makes key :a present in the map
-      Enum.reduce(negs, Map.merge(acc, fields), fn {_tag, neg_fields}, acc ->
-        Map.merge(acc, neg_fields)
-      end)
+      if static_optional? do
+        union(type, acc) |> nil_or_type() |> if_set()
+      else
+        union(type, acc)
+      end
     end)
   end
 
   # Take a map bdd and return the union of types for the given key domain.
-  defp map_get_domain(dnf, domain_key(_) = domain_key) do
-    Enum.reduce(dnf, none(), fn
+  defp map_get_domain(dnf, domain_key(_) = domain_key, acc) do
+    Enum.reduce(dnf, acc, fn
       {:open, _fields, []}, acc ->
         union(term_or_optional(), acc)
 
@@ -3210,6 +3224,63 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  defp map_materialize_negated_set(nil, _bdd), do: []
+
+  defp map_materialize_negated_set(set, bdd) do
+    all_fields = bdd_reduce(bdd, %{}, fn {_, fields}, acc -> Map.merge(fields, acc) end)
+    for {atom, _} <- all_fields, not :sets.is_element(atom, set), do: atom
+  end
+
+  # Compute which keys are optional, which ones are required, as well as domain keys
+  defp map_split_keys(%{dynamic: dynamic} = static) do
+    {required_keys, optional_keys, maybe_negated_set} =
+      case {static, dynamic} do
+        {%{atom: {:union, static_union}}, %{atom: {:union, dynamic_union}}} ->
+          # The static union is required, extract them from optional
+          {:sets.to_list(static_union),
+           :sets.to_list(:sets.subtract(dynamic_union, static_union)), nil}
+
+        {%{atom: {:union, static_union}}, %{atom: {:negation, dynamic_negation}}} ->
+          # The static union will already be checked, merge them into the negation
+          {:sets.to_list(static_union), [], :sets.union(dynamic_negation, static_union)}
+
+        {%{atom: {:union, static_union}}, _} ->
+          {:sets.to_list(static_union), [], nil}
+
+        {%{atom: {:negation, static_negation}}, %{atom: {:union, dynamic_union}}} ->
+          # The dynamic union will already be checked, merge them into the negation
+          {[], :sets.to_list(dynamic_union), :sets.union(static_negation, dynamic_union)}
+
+        {%{atom: {:negation, static_negation}}, %{atom: {:negation, dynamic_negation}}} ->
+          {[], [], :sets.union(dynamic_negation, static_negation)}
+
+        {_, %{atom: {:union, dynamic_union}}} ->
+          {[], :sets.to_list(dynamic_union), nil}
+
+        {_, %{atom: {:negation, dynamic_negation}}} ->
+          {[], [], dynamic_negation}
+
+        {_, _} ->
+          {[], [], nil}
+      end
+
+    required_domain = to_domain_keys(Map.delete(static, :dynamic))
+    optional_domain = to_domain_keys(dynamic) -- required_domain
+    {required_keys, optional_keys, maybe_negated_set, required_domain, optional_domain}
+  end
+
+  defp map_split_keys(%{atom: {:union, atoms}} = key_descr) do
+    {:sets.to_list(atoms), [], nil, to_domain_keys(key_descr), []}
+  end
+
+  defp map_split_keys(%{atom: {:negation, atoms}} = key_descr) do
+    {[], [], atoms, to_domain_keys(key_descr), []}
+  end
+
+  defp map_split_keys(key_descr) do
+    {[], [], nil, to_domain_keys(key_descr), []}
+  end
+
   defp non_empty_map_literals_intersection(maps) do
     try do
       Enum.reduce(maps, {:open, %{}}, fn {next_tag, next_fields}, {tag, fields} ->
@@ -4586,6 +4657,26 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp bdd_reduce(bdd, acc, fun) do
+    case bdd do
+      :bdd_bot ->
+        acc
+
+      :bdd_top ->
+        acc
+
+      {_, _} ->
+        fun.(bdd, acc)
+
+      {literal, left, union, right} ->
+        acc = fun.(literal, acc)
+        acc = bdd_reduce(left, acc, fun)
+        acc = bdd_reduce(union, acc, fun)
+        acc = bdd_reduce(right, acc, fun)
+        acc
+    end
+  end
+
   @compile {:inline, bdd_expand: 1, bdd_head: 1}
   defp bdd_expand({_, _} = pair), do: {pair, :bdd_top, :bdd_bot, :bdd_bot}
   defp bdd_expand(bdd), do: bdd

From 4c5e1ac84be48e044c54ccbc72663e51d86c2f11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 12:25:50 +0100
Subject: [PATCH 5/9] done

---
 lib/elixir/lib/module/types/descr.ex | 307 ++++++++++++++++-----------
 1 file changed, 178 insertions(+), 129 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 73879ab3d03..84d8110f001 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2311,6 +2311,19 @@ defmodule Module.Types.Descr do
     acc
   end
 
+  defp domain_key_to_descr(domain_key(:atom)), do: atom()
+  defp domain_key_to_descr(domain_key(:binary)), do: binary()
+  defp domain_key_to_descr(domain_key(:empty_list)), do: empty_list()
+  defp domain_key_to_descr(domain_key(:integer)), do: integer()
+  defp domain_key_to_descr(domain_key(:float)), do: float()
+  defp domain_key_to_descr(domain_key(:pid)), do: pid()
+  defp domain_key_to_descr(domain_key(:port)), do: port()
+  defp domain_key_to_descr(domain_key(:reference)), do: reference()
+  defp domain_key_to_descr(domain_key(:fun)), do: fun()
+  defp domain_key_to_descr(domain_key(:tuple)), do: tuple()
+  defp domain_key_to_descr(domain_key(:map)), do: open_map()
+  defp domain_key_to_descr(domain_key(:list)), do: non_empty_list(term(), term())
+
   defp map_descr(tag, pairs, default, force_domains?) do
     {fields, domains, dynamic?} = map_descr_pairs(pairs, [], %{}, false)
 
@@ -2921,148 +2934,184 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # def map_update(:term, key_descr, _type), do: :badmap
-
-  # def map_update(descr, key_descr, :term),
-  #   do: map_update_shared(descr, key_descr, :term)
-
-  # def map_update(descr, key_descr, type) do
-  #   case :maps.take(:dynamic, type) do
-  #     :error -> map_update_shared(descr, key_descr, type)
-  #     {dynamic, _static} -> map_update_shared(dynamic(descr), key_descr, dynamic)
-  #   end
-  # end
-
-  # defp map_update_shared(descr, key_descr, type) do
-  #   key_descr = upper_bound(key_descr)
-
-  #   case :maps.take(:dynamic, descr) do
-  #     :error ->
-  #       if descr_key?(descr, :map) and map_only?(descr) do
-  #         case map_existing_domains(descr, domain_keys) do
-  #           [] -> :badkey
-  #           domain_keys -> {:ok, map_update_domains(descr, domain_keys, type)}
-  #         end
-  #       else
-  #         :badmap
-  #       end
-
-  #     {dynamic, static} ->
-  #       if descr_key?(dynamic, :map) and map_only?(static) do
-  #         case map_existing_domains(dynamic, domain_keys) do
-  #           [] ->
-  #             :badkey
-
-  #           domain_keys ->
-  #             {:ok,
-  #              union(
-  #                dynamic(map_update_domains(dynamic, domain_keys, type)),
-  #                map_update_domains(static, domain_keys, type)
-  #              )}
-  #         end
-  #       else
-  #         :badmap
-  #       end
-  #   end
-  # end
-
-  # defp map_update_static(%{map: bdd}, key_descr, type) do
-  #   dnf = map_bdd_to_dnf(bdd)
-  #   {keys, key_descr} = map_split_keys(key_descr, bdd)
-  #   {optional, value, descr} = map_update_keys(dnf, keys, type)
-
-  #   key_descr
-  #   |> to_domain_keys()
-  #   |> Enum.reduce({optional, value, descr}, fn domain_key, acc ->
-  #     map_update_domain(dnf, domain_key) |> union(acc)
-  #   end)
-  # end
-
-  # defp map_update_static(%{}, _key_descr, _type) do
-  #   # No optional keys, no returned value, none is returned
-  #   {none(), none(), none()}
-  # end
-
-  # defp map_update_static(:term, key_descr, _type) do
-  #   # The whole key_descr is optional, returned value is term, open map is returned
-  #   {key_descr, term(), open_map()}
-  # end
-
-  # defp map_update_keys(dnf, keys, type) do
-  #   Enum.reduce(keys, {none(), none(), none()}, fn atom, {optional, value, acc} ->
-  #     {optional?, value, descr} = map_dnf_take_static(dnf, atom, value)
-  #     optional = if optional?, do: union(optional, atom([atom])), else: optional
-  #     descr = union(map_put_key_static(descr, atom, type), acc)
-  #     {optional, value, descr}
-  #   end)
-  # end
-
-  # defp map_update_atom_negation(%{atom: {:negation, atoms}} = descr, type) do
-  #   # 1) Fetch all the possible keys in the bdd
-  #   # 2) Get them all, except the ones in neg_atoms
-  #   all_fields = map_merge_all_fields(dnf)
-  #   acc = map_get_domain(dnf, domain_key(:atom))
-
-  #   for {atom, _} <- all_fields, not :sets.is_element(atom, atoms), reduce: acc do
-  #     acc ->
-  #       {static_optional?, type} = map_dnf_fetch_static(dnf, atom)
-
-  #       if static_optional? do
-  #         union(type, acc) |> nil_or_type() |> if_set()
-  #       else
-  #         union(type, acc)
-  #       end
-  #   end
-  # end
-
-  defp map_existing_domains(%{map: bdd}, domain_keys) do
-    dnf = map_bdd_to_dnf(bdd)
+  @doc """
+  TODO
+  """
+  def map_update(:term, _key_descr, _type), do: :badmap
 
-    Enum.filter(domain_keys, fn domain_key ->
-      Enum.any?(dnf, fn
-        {:open, _fields, []} ->
-          true
+  def map_update(descr, key_descr, :term),
+    do: map_update_shared(descr, key_descr, :term)
 
-        {:closed, _fields, []} ->
-          false
+  def map_update(descr, key_descr, type) do
+    case :maps.take(:dynamic, type) do
+      :error -> map_update_shared(descr, key_descr, type)
+      {dynamic, _static} -> map_update_shared(dynamic(descr), key_descr, dynamic)
+    end
+  end
+
+  defp map_update_shared(descr, key_descr, type) do
+    split_keys = map_split_keys_and_domains(key_descr)
 
-        {domains, _fields, []} ->
-          case domains do
-            %{^domain_key => type} -> not empty_or_optional?(type)
-            %{} -> false
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if descr_key?(descr, :map) and map_only?(descr) do
+          {present?, _value, descr} =
+            map_update_static(descr, split_keys, type, fn optional?, value ->
+              optional? or empty?(value)
+            end)
+
+          if present? do
+            {:ok, descr}
+          else
+            {:badomain, key_descr}
           end
+        else
+          :badmap
+        end
 
-        {tag_or_domains, fields, negs} ->
-          {fst, snd} = map_pop_domain(tag_or_domains, fields, domain_key)
+      {dynamic, static} ->
+        if descr_key?(dynamic, :map) and map_only?(static) do
+          {static_present?, _value, static_descr} =
+            map_update_static(descr, split_keys, type, fn optional?, _ -> optional? end)
 
-          case map_split_negative_domain(negs, domain_key) do
-            :empty ->
-              false
+          {dynamic_present?, _value, dynamic_descr} =
+            map_update_static(descr, split_keys, type, fn _, value -> empty?(value) end)
 
-            negative ->
-              type =
+          if static_present? or dynamic_present? do
+            {:ok, union(static_descr, dynamic(dynamic_descr))}
+          else
+            {:badomain, key_descr}
+          end
+        else
+          :badmap
+        end
+    end
+  end
+
+  defp map_update_static(%{map: bdd}, split_keys, type, missing_fun) do
+    {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
+      split_keys
+
+    non_negated = map_materialize_negated_set(maybe_negated_set, bdd)
+    dnf = map_bdd_to_dnf(bdd)
+
+    case map_update_get_domains(dnf, required_domains, none()) do
+      {required_domains, [], value} ->
+        # Optional domains can miss
+        {optional_domains, _, value} = map_update_get_domains(dnf, optional_domains, value)
+
+        # If any of required or optional domains are satisfied, we are already good
+        present? = required_domains != [] or optional_domains != []
+
+        # Now compute the initial return type. Note that map_update_static_keys works
+        # on the original bdd/dnf, not the one with updated domains
+        descr = map_update_put_domains(bdd, required_domains ++ optional_domains, type)
+
+        map_update_static_keys(
+          dnf,
+          required_keys,
+          optional_keys,
+          non_negated,
+          type,
+          missing_fun,
+          {present?, value, descr}
+        )
+
+      {_, [missing_domain | _], _} ->
+        {:baddomain, domain_key_to_descr(missing_domain)}
+    end
+  end
+
+  defp map_update_static(%{}, _split_keys, _type, _missing_fun) do
+    {false, none(), none()}
+  end
+
+  defp map_update_static(:term, split_keys, type, missing_fun) do
+    # Since it is an open map, we don't need to check the domains...
+    {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
+      split_keys
+
+    non_negated = :sets.to_list(maybe_negated_set)
+    dnf = map_bdd_to_dnf(@map_top)
+    acc = {required_domains != [] or optional_domains != [], term(), open_map()}
+    map_update_static_keys(dnf, required_keys, optional_keys, non_negated, type, missing_fun, acc)
+  end
+
+  defp map_update_static_keys(dnf, required, optional, non_negated, type, missing_fun, acc) do
+    acc = map_update_keys(dnf, required, type, :required, missing_fun, acc)
+    acc = map_update_keys(dnf, optional, type, :optional, missing_fun, acc)
+    acc = map_update_keys(dnf, non_negated, type, :optional, missing_fun, acc)
+    acc
+  catch
+    {:badkey, key} -> {:badkey, key}
+  end
+
+  defp map_update_keys(dnf, keys, type, required_or_optional, missing_fun, acc) do
+    Enum.reduce(keys, acc, fn key, {present?, acc_value, acc_descr} ->
+      {optional?, value, descr} = map_dnf_take_static(dnf, key, none())
+      value = union(value, acc_value)
+      descr = union(map_put_key_static(descr, key, type), acc_descr)
+
+      missing? = missing_fun.(optional?, value)
+      required_or_optional == :required and missing? and throw({:badkey, key})
+      {present? or not missing?, value, descr}
+    end)
+  end
+
+  defp map_update_get_domains(dnf, domain_keys, acc) do
+    Enum.reduce(domain_keys, {[], [], acc}, fn domain_key, {valid, invalid, acc} ->
+      value =
+        Enum.reduce(dnf, none(), fn
+          {:open, _fields, []}, _acc ->
+            term()
+
+          {:closed, _fields, []}, acc ->
+            acc
+
+          {domains, _fields, []}, acc ->
+            case domains do
+              %{^domain_key => type} -> union(remove_optional_static(type), acc)
+              %{} -> acc
+            end
+
+          {tag_or_domains, fields, negs}, acc ->
+            {fst, snd} = map_pop_domain(tag_or_domains, fields, domain_key)
+
+            case map_split_negative_domain(negs, domain_key) do
+              :empty ->
+                acc
+
+              negative ->
                 negative
                 |> pair_make_disjoint()
                 |> pair_eliminate_negations_fst(fst, snd)
+                |> remove_optional_static()
+                |> union(acc)
+            end
+        end)
 
-              not empty_or_optional?(type)
-          end
-      end)
+      if empty?(value) do
+        {valid, [domain_key | invalid], acc}
+      else
+        {[domain_key | valid], invalid, union(acc, value)}
+      end
     end)
   end
 
-  defp map_update_domains(%{map: bdd}, domain_keys, type) do
+  defp map_update_put_domains(bdd, domain_keys, type) do
     # For negations, we count on the idea that a negation will not remove any
     # type from a domain unless it completely cancels out the type.
     # So for any non-empty map bdd, we just update the domain with the new type,
     # as well as its negations to keep them accurate.
     %{
       map:
-        bdd_map(bdd, fn {tag, fields} -> {map_update_domain(tag, domain_keys, type), fields} end)
+        bdd_map(bdd, fn {tag, fields} ->
+          {map_update_put_domain(tag, domain_keys, type), fields}
+        end)
     }
   end
 
-  defp map_update_domain(tag_or_domains, domain_keys, type) do
+  defp map_update_put_domain(tag_or_domains, domain_keys, type) do
     case tag_or_domains do
       :open ->
         :open
@@ -3122,7 +3171,7 @@ defmodule Module.Types.Descr do
   def map_get(:term, _key_descr), do: :badmap
 
   def map_get(%{} = descr, key_descr) do
-    split_keys = map_split_keys(key_descr)
+    split_keys = map_split_keys_and_domains(key_descr)
 
     case :maps.take(:dynamic, descr) do
       :error ->
@@ -3162,11 +3211,11 @@ defmodule Module.Types.Descr do
   defp nil_or_type(type), do: union(type, atom([nil]))
 
   defp map_get_static(%{map: bdd}, split_keys) do
-    dnf = map_bdd_to_dnf(bdd)
-
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
+    dnf = map_bdd_to_dnf(bdd)
+
     acc = none()
     acc = map_get_keys(dnf, required_keys, acc)
     acc = map_get_keys(dnf, optional_keys, acc)
@@ -3232,7 +3281,7 @@ defmodule Module.Types.Descr do
   end
 
   # Compute which keys are optional, which ones are required, as well as domain keys
-  defp map_split_keys(%{dynamic: dynamic} = static) do
+  defp map_split_keys_and_domains(%{dynamic: dynamic} = static) do
     {required_keys, optional_keys, maybe_negated_set} =
       case {static, dynamic} do
         {%{atom: {:union, static_union}}, %{atom: {:union, dynamic_union}}} ->
@@ -3264,20 +3313,20 @@ defmodule Module.Types.Descr do
           {[], [], nil}
       end
 
-    required_domain = to_domain_keys(Map.delete(static, :dynamic))
-    optional_domain = to_domain_keys(dynamic) -- required_domain
-    {required_keys, optional_keys, maybe_negated_set, required_domain, optional_domain}
+    required_domains = to_domain_keys(Map.delete(static, :dynamic))
+    optional_domains = to_domain_keys(dynamic) -- required_domains
+    {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains}
   end
 
-  defp map_split_keys(%{atom: {:union, atoms}} = key_descr) do
+  defp map_split_keys_and_domains(%{atom: {:union, atoms}} = key_descr) do
     {:sets.to_list(atoms), [], nil, to_domain_keys(key_descr), []}
   end
 
-  defp map_split_keys(%{atom: {:negation, atoms}} = key_descr) do
+  defp map_split_keys_and_domains(%{atom: {:negation, atoms}} = key_descr) do
     {[], [], atoms, to_domain_keys(key_descr), []}
   end
 
-  defp map_split_keys(key_descr) do
+  defp map_split_keys_and_domains(key_descr) do
     {[], [], nil, to_domain_keys(key_descr), []}
   end
 

From 4e71e2b1ae326d936d6431c08d64740575855d1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 13:52:03 +0100
Subject: [PATCH 6/9] More comments

---
 lib/elixir/lib/module/types/descr.ex | 102 ++++++++++++++-------------
 1 file changed, 53 insertions(+), 49 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 84d8110f001..f0dae20c1dc 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2955,7 +2955,7 @@ defmodule Module.Types.Descr do
     case :maps.take(:dynamic, descr) do
       :error ->
         if descr_key?(descr, :map) and map_only?(descr) do
-          {present?, _value, descr} =
+          {present?, _maybe_optional_value, descr} =
             map_update_static(descr, split_keys, type, fn optional?, value ->
               optional? or empty?(value)
             end)
@@ -2971,10 +2971,10 @@ defmodule Module.Types.Descr do
 
       {dynamic, static} ->
         if descr_key?(dynamic, :map) and map_only?(static) do
-          {static_present?, _value, static_descr} =
+          {static_present?, _maybe_optional_static_value, static_descr} =
             map_update_static(descr, split_keys, type, fn optional?, _ -> optional? end)
 
-          {dynamic_present?, _value, dynamic_descr} =
+          {dynamic_present?, _maybe_optional_dynamic_value, dynamic_descr} =
             map_update_static(descr, split_keys, type, fn _, value -> empty?(value) end)
 
           if static_present? or dynamic_present? do
@@ -2997,15 +2997,21 @@ defmodule Module.Types.Descr do
 
     case map_update_get_domains(dnf, required_domains, none()) do
       {required_domains, [], value} ->
-        # Optional domains can miss
+        # Optional domains can be missing
+        # TODO: In order to support map_put, we need to add these missing domains as ORs
         {optional_domains, _, value} = map_update_get_domains(dnf, optional_domains, value)
 
-        # If any of required or optional domains are satisfied, we are already good
-        present? = required_domains != [] or optional_domains != []
-
-        # Now compute the initial return type. Note that map_update_static_keys works
-        # on the original bdd/dnf, not the one with updated domains
-        descr = map_update_put_domains(bdd, required_domains ++ optional_domains, type)
+        acc =
+          if required_domains == [] and optional_domains == [] do
+            # Value can only be none
+            {false, value, none()}
+          else
+            # If any of required or optional domains are satisfied, then we compute the
+            # initial return type. `map_update_static_keys` 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, required_domains ++ optional_domains, type)
+            {true, value, descr}
+          end
 
         map_update_static_keys(
           dnf,
@@ -3014,7 +3020,7 @@ defmodule Module.Types.Descr do
           non_negated,
           type,
           missing_fun,
-          {present?, value, descr}
+          acc
         )
 
       {_, [missing_domain | _], _} ->
@@ -3031,10 +3037,17 @@ defmodule Module.Types.Descr do
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
-    non_negated = :sets.to_list(maybe_negated_set)
-    dnf = map_bdd_to_dnf(@map_top)
-    acc = {required_domains != [] or optional_domains != [], term(), open_map()}
-    map_update_static_keys(dnf, required_keys, optional_keys, non_negated, type, missing_fun, acc)
+    # But any required key will fail
+    case required_keys do
+      [key | _] ->
+        {:badkey, key}
+
+      _ ->
+        non_negated = :sets.to_list(maybe_negated_set)
+        dnf = map_bdd_to_dnf(@map_top)
+        acc = {required_domains != [] or optional_domains != [], term(), open_map()}
+        map_update_static_keys(dnf, [], optional_keys, non_negated, type, missing_fun, acc)
+    end
   end
 
   defp map_update_static_keys(dnf, required, optional, non_negated, type, missing_fun, acc) do
@@ -3060,37 +3073,9 @@ defmodule Module.Types.Descr do
 
   defp map_update_get_domains(dnf, domain_keys, acc) do
     Enum.reduce(domain_keys, {[], [], acc}, fn domain_key, {valid, invalid, acc} ->
-      value =
-        Enum.reduce(dnf, none(), fn
-          {:open, _fields, []}, _acc ->
-            term()
-
-          {:closed, _fields, []}, acc ->
-            acc
-
-          {domains, _fields, []}, acc ->
-            case domains do
-              %{^domain_key => type} -> union(remove_optional_static(type), acc)
-              %{} -> acc
-            end
-
-          {tag_or_domains, fields, negs}, acc ->
-            {fst, snd} = map_pop_domain(tag_or_domains, fields, domain_key)
+      value = map_get_domain(dnf, domain_key, none())
 
-            case map_split_negative_domain(negs, domain_key) do
-              :empty ->
-                acc
-
-              negative ->
-                negative
-                |> pair_make_disjoint()
-                |> pair_eliminate_negations_fst(fst, snd)
-                |> remove_optional_static()
-                |> union(acc)
-            end
-        end)
-
-      if empty?(value) do
+      if empty_or_optional?(value) do
         {valid, [domain_key | invalid], acc}
       else
         {[domain_key | valid], invalid, union(acc, value)}
@@ -3098,11 +3083,30 @@ 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, domain_keys, type) do
-    # For negations, we count on the idea that a negation will not remove any
-    # type from a domain unless it completely cancels out the type.
-    # So for any non-empty map bdd, we just update the domain with the new type,
-    # as well as its negations to keep them accurate.
     %{
       map:
         bdd_map(bdd, fn {tag, fields} ->

From 5a4cc999aed0a70f059d3a11cdd8355ba39ac2b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 17:00:08 +0100
Subject: [PATCH 7/9] progress

---
 lib/elixir/lib/module/types/descr.ex          | 177 +++++++++++-------
 lib/elixir/lib/module/types/expr.ex           |  63 ++++---
 lib/elixir/lib/module/types/of.ex             | 104 +++++-----
 .../test/elixir/module/types/descr_test.exs   |  14 ++
 4 files changed, 198 insertions(+), 160 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index f0dae20c1dc..2c5621a7702 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2955,15 +2955,15 @@ defmodule Module.Types.Descr do
     case :maps.take(:dynamic, descr) do
       :error ->
         if descr_key?(descr, :map) and map_only?(descr) do
-          {present?, _maybe_optional_value, descr} =
-            map_update_static(descr, split_keys, type, fn optional?, value ->
-              optional? or empty?(value)
-            end)
-
-          if present? do
-            {:ok, descr}
-          else
-            {:badomain, key_descr}
+          with {present?, _maybe_optional_value, descr} <-
+                 map_update_static(descr, split_keys, type, fn optional?, value ->
+                   optional? or empty?(value)
+                 end) do
+            if present? do
+              {:ok, descr}
+            else
+              {:baddomain, key_descr}
+            end
           end
         else
           :badmap
@@ -2971,16 +2971,15 @@ defmodule Module.Types.Descr do
 
       {dynamic, static} ->
         if descr_key?(dynamic, :map) and map_only?(static) do
-          {static_present?, _maybe_optional_static_value, static_descr} =
-            map_update_static(descr, split_keys, type, fn optional?, _ -> optional? end)
-
-          {dynamic_present?, _maybe_optional_dynamic_value, dynamic_descr} =
-            map_update_static(descr, split_keys, type, fn _, value -> empty?(value) end)
-
-          if static_present? or dynamic_present? do
-            {:ok, union(static_descr, dynamic(dynamic_descr))}
-          else
-            {:badomain, key_descr}
+          with {static_present?, _maybe_optional_static_value, static_descr} <-
+                 map_update_static(static, split_keys, type, fn optional?, _ -> optional? end),
+               {dynamic_present?, _maybe_optional_dynamic_value, dynamic_descr} <-
+                 map_update_static(dynamic, split_keys, type, fn _, value -> empty?(value) end) do
+            if static_present? or dynamic_present? do
+              {:ok, union(static_descr, dynamic(dynamic_descr))}
+            else
+              {:baddomain, key_descr}
+            end
           end
         else
           :badmap
@@ -2992,36 +2991,37 @@ defmodule Module.Types.Descr do
     {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
       split_keys
 
-    non_negated = map_materialize_negated_set(maybe_negated_set, bdd)
+    bdd = map_update_negated(bdd, maybe_negated_set, type)
     dnf = map_bdd_to_dnf(bdd)
 
-    case map_update_get_domains(dnf, required_domains, none()) do
-      {required_domains, [], value} ->
+    callback = fn ->
+      # If we have required keys, we can assume domain_atom always work
+      if required_keys != [] do
+        true
+      else
+        map_update_any_atom_key(bdd, dnf)
+      end
+    end
+
+    case map_update_get_domains(dnf, required_domains, none(), callback) do
+      {found_required?, required_domains, [], value} ->
         # Optional domains can be missing
         # TODO: In order to support map_put, we need to add these missing domains as ORs
-        {optional_domains, _, value} = map_update_get_domains(dnf, optional_domains, value)
+        {found_optional?, optional_domains, _, value} =
+          map_update_get_domains(dnf, optional_domains, value, callback)
 
         acc =
-          if required_domains == [] and optional_domains == [] do
-            # Value can only be none
-            {false, value, none()}
-          else
+          if found_optional? or found_required? do
             # If any of required or optional domains are satisfied, then we compute the
             # initial return type. `map_update_static_keys` 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, required_domains ++ optional_domains, type)
             {true, value, descr}
+          else
+            {false, value, none()}
           end
 
-        map_update_static_keys(
-          dnf,
-          required_keys,
-          optional_keys,
-          non_negated,
-          type,
-          missing_fun,
-          acc
-        )
+        map_update_static_keys(dnf, required_keys, optional_keys, type, missing_fun, acc)
 
       {_, [missing_domain | _], _} ->
         {:baddomain, domain_key_to_descr(missing_domain)}
@@ -3033,27 +3033,20 @@ defmodule Module.Types.Descr do
   end
 
   defp map_update_static(:term, split_keys, type, missing_fun) do
-    # Since it is an open map, we don't need to check the domains...
-    {required_keys, optional_keys, maybe_negated_set, required_domains, optional_domains} =
+    # 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
 
-    # But any required key will fail
-    case required_keys do
-      [key | _] ->
-        {:badkey, key}
-
-      _ ->
-        non_negated = :sets.to_list(maybe_negated_set)
-        dnf = map_bdd_to_dnf(@map_top)
-        acc = {required_domains != [] or optional_domains != [], term(), open_map()}
-        map_update_static_keys(dnf, [], optional_keys, non_negated, type, missing_fun, acc)
-    end
+    dnf = map_bdd_to_dnf(@map_top)
+    acc = {required_domains != [] or optional_domains != [], term(), open_map()}
+    map_update_static_keys(dnf, required_keys, optional_keys, type, missing_fun, acc)
   end
 
-  defp map_update_static_keys(dnf, required, optional, non_negated, type, missing_fun, acc) do
+  defp map_update_static_keys(dnf, required, optional, type, missing_fun, acc) do
     acc = map_update_keys(dnf, required, type, :required, missing_fun, acc)
     acc = map_update_keys(dnf, optional, type, :optional, missing_fun, acc)
-    acc = map_update_keys(dnf, non_negated, type, :optional, missing_fun, acc)
     acc
   catch
     {:badkey, key} -> {:badkey, key}
@@ -3062,23 +3055,63 @@ defmodule Module.Types.Descr do
   defp map_update_keys(dnf, keys, type, required_or_optional, missing_fun, acc) do
     Enum.reduce(keys, acc, fn key, {present?, acc_value, acc_descr} ->
       {optional?, value, descr} = map_dnf_take_static(dnf, key, none())
-      value = union(value, acc_value)
-      descr = union(map_put_key_static(descr, key, type), acc_descr)
-
       missing? = missing_fun.(optional?, value)
+
       required_or_optional == :required and missing? and throw({:badkey, key})
-      {present? or not missing?, value, descr}
+      acc_value = union(value, acc_value)
+      acc_descr = union(map_put_key_static(descr, key, type), acc_descr)
+      {present? or not missing?, acc_value, acc_descr}
     end)
   end
 
-  defp map_update_get_domains(dnf, domain_keys, acc) do
-    Enum.reduce(domain_keys, {[], [], acc}, fn domain_key, {valid, invalid, acc} ->
+  # For keys with `not :foo`, we generate an approximation
+  # by adding the type to all keys, except `:foo`.
+  defp map_update_negated(bdd, nil, _type), do: bdd
+
+  defp map_update_negated(bdd, negated, type) do
+    bdd_map(bdd, fn {tag, fields} ->
+      fields =
+        Map.new(fields, fn {key, value} ->
+          if :sets.is_element(key, negated) do
+            {key, value}
+          else
+            {key, union(value, type)}
+          end
+        end)
+
+      {tag, fields}
+    end)
+  end
+
+  defp map_update_any_atom_key(bdd, dnf) do
+    bdd_reduce(bdd, %{}, fn {_tag, fields}, acc ->
+      Enum.reduce(fields, acc, fn {key, _type}, acc ->
+        if Map.has_key?(acc, key) do
+          acc
+        else
+          {_, value} = map_dnf_fetch_static(dnf, key)
+          not empty?(value) and throw(:found_key)
+          Map.put(acc, key, [])
+        end
+      end)
+    end)
+  catch
+    :found_key -> true
+  end
+
+  defp map_update_get_domains(dnf, domain_keys, acc, any_atom_key) do
+    Enum.reduce(domain_keys, {false, [], [], acc}, fn domain_key, {found?, valid, invalid, acc} ->
       value = map_get_domain(dnf, domain_key, none())
 
-      if empty_or_optional?(value) do
-        {valid, [domain_key | invalid], acc}
-      else
-        {[domain_key | valid], invalid, union(acc, value)}
+      cond do
+        not empty_or_optional?(value) ->
+          {true, [domain_key | valid], invalid, union(acc, value)}
+
+        domain_key == domain_key(:atom) and any_atom_key.() ->
+          {true, valid, [domain_key | invalid], acc}
+
+        true ->
+          {found?, valid, [domain_key | invalid], acc}
       end
     end)
   end
@@ -3106,13 +3139,15 @@ defmodule Module.Types.Descr do
   # 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), do: %{map: bdd}
+
   defp map_update_put_domains(bdd, domain_keys, type) do
-    %{
-      map:
-        bdd_map(bdd, fn {tag, fields} ->
-          {map_update_put_domain(tag, domain_keys, type), fields}
-        end)
-    }
+    bdd =
+      bdd_map(bdd, fn {tag, fields} ->
+        {map_update_put_domain(tag, domain_keys, type), fields}
+      end)
+
+    %{map: bdd}
   end
 
   defp map_update_put_domain(tag_or_domains, domain_keys, type) do
@@ -3287,7 +3322,7 @@ defmodule Module.Types.Descr do
   # Compute which keys are optional, which ones are required, as well as domain keys
   defp map_split_keys_and_domains(%{dynamic: dynamic} = static) do
     {required_keys, optional_keys, maybe_negated_set} =
-      case {static, dynamic} do
+      case {static, unfold(dynamic)} do
         {%{atom: {:union, static_union}}, %{atom: {:union, dynamic_union}}} ->
           # The static union is required, extract them from optional
           {:sets.to_list(static_union),
@@ -3307,13 +3342,13 @@ defmodule Module.Types.Descr do
         {%{atom: {:negation, static_negation}}, %{atom: {:negation, dynamic_negation}}} ->
           {[], [], :sets.union(dynamic_negation, static_negation)}
 
-        {_, %{atom: {:union, dynamic_union}}} ->
+        {%{}, %{atom: {:union, dynamic_union}}} ->
           {[], :sets.to_list(dynamic_union), nil}
 
-        {_, %{atom: {:negation, dynamic_negation}}} ->
+        {%{}, %{atom: {:negation, dynamic_negation}}} ->
           {[], [], dynamic_negation}
 
-        {_, _} ->
+        {%{}, %{}} ->
           {[], [], nil}
       end
 
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index e0d2e91c850..f05e8d25835 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -173,11 +173,9 @@ defmodule Module.Types.Expr do
     # on the right side, this is safe.
     {pairs_types, context} =
       Enum.map_reduce(args, context, fn {key, value}, context ->
-        {key_tagged_type, dynamic_key?, context} =
-          Of.map_key_type(key, stack, context, &of_expr(&1, &2, expr, &3, &4))
-
+        {key_type, context} = of_expr(key, term(), expr, stack, context)
         {value_type, context} = of_expr(value, term(), expr, stack, context)
-        {{key_tagged_type, dynamic_key? or gradual?(value_type), value_type}, context}
+        {{key_type, value_type}, context}
       end)
 
     expected =
@@ -186,19 +184,12 @@ defmodule Module.Types.Expr do
       else
         # The only information we can attach to the expected types is that
         # certain keys are expected.
-        #
-        # * If we have a single key, that's straight-forward
-        #
-        # * If we have multiple keys, it may be one or the other,
-        #   so we would need to generate unions, therefore we abort
-        #
-        # * If it is a domain key, then we could say such key is expected,
-        #   but it wouldn't effectively add any new information, so we skip it
         expected_pairs =
-          Enum.reduce_while(pairs_types, [], fn
-            {{:domain, _}, _, _}, acc -> {:cont, acc}
-            {{:keys, [key]}, _, _}, acc -> {:cont, [{key, term()} | acc]}
-            {_, _, _}, _acc -> {:halt, []}
+          Enum.flat_map(pairs_types, fn {key_type, _value_type} ->
+            case atom_fetch(key_type) do
+              {:finite, [key]} -> [{key, term()}]
+              _ -> []
+            end
           end)
 
         intersection(expected, open_map(expected_pairs))
@@ -207,18 +198,13 @@ defmodule Module.Types.Expr do
     {map_type, context} = of_expr(map, expected, expr, stack, context)
 
     try do
-      Of.permutate_map(pairs_types, stack, fn pairs ->
-        Enum.reduce(pairs, map_type, fn {key_or_domains, type}, acc ->
-          if is_atom(key_or_domains) do
-            case map_put_existing(acc, key_or_domains, type) do
-              {:ok, descr} -> descr
-              :badkey -> throw({:badkey, map_type, key_or_domains, update, context})
-              :badmap -> throw({:badmap, map_type, update, context})
-            end
-          else
-            acc
-          end
-        end)
+      Enum.reduce(pairs_types, map_type, fn {key_type, value_type}, acc ->
+        case map_update(acc, key_type, value_type) do
+          {:ok, descr} -> descr
+          {:badkey, key} -> throw({:badkey, map_type, key, update, context})
+          {:baddomain, domain} -> throw({:baddomain, map_type, domain, update, context})
+          :badmap -> throw({:badmap, map_type, update, context})
+        end
       end)
     catch
       error -> {error_type(), error(__MODULE__, error, meta, stack, context)}
@@ -903,6 +889,27 @@ defmodule Module.Types.Expr do
     }
   end
 
+  def format_diagnostic({:baddomain, type, key_type, expr, context}) do
+    traces = collect_traces(expr, context)
+
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          expected a map with key #{to_quoted_string(key_type)} in map update syntax:
+
+              #{expr_to_string(expr, collapse_structs: false) |> indent(4)}
+
+          but got type:
+
+              #{to_quoted_string(type, collapse_structs: false) |> indent(4)}
+          """,
+          format_traces(traces)
+        ])
+    }
+  end
+
   def format_diagnostic({:badbinary, type, expr, context}) do
     traces = collect_traces(expr, context)
 
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index 82cab17519e..a46210c3a83 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -175,69 +175,20 @@ defmodule Module.Types.Of do
   @doc """
   Builds a closed map.
   """
-  def closed_map(pairs, expected, stack, context, of_fun) do
-    {pairs_types, context} = pairs(pairs, expected, stack, context, of_fun)
-
-    map =
-      permutate_map(pairs_types, stack, fn pairs ->
-        closed_map(pairs)
+  def closed_map(pairs, _expected, %{mode: :traversal} = stack, context, of_fun) do
+    context =
+      Enum.reduce(pairs, context, fn {key, value}, context ->
+        {_key_type, context} = of_fun.(key, term(), stack, context)
+        {_, context} = of_fun.(value, term(), stack, context)
+        context
       end)
 
-    {map, context}
-  end
-
-  @doc """
-  Computes the types of key-value pairs.
-  """
-  def pairs(pairs, _expected, %{mode: :traversal} = stack, context, of_fun) do
-    Enum.map_reduce(pairs, context, fn {key, value}, context ->
-      {_key_type, context} = of_fun.(key, term(), stack, context)
-      {value_type, context} = of_fun.(value, term(), stack, context)
-      {{{:domain, to_domain_keys(:term)}, true, value_type}, context}
-    end)
-  end
-
-  def pairs(pairs, expected, stack, context, of_fun) do
-    Enum.map_reduce(pairs, context, fn {key, value}, context ->
-      {key_tagged_type, dynamic_key?, context} = map_key_type(key, stack, context, of_fun)
-
-      expected_value_type =
-        with {:keys, [key]} <- key_tagged_type,
-             {_, expected_value_type} <- map_fetch_key(expected, key) do
-          expected_value_type
-        else
-          _ -> term()
-        end
-
-      {value_type, context} = of_fun.(value, expected_value_type, stack, context)
-      {{key_tagged_type, dynamic_key? or gradual?(value_type), value_type}, context}
-    end)
-  end
-
-  @doc """
-  Returns the type of a map key.
-  """
-  def map_key_type(key, _stack, context, _of_fun) when is_atom(key) do
-    {{:keys, [key]}, false, context}
+    {dynamic(), context}
   end
 
-  def map_key_type(key, stack, context, of_fun) do
-    {key_type, context} = of_fun.(key, term(), stack, context)
-
-    case atom_fetch(key_type) do
-      {:finite, list} -> {{:keys, list}, gradual?(key_type), context}
-      _ -> {{:domain, to_domain_keys(key_type)}, gradual?(key_type), context}
-    end
-  end
-
-  @doc """
-  Builds permutation of maps according to the given pairs types.
-  """
-  def permutate_map(_pairs_types, %{mode: :traversal}, _of_map) do
-    dynamic()
-  end
+  def closed_map(pairs, expected, stack, context, of_fun) do
+    {pairs_types, context} = pairs(pairs, expected, stack, context, of_fun)
 
-  def permutate_map(pairs_types, _stack, of_map) do
     {dynamic?, domain, single, multiple} =
       Enum.reduce(pairs_types, {false, [], [], []}, fn
         {key_tagged_type, dynamic_pair?, value_type}, {dynamic?, domain, single, multiple} ->
@@ -262,16 +213,47 @@ defmodule Module.Types.Of do
     map =
       case Enum.reverse(multiple) do
         [] ->
-          of_map.(non_multiple)
+          closed_map(non_multiple)
 
         [{keys, type} | tail] ->
           for key <- keys, t <- cartesian_map(tail) do
-            of_map.(non_multiple ++ [{key, type} | t])
+            closed_map(non_multiple ++ [{key, type} | t])
           end
           |> Enum.reduce(&union/2)
       end
 
-    if dynamic?, do: dynamic(map), else: map
+    {if(dynamic?, do: dynamic(map), else: map), context}
+  end
+
+  defp pairs(pairs, expected, stack, context, of_fun) do
+    Enum.map_reduce(pairs, context, fn {key, value}, context ->
+      {key_tagged_type, dynamic_key?, context} = map_key_type(key, stack, context, of_fun)
+
+      expected_value_type =
+        with {:keys, [key]} <- key_tagged_type,
+             {_, expected_value_type} <- map_fetch_key(expected, key) do
+          expected_value_type
+        else
+          _ -> term()
+        end
+
+      {value_type, context} = of_fun.(value, expected_value_type, stack, context)
+      {{key_tagged_type, dynamic_key? or gradual?(value_type), value_type}, context}
+    end)
+  end
+
+  defp map_key_type(key, _stack, context, _of_fun) when is_atom(key) do
+    {{:keys, [key]}, false, context}
+  end
+
+  defp map_key_type(key, stack, context, of_fun) do
+    {key_type, context} = of_fun.(key, term(), stack, context)
+
+    # TODO: deal with negations here too
+    case atom_fetch(key_type) do
+      {:finite, list} -> {{:keys, list}, gradual?(key_type), context}
+      _ -> {{:domain, to_domain_keys(key_type)}, gradual?(key_type), context}
+    end
   end
 
   defp cartesian_map(lists) do
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 0c73642dcd1..d3ceba3e5b5 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1722,6 +1722,20 @@ defmodule Module.Types.DescrTest do
                {:ok, union(atom([:b]), pid() |> nil_or_type())}
     end
 
+    test "map_update" do
+      assert map_update(open_map(key: atom([:value])), atom([:key]), atom([:new_value])) ==
+               {:ok, open_map(key: atom([:new_value]))}
+
+      assert map_update(dynamic(open_map(key: atom([:value]))), atom([:key]), atom([:new_value])) ==
+               {:ok, dynamic(open_map(key: atom([:new_value])))}
+
+      assert map_update(closed_map(key: atom([:value])), dynamic(), atom([:new_value])) ==
+               {:ok, closed_map(key: atom([:value, :new_value]))}
+
+      assert map_update(dynamic(closed_map(key: atom([:value]))), dynamic(), atom([:new_value])) ==
+               {:ok, dynamic(closed_map(key: atom([:value, :new_value])))}
+    end
+
     # TODO: needs to be rewritten to key types
     test "map_delete" do
       assert map_delete(term(), :a) == :badmap

From b1c0096eaf08961d337c780e897089f3af9b3e11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 17:21:06 +0100
Subject: [PATCH 8/9] done

---
 lib/elixir/lib/module/types/descr.ex              |  1 -
 lib/elixir/lib/module/types/of.ex                 |  4 +++-
 .../test/elixir/module/types/integration_test.exs | 15 +++++++++++----
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 2c5621a7702..fe1f125f7d5 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -3006,7 +3006,6 @@ defmodule Module.Types.Descr do
     case map_update_get_domains(dnf, required_domains, none(), callback) do
       {found_required?, required_domains, [], value} ->
         # Optional domains can be missing
-        # TODO: In order to support map_put, we need to add these missing domains as ORs
         {found_optional?, optional_domains, _, value} =
           map_update_get_domains(dnf, optional_domains, value, callback)
 
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index a46210c3a83..18ca3b10f90 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -249,7 +249,9 @@ defmodule Module.Types.Of do
   defp map_key_type(key, stack, context, of_fun) do
     {key_type, context} = of_fun.(key, term(), stack, context)
 
-    # TODO: deal with negations here too
+    # TODO: Deal with negations such that
+    # `%{not :key => value}` => `%{atom() => value, key: none()}`
+    # `%{:key => value, not :key => value}` => `%{atom() => value, key: value}`
     case atom_fetch(key_type) do
       {:finite, list} -> {{:keys, list}, gradual?(key_type), context}
       _ -> {{:domain, to_domain_keys(key_type)}, gradual?(key_type), context}
diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs
index ac1be7bd890..21be9f8f31f 100644
--- a/lib/elixir/test/elixir/module/types/integration_test.exs
+++ b/lib/elixir/test/elixir/module/types/integration_test.exs
@@ -106,8 +106,8 @@ defmodule Module.Types.IntegrationTest do
             x
           end
 
-          def map_update_with_unknown_keys(x, y) do
-            infer(%{x | y => 123})
+          def map_update_with_unknown_keys(x, key) do
+            infer(%{x | key => 123})
             x
           end
 
@@ -147,13 +147,20 @@ defmodule Module.Types.IntegrationTest do
                  closed_map(
                    __struct__: atom([A]),
                    x: binary(),
-                   y: term(),
+                   y: atom([nil]),
                    z: term()
                  )
                )
 
       assert return.(:map_update_with_unknown_keys, 2) ==
-               dynamic(open_map())
+               dynamic(
+                 closed_map(
+                   __struct__: atom([A]),
+                   x: binary(),
+                   y: atom([nil]),
+                   z: term()
+                 )
+               )
     end
 
     test "writes exports with inferred function types" do

From 02bf28577b0f9eab77ce3a1c519ecd6a263a2f35 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@dashbit.co>
Date: Tue, 4 Nov 2025 17:57:51 +0100
Subject: [PATCH 9/9] More renamings for consistency

---
 lib/elixir/lib/module/types/descr.ex          |  71 ++++--------
 .../test/elixir/module/types/descr_test.exs   | 101 ++++--------------
 2 files changed, 41 insertions(+), 131 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index fe1f125f7d5..2d9e831539f 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2783,7 +2783,7 @@ defmodule Module.Types.Descr do
   end
 
   defp map_put_key_shared(descr, key, type) do
-    with {nil, descr} <- map_take(descr, key, nil, &map_put_key_static(&1, key, type)) do
+    with {nil, descr} <- map_take_key(descr, key, nil, &map_put_key_static(&1, key, type)) do
       {:ok, descr}
     end
   end
@@ -2796,17 +2796,6 @@ defmodule Module.Types.Descr do
 
   defp map_put_key_static(descr, _key, _type), do: descr
 
-  @doc """
-  Removes a key from a map type.
-  """
-  def map_delete(descr, key) do
-    # We pass nil as the initial value so we can avoid computing the unions.
-    with {nil, descr} <-
-           map_take(descr, key, nil, &intersection_static(&1, open_map([{key, not_set()}]))) do
-      {:ok, descr}
-    end
-  end
-
   @doc """
   Removes a key from a map type and return its type.
 
@@ -2818,19 +2807,20 @@ defmodule Module.Types.Descr do
   3. Intersect this with an open record type where the key is explicitly absent.
      This step eliminates the key from open record types where it was implicitly present.
   """
-  def map_take(descr, key) do
-    map_take(descr, key, none(), &intersection_static(&1, open_map([{key, not_set()}])))
+  # TODO: This should not be exposed
+  def map_take_key(descr, key) do
+    map_take_key(descr, key, none(), &intersection_static(&1, open_map([{key, not_set()}])))
   end
 
-  # If initial is nil, note we don't compute the value.
-  defp map_take(:term, _key, _initial, _updater), do: :badmap
+  # If initial is nil, note we don't compute the value
+  defp map_take_key(:term, _key, _initial, _updater), do: :badmap
 
-  defp map_take(descr, key, initial, updater) when is_atom(key) do
+  defp map_take_key(descr, key, initial, updater) when is_atom(key) do
     case :maps.take(:dynamic, descr) do
       :error ->
         if descr_key?(descr, :map) and map_only?(descr) do
           {optional?, taken, result} =
-            map_take_static(descr, key, initial)
+            map_take_key_static(descr, key, initial)
 
           cond do
             taken == nil -> {nil, updater.(result)}
@@ -2843,8 +2833,11 @@ defmodule Module.Types.Descr do
 
       {dynamic, static} ->
         if descr_key?(dynamic, :map) and map_only?(static) do
-          {_, dynamic_taken, dynamic_result} = map_take_static(dynamic, key, initial)
-          {static_optional?, static_taken, static_result} = map_take_static(static, key, initial)
+          {_, dynamic_taken, dynamic_result} = map_take_key_static(dynamic, key, initial)
+
+          {static_optional?, static_taken, static_result} =
+            map_take_key_static(static, key, initial)
+
           result = union(dynamic(updater.(dynamic_result)), updater.(static_result))
 
           cond do
@@ -2865,20 +2858,20 @@ defmodule Module.Types.Descr do
 
   # Takes a static map type and removes a key from it.
   # This allows the key to be put or deleted later on.
-  defp map_take_static(%{map: bdd}, key, initial) do
-    map_dnf_take_static(map_bdd_to_dnf(bdd), key, initial)
+  defp map_take_key_static(%{map: bdd}, key, initial) do
+    map_dnf_take_key_static(map_bdd_to_dnf(bdd), key, initial)
   end
 
   # If there is no map part to this static type, there is nothing to delete.
-  defp map_take_static(%{}, _key, initial) do
+  defp map_take_key_static(%{}, _key, initial) do
     {false, initial, none()}
   end
 
-  defp map_take_static(:term, _key, initial) do
+  defp map_take_key_static(:term, _key, initial) do
     {true, maybe_union(initial, fn -> term() end), open_map()}
   end
 
-  defp map_dnf_take_static(dnf, key, initial) do
+  defp map_dnf_take_key_static(dnf, key, initial) do
     {value, descr} =
       Enum.reduce(dnf, {initial, none()}, fn
         # Optimization: if there are no negatives, we can directly remove the key.
@@ -2911,31 +2904,9 @@ defmodule Module.Types.Descr do
   end
 
   @doc """
-  Fetches and puts a `key_or_domains`, assuming that the descr is exclusively
-  a map (or dynamic).
-
-  This is a counter-part to `map_put/3` but one that assumes the `key_or_domains` exist.
-  """
-  def map_put_existing(:term, _key_or_domains, _type), do: :badmap
-
-  def map_put_existing(descr, key_or_domains, :term),
-    do: map_put_existing_shared(descr, key_or_domains, :term)
-
-  def map_put_existing(descr, key_or_domains, type) do
-    case :maps.take(:dynamic, type) do
-      :error -> map_put_existing_shared(descr, key_or_domains, type)
-      {dynamic, _static} -> map_put_existing_shared(dynamic(descr), key_or_domains, dynamic)
-    end
-  end
+  Updates the `key_descr` with `type`.
 
-  defp map_put_existing_shared(descr, key, type) when is_atom(key) do
-    with {_, type} <- map_take(descr, key, none(), &map_put_key_static(&1, key, type)) do
-      {:ok, type}
-    end
-  end
-
-  @doc """
-  TODO
+  `key_descr` is split into optional and required keys and tracked accordingly.
   """
   def map_update(:term, _key_descr, _type), do: :badmap
 
@@ -3053,7 +3024,7 @@ defmodule Module.Types.Descr do
 
   defp map_update_keys(dnf, keys, type, required_or_optional, missing_fun, acc) do
     Enum.reduce(keys, acc, fn key, {present?, acc_value, acc_descr} ->
-      {optional?, value, descr} = map_dnf_take_static(dnf, key, none())
+      {optional?, value, descr} = map_dnf_take_key_static(dnf, key, none())
       missing? = missing_fun.(optional?, value)
 
       required_or_optional == :required and missing? and throw({:badkey, key})
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index d3ceba3e5b5..78daad7b661 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1736,120 +1736,59 @@ defmodule Module.Types.DescrTest do
                {:ok, dynamic(closed_map(key: atom([:value, :new_value])))}
     end
 
-    # TODO: needs to be rewritten to key types
-    test "map_delete" do
-      assert map_delete(term(), :a) == :badmap
-      assert map_delete(integer(), :a) == :badmap
-      assert map_delete(union(open_map(), integer()), :a) == :badmap
+    test "map_take_key" do
+      assert map_take_key(term(), :a) == :badmap
+      assert map_take_key(integer(), :a) == :badmap
+      assert map_take_key(union(open_map(), integer()), :a) == :badmap
 
-      assert map_delete(closed_map(a: integer(), b: atom()), :a)
-             |> elem(1)
-             |> equal?(closed_map(b: atom()))
-
-      assert map_delete(empty_map(), :a) |> elem(1) |> equal?(empty_map())
-
-      assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a)
-             |> elem(1)
-             |> equal?(closed_map(b: atom()))
-
-      # Deleting a non-existent key
-      assert map_delete(closed_map(a: integer(), b: atom()), :c)
-             |> elem(1)
-             |> equal?(closed_map(a: integer(), b: atom()))
-
-      # Deleting from a dynamic map
-      assert map_delete(dynamic(), :a) == {:ok, dynamic(open_map(a: not_set()))}
-
-      # Deleting from an open map
-      {:ok, type} = map_delete(open_map(a: integer(), b: atom()), :a)
-      assert equal?(type, open_map(a: not_set(), b: atom()))
-
-      # Deleting from a union of maps
-      {:ok, type} = map_delete(union(closed_map(a: integer()), closed_map(b: atom())), :a)
-      assert equal?(type, union(empty_map(), closed_map(b: atom())))
-
-      # Deleting from a gradual map
-      {:ok, type} = map_delete(union(dynamic(), closed_map(a: integer())), :a)
-      assert equal?(type, union(dynamic(open_map(a: not_set())), empty_map()))
-
-      {:ok, type} = map_delete(dynamic(open_map(a: not_set())), :b)
-      assert equal?(type, dynamic(open_map(a: not_set(), b: not_set())))
-
-      # Deleting from an intersection of maps
-      {:ok, type} = map_delete(intersection(open_map(a: integer()), open_map(b: atom())), :a)
-      assert equal?(type, open_map(a: not_set(), b: atom()))
-
-      # Deleting from a difference of maps
-      {:ok, type} =
-        map_delete(
-          difference(closed_map(a: integer(), b: atom()), closed_map(a: integer())),
-          :b
-        )
-
-      assert equal?(type, closed_map(a: integer()))
-
-      {:ok, type} = map_delete(difference(open_map(), open_map(a: not_set())), :a)
-      assert equal?(type, open_map(a: not_set()))
-    end
-
-    test "map_delete with atom fallback" do
-      assert closed_map(a: integer(), b: atom(), atom: pid())
-             |> map_delete(:a)
-             |> elem(1)
-             |> equal?(closed_map(a: not_set(), b: atom(), atom: pid()))
-    end
-
-    # TODO: needs to be rewritten to key types
-    test "map_take" do
-      assert map_take(term(), :a) == :badmap
-      assert map_take(integer(), :a) == :badmap
-      assert map_take(union(open_map(), integer()), :a) == :badmap
-
-      {took, rest} = map_take(closed_map(a: integer(), b: atom()), :a)
+      {took, rest} = map_take_key(closed_map(a: integer(), b: atom()), :a)
       assert equal?(took, integer()) and equal?(rest, closed_map(b: atom()))
 
       # Deleting a non-existent key
-      assert map_take(empty_map(), :a) == :badkey
-      assert map_take(closed_map(a: integer(), b: atom()), :c) == :badkey
-      assert map_take(closed_map(a: if_set(integer()), b: atom()), :a) == :badkey
+      assert map_take_key(empty_map(), :a) == :badkey
+      assert map_take_key(closed_map(a: integer(), b: atom()), :c) == :badkey
+      assert map_take_key(closed_map(a: if_set(integer()), b: atom()), :a) == :badkey
 
       # Deleting from a dynamic map
-      assert map_take(dynamic(), :a) == {dynamic(), dynamic(open_map(a: not_set()))}
+      assert map_take_key(dynamic(), :a) == {dynamic(), dynamic(open_map(a: not_set()))}
 
       # Deleting from an open map
-      {value, type} = map_take(open_map(a: integer(), b: atom()), :a)
+      {value, type} = map_take_key(open_map(a: integer(), b: atom()), :a)
       assert value == integer()
       assert equal?(type, open_map(a: not_set(), b: atom()))
 
       # Deleting from a union of maps
       union = union(closed_map(a: integer()), closed_map(b: atom()))
-      assert map_take(union, :a) == :badkey
-      {value, type} = map_take(dynamic(union), :a)
+      assert map_take_key(union, :a) == :badkey
+      {value, type} = map_take_key(dynamic(union), :a)
       assert value == dynamic(integer())
       assert equal?(type, dynamic(union(empty_map(), closed_map(b: atom()))))
 
       # Deleting from a gradual map
-      {value, type} = map_take(union(dynamic(), closed_map(a: integer())), :a)
+      {value, type} = map_take_key(union(dynamic(), closed_map(a: integer())), :a)
       assert value == union(dynamic(), integer())
       assert equal?(type, union(dynamic(open_map(a: not_set())), empty_map()))
 
-      {value, type} = map_take(dynamic(open_map(a: not_set())), :b)
+      {value, type} = map_take_key(dynamic(open_map(a: not_set())), :b)
       assert equal?(value, dynamic())
       assert equal?(type, dynamic(open_map(a: not_set(), b: not_set())))
 
       # Deleting from an intersection of maps
-      {value, type} = map_take(intersection(open_map(a: integer()), open_map(b: atom())), :a)
+      {value, type} = map_take_key(intersection(open_map(a: integer()), open_map(b: atom())), :a)
       assert value == integer()
       assert equal?(type, open_map(a: not_set(), b: atom()))
 
       # Deleting from a difference of maps
       {value, type} =
-        map_take(difference(closed_map(a: integer(), b: atom()), closed_map(a: integer())), :b)
+        map_take_key(
+          difference(closed_map(a: integer(), b: atom()), closed_map(a: integer())),
+          :b
+        )
 
       assert value == atom()
       assert equal?(type, closed_map(a: integer()))
 
-      {value, type} = map_take(difference(open_map(), open_map(a: not_set())), :a)
+      {value, type} = map_take_key(difference(open_map(), open_map(a: not_set())), :a)
       assert equal?(value, term())
       assert equal?(type, open_map(a: not_set()))
     end