From b669d1206b92e173e81866ae0cf899c59e218519 Mon Sep 17 00:00:00 2001
From: gldubc <guilduboc@gmail.com>
Date: Fri, 17 May 2024 18:00:15 +0200
Subject: [PATCH 1/2] Set-theoretic tuple types

---
 lib/elixir/lib/module/types/descr.ex          | 232 +++++++++++++++++-
 .../test/elixir/module/types/descr_test.exs   | 105 ++++++++
 2 files changed, 329 insertions(+), 8 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 15a06c3e11e..d167fb52964 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -23,21 +23,22 @@ defmodule Module.Types.Descr do
   @bit_reference 1 <<< 6
 
   @bit_non_empty_list 1 <<< 7
-  @bit_tuple 1 <<< 8
-  @bit_fun 1 <<< 9
-  @bit_top (1 <<< 10) - 1
+  @bit_fun 1 <<< 8
+  @bit_top (1 <<< 9) - 1
 
   @bit_list @bit_empty_list ||| @bit_non_empty_list
   @bit_number @bit_integer ||| @bit_float
-  @bit_optional 1 <<< 10
+  @bit_optional 1 <<< 9
 
   @atom_top {:negation, :sets.new(version: 2)}
+  @tuple_top [{:open, %{}, []}]
+  @tuple_empty [{:closed, %{}, []}]
   @map_top [{:open, %{}, []}]
   @map_empty [{:closed, %{}, []}]
 
   # Guard helpers
 
-  @term %{bitmap: @bit_top, atom: @atom_top, map: @map_top}
+  @term %{bitmap: @bit_top, atom: @atom_top, tuple: @tuple_top, map: @map_top}
   @none %{}
   @dynamic %{dynamic: @term}
 
@@ -63,7 +64,11 @@ defmodule Module.Types.Descr do
   def pid(), do: %{bitmap: @bit_pid}
   def port(), do: %{bitmap: @bit_port}
   def reference(), do: %{bitmap: @bit_reference}
-  def tuple(), do: %{bitmap: @bit_tuple}
+  def empty_tuple(), do: %{tuple: @tuple_empty}
+  def tuple(), do: %{tuple: @tuple_top}
+  def open_tuple(), do: %{tuple: @tuple_top}
+  def open_tuple(elements), do: %{tuple: tuple_new(:open, elements)}
+  def tuple(elements), do: %{tuple: tuple_new(:closed, elements)}
 
   @boolset :sets.from_list([true, false], version: 2)
   def boolean(), do: %{atom: {:union, @boolset}}
@@ -81,7 +86,12 @@ defmodule Module.Types.Descr do
   # `not_set()` has no meaning outside of map types.
 
   @not_set %{bitmap: @bit_optional}
-  @term_or_optional %{bitmap: @bit_top ||| @bit_optional, atom: @atom_top, map: @map_top}
+  @term_or_optional %{
+    bitmap: @bit_top ||| @bit_optional,
+    atom: @atom_top,
+    tuple: @tuple_top,
+    map: @map_top
+  }
 
   def not_set(), do: @not_set
   def if_set(type), do: Map.update(type, :bitmap, @bit_optional, &(&1 ||| @bit_optional))
@@ -132,6 +142,7 @@ defmodule Module.Types.Descr do
   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)
+  defp union(:tuple, v1, v2), do: tuple_union(v1, v2)
 
   @doc """
   Computes the intersection of two descrs.
@@ -160,6 +171,7 @@ defmodule Module.Types.Descr do
   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)
+  defp intersection(:tuple, v1, v2), do: tuple_intersection(v1, v2)
 
   @doc """
   Computes the difference between two types.
@@ -189,6 +201,7 @@ defmodule Module.Types.Descr do
   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)
+  defp difference(:tuple, v1, v2), do: tuple_difference(v1, v2)
 
   @doc """
   Compute the negation of a type.
@@ -208,6 +221,7 @@ defmodule Module.Types.Descr do
 
     descr == @none or
       (not Map.has_key?(descr, :bitmap) and not Map.has_key?(descr, :atom) and
+         (not Map.has_key?(descr, :tuple) or tuple_empty?(descr.tuple)) and
          (not Map.has_key?(descr, :map) or map_empty?(descr.map)))
   end
 
@@ -230,6 +244,7 @@ defmodule Module.Types.Descr do
   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)
+  defp to_quoted(:tuple, dnf), do: tuple_to_quoted(dnf)
 
   @doc """
   Converts a descr to its quoted string representation.
@@ -361,7 +376,6 @@ defmodule Module.Types.Descr do
         port: @bit_port,
         reference: @bit_reference,
         non_empty_list: @bit_non_empty_list,
-        tuple: @bit_tuple,
         fun: @bit_fun
       ]
 
@@ -576,6 +590,113 @@ defmodule Module.Types.Descr do
     end
   end
 
+  ## Tuple
+
+  defp tuple_new(tag, elements) do
+    pairs =
+      elements
+      |> Enum.map_reduce(0, fn type, acc -> {{acc, type}, acc + 1} end)
+      |> elem(0)
+
+    map_new(tag, :maps.from_list(pairs))
+  end
+
+  defp tuple_intersection(left, right), do: map_intersection(left, right)
+  defp tuple_difference(left, right), do: map_difference(left, right)
+  defp tuple_union(left, right), do: map_union(left, right)
+
+  def tuple_fetch(%{} = descr, key) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if is_map_key(descr, :tuple) and tuple_only?(descr) do
+          {static_optional?, static_type} = tuple_fetch_static(descr, key) |> pop_optional()
+
+          if static_optional? or empty?(static_type) do
+            :badindex
+          else
+            {false, static_type}
+          end
+        else
+          :badtuple
+        end
+
+      {%{map: {:open, fields, []}}, static} when fields == %{} and static == @none ->
+        {true, dynamic()}
+
+      {dynamic, static} ->
+        if is_map_key(dynamic, :tuple) and tuple_only?(static) do
+          {dynamic_optional?, dynamic_type} = tuple_fetch_static(dynamic, key) |> pop_optional()
+          {static_optional?, static_type} = tuple_fetch_static(static, key) |> pop_optional()
+
+          if static_optional? or empty?(dynamic_type) do
+            :badindex
+          else
+            {dynamic_optional?, union(dynamic(dynamic_type), static_type)}
+          end
+        else
+          :badtuple
+        end
+    end
+  end
+
+  defp tuple_only?(descr), do: empty?(Map.delete(descr, :tuple))
+
+  defp tuple_fetch_static(descr, index) when is_integer(index) do
+    case descr do
+      %{tuple: tuple} -> Enum.reduce(map_split_on_key(tuple, index), none(), &union/2)
+      %{} -> none()
+    end
+  end
+
+  defp tuple_to_quoted(dnf) do
+    dnf
+    |> map_normalize()
+    |> Enum.map(&tuple_each_to_quoted/1)
+    |> case do
+      [] -> []
+      dnf -> Enum.reduce(dnf, &{:or, [], [&2, &1]}) |> List.wrap()
+    end
+  end
+
+  defp tuple_each_to_quoted({tag, positive_map, negative_maps}) do
+    case negative_maps do
+      [] ->
+        tuple_literal_to_quoted({tag, positive_map})
+
+      _ ->
+        negative_maps
+        |> Enum.map(&tuple_literal_to_quoted/1)
+        |> Enum.reduce(&{:or, [], [&2, &1]})
+        |> Kernel.then(
+          &{:and, [], [tuple_literal_to_quoted({tag, positive_map}), {:not, [], [&1]}]}
+        )
+    end
+  end
+
+  def tuple_literal_to_quoted({:closed, fields}) when map_size(fields) == 0 do
+    {:empty_map, [], []}
+  end
+
+  def tuple_literal_to_quoted({tag, fields}) do
+    case tag do
+      :closed -> {:{}, [], tuple_fields_to_quoted(tag, fields)}
+      :open -> {:{}, [], tuple_fields_to_quoted(tag, fields) ++ [{:..., [], nil}]}
+    end
+  end
+
+  defp tuple_fields_to_quoted(tag, map) do
+    sorted = Enum.sort(map)
+
+    for {_, type} <- sorted,
+        not (tag == :open and optional?(type) and term_type?(type)) do
+      cond do
+        not optional?(type) -> to_quoted(type)
+        empty?(type) -> {:not_set, [], []}
+        true -> {:if_set, [], [to_quoted(type)]}
+      end
+    end
+  end
+
   ## Map
   #
   # Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs
@@ -672,6 +793,19 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp remove_optional(type) do
+    case type do
+      %{bitmap: @bit_optional} ->
+        Map.delete(type, :bitmap)
+
+      %{bitmap: bitmap} when (bitmap &&& @bit_optional) != 0 ->
+        %{type | bitmap: bitmap - @bit_optional}
+
+      _ ->
+        type
+    end
+  end
+
   # Union is list concatenation
   defp map_union(dnf1, dnf2), do: dnf1 ++ dnf2
 
@@ -826,6 +960,86 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # Emptiness checking for tuples.
+  #
+  # Short-circuits if it finds a non-empty map literal in the union.
+  # Since the algorithm is recursive, we implement the short-circuiting
+  # as throw/catch.
+  defp tuple_empty?(dnf) do
+    try do
+      for {tag, pos, negs} <- dnf do
+        tuple_empty?(tag, pos, negs)
+      end
+
+      true
+    catch
+      :not_empty -> false
+    end
+  end
+
+  defp tuple_empty?(_, _, []), do: throw(:not_empty)
+  defp tuple_empty?(_, _, [{:open, fs} | _]) when fs == %{}, do: true
+
+  defp tuple_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
+          # The key is not shared between positive and negative maps,
+          # and because the negative type is required, there is no value in common
+          tag == :closed and not optional?(neg_type) ->
+            throw(:discard_negative)
+
+          # The key is not shared between positive and negative maps,
+          # but because the negative type is not required, there may be a value in common
+          tag == :closed ->
+            true
+
+          # There may be value in common
+          tag == :open ->
+            diff = difference(term_or_optional(), neg_type)
+            # if the diff type contains optional, then we call tuple_empty on two arguments
+            if optional?(diff) do
+              # remove all the elements with an index larger of equal to neg_key
+              keys_to_drop = for key <- Map.keys(fields), key >= neg_key, do: key
+              closed_pos = Map.drop(fields, keys_to_drop)
+
+              # for neg_key index, remove the absent part
+              open_pos = Map.put(fields, neg_key, remove_optional(diff))
+
+              tuple_empty?(:closed, closed_pos, negs) and tuple_empty?(tag, open_pos, negs)
+            else
+              empty?(diff) or tuple_empty?(tag, Map.put(fields, neg_key, diff), negs)
+            end
+        end
+      end
+
+      # Keys from the positive map that may be present in the negative one
+      # Invariant on tuples : the types do not contain absent, so this does not
+      # induce special cases.
+      for {key, type} <- fields do
+        case neg_fields do
+          %{^key => neg_type} ->
+            diff = difference(type, neg_type)
+            empty?(diff) or tuple_empty?(tag, Map.put(fields, key, diff), negs)
+
+          %{} ->
+            if neg_tag == :closed and not optional?(type) do
+              throw(:discard_negative)
+            else
+              # an absent key in a open negative map can be ignored
+              diff = difference(type, map_tag_to_type(neg_tag))
+              empty?(diff) or tuple_empty?(tag, Map.put(fields, key, diff), negs)
+            end
+        end
+      end
+
+      true
+    catch
+      :discard_negative -> tuple_empty?(tag, fields, negs)
+    end
+  end
+
   # Takes a map dnf and a key and returns a list of unions of types
   # for that key. It has to traverse both fields and negative entries.
   defp map_split_on_key(dnf, key) do
@@ -1122,3 +1336,5 @@ defmodule Module.Types.Descr do
 
   defp iterator_difference(:none, map), do: map
 end
+
+# execute function test from module above
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index ef7c1f932c9..0c8109e79d4 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -55,6 +55,22 @@ defmodule Module.Types.DescrTest do
       assert equal?(union(intersection(dynamic(), atom()), atom()), atom())
     end
 
+    test "tuple" do
+      assert equal?(union(tuple(), tuple()), tuple())
+
+      t = tuple([integer(), atom()])
+      assert equal?(union(t, t), t)
+
+      assert union(tuple([integer(), atom()]), tuple([float(), atom()]))
+             |> equal?(tuple([union(integer(), float()), atom()]))
+
+      assert union(tuple([integer(), atom()]), tuple([integer(), binary()]))
+             |> equal?(tuple([integer(), union(atom(), binary())]))
+
+      assert union(open_tuple([atom()]), tuple([atom(), integer()]))
+             |> equal?(open_tuple([atom()]))
+    end
+
     test "map" do
       assert equal?(union(open_map(), open_map()), open_map())
       assert equal?(union(closed_map(a: integer()), open_map()), open_map())
@@ -100,6 +116,16 @@ defmodule Module.Types.DescrTest do
       assert empty?(intersection(intersection(dynamic(), atom()), integer()))
     end
 
+    test "tuple" do
+      assert empty?(intersection(open_tuple([atom()]), open_tuple([integer()])))
+
+      assert intersection(open_tuple([atom()]), tuple([term(), integer()]))
+             |> equal?(tuple([atom(), integer()]))
+
+      assert intersection(tuple([term(), integer()]), tuple([atom(), term()]))
+             |> equal?(tuple([atom(), integer()]))
+    end
+
     test "map" do
       assert intersection(open_map(), open_map()) == open_map()
       assert equal?(intersection(closed_map(a: integer()), open_map()), closed_map(a: integer()))
@@ -150,6 +176,39 @@ defmodule Module.Types.DescrTest do
       assert empty?(difference(none(), dynamic()))
     end
 
+    test "tuple" do
+      assert empty?(difference(open_tuple([atom()]), open_tuple([term()])))
+
+      assert difference(open_tuple([atom()]), tuple([integer(), integer()]))
+             |> equal?(open_tuple([atom()]))
+
+      assert tuple([union(atom(), integer()), term()])
+             |> difference(open_tuple([atom(), term()]))
+             |> equal?(tuple([integer(), term()]))
+
+      assert tuple([union(atom(), integer()), term()])
+             |> difference(open_tuple([atom(), term()]))
+             |> difference(open_tuple([integer(), term()]))
+             |> empty?()
+
+      assert tuple([term(), union(atom(), integer()), term()])
+             |> difference(open_tuple([term(), integer()]))
+             |> equal?(tuple([term(), atom(), term()]))
+
+      assert tuple([term(), union(atom(), integer()), term()])
+             |> difference(open_tuple([term(), atom()]))
+             |> equal?(tuple([term(), integer(), term()]))
+
+      assert open_tuple()
+             |> difference(open_tuple([term()]))
+             |> difference(empty_tuple())
+             |> empty?()
+
+      assert open_tuple()
+             |> difference(open_tuple([term(), term()]))
+             |> equal?(union(tuple([term()]), tuple([])))
+    end
+
     test "map" do
       assert empty?(difference(open_map(), open_map()))
       assert empty?(difference(open_map(), term()))
@@ -194,6 +253,17 @@ defmodule Module.Types.DescrTest do
       assert subtype?(integer(), union(dynamic(), integer()))
     end
 
+    test "tuple" do
+      assert subtype?(tuple([integer(), atom()]), tuple([term(), term()]))
+      refute subtype?(tuple([integer(), atom()]), tuple([integer(), integer()]))
+      refute subtype?(tuple([integer(), atom()]), tuple([atom(), atom()]))
+
+      assert subtype?(tuple([integer(), atom()]), open_tuple([integer(), atom()]))
+      refute subtype?(tuple([term()]), open_tuple([term(), term()]))
+      refute subtype?(tuple([integer(), atom()]), open_tuple([integer(), integer()]))
+      refute subtype?(open_tuple([integer(), atom()]), tuple([integer(), integer()]))
+    end
+
     test "map" do
       assert subtype?(open_map(), term())
       assert subtype?(closed_map(a: integer()), open_map())
@@ -232,6 +302,10 @@ defmodule Module.Types.DescrTest do
       assert compatible?(integer(), dynamic())
     end
 
+    test "tuple" do
+      assert compatible?(dynamic(tuple()), tuple([integer(), atom()]))
+    end
+
     test "map" do
       assert compatible?(closed_map(a: integer()), open_map())
       assert compatible?(intersection(dynamic(), open_map()), closed_map(a: integer()))
@@ -239,6 +313,10 @@ defmodule Module.Types.DescrTest do
   end
 
   describe "empty" do
+    test "tuple" do
+      assert intersection(tuple([integer(), atom()]), open_tuple([atom()])) |> empty?
+    end
+
     test "map" do
       assert intersection(closed_map(b: atom()), open_map(a: integer())) |> empty?
     end
@@ -258,6 +336,19 @@ defmodule Module.Types.DescrTest do
       assert atom_fetch(union(atom([:foo, :bar]), dynamic(term()))) == {:infinite, []}
     end
 
+    test "tuple_fetch" do
+      assert tuple_fetch(term(), 0) == :badtuple
+      assert tuple_fetch(tuple([integer(), atom()]), 0) == {false, integer()}
+      assert tuple_fetch(tuple([integer(), atom()]), 1) == {false, atom()}
+      assert tuple_fetch(tuple([integer(), atom()]), 2) == :badindex
+      assert tuple_fetch(tuple([integer(), atom()]), -1) == :badindex
+
+      {true, type} =
+        tuple_fetch(union(tuple([integer(), atom()]), dynamic(open_tuple([atom()]))), 1)
+
+      assert equal?(type, union(atom(), dynamic()))
+    end
+
     test "map_fetch" do
       assert map_fetch(term(), :a) == :badmap
       assert map_fetch(union(open_map(), integer()), :a) == :badmap
@@ -396,6 +487,20 @@ defmodule Module.Types.DescrTest do
                "dynamic(%{a: integer()})"
     end
 
+    test "tuples" do
+      assert tuple([integer(), atom()]) |> to_quoted_string() == "{integer(), atom()}"
+      assert open_tuple([integer(), atom()]) |> to_quoted_string() == "{integer(), atom(), ...}"
+
+      assert union(tuple([integer(), atom()]), open_tuple([atom()])) |> to_quoted_string() ==
+               "{integer(), atom()} or {atom(), ...}"
+
+      assert difference(tuple([integer(), atom()]), open_tuple([atom()])) |> to_quoted_string() ==
+               "{integer(), atom()} and not {atom(), ...}"
+
+      assert tuple([closed_map(a: integer()), open_map()]) |> to_quoted_string() ==
+               "{%{a: integer()}, %{...}}"
+    end
+
     test "map" do
       assert empty_map() |> to_quoted_string() == "empty_map()"
       assert open_map() |> to_quoted_string() == "%{...}"

From 2d696228b2524db50b2903320917862c7c71cb30 Mon Sep 17 00:00:00 2001
From: gldubc <guilduboc@gmail.com>
Date: Mon, 20 May 2024 17:58:55 +0200
Subject: [PATCH 2/2] Improve testing and code

---
 lib/elixir/lib/module/types/descr.ex          | 380 +++++++++---------
 .../test/elixir/module/types/descr_test.exs   |  12 +
 2 files changed, 203 insertions(+), 189 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index d167fb52964..12fa9f44215 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -590,113 +590,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  ## Tuple
-
-  defp tuple_new(tag, elements) do
-    pairs =
-      elements
-      |> Enum.map_reduce(0, fn type, acc -> {{acc, type}, acc + 1} end)
-      |> elem(0)
-
-    map_new(tag, :maps.from_list(pairs))
-  end
-
-  defp tuple_intersection(left, right), do: map_intersection(left, right)
-  defp tuple_difference(left, right), do: map_difference(left, right)
-  defp tuple_union(left, right), do: map_union(left, right)
-
-  def tuple_fetch(%{} = descr, key) do
-    case :maps.take(:dynamic, descr) do
-      :error ->
-        if is_map_key(descr, :tuple) and tuple_only?(descr) do
-          {static_optional?, static_type} = tuple_fetch_static(descr, key) |> pop_optional()
-
-          if static_optional? or empty?(static_type) do
-            :badindex
-          else
-            {false, static_type}
-          end
-        else
-          :badtuple
-        end
-
-      {%{map: {:open, fields, []}}, static} when fields == %{} and static == @none ->
-        {true, dynamic()}
-
-      {dynamic, static} ->
-        if is_map_key(dynamic, :tuple) and tuple_only?(static) do
-          {dynamic_optional?, dynamic_type} = tuple_fetch_static(dynamic, key) |> pop_optional()
-          {static_optional?, static_type} = tuple_fetch_static(static, key) |> pop_optional()
-
-          if static_optional? or empty?(dynamic_type) do
-            :badindex
-          else
-            {dynamic_optional?, union(dynamic(dynamic_type), static_type)}
-          end
-        else
-          :badtuple
-        end
-    end
-  end
-
-  defp tuple_only?(descr), do: empty?(Map.delete(descr, :tuple))
-
-  defp tuple_fetch_static(descr, index) when is_integer(index) do
-    case descr do
-      %{tuple: tuple} -> Enum.reduce(map_split_on_key(tuple, index), none(), &union/2)
-      %{} -> none()
-    end
-  end
-
-  defp tuple_to_quoted(dnf) do
-    dnf
-    |> map_normalize()
-    |> Enum.map(&tuple_each_to_quoted/1)
-    |> case do
-      [] -> []
-      dnf -> Enum.reduce(dnf, &{:or, [], [&2, &1]}) |> List.wrap()
-    end
-  end
-
-  defp tuple_each_to_quoted({tag, positive_map, negative_maps}) do
-    case negative_maps do
-      [] ->
-        tuple_literal_to_quoted({tag, positive_map})
-
-      _ ->
-        negative_maps
-        |> Enum.map(&tuple_literal_to_quoted/1)
-        |> Enum.reduce(&{:or, [], [&2, &1]})
-        |> Kernel.then(
-          &{:and, [], [tuple_literal_to_quoted({tag, positive_map}), {:not, [], [&1]}]}
-        )
-    end
-  end
-
-  def tuple_literal_to_quoted({:closed, fields}) when map_size(fields) == 0 do
-    {:empty_map, [], []}
-  end
-
-  def tuple_literal_to_quoted({tag, fields}) do
-    case tag do
-      :closed -> {:{}, [], tuple_fields_to_quoted(tag, fields)}
-      :open -> {:{}, [], tuple_fields_to_quoted(tag, fields) ++ [{:..., [], nil}]}
-    end
-  end
-
-  defp tuple_fields_to_quoted(tag, map) do
-    sorted = Enum.sort(map)
-
-    for {_, type} <- sorted,
-        not (tag == :open and optional?(type) and term_type?(type)) do
-      cond do
-        not optional?(type) -> to_quoted(type)
-        empty?(type) -> {:not_set, [], []}
-        true -> {:if_set, [], [to_quoted(type)]}
-      end
-    end
-  end
-
   ## Map
   #
   # Maps are in disjunctive normal form (DNF), that is, a list (union) of pairs
@@ -960,86 +853,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Emptiness checking for tuples.
-  #
-  # Short-circuits if it finds a non-empty map literal in the union.
-  # Since the algorithm is recursive, we implement the short-circuiting
-  # as throw/catch.
-  defp tuple_empty?(dnf) do
-    try do
-      for {tag, pos, negs} <- dnf do
-        tuple_empty?(tag, pos, negs)
-      end
-
-      true
-    catch
-      :not_empty -> false
-    end
-  end
-
-  defp tuple_empty?(_, _, []), do: throw(:not_empty)
-  defp tuple_empty?(_, _, [{:open, fs} | _]) when fs == %{}, do: true
-
-  defp tuple_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
-          # The key is not shared between positive and negative maps,
-          # and because the negative type is required, there is no value in common
-          tag == :closed and not optional?(neg_type) ->
-            throw(:discard_negative)
-
-          # The key is not shared between positive and negative maps,
-          # but because the negative type is not required, there may be a value in common
-          tag == :closed ->
-            true
-
-          # There may be value in common
-          tag == :open ->
-            diff = difference(term_or_optional(), neg_type)
-            # if the diff type contains optional, then we call tuple_empty on two arguments
-            if optional?(diff) do
-              # remove all the elements with an index larger of equal to neg_key
-              keys_to_drop = for key <- Map.keys(fields), key >= neg_key, do: key
-              closed_pos = Map.drop(fields, keys_to_drop)
-
-              # for neg_key index, remove the absent part
-              open_pos = Map.put(fields, neg_key, remove_optional(diff))
-
-              tuple_empty?(:closed, closed_pos, negs) and tuple_empty?(tag, open_pos, negs)
-            else
-              empty?(diff) or tuple_empty?(tag, Map.put(fields, neg_key, diff), negs)
-            end
-        end
-      end
-
-      # Keys from the positive map that may be present in the negative one
-      # Invariant on tuples : the types do not contain absent, so this does not
-      # induce special cases.
-      for {key, type} <- fields do
-        case neg_fields do
-          %{^key => neg_type} ->
-            diff = difference(type, neg_type)
-            empty?(diff) or tuple_empty?(tag, Map.put(fields, key, diff), negs)
-
-          %{} ->
-            if neg_tag == :closed and not optional?(type) do
-              throw(:discard_negative)
-            else
-              # an absent key in a open negative map can be ignored
-              diff = difference(type, map_tag_to_type(neg_tag))
-              empty?(diff) or tuple_empty?(tag, Map.put(fields, key, diff), negs)
-            end
-        end
-      end
-
-      true
-    catch
-      :discard_negative -> tuple_empty?(tag, fields, negs)
-    end
-  end
-
   # Takes a map dnf and a key and returns a list of unions of types
   # for that key. It has to traverse both fields and negative entries.
   defp map_split_on_key(dnf, key) do
@@ -1168,6 +981,197 @@ defmodule Module.Types.Descr do
     end
   end
 
+  ## Tuple
+
+  # Tuple types {integer(), atom()} and open tuple types {atom(), boolean(), ...}
+  # which represents every tuple of at least two elements that are an atom and a boolean.
+  #
+  # Tuples are encoded as map records, where the keys are the indices.
+  # E.g., type {integer(), atom()} is encoded as type %{0 => integer(), 1 => atom()}.
+  # and {atom(), boolean(), ...} is encoded as the open map %{..., 0 => atom(), 1 => boolean()}.
+  #
+  # There is no overlap because map types and tuple types exist in different fields
+  # of the descr (:map and :tuple). While this encoding reuses the set-theoretic
+  # map operations, emptiness is slightly modified to account for the fact that
+  # tuple types do not admit optional indices.
+
+  defp tuple_new(tag, elements) do
+    pairs =
+      elements
+      |> Enum.map_reduce(0, fn type, acc -> {{acc, type}, acc + 1} end)
+      |> elem(0)
+
+    map_new(tag, :maps.from_list(pairs))
+  end
+
+  defp tuple_intersection(left, right), do: map_intersection(left, right)
+  defp tuple_difference(left, right), do: map_difference(left, right)
+  defp tuple_union(left, right), do: map_union(left, right)
+
+  # Same as map_fetch, only the tuple descr field is accessed
+  def tuple_fetch(%{} = descr, key) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if is_map_key(descr, :tuple) and tuple_only?(descr) do
+          {static_optional?, static_type} = tuple_fetch_static(descr, key) |> pop_optional()
+
+          if static_optional? or empty?(static_type) do
+            :badindex
+          else
+            {false, static_type}
+          end
+        else
+          :badtuple
+        end
+
+      {%{map: {:open, fields, []}}, static} when fields == %{} and static == @none ->
+        {true, dynamic()}
+
+      {dynamic, static} ->
+        if is_map_key(dynamic, :tuple) and tuple_only?(static) do
+          {dynamic_optional?, dynamic_type} = tuple_fetch_static(dynamic, key) |> pop_optional()
+          {static_optional?, static_type} = tuple_fetch_static(static, key) |> pop_optional()
+
+          if static_optional? or empty?(dynamic_type) do
+            :badindex
+          else
+            {dynamic_optional?, union(dynamic(dynamic_type), static_type)}
+          end
+        else
+          :badtuple
+        end
+    end
+  end
+
+  defp tuple_only?(descr), do: empty?(Map.delete(descr, :tuple))
+
+  defp tuple_fetch_static(descr, index) when is_integer(index) do
+    case descr do
+      %{tuple: tuple} -> Enum.reduce(map_split_on_key(tuple, index), none(), &union/2)
+      %{} -> none()
+    end
+  end
+
+  defp tuple_to_quoted(dnf) do
+    dnf
+    |> map_normalize()
+    |> Enum.map(&tuple_each_to_quoted/1)
+    |> case do
+      [] -> []
+      dnf -> Enum.reduce(dnf, &{:or, [], [&2, &1]}) |> List.wrap()
+    end
+  end
+
+  defp tuple_each_to_quoted({tag, positive_map, negative_maps}) do
+    case negative_maps do
+      [] ->
+        tuple_literal_to_quoted({tag, positive_map})
+
+      _ ->
+        negative_maps
+        |> Enum.map(&tuple_literal_to_quoted/1)
+        |> Enum.reduce(&{:or, [], [&2, &1]})
+        |> Kernel.then(
+          &{:and, [], [tuple_literal_to_quoted({tag, positive_map}), {:not, [], [&1]}]}
+        )
+    end
+  end
+
+  def tuple_literal_to_quoted({:closed, fields}) when map_size(fields) == 0 do
+    {:empty_map, [], []}
+  end
+
+  def tuple_literal_to_quoted({tag, fields}) do
+    case tag do
+      :closed -> {:{}, [], tuple_fields_to_quoted(tag, fields)}
+      :open -> {:{}, [], tuple_fields_to_quoted(tag, fields) ++ [{:..., [], nil}]}
+    end
+  end
+
+  defp tuple_fields_to_quoted(tag, map) do
+    sorted = Enum.sort(map)
+
+    for {_, type} <- sorted,
+        not (tag == :open and optional?(type) and term_type?(type)) do
+      cond do
+        not optional?(type) -> to_quoted(type)
+        empty?(type) -> {:not_set, [], []}
+        true -> {:if_set, [], [to_quoted(type)]}
+      end
+    end
+  end
+
+  # Emptiness checking for tuples.
+  #
+  # Short-circuits if it finds a non-empty map tuple in the union.
+  # Since the algorithm is recursive, we implement the short-circuiting
+  # as throw/catch.
+  #
+  # For tuples, the explicit types do not contain optional
+  defp tuple_empty?(dnf) do
+    try do
+      for {tag, pos, negs} <- dnf do
+        tuple_empty?(tag, pos, negs)
+      end
+
+      true
+    catch
+      :not_empty -> false
+    end
+  end
+
+  defp tuple_empty?(_, _, []), do: throw(:not_empty)
+  defp tuple_empty?(_, _, [{:open, fs} | _]) when fs == %{}, do: true
+
+  defp tuple_empty?(tag, fields, [{neg_tag, neg_fields} | negs]) do
+    try do
+      # Indices that exists in the negative tuple, but not in the positive one
+      for {neg_index, neg_type} <- neg_fields, not is_map_key(fields, neg_index) do
+        cond do
+          # This index is not in the closed positive tuple, so there is no value in common
+          # Tthere are no explicit optional types in tuples
+          tag == :closed ->
+            throw(:discard_negative)
+
+          # There may be value in common
+          tag == :open ->
+            diff = difference(term_or_optional(), neg_type)
+
+            # Remove all the elements with an index larger or equal to neg_index
+            keys_to_drop = for key <- Map.keys(fields), key >= neg_index, do: key
+            closed_pos = Map.drop(fields, keys_to_drop)
+
+            # For neg_key index, remove the absent part
+            open_pos = Map.put(fields, neg_index, remove_optional(diff))
+
+            tuple_empty?(:closed, closed_pos, negs) and tuple_empty?(tag, open_pos, negs)
+        end
+      end
+
+      # Indices from the positive tuple that may be present in the negative one
+      for {index, type} <- fields do
+        case neg_fields do
+          %{^index => neg_type} ->
+            diff = difference(type, neg_type)
+            empty?(diff) or tuple_empty?(tag, Map.put(fields, index, diff), negs)
+
+          %{} ->
+            if neg_tag == :closed do
+              throw(:discard_negative)
+            else
+              # an absent key in a open negative map can be ignored
+              diff = difference(type, map_tag_to_type(neg_tag))
+              empty?(diff) or tuple_empty?(tag, Map.put(fields, index, diff), negs)
+            end
+        end
+      end
+
+      true
+    catch
+      :discard_negative -> tuple_empty?(tag, fields, negs)
+    end
+  end
+
   ## Pairs
   #
   # To simplify disjunctive normal forms of e.g., map types, it is useful to
@@ -1336,5 +1340,3 @@ defmodule Module.Types.Descr do
 
   defp iterator_difference(:none, map), do: map
 end
-
-# execute function test from module above
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 0c8109e79d4..dae18490dab 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -347,6 +347,18 @@ defmodule Module.Types.DescrTest do
         tuple_fetch(union(tuple([integer(), atom()]), dynamic(open_tuple([atom()]))), 1)
 
       assert equal?(type, union(atom(), dynamic()))
+
+      assert tuple_fetch(union(tuple([integer()]), tuple([atom()])), 0) ==
+               {false, union(integer(), atom())}
+
+      assert tuple_fetch(tuple(), 0) == :badindex
+    end
+
+    test "tuple_fetch with dynamic" do
+      assert tuple_fetch(dynamic(), 0) == {true, dynamic()}
+
+      assert tuple_fetch(union(dynamic(), open_tuple([atom()])), 0) ==
+               {true, union(atom(), dynamic())}
     end
 
     test "map_fetch" do