diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index d4a1e47fac8..179da01abef 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -6,6 +6,9 @@ defmodule Module.Types.Descr do
   # A bitmap is used to represent non-divisible types. All other
   # types require specific data structures.
 
+  # Vocabulary:
+  # DNF: disjunctive normal form
+
   # TODO: When we convert from AST to descr, we need to normalize
   # the dynamic type.
   import Bitwise
@@ -19,19 +22,26 @@ defmodule Module.Types.Descr do
   @bit_reference 1 <<< 6
 
   @bit_non_empty_list 1 <<< 7
-  @bit_map 1 <<< 8
-  @bit_tuple 1 <<< 9
-  @bit_fun 1 <<< 10
-  @bit_top (1 <<< 11) - 1
+  @bit_tuple 1 <<< 8
+  @bit_fun 1 <<< 9
+  @bit_top (1 <<< 10) - 1
+
+  @bit_unset 1 <<< 10
 
   @atom_top {:negation, :sets.new(version: 2)}
+  @map_top [{:open, %{}, []}]
 
   # Guard helpers
 
-  @term %{bitmap: @bit_top, atom: @atom_top}
+  @term %{bitmap: @bit_top, atom: @atom_top, map: @map_top}
   @none %{}
   @dynamic %{dynamic: @term}
 
+  # Map helpers
+
+  @unset %{bitmap: @bit_unset}
+  @term_or_unset %{bitmap: @bit_top ||| @bit_unset, atom: @atom_top, map: @map_top}
+
   # Type definitions
 
   def dynamic(), do: @dynamic
@@ -45,7 +55,10 @@ defmodule Module.Types.Descr do
   def integer(), do: %{bitmap: @bit_integer}
   def float(), do: %{bitmap: @bit_float}
   def fun(), do: %{bitmap: @bit_fun}
-  def map(), do: %{bitmap: @bit_map}
+  def map(pairs, open_or_closed), do: %{map: map_new(open_or_closed, pairs)}
+  def map(pairs), do: %{map: map_new(:closed, pairs)}
+  def map(), do: %{map: @map_top}
+  def empty_map(), do: map([])
   def non_empty_list(), do: %{bitmap: @bit_non_empty_list}
   def pid(), do: %{bitmap: @bit_pid}
   def port(), do: %{bitmap: @bit_port}
@@ -57,11 +70,7 @@ defmodule Module.Types.Descr do
 
   ## Set operations
 
-  @doc """
-  Check type is empty.
-  """
-  def empty?(descr), do: descr == @none
-  def term?(descr), do: Map.delete(descr, :dynamic) == @term
+  def term?(descr), do: subtype_static(@term, Map.delete(descr, :dynamic))
   def gradual?(descr), do: is_map_key(descr, :dynamic)
 
   @doc """
@@ -99,6 +108,7 @@ defmodule Module.Types.Descr do
   defp union(:bitmap, v1, v2), do: bitmap_union(v1, v2)
   defp union(:atom, v1, v2), do: atom_union(v1, v2)
   defp union(:dynamic, v1, v2), do: dynamic_union(v1, v2)
+  defp union(:map, v1, v2), do: map_union(v1, v2)
 
   @doc """
   Computes the intersection of two descrs.
@@ -136,6 +146,7 @@ defmodule Module.Types.Descr do
   defp intersection(:bitmap, v1, v2), do: bitmap_intersection(v1, v2)
   defp intersection(:atom, v1, v2), do: atom_intersection(v1, v2)
   defp intersection(:dynamic, v1, v2), do: dynamic_intersection(v1, v2)
+  defp intersection(:map, v1, v2), do: map_intersection(v1, v2)
 
   @doc """
   Computes the difference between two types.
@@ -164,12 +175,29 @@ defmodule Module.Types.Descr do
   defp difference(:bitmap, v1, v2), do: bitmap_difference(v1, v2)
   defp difference(:atom, v1, v2), do: atom_difference(v1, v2)
   defp difference(:dynamic, v1, v2), do: dynamic_difference(v1, v2)
+  defp difference(:map, v1, v2), do: map_difference(v1, v2)
 
   @doc """
   Compute the negation of a type.
   """
   def negation(%{} = descr), do: difference(term(), descr)
 
+  @doc """
+  Check if a type is empty. For gradual types, check that the upper bound
+  (the dynamic part) is empty. Stop as soon as one non-empty component is found.
+  Simpler components (bitmap, atom) are checked first for speed since, if they are
+  present, the type is non-empty as we normalize then during construction.
+  """
+  def empty?(%{} = descr) do
+    descr = Map.get(descr, :dynamic, descr)
+
+    descr == @none or
+      (not Map.has_key?(descr, :bitmap) and not Map.has_key?(descr, :atom) and
+         (not Map.has_key?(descr, :map) or map_empty?(descr.map)))
+  end
+
+  def not_empty?(descr), do: not empty?(descr)
+
   @doc """
   Converts a descr to its quoted representation.
   """
@@ -184,6 +212,7 @@ defmodule Module.Types.Descr do
   defp to_quoted(:bitmap, val), do: bitmap_to_quoted(val)
   defp to_quoted(:atom, val), do: atom_to_quoted(val)
   defp to_quoted(:dynamic, descr), do: dynamic_to_quoted(descr)
+  defp to_quoted(:map, dnf), do: map_to_quoted(dnf)
 
   @doc """
   Converts a descr to its quoted string representation.
@@ -216,6 +245,7 @@ defmodule Module.Types.Descr do
         %{^key => v2} ->
           case intersection(key, v1, v2) do
             0 -> acc
+            [] -> acc
             value -> [{key, value} | acc]
           end
 
@@ -234,6 +264,7 @@ defmodule Module.Types.Descr do
         %{^key => v1} ->
           case difference(key, v1, v2) do
             0 -> Map.delete(map, key)
+            [] -> Map.delete(map, key)
             value -> %{map | key => value}
           end
 
@@ -289,12 +320,14 @@ defmodule Module.Types.Descr do
 
   It is currently not optimized. Only to be used in tests.
   """
-  def equal?(left, right), do: subtype?(left, right) and subtype?(right, left)
+  def equal?(left, right) do
+    left == right or (subtype?(left, right) and subtype?(right, left))
+  end
 
   @doc """
   Check if two types have a non-empty intersection.
   """
-  def intersect?(left, right), do: not empty?(intersection(left, right))
+  def intersect?(left, right), do: not_empty?(intersection(left, right))
 
   @doc """
   Checks if a type is a compatible subtype of another.
@@ -340,7 +373,6 @@ defmodule Module.Types.Descr do
         port: @bit_port,
         reference: @bit_reference,
         non_empty_list: @bit_non_empty_list,
-        map: @bit_map,
         tuple: @bit_tuple,
         fun: @bit_fun
       ]
@@ -426,7 +458,7 @@ defmodule Module.Types.Descr do
     |> List.wrap()
   end
 
-  # Dynamic
+  ## Dynamic
   #
   # A type with a dynamic component is a gradual type; without, it is a static
   # type. The dynamic component itself is a static type; hence, any gradual type
@@ -495,4 +527,451 @@ defmodule Module.Types.Descr do
       _ -> nil
     end
   end
+
+  ## Not_set
+
+  # `not_set()` is a special base type that represents an unset field in a map.
+  # E.g., `%{a: integer(), b: not_set(), ...}` represents a map with an integer
+  # field `a` and an unset field `b`, and possibly other fields.
+
+  # The `if_set()` modifier is syntactic sugar for specifying the key as a union
+  # of the key type and `not_set()`. For example, `%{:foo => if_set(integer())}`
+  # is equivalent to `%{:foo => integer() or not_set()}`.
+
+  # `not_set()` has no meaning outside of map types.
+
+  def not_set(), do: @unset
+  def if_set(type), do: Map.update(type, :bitmap, @bit_unset, &(&1 ||| @bit_unset))
+
+  defp is_optional?(type), do: (Map.get(type, :bitmap, 0) &&& @bit_unset) != 0
+
+  defp remove_not_set(type) do
+    case type do
+      %{:bitmap => @bit_unset} -> Map.delete(type, :bitmap)
+      %{:bitmap => bitmap} -> Map.put(type, :bitmap, bitmap &&& ~~~@bit_unset)
+      _ -> type
+    end
+  end
+
+  ## Map
+  #
+  # Map operations.
+  #
+  # Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs
+  # `{map_literal, negated_literals}` where `map_literal` is a map type literal
+  # and `negated_literals` is a list of map type literals that are negated from it.
+  #
+  # A map literal is a pair `{:open | :closed, %{keys => value_types}}`.
+  #
+  # For instance, the type `%{..., a: integer()} and not %{b: atom()}` can be represented
+  # by the DNF containing one pair, where the positive literal is `{:open, %{a => integer()}}`
+  # and the negated literal is `{:closed, %{b => atom()}}`.
+  #
+  # The goal of keeping symbolic negations is to avoid 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.
+  #
+  # Set-theoretic operations take two DNFs (lists) and return a DNF (list).
+  # Simplifications can be done to prune the latter.
+
+  # Create a DNF from a specification of a map type.
+  defp map_new(open_or_closed, pairs), do: [{open_or_closed, Map.new(pairs), []}]
+
+  defp map_descr(tag, fields), do: %{map: [{tag, fields, []}]}
+
+  @doc """
+  Gets the type of the value returned by accessing `key` on `map`.
+  Does not guarantee the key exists. To do that, use `map_has_key?`.
+  """
+  def map_get!(%{} = descr, key) do
+    if not gradual?(descr) do
+      map_get_static(descr, key)
+    else
+      {dynamic, static} = Map.pop(descr, :dynamic)
+      dynamic_value_type = map_get_static(dynamic, key)
+      static_value_type = map_get_static(static, key)
+      union(intersection(dynamic(), dynamic_value_type), static_value_type)
+    end
+  end
+
+  @doc """
+  Check that a key is present.
+  """
+  def map_has_key?(descr, key) do
+    subtype?(descr, map([{key, term()}], :open))
+  end
+
+  # Assuming `descr` is a static type. Accessing `key` will, if it succeeds,
+  # return a value of the type returned. To guarantee that the key is always
+  # present, use `map_has_key?`. To guarantee that the key may be present
+  # use `map_may_have_key?`. If key is never present, result will be `none()`.
+  defp map_get_static(descr, key) when is_atom(key) do
+    descr_map = intersection(descr, map())
+
+    if empty?(descr_map) do
+      none()
+    else
+      map_split_on_key(descr_map.map, key)
+      |> Enum.reduce(none(), fn typeof_key, union -> union(typeof_key, union) end)
+      |> remove_not_set()
+    end
+  end
+
+  @doc """
+  Check that a key may be present.
+  """
+  def map_may_have_key?(descr, key) do
+    compatible?(descr, map([{key, term()}], :open))
+  end
+
+  # Union is list concatenation
+  defp map_union(dnf1, dnf2), do: dnf1 ++ dnf2
+
+  # Given two unions of maps, intersects each pair of maps.
+  defp map_intersection(dnf1, dnf2) do
+    Enum.flat_map(dnf1, &map_intersection_aux(&1, dnf2))
+  end
+
+  # Intersects a map with a union of maps.
+  defp map_intersection_aux({tag1, pos1, negs1}, dnf2) do
+    Enum.reduce(dnf2, [], fn {tag2, pos2, negs2}, acc ->
+      try do
+        {tag, fields} = map_literal_intersection(tag1, pos1, tag2, pos2)
+        [{tag, fields, negs1 ++ negs2} | acc]
+      catch
+        :empty_intersection -> acc
+      end
+    end)
+  end
+
+  # Intersects two map literals; throws if their intersection is empty.
+  defp map_literal_intersection(tag1, map1, tag2, map2) do
+    default1 = if tag1 == :open, do: @term_or_unset, else: @unset
+    default2 = if tag2 == :open, do: @term_or_unset, else: @unset
+
+    # if any intersection of values is empty, the whole intersection is empty
+    new_fields =
+      (for {key, value_type} <- map1 do
+         value_type2 = Map.get(map2, key, default2)
+         t = intersection(value_type, value_type2)
+         if empty?(t), do: throw(:empty_intersection), else: {key, t}
+       end ++
+         for {key, value_type} <- map2, not is_map_key(map1, key) do
+           t = intersection(default1, value_type)
+           if empty?(t), do: throw(:empty_intersection), else: {key, t}
+         end)
+      |> Map.new()
+
+    case {tag1, tag2} do
+      {:open, :open} -> {:open, new_fields}
+      _ -> {:closed, new_fields}
+    end
+  end
+
+  defp map_difference(dnf1, dnf2) do
+    case dnf2 do
+      [] ->
+        dnf1
+
+      [lit2 | dnf2] ->
+        Enum.flat_map(dnf1, fn lit1 -> map_single_difference(lit1, lit2) end)
+        |> map_difference(dnf2)
+    end
+  end
+
+  # Computes the difference between two maps union.
+  defp map_single_difference({tag1, fields1, negs1}, {tag2, fields2, negs2}) do
+    Enum.reduce(negs2, [{tag1, fields1, [{tag2, fields2} | negs1]}], fn
+      {tag2, fields2}, acc ->
+        try do
+          {tag, fields} = map_literal_intersection(tag1, fields1, tag2, fields2)
+          [{tag, fields, negs1} | acc]
+        catch
+          :empty_intersection -> acc
+        end
+    end)
+  end
+
+  # Emptiness checking for maps. Short-circuits if it finds a non-empty map literal in the union.
+  defp map_empty?(dnf) do
+    try do
+      for {tag, pos, negs} <- dnf do
+        map_empty?(tag, pos, negs)
+      end
+
+      true
+    catch
+      :not_empty -> false
+    end
+  end
+
+  defp map_empty?(_, _, []), do: throw(:not_empty)
+  defp map_empty?(_, _, [{:open, neg_fields} | _]) when neg_fields == %{}, do: true
+  defp map_empty?(:open, fs, [{:closed, _} | negs]), do: map_empty?(:open, fs, negs)
+
+  defp map_empty?(tag, fields, [{neg_tag, neg_fields} | negs]) do
+    try do
+      # keys that are present in the negative map, but not in the positive one
+      for {neg_key, neg_type} <- neg_fields, not is_map_key(fields, neg_key) do
+        cond do
+          # key is required, and the positive map is closed: empty intersection
+          tag == :closed and not is_optional?(neg_type) ->
+            throw(:no_intersection)
+
+          # if the positive map is open
+          tag == :open ->
+            diff = difference(@term_or_unset, neg_type)
+            empty?(diff) or map_empty?(tag, Map.put(fields, neg_key, diff), negs)
+        end
+      end
+
+      for {key, type} <- fields do
+        case neg_fields do
+          %{^key => neg_type} ->
+            diff = difference(type, neg_type)
+            empty?(diff) or map_empty?(tag, Map.put(fields, key, diff), negs)
+
+          %{} ->
+            if neg_tag == :closed and not is_optional?(type) do
+              throw(:no_intersection)
+            else
+              # an absent key in a open negative map can be ignored
+              default2 = if neg_tag == :open, do: @term_or_unset, else: @unset
+              diff = difference(type, default2)
+              empty?(diff) or map_empty?(tag, Map.put(fields, key, diff), negs)
+            end
+        end
+      end
+    catch
+      :no_intersection -> map_empty?(tag, fields, negs)
+    end
+  end
+
+  # Takes a map bdd and a key, and returns an equivalent dnf of pairs, in which
+  # the type of the key in the map can be found in the first element of the pair.
+  # See `split_line_on_key/5`.
+  defp map_split_on_key(dnf, key) do
+    Enum.flat_map(dnf, fn {tag, fields, negs} ->
+      {fst, snd} =
+        case single_split({tag, fields}, key) do
+          # { .. } the open map in a positive intersection can be ignored
+          :no_split -> {@term_or_unset, @term_or_unset}
+          # {typeof l, rest} is added to the positive accumulator
+          {value_type, rest_of_map} -> {value_type, rest_of_map}
+        end
+
+      case split_negative(negs, key, []) do
+        :no_split -> []
+        negative -> make_pairs_disjoint(negative) |> eliminate_negations(fst, snd)
+      end
+    end)
+  end
+
+  # Splits a map literal on a key. This means that given a map literal, compute
+  # the pair of types `{value_type, rest_of_map}` where `value_type` is the type
+  # associated with `key`, and `rest_of_map` is obtained by removing `key`.
+  defp single_split({tag, fields}, key) do
+    {value_type, rest_of_map} = Map.pop(fields, key)
+
+    cond do
+      value_type != nil -> {value_type, map_descr(tag, rest_of_map)}
+      tag == :closed -> {@unset, map_descr(tag, rest_of_map)}
+      # case where there is an open map with no keys { .. }
+      map_size(fields) == 0 -> :no_split
+      true -> {@term_or_unset, map_descr(tag, rest_of_map)}
+    end
+  end
+
+  # Given a line, that is, a list `positive` of map literals and `negative` of
+  # negated map literals, and a `key`, splits every map literal on the key and
+  # outputs a DNF of pairs, that is, a list (union) of (intersections) of pairs.
+  defp split_negative([], _key, neg_acc), do: neg_acc
+
+  defp split_negative([map_literal | negative], key, neg_acc) do
+    case single_split(map_literal, key) do
+      # an intersection that contains %{...} is empty, so we discard it entirely
+      :no_split ->
+        :no_split
+
+      # {typeof l, rest_of_map} is added to the negative accumulator
+      {value_type, rest_of_map} ->
+        split_negative(negative, key, [{value_type, rest_of_map} | neg_acc])
+    end
+  end
+
+  defp map_to_quoted(dnf) do
+    map_normalize(dnf)
+    |> case do
+      [] -> []
+      x -> Enum.map(x, &map_line_to_quoted/1) |> Enum.reduce(&{:or, [], [&2, &1]}) |> List.wrap()
+    end
+  end
+
+  # Use heuristics to normalize a map dnf for pretty printing.
+  # TODO: eliminate some simple negations, those which have only zero or one key in common.
+  defp map_normalize(dnf) do
+    dnf
+    |> Enum.filter(&(not map_empty?([&1])))
+    |> Enum.map(fn {tag, fields, negs} ->
+      {tag, fields, filter_empty_negations(tag, fields, negs)}
+    end)
+  end
+
+  # Adapted from `map_empty?` to remove useless negations.
+  defp filter_empty_negations(_tag, _fields, []), do: []
+
+  defp filter_empty_negations(tag, fields, [{neg_tag, neg_fields} | negs]) do
+    try do
+      for {neg_key, neg_type} when not is_map_key(fields, neg_key) <- neg_fields do
+        # key is required, and the positive map is closed: empty intersection
+        if tag == :closed and not is_optional?(neg_type), do: throw(:no_intersection)
+      end
+
+      for {key, type} when not is_map_key(neg_fields, key) <- fields,
+          # key is required, and the negative map is closed: empty intersection
+          not is_optional?(type) and neg_tag == :closed do
+        throw(:no_intersection)
+      end
+
+      [{neg_tag, neg_fields} | filter_empty_negations(tag, fields, negs)]
+    catch
+      :no_intersection -> filter_empty_negations(tag, fields, negs)
+    end
+  end
+
+  defp map_line_to_quoted({tag, positive_map, negative_maps}) do
+    case negative_maps do
+      [] ->
+        map_literal_to_quoted({tag, positive_map})
+
+      _ ->
+        negative_maps
+        |> Enum.map(&map_literal_to_quoted/1)
+        |> Enum.reduce(&{:or, [], [&2, &1]})
+        |> Kernel.then(
+          &{:and, [], [map_literal_to_quoted({tag, positive_map}), {:not, [], [&1]}]}
+        )
+    end
+  end
+
+  def map_literal_to_quoted({tag, fields}) do
+    case tag do
+      :closed -> {:%{}, [], fields_to_quoted(tag, fields)}
+      :open -> {:%{}, [], [{:..., [], nil} | fields_to_quoted(tag, fields)]}
+    end
+  end
+
+  defp fields_to_quoted(tag, map) do
+    for {key, type} <- map,
+        not (tag == :open and is_optional?(type) and term?(type)) do
+      cond do
+        is_optional?(type) and empty?(type) -> {literal(key), {:not_set, [], []}}
+        is_optional?(type) -> {literal(key), {:if_set, [], [to_quoted(type)]}}
+        true -> {literal(key), to_quoted(type)}
+      end
+    end
+  end
+
+  ## Pairs
+  #
+  # To simplify disjunctive normal forms of e.g., map types, it is useful to
+  # convert them into disjunctive normal forms of pairs of types, and define
+  # normalization algorithms on pairs.
+
+  # Takes a DNF of pairs and simplifies it into a equivalent single list (union)
+  # of type pairs. The `term` argument should be either `@term_or_unset` (for
+  # map value types) or `@term` in general.
+  # Remark: all lines of a pair dnf are naturally disjoint, because choosing a
+  # different edge means intersection with a literal or its negation.
+
+  # A line is a list of pairs `{positive, negative}` where `positive` is a list of
+  # literals and `negative` is a list of negated literals. Positive pairs can
+  # all be intersected component-wise. Negative ones are eliminated iteratively.
+
+  # Eliminates negations from `{t, s} and not negative` where `negative` is a
+  # union of pairs disjoint on their first component.
+  # Formula:
+  #   {t, s} and not (union<i=1..n> {t_i, s_i})
+  #       = union<i=1..n> {t and t_i, s and not s_i}
+  #            or {t and not (union{i=1..n} t_i), s}
+  # This eliminates all top-level negations and produces a union of pairs that
+  # are disjoint on their first component.
+  defp eliminate_negations(negative, t, s) do
+    {pair_union, diff_of_t_i} =
+      Enum.reduce(
+        negative,
+        {[], t},
+        fn {t_i, s_i}, {accu, diff_of_t_i} ->
+          i = intersection(t, t_i)
+
+          if not_empty?(i) do
+            diff_of_t_i = difference(diff_of_t_i, t_i)
+            s_diff = difference(s, s_i)
+
+            if not_empty?(s_diff),
+              do: {[i | accu], diff_of_t_i},
+              else: {accu, diff_of_t_i}
+          else
+            {accu, diff_of_t_i}
+          end
+        end
+      )
+
+    [diff_of_t_i | pair_union]
+  end
+
+  # Inserts a pair of types {fst, snd} into a list of pairs that are disjoint
+  # on their first component. The invariant on `acc` is that its elements are
+  # two-to-two disjoint with the first argument's `pairs`.
+  #
+  # To insert {fst, snd} into a disjoint pairs list, we go through the list to find
+  # each pair whose first element has a non-empty intersection with `fst`. Then
+  # we decompose {fst, snd} over each such pair to produce disjoint ones, and add
+  # the decompositions into the accumulator.
+  defp add_pair_to_disjoint_list([], fst, snd, acc), do: [{fst, snd} | acc]
+
+  defp add_pair_to_disjoint_list([{s1, s2} | pairs], fst, snd, acc) do
+    x = intersection(fst, s1)
+
+    if empty?(x) do
+      add_pair_to_disjoint_list(pairs, fst, snd, [{s1, s2} | acc])
+    else
+      fst_diff = difference(fst, s1)
+      s1_diff = difference(s1, fst)
+      empty_fst_diff = empty?(fst_diff)
+      empty_s1_diff = empty?(s1_diff)
+
+      cond do
+        # if fst is a subtype of s1, the disjointness invariant ensures we can
+        # add those two pairs and end the recursion
+        empty_fst_diff and empty_s1_diff ->
+          [{x, union(snd, s2)} | pairs ++ acc]
+
+        empty_fst_diff ->
+          [{s1_diff, s2}, {x, union(snd, s2)} | pairs ++ acc]
+
+        empty_s1_diff ->
+          add_pair_to_disjoint_list(pairs, fst_diff, snd, [{x, union(snd, s2)} | acc])
+
+        true ->
+          # case where, when comparing {fst, snd} and {s1, s2}, both (fst and not s1)
+          # and (s1 and not fst) are non empty. that is, there is something in fst
+          # that is not in s1, and something in s1 that is not in fst
+          add_pair_to_disjoint_list(pairs, fst_diff, snd, [
+            {s1_diff, s2},
+            {x, union(snd, s2)} | acc
+          ])
+      end
+    end
+  end
+
+  # Makes a union of pairs into an equivalent union of disjoint pairs.
+  defp make_pairs_disjoint(pairs) do
+    Enum.reduce(pairs, [], fn {t1, t2}, acc -> add_pair_to_disjoint_list(acc, t1, t2, []) end)
+  end
 end
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index b680c893c2e..4d024e4ea5e 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -24,7 +24,9 @@ defmodule Module.Types.DescrTest do
       assert union(atom(), atom([:a])) == atom()
       assert union(atom([:a]), atom([:b])) == atom([:a, :b])
       assert union(atom([:a]), negation(atom([:b]))) == negation(atom([:b]))
-      assert union(negation(atom([:a, :b])), negation(atom([:b, :c]))) == negation(atom([:b]))
+
+      assert union(negation(atom([:a, :b])), negation(atom([:b, :c])))
+             |> equal?(negation(atom([:b])))
     end
 
     test "all primitive types" do
@@ -52,6 +54,18 @@ defmodule Module.Types.DescrTest do
       assert equal?(union(term(), dynamic()), term())
       assert equal?(union(intersection(dynamic(), atom()), atom()), atom())
     end
+
+    test "map" do
+      assert equal?(union(map(), map()), map())
+      assert equal?(union(map(a: integer()), map()), map())
+      assert equal?(union(map(a: integer()), negation(map(a: integer()))), term())
+
+      a_integer_open = map([a: integer()], :open)
+      assert equal?(union(map(a: integer()), a_integer_open), a_integer_open)
+
+      assert difference(map([a: integer()], :open), map(b: boolean()))
+             |> equal?(map([a: integer()], :open))
+    end
   end
 
   describe "intersection" do
@@ -85,6 +99,19 @@ defmodule Module.Types.DescrTest do
       assert empty?(intersection(dynamic(), none()))
       assert empty?(intersection(intersection(dynamic(), atom()), integer()))
     end
+
+    test "map" do
+      assert intersection(map(), map()) == map()
+      assert equal?(intersection(map(a: integer()), map()), map(a: integer()))
+
+      a_integer_open = map([a: integer()], :open)
+      assert equal?(intersection(map(a: integer()), a_integer_open), map(a: integer()))
+
+      optional_a_integer_closed = map([a: if_set(integer())], :closed)
+      assert equal?(intersection(map(a: integer()), optional_a_integer_closed), map(a: integer()))
+
+      assert empty?(intersection(map(a: integer()), map(a: atom())))
+    end
   end
 
   describe "difference" do
@@ -118,6 +145,22 @@ defmodule Module.Types.DescrTest do
       assert empty?(difference(dynamic(), term()))
       assert empty?(difference(none(), dynamic()))
     end
+
+    test "map" do
+      assert empty?(difference(map(), map()))
+      assert empty?(difference(map(), term()))
+      assert equal?(difference(map(), none()), map())
+      assert empty?(difference(map(a: integer()), map()))
+      assert empty?(difference(map(a: integer()), map(a: integer())))
+      assert empty?(difference(map(a: integer()), map([a: integer()], :open)))
+
+      assert difference(map(a: integer(), b: if_set(atom())), map(a: integer()))
+             |> difference(map(a: integer(), b: atom()))
+             |> empty?()
+
+      assert difference(map([a: atom()], :open), map(b: integer()))
+             |> equal?(map([a: atom()], :open))
+    end
   end
 
   describe "subtype" do
@@ -145,6 +188,19 @@ defmodule Module.Types.DescrTest do
       assert subtype?(intersection(dynamic(), integer()), integer())
       assert subtype?(integer(), union(dynamic(), integer()))
     end
+
+    test "map" do
+      assert subtype?(map(), term())
+      assert subtype?(map([a: integer()], :closed), map())
+      assert subtype?(map([a: integer()], :closed), map([a: integer()], :closed))
+      assert subtype?(map([a: integer()], :closed), map([a: integer()], :open))
+      assert subtype?(map([a: integer(), b: atom()], :closed), map([a: integer()], :open))
+      assert subtype?(map(a: integer()), map(a: union(integer(), atom())))
+
+      # optional
+      refute subtype?(map(a: if_set(integer())), map(a: integer()))
+      assert subtype?(map(a: integer()), map(a: if_set(integer())))
+    end
   end
 
   describe "compatible" do
@@ -170,6 +226,109 @@ defmodule Module.Types.DescrTest do
       assert compatible?(dynamic(), integer())
       assert compatible?(integer(), dynamic())
     end
+
+    test "map" do
+      assert compatible?(map(a: integer()), map())
+      assert compatible?(intersection(dynamic(), map()), map(a: integer()))
+    end
+  end
+
+  describe "empty" do
+    test "map" do
+      assert intersection(map(b: atom()), map([a: integer()], :open)) |> empty?
+    end
+  end
+
+  describe "map operations" do
+    test "get field" do
+      assert map_get!(map(a: integer()), :a) == integer()
+      assert map_get!(dynamic(), :a) == dynamic()
+
+      assert intersection(dynamic(), map([a: integer()], :open))
+             |> map_get!(:a) == intersection(integer(), dynamic())
+
+      assert map([my_map: map([foo: integer()], :open)], :open)
+             |> intersection(map([my_map: map([bar: boolean()], :open)], :open))
+             |> map_get!(:my_map)
+             |> equal?(map([foo: integer(), bar: boolean()], :open))
+
+      assert map_get!(union(map(a: integer()), map(a: atom())), :a) == union(integer(), atom())
+      assert map_get!(union(map(a: integer()), map(b: atom())), :a) == integer()
+      assert map_get!(term(), :a) == term()
+
+      assert map(a: union(integer(), atom()))
+             |> difference(map([a: integer()], :open))
+             |> map_get!(:a)
+             |> equal?(atom())
+
+      assert map(a: integer(), b: atom())
+             |> difference(map(a: integer(), b: atom([:foo])))
+             |> map_get!(:a)
+             |> equal?(integer())
+
+      assert map(a: integer())
+             |> difference(map(a: atom()))
+             |> map_get!(:a)
+             |> equal?(integer())
+
+      assert map([a: integer(), b: atom()], :open)
+             |> union(map(a: tuple()))
+             |> map_get!(:a)
+             |> equal?(union(integer(), tuple()))
+
+      assert map(a: atom())
+             |> difference(map(a: atom([:foo, :bar])))
+             |> difference(map(a: atom([:bar])))
+             |> map_get!(:a)
+             |> equal?(intersection(atom(), negation(atom([:foo, :bar]))))
+
+      assert map(a: union(atom(), pid()), b: integer(), c: tuple())
+             |> difference(map([a: atom(), b: integer()], :open))
+             |> difference(map([a: atom(), c: tuple()], :open))
+             |> map_get!(:a) == pid()
+
+      assert map(a: union(atom([:foo]), pid()), b: integer(), c: tuple())
+             |> difference(map([a: atom([:foo]), b: integer()], :open))
+             |> difference(map([a: atom(), c: tuple()], :open))
+             |> map_get!(:a) == pid()
+
+      assert map(a: union(atom([:foo, :bar, :baz]), integer()))
+             |> difference(map([a: atom([:foo, :bar])], :open))
+             |> difference(map([a: atom([:foo, :baz])], :open))
+             |> map_get!(:a) == integer()
+    end
+
+    test "key presence" do
+      assert map_has_key?(map(a: integer()), :a)
+      refute map_has_key?(map(a: integer()), :b)
+      refute map_has_key?(map(), :a)
+      refute map_has_key?(map(a: union(integer(), not_set())), :a)
+      refute map_has_key?(union(map(a: integer()), map(b: atom())), :a)
+      assert map_has_key?(union(map(a: integer()), map(a: atom())), :a)
+      assert map_has_key?(intersection(dynamic(), map(a: integer())), :a)
+      refute map_has_key?(intersection(dynamic(), map(a: integer())), :b)
+
+      refute map_may_have_key?(map(foo: integer()), :bar)
+      assert map_may_have_key?(map(foo: integer()), :foo)
+      assert map_may_have_key?(dynamic(), :foo)
+      refute map_may_have_key?(intersection(dynamic(), map([foo: not_set()], :open)), :foo)
+    end
+
+    test "type-checking map access" do
+      # dynamic() and %{..., :a => integer(), b: not_set()}
+      t = intersection(dynamic(), map([a: integer(), c: not_set()], :open))
+
+      assert subtype?(map_get!(t, :a), integer())
+      assert map_get!(t, :b) == dynamic()
+
+      assert map_has_key?(t, :a)
+      refute map_has_key?(t, :b)
+      refute map_has_key?(t, :c)
+
+      assert map_may_have_key?(t, :a)
+      assert map_may_have_key?(t, :b)
+      refute map_may_have_key?(t, :c)
+    end
   end
 
   describe "to_quoted" do
@@ -212,6 +371,39 @@ defmodule Module.Types.DescrTest do
 
       assert union(atom([:foo, :bar]), dynamic()) |> to_quoted_string() ==
                "dynamic() or (:bar or :foo)"
+
+      assert intersection(dynamic(), map(a: integer())) |> to_quoted_string() ==
+               "dynamic() and %{:a => integer()}"
+    end
+
+    test "map" do
+      assert map() |> to_quoted_string() == "%{...}"
+      assert map(a: integer()) |> to_quoted_string() == "%{:a => integer()}"
+      assert map([a: float()], :open) |> to_quoted_string() == "%{..., :a => float()}"
+
+      # TODO: support this simplification
+      # assert difference(map(), map([a: term()], :open)) |> to_quoted_string() ==
+      #          "%{..., :a => not_set()}"
+
+      assert map(a: integer(), b: atom()) |> to_quoted_string() ==
+               "%{:a => integer(), :b => atom()}"
+
+      assert map([a: float()], :open)
+             |> difference(map([a: float()], :closed))
+             |> to_quoted_string() == "%{..., :a => float()} and not %{:a => float()}"
+
+      assert difference(map(), empty_map()) |> to_quoted_string() == "%{...} and not %{}"
+
+      assert map(foo: union(integer(), not_set())) |> to_quoted_string() ==
+               "%{:foo => if_set(integer())}"
+
+      assert difference(map([a: integer()], :open), map(b: boolean())) |> to_quoted_string() ==
+               "%{..., :a => integer()}"
+
+      assert map([a: integer(), b: atom()], :open)
+             |> difference(map([b: atom()], :open))
+             |> union(map([a: integer()], :open))
+             |> to_quoted_string() == "%{..., :a => integer()}"
     end
   end
 end