diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index c77215994f6..19a18603091 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -6,7 +6,7 @@ defmodule Module.Types do
   end
 
   import Module.Types.Helpers
-  alias Module.Types.{Expr, Pattern}
+  alias Module.Types.{Expr, Pattern, Infer}
 
   @doc false
   def warnings(module, file, defs, no_warn_undefined, cache) do
@@ -179,9 +179,9 @@ defmodule Module.Types do
     end
   end
 
-  defp do_lift_type({:tuple, types}, context) do
+  defp do_lift_type({:tuple, n, types}, context) do
     {types, context} = Enum.map_reduce(types, context, &do_lift_type/2)
-    {{:tuple, types}, context}
+    {{:tuple, n, types}, context}
   end
 
   defp do_lift_type({:map, pairs}, context) do
@@ -300,9 +300,9 @@ defmodule Module.Types do
 
         [
           "incompatible types:\n\n    ",
-          format_type(left, simplify_left?),
+          Infer.format_type(left, simplify_left?),
           " !~ ",
-          format_type(right, simplify_right?),
+          Infer.format_type(right, simplify_right?),
           "\n\n",
           format_expr(expr, location),
           traces,
@@ -352,7 +352,7 @@ defmodule Module.Types do
           "where \"",
           Macro.to_string(var),
           "\" was given the type ",
-          format_type(type, simplify?),
+          Infer.format_type(type, simplify?),
           hint,
           " in:\n\n    # ",
           format_location(location),
@@ -390,73 +390,10 @@ defmodule Module.Types do
     [file, ?:, line, ?\n]
   end
 
-  ## TYPE FORMATTING
-
   defp simplify_type?(type, other) do
     map_type?(type) and not map_type?(other)
   end
 
-  @doc false
-  def format_type({:map, pairs}, true) do
-    case List.keyfind(pairs, {:atom, :__struct__}, 1) do
-      {:required, {:atom, :__struct__}, {:atom, struct}} ->
-        "%#{inspect(struct)}{}"
-
-      _ ->
-        "map()"
-    end
-  end
-
-  def format_type({:union, types}, simplify?) do
-    "#{Enum.map_join(types, " | ", &format_type(&1, simplify?))}"
-  end
-
-  def format_type({:tuple, types}, simplify?) do
-    "{#{Enum.map_join(types, ", ", &format_type(&1, simplify?))}}"
-  end
-
-  def format_type({:list, type}, simplify?) do
-    "[#{format_type(type, simplify?)}]"
-  end
-
-  def format_type({:map, pairs}, false) do
-    case List.keytake(pairs, {:atom, :__struct__}, 1) do
-      {{:required, {:atom, :__struct__}, {:atom, struct}}, pairs} ->
-        "%#{inspect(struct)}{#{format_map_pairs(pairs)}}"
-
-      _ ->
-        "%{#{format_map_pairs(pairs)}}"
-    end
-  end
-
-  def format_type({:atom, literal}, _simplify?) do
-    inspect(literal)
-  end
-
-  def format_type({:var, index}, _simplify?) do
-    "var#{index}"
-  end
-
-  def format_type(atom, _simplify?) when is_atom(atom) do
-    "#{atom}()"
-  end
-
-  defp format_map_pairs(pairs) do
-    {atoms, others} = Enum.split_with(pairs, &match?({:required, {:atom, _}, _}, &1))
-    {required, optional} = Enum.split_with(others, &match?({:required, _, _}, &1))
-
-    Enum.map_join(atoms ++ required ++ optional, ", ", fn
-      {:required, {:atom, atom}, right} ->
-        "#{atom}: #{format_type(right, false)}"
-
-      {:required, left, right} ->
-        "#{format_type(left, false)} => #{format_type(right, false)}"
-
-      {:optional, left, right} ->
-        "optional(#{format_type(left, false)}) => #{format_type(right, false)}"
-    end)
-  end
-
   ## EXPRESSION FORMATTING
 
   defp format_expr(nil, _location) do
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index b4df5325e18..27bc16ec8de 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -100,10 +100,10 @@ defmodule Module.Types.Expr do
 
   # __STACKTRACE__
   def of_expr({:__STACKTRACE__, _meta, var_context}, _stack, context) when is_atom(var_context) do
-    file = {:tuple, [{:atom, :file}, {:list, :integer}]}
-    line = {:tuple, [{:atom, :line}, :integer]}
+    file = {:tuple, 2, [{:atom, :file}, {:list, :integer}]}
+    line = {:tuple, 2, [{:atom, :line}, :integer]}
     file_line = {:list, {:union, [file, line]}}
-    type = {:list, {:tuple, [:atom, :atom, :integer, file_line]}}
+    type = {:list, {:tuple, 4, [:atom, :atom, :integer, file_line]}}
     {:ok, type, context}
   end
 
@@ -123,7 +123,7 @@ defmodule Module.Types.Expr do
     stack = push_expr_stack(expr, stack)
 
     case map_reduce_ok(exprs, context, &of_expr(&1, stack, &2)) do
-      {:ok, types, context} -> {:ok, {:tuple, types}, context}
+      {:ok, types, context} -> {:ok, {:tuple, length(types), types}, context}
       {:error, reason} -> {:error, reason}
     end
   end
diff --git a/lib/elixir/lib/module/types/infer.ex b/lib/elixir/lib/module/types/infer.ex
index 10ccea76233..d20d6576559 100644
--- a/lib/elixir/lib/module/types/infer.ex
+++ b/lib/elixir/lib/module/types/infer.ex
@@ -3,6 +3,38 @@ defmodule Module.Types.Infer do
 
   import Module.Types.Helpers
 
+  # Those are the simple types known to the system:
+  #
+  #   :dynamic
+  #   {:var, var}
+  #   {:atom, atom} < :atom
+  #   :integer
+  #   :float
+  #   :pid
+  #   :port
+  #   :reference
+  #
+  # Those are the composite types:
+  #
+  #   {:list, type}
+  #   {:tuple, size, [type]} < :tuple
+  #   {:union, [type]}
+  #   {:map, [{:required | :optional, key_type, value_type}]}
+  #
+  # TODO: Those types should be removed:
+  #
+  #   :boolean
+  #   :number
+  #
+  # Once new types are added, they should be considered in:
+  #
+  #   * unify (all)
+  #   * format_type (all)
+  #   * subtype? (subtypes only)
+  #   * has_unbound_var? (composite only)
+  #   * recursive_type? (composite only)
+  #
+
   @doc """
   Unifies two types and returns the unified type and an updated typing context
   or an error in case of a typing conflict.
@@ -51,15 +83,14 @@ defmodule Module.Types.Infer do
     end
   end
 
-  defp do_unify({:tuple, sources}, {:tuple, targets}, stack, context)
-       when length(sources) == length(targets) do
+  defp do_unify({:tuple, n, sources}, {:tuple, n, targets}, stack, context) do
     result =
       map_reduce_ok(Enum.zip(sources, targets), context, fn {source, target}, context ->
         unify(source, target, stack, context)
       end)
 
     case result do
-      {:ok, types, context} -> {:ok, {:tuple, types}, context}
+      {:ok, types, context} -> {:ok, {:tuple, n, types}, context}
       {:error, reason} -> {:error, reason}
     end
   end
@@ -86,8 +117,11 @@ defmodule Module.Types.Infer do
   defp do_unify(source, target, stack, context) do
     cond do
       # This condition exists to handle unions with unbound vars.
-      # TODO: handle unions properly.
-      has_unbound_var?(source, context) or has_unbound_var?(target, context) ->
+      # TODO: handle unions properly. Note we can easily unify
+      # "union < type" even if union has vars as the vars must be
+      # type
+      (match?({:union, _}, source) and has_unbound_var?(source, context)) or
+          (match?({:union, _}, target) and has_unbound_var?(target, context)) ->
         {:ok, source, context}
 
       subtype?(source, target, context) ->
@@ -270,6 +304,8 @@ defmodule Module.Types.Infer do
     {required, optional}
   end
 
+  defp error(type, reason, context), do: {:error, {type, reason, context}}
+
   @doc """
   Adds a variable to the typing context and returns its type variable.
   If the variable has already been added, return the existing type variable.
@@ -405,7 +441,11 @@ defmodule Module.Types.Infer do
     recursive_type?(type, [parent | parents], context)
   end
 
-  defp recursive_type?({:tuple, types} = parent, parents, context) do
+  defp recursive_type?({:union, types} = parent, parents, context) do
+    Enum.any?(types, &recursive_type?(&1, [parent | parents], context))
+  end
+
+  defp recursive_type?({:tuple, _, types} = parent, parents, context) do
     Enum.any?(types, &recursive_type?(&1, [parent | parents], context))
   end
 
@@ -430,12 +470,21 @@ defmodule Module.Types.Infer do
     end
   end
 
-  def has_unbound_var?({:tuple, args}, context),
+  def has_unbound_var?({:tuple, _, args}, context),
     do: Enum.any?(args, &has_unbound_var?(&1, context))
 
   def has_unbound_var?({:union, args}, context),
     do: Enum.any?(args, &has_unbound_var?(&1, context))
 
+  def has_unbound_var?({:list, arg}, context),
+    do: has_unbound_var?(arg, context)
+
+  def has_unbound_var?({:map, pairs}, context) do
+    Enum.any?(pairs, fn {_, key, value} ->
+      has_unbound_var?(key, context) or has_unbound_var?(value, context)
+    end)
+  end
+
   def has_unbound_var?(_type, _context), do: false
 
   @doc """
@@ -447,9 +496,6 @@ defmodule Module.Types.Infer do
     * unbound variables are not subtype of anything
 
   """
-  # TODO: boolean <: false | true
-  # TODO: number <: float | integer
-  # TODO: implement subtype for maps
   def subtype?(type, type, _context), do: true
 
   def subtype?({:var, var}, other, context) do
@@ -467,12 +513,38 @@ defmodule Module.Types.Infer do
   end
 
   def subtype?(_, :dynamic, _context), do: true
-  def subtype?({:atom, boolean}, :boolean, _context) when is_boolean(boolean), do: true
   def subtype?({:atom, atom}, :atom, _context) when is_atom(atom), do: true
+
+  def subtype?({:atom, boolean}, :boolean, _context) when is_boolean(boolean), do: true
   def subtype?(:boolean, :atom, _context), do: true
   def subtype?(:float, :number, _context), do: true
   def subtype?(:integer, :number, _context), do: true
-  def subtype?({:tuple, _}, :tuple, _context), do: true
+
+  # Composite
+
+  def subtype?({:tuple, _, _}, :tuple, _context), do: true
+
+  def subtype?({:tuple, n, left_types}, {:tuple, n, right_types}, context) do
+    left_types
+    |> Enum.zip(right_types)
+    |> Enum.any?(fn {left, right} -> subtype?(left, right, context) end)
+  end
+
+  def subtype?({:map, left_pairs}, {:map, right_pairs}, context) do
+    Enum.all?(left_pairs, fn
+      {:required, left_key, left_value} ->
+        Enum.any?(right_pairs, fn {_, right_key, right_value} ->
+          subtype?(left_key, right_key, context) and subtype?(left_value, right_value, context)
+        end)
+
+      {:optional, _, _} ->
+        true
+    end)
+  end
+
+  def subtype?({:list, left}, {:list, right}, context) do
+    subtype?(left, right, context)
+  end
 
   def subtype?({:union, left_types}, {:union, _} = right_union, context) do
     Enum.all?(left_types, &subtype?(&1, right_union, context))
@@ -482,6 +554,10 @@ defmodule Module.Types.Infer do
     Enum.any?(right_types, &subtype?(left, &1, context))
   end
 
+  def subtype?({:union, left_types}, right, context) do
+    Enum.all?(left_types, &subtype?(&1, right, context))
+  end
+
   def subtype?(_left, _right, _context), do: false
 
   @doc """
@@ -511,9 +587,11 @@ defmodule Module.Types.Infer do
   end
 
   # Filter subtypes
+  #
   # `boolean() | atom()` => `atom()`
   # `:foo | atom()` => `atom()`
-  # Does not unify `true | false` => `boolean()`
+  #
+  # Does not merge `true | false` => `boolean()`
   defp unique_super_types([type | types], context) do
     types = Enum.reject(types, &subtype?(&1, type, context))
 
@@ -528,5 +606,69 @@ defmodule Module.Types.Infer do
     []
   end
 
-  defp error(type, reason, context), do: {:error, {type, reason, context}}
+  @doc """
+  Formats types.
+
+  The second argument says when complex types such as maps and
+  structs should be simplified and not shown.
+  """
+  def format_type({:map, pairs}, true) do
+    case List.keyfind(pairs, {:atom, :__struct__}, 1) do
+      {:required, {:atom, :__struct__}, {:atom, struct}} ->
+        "%#{inspect(struct)}{}"
+
+      _ ->
+        "map()"
+    end
+  end
+
+  def format_type({:union, types}, simplify?) do
+    "#{Enum.map_join(types, " | ", &format_type(&1, simplify?))}"
+  end
+
+  def format_type({:tuple, _, types}, simplify?) do
+    "{#{Enum.map_join(types, ", ", &format_type(&1, simplify?))}}"
+  end
+
+  def format_type({:list, type}, simplify?) do
+    "[#{format_type(type, simplify?)}]"
+  end
+
+  def format_type({:map, pairs}, false) do
+    case List.keytake(pairs, {:atom, :__struct__}, 1) do
+      {{:required, {:atom, :__struct__}, {:atom, struct}}, pairs} ->
+        "%#{inspect(struct)}{#{format_map_pairs(pairs)}}"
+
+      _ ->
+        "%{#{format_map_pairs(pairs)}}"
+    end
+  end
+
+  def format_type({:atom, literal}, _simplify?) do
+    inspect(literal)
+  end
+
+  def format_type({:var, index}, _simplify?) do
+    "var#{index}"
+  end
+
+  def format_type(atom, _simplify?) when is_atom(atom) do
+    "#{atom}()"
+  end
+
+  defp format_map_pairs(pairs) do
+    {atoms, others} = Enum.split_with(pairs, &match?({:required, {:atom, _}, _}, &1))
+    {required, optional} = Enum.split_with(others, &match?({:required, _, _}, &1))
+
+    Enum.map_join(atoms ++ required ++ optional, ", ", fn
+      {:required, {:atom, atom}, right} ->
+        "#{atom}: #{format_type(right, false)}"
+
+      {:required, left, right} ->
+        "#{format_type(left, false)} => #{format_type(right, false)}"
+
+      {:optional, left, right} ->
+        "optional(#{format_type(left, false)}) => #{format_type(right, false)}"
+    end)
+  end
 end
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index ac5d2a58eb3..502857d198f 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -149,7 +149,7 @@ defmodule Module.Types.Pattern do
     stack = push_expr_stack(expr, stack)
 
     case map_reduce_ok(exprs, context, &of_pattern(&1, stack, &2)) do
-      {:ok, types, context} -> {:ok, {:tuple, types}, context}
+      {:ok, types, context} -> {:ok, {:tuple, length(types), types}, context}
       {:error, reason} -> {:error, reason}
     end
   end
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index ebcba9ee730..fe0e345349e 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -36,9 +36,9 @@ defmodule Module.Types.ExprTest do
   end
 
   test "tuple" do
-    assert quoted_expr({}) == {:ok, {:tuple, []}}
-    assert quoted_expr({:a}) == {:ok, {:tuple, [{:atom, :a}]}}
-    assert quoted_expr({:a, 123}) == {:ok, {:tuple, [{:atom, :a}, :integer]}}
+    assert quoted_expr({}) == {:ok, {:tuple, 0, []}}
+    assert quoted_expr({:a}) == {:ok, {:tuple, 1, [{:atom, :a}]}}
+    assert quoted_expr({:a, 123}) == {:ok, {:tuple, 2, [{:atom, :a}, :integer]}}
   end
 
   # Use module attribute to avoid formatter adding parentheses
@@ -80,11 +80,13 @@ defmodule Module.Types.ExprTest do
                )
              ) == {:ok, :binary}
 
-      assert quoted_expr([foo], {<<foo::integer>>, foo}) == {:ok, {:tuple, [:binary, :integer]}}
-      assert quoted_expr([foo], {<<foo::binary>>, foo}) == {:ok, {:tuple, [:binary, :binary]}}
+      assert quoted_expr([foo], {<<foo::integer>>, foo}) ==
+               {:ok, {:tuple, 2, [:binary, :integer]}}
+
+      assert quoted_expr([foo], {<<foo::binary>>, foo}) == {:ok, {:tuple, 2, [:binary, :binary]}}
 
       assert quoted_expr([foo], {<<foo::utf8>>, foo}) ==
-               {:ok, {:tuple, [:binary, {:union, [:integer, :binary]}]}}
+               {:ok, {:tuple, 2, [:binary, {:union, [:integer, :binary]}]}}
 
       assert {:error, {:unable_unify, {:integer, :binary, _}}} =
                quoted_expr(
@@ -101,8 +103,8 @@ defmodule Module.Types.ExprTest do
 
   test "variables" do
     assert quoted_expr([foo], foo) == {:ok, {:var, 0}}
-    assert quoted_expr([foo], {foo}) == {:ok, {:tuple, [{:var, 0}]}}
-    assert quoted_expr([foo, bar], {foo, bar}) == {:ok, {:tuple, [{:var, 0}, {:var, 1}]}}
+    assert quoted_expr([foo], {foo}) == {:ok, {:tuple, 1, [{:var, 0}]}}
+    assert quoted_expr([foo, bar], {foo, bar}) == {:ok, {:tuple, 2, [{:var, 0}, {:var, 1}]}}
   end
 
   test "pattern match" do
diff --git a/lib/elixir/test/elixir/module/types/infer_test.exs b/lib/elixir/test/elixir/module/types/infer_test.exs
index 175f6946691..892cf5232e1 100644
--- a/lib/elixir/test/elixir/module/types/infer_test.exs
+++ b/lib/elixir/test/elixir/module/types/infer_test.exs
@@ -78,15 +78,19 @@ defmodule Module.Types.InferTest do
     end
 
     test "tuple" do
-      assert unify_lift({:tuple, []}, {:tuple, []}) == {:ok, {:tuple, []}}
-      assert unify_lift({:tuple, [:integer]}, {:tuple, [:integer]}) == {:ok, {:tuple, [:integer]}}
-      assert unify_lift({:tuple, [:boolean]}, {:tuple, [:atom]}) == {:ok, {:tuple, [:boolean]}}
+      assert unify_lift({:tuple, 0, []}, {:tuple, 0, []}) == {:ok, {:tuple, 0, []}}
 
-      assert {:error, {:unable_unify, {{:tuple, [:integer]}, {:tuple, []}, _}}} =
-               unify_lift({:tuple, [:integer]}, {:tuple, []})
+      assert unify_lift({:tuple, 1, [:integer]}, {:tuple, 1, [:integer]}) ==
+               {:ok, {:tuple, 1, [:integer]}}
+
+      assert unify_lift({:tuple, 1, [:boolean]}, {:tuple, 1, [:atom]}) ==
+               {:ok, {:tuple, 1, [:boolean]}}
+
+      assert {:error, {:unable_unify, {{:tuple, 1, [:integer]}, {:tuple, 0, []}, _}}} =
+               unify_lift({:tuple, 1, [:integer]}, {:tuple, 0, []})
 
       assert {:error, {:unable_unify, {:integer, :atom, _}}} =
-               unify_lift({:tuple, [:integer]}, {:tuple, [:atom]})
+               unify_lift({:tuple, 1, [:integer]}, {:tuple, 1, [:atom]})
     end
 
     test "list" do
@@ -326,26 +330,26 @@ defmodule Module.Types.InferTest do
       assert {{:var, 0}, var_context} = new_var({:foo, [version: 0], nil}, new_context())
       assert {{:var, 1}, var_context} = new_var({:bar, [version: 1], nil}, var_context)
 
-      assert {:ok, {:tuple, [{:var, 0}]}, context} =
-               unify({:tuple, [{:var, 0}]}, {:tuple, [:integer]}, var_context)
+      assert {:ok, {:tuple, 1, [{:var, 0}]}, context} =
+               unify({:tuple, 1, [{:var, 0}]}, {:tuple, 1, [:integer]}, var_context)
 
       assert Types.lift_type({:var, 0}, context) == :integer
 
       assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, var_context)
       assert {:ok, {:var, 1}, context} = unify({:var, 1}, :integer, context)
 
-      assert {:ok, {:tuple, [{:var, _}]}, _context} =
-               unify({:tuple, [{:var, 0}]}, {:tuple, [{:var, 1}]}, context)
+      assert {:ok, {:tuple, 1, [{:var, _}]}, _context} =
+               unify({:tuple, 1, [{:var, 0}]}, {:tuple, 1, [{:var, 1}]}, context)
 
-      assert {:ok, {:var, 1}, context} = unify({:var, 1}, {:tuple, [{:var, 0}]}, var_context)
+      assert {:ok, {:var, 1}, context} = unify({:var, 1}, {:tuple, 1, [{:var, 0}]}, var_context)
       assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, context)
-      assert Types.lift_type({:var, 1}, context) == {:tuple, [:integer]}
+      assert Types.lift_type({:var, 1}, context) == {:tuple, 1, [:integer]}
 
       assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, var_context)
       assert {:ok, {:var, 1}, context} = unify({:var, 1}, :binary, context)
 
       assert {:error, {:unable_unify, {:integer, :binary, _}}} =
-               unify_lift({:tuple, [{:var, 0}]}, {:tuple, [{:var, 1}]}, context)
+               unify_lift({:tuple, 1, [{:var, 0}]}, {:tuple, 1, [{:var, 1}]}, context)
     end
 
     # TODO: Vars inside unions
@@ -364,14 +368,14 @@ defmodule Module.Types.InferTest do
 
       assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, var_context)
 
-      assert {:error, {:unable_unify, {{:var, 0}, {:tuple, [{:var, 0}]}, _}}} =
-               unify_lift({:var, 1}, {:tuple, [{:var, 0}]}, context)
+      assert {:error, {:unable_unify, {{:var, 0}, {:tuple, 1, [{:var, 0}]}, _}}} =
+               unify_lift({:var, 1}, {:tuple, 1, [{:var, 0}]}, context)
 
       assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, var_context)
       assert {:ok, {:var, _}, context} = unify({:var, 1}, {:var, 2}, context)
 
-      assert {:error, {:unable_unify, {{:var, 0}, {:tuple, [{:var, 0}]}, _}}} =
-               unify_lift({:var, 2}, {:tuple, [{:var, 0}]}, context)
+      assert {:error, {:unable_unify, {{:var, 0}, {:tuple, 1, [{:var, 0}]}, _}}} =
+               unify_lift({:var, 2}, {:tuple, 1, [{:var, 0}]}, context)
     end
 
     test "error with internal variable" do
@@ -399,29 +403,101 @@ defmodule Module.Types.InferTest do
          %{context: context, unbound_var: unbound_var} do
       assert has_unbound_var?(unbound_var, context)
       assert has_unbound_var?({:union, [unbound_var]}, context)
-      assert has_unbound_var?({:tuple, [unbound_var]}, context)
+      assert has_unbound_var?({:tuple, 1, [unbound_var]}, context)
+      assert has_unbound_var?({:list, unbound_var}, context)
+      assert has_unbound_var?({:map, [{:required, unbound_var, :atom}]}, context)
+      assert has_unbound_var?({:map, [{:required, :atom, unbound_var}]}, context)
     end
 
     test "returns false when there are no unbound vars",
          %{context: context, bound_var: bound_var} do
       refute has_unbound_var?(bound_var, context)
       refute has_unbound_var?({:union, [bound_var]}, context)
-      refute has_unbound_var?({:tuple, [bound_var]}, context)
+      refute has_unbound_var?({:tuple, 1, [bound_var]}, context)
       refute has_unbound_var?(:integer, context)
+      refute has_unbound_var?({:list, bound_var}, context)
+      refute has_unbound_var?({:map, [{:required, :atom, :atom}]}, context)
+      refute has_unbound_var?({:map, [{:required, bound_var, :atom}]}, context)
+      refute has_unbound_var?({:map, [{:required, :atom, bound_var}]}, context)
     end
   end
 
-  test "subtype?/3" do
-    assert subtype?({:atom, :foo}, :atom, new_context())
-    assert subtype?({:atom, true}, :boolean, new_context())
-    assert subtype?({:atom, true}, :atom, new_context())
-    assert subtype?(:boolean, :atom, new_context())
-
-    refute subtype?(:integer, :binary, new_context())
-    refute subtype?(:atom, {:atom, :foo}, new_context())
-    refute subtype?(:boolean, {:atom, true}, new_context())
-    refute subtype?(:atom, {:atom, true}, new_context())
-    refute subtype?(:atom, :boolean, new_context())
+  describe "subtype?/3" do
+    test "with simple types" do
+      assert subtype?({:atom, :foo}, :atom, new_context())
+      assert subtype?({:atom, true}, :boolean, new_context())
+      assert subtype?({:atom, true}, :atom, new_context())
+      assert subtype?(:boolean, :atom, new_context())
+
+      refute subtype?(:integer, :binary, new_context())
+      refute subtype?(:atom, {:atom, :foo}, new_context())
+      refute subtype?(:boolean, {:atom, true}, new_context())
+      refute subtype?(:atom, {:atom, true}, new_context())
+      refute subtype?(:atom, :boolean, new_context())
+    end
+
+    test "with composite types" do
+      assert subtype?({:list, {:atom, :foo}}, {:list, :atom}, new_context())
+      assert subtype?({:tuple, 1, [{:atom, :foo}]}, {:tuple, 1, [:atom]}, new_context())
+
+      refute subtype?({:list, :atom}, {:list, {:atom, :foo}}, new_context())
+      refute subtype?({:tuple, 1, [:atom]}, {:tuple, 1, [{:atom, :foo}]}, new_context())
+      refute subtype?({:tuple, 1, [:atom]}, {:tuple, 2, [:atom, :atom]}, new_context())
+      refute subtype?({:tuple, 2, [:atom, :atom]}, {:tuple, 1, [:atom]}, new_context())
+    end
+
+    test "with maps" do
+      assert subtype?({:map, [{:optional, :atom, :integer}]}, {:map, []}, new_context())
+
+      assert subtype?(
+               {:map, [{:required, :atom, :integer}]},
+               {:map, [{:required, :atom, :integer}]},
+               new_context()
+             )
+
+      assert subtype?(
+               {:map, [{:required, {:atom, :foo}, :integer}]},
+               {:map, [{:required, :atom, :integer}]},
+               new_context()
+             )
+
+      assert subtype?(
+               {:map, [{:required, :integer, {:atom, :foo}}]},
+               {:map, [{:required, :integer, :atom}]},
+               new_context()
+             )
+
+      refute subtype?({:map, [{:required, :atom, :integer}]}, {:map, []}, new_context())
+
+      refute subtype?(
+               {:map, [{:required, :atom, :integer}]},
+               {:map, [{:required, {:atom, :foo}, :integer}]},
+               new_context()
+             )
+
+      refute subtype?(
+               {:map, [{:required, :integer, :atom}]},
+               {:map, [{:required, :integer, {:atom, :foo}}]},
+               new_context()
+             )
+    end
+
+    test "with unions" do
+      assert subtype?({:union, [{:atom, :foo}]}, {:union, [:atom]}, new_context())
+      assert subtype?({:union, [{:atom, :foo}, {:atom, :bar}]}, {:union, [:atom]}, new_context())
+      assert subtype?({:union, [{:atom, :foo}]}, {:union, [:integer, :atom]}, new_context())
+
+      assert subtype?({:atom, :foo}, {:union, [:atom]}, new_context())
+      assert subtype?({:atom, :foo}, {:union, [:integer, :atom]}, new_context())
+
+      assert subtype?({:union, [{:atom, :foo}]}, :atom, new_context())
+      assert subtype?({:union, [{:atom, :foo}, {:atom, :bar}]}, :atom, new_context())
+
+      refute subtype?({:union, [:atom]}, {:union, [{:atom, :foo}]}, new_context())
+      refute subtype?({:union, [:atom]}, {:union, [{:atom, :foo}, :integer]}, new_context())
+      refute subtype?(:atom, {:union, [{:atom, :foo}, :integer]}, new_context())
+      refute subtype?({:union, [:atom]}, {:atom, :foo}, new_context())
+    end
   end
 
   test "to_union/2" do
@@ -439,7 +515,44 @@ defmodule Module.Types.InferTest do
     assert {{:var, 0}, var_context} = new_var({:foo, [version: 0], nil}, new_context())
     assert to_union([{:var, 0}], var_context) == {:var, 0}
 
-    assert to_union([{:tuple, [:integer]}, {:tuple, [:integer]}], new_context()) ==
-             {:tuple, [:integer]}
+    assert to_union([{:tuple, 1, [:integer]}, {:tuple, 1, [:integer]}], new_context()) ==
+             {:tuple, 1, [:integer]}
+  end
+
+  test "format_type/1" do
+    assert format_type(:binary, false) == "binary()"
+    assert format_type({:atom, true}, false) == "true"
+    assert format_type({:atom, :atom}, false) == ":atom"
+    assert format_type({:list, :binary}, false) == "[binary()]"
+    assert format_type({:tuple, 0, []}, false) == "{}"
+    assert format_type({:tuple, 1, [:integer]}, false) == "{integer()}"
+
+    assert format_type({:map, []}, true) == "map()"
+    assert format_type({:map, [{:required, {:atom, :foo}, :atom}]}, true) == "map()"
+
+    assert format_type({:map, []}, false) ==
+             "%{}"
+
+    assert format_type({:map, [{:required, {:atom, :foo}, :atom}]}, false) ==
+             "%{foo: atom()}"
+
+    assert format_type({:map, [{:required, :integer, :atom}]}, false) ==
+             "%{integer() => atom()}"
+
+    assert format_type({:map, [{:optional, :integer, :atom}]}, false) ==
+             "%{optional(integer()) => atom()}"
+
+    assert format_type({:map, [{:optional, {:atom, :foo}, :atom}]}, false) ==
+             "%{optional(:foo) => atom()}"
+
+    assert format_type({:map, [{:required, {:atom, :__struct__}, {:atom, Struct}}]}, false) ==
+             "%Struct{}"
+
+    assert format_type(
+             {:map,
+              [{:required, {:atom, :__struct__}, {:atom, Struct}}, {:required, :integer, :atom}]},
+             false
+           ) ==
+             "%Struct{integer() => atom()}"
   end
 end
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index c73e9d59ed9..6df9d9b4b24 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -105,9 +105,9 @@ defmodule Module.Types.PatternTest do
     end
 
     test "tuple" do
-      assert quoted_pattern({}) == {:ok, {:tuple, []}}
-      assert quoted_pattern({:a}) == {:ok, {:tuple, [{:atom, :a}]}}
-      assert quoted_pattern({:a, 123}) == {:ok, {:tuple, [{:atom, :a}, :integer]}}
+      assert quoted_pattern({}) == {:ok, {:tuple, 0, []}}
+      assert quoted_pattern({:a}) == {:ok, {:tuple, 1, [{:atom, :a}]}}
+      assert quoted_pattern({:a, 123}) == {:ok, {:tuple, 2, [{:atom, :a}, :integer]}}
     end
 
     test "map" do
@@ -190,9 +190,9 @@ defmodule Module.Types.PatternTest do
       assert quoted_pattern(<<123::utf8>>) == {:ok, :binary}
       assert quoted_pattern(<<"foo"::utf8>>) == {:ok, :binary}
 
-      assert quoted_pattern({<<foo::integer>>, foo}) == {:ok, {:tuple, [:binary, :integer]}}
-      assert quoted_pattern({<<foo::binary>>, foo}) == {:ok, {:tuple, [:binary, :binary]}}
-      assert quoted_pattern({<<foo::utf8>>, foo}) == {:ok, {:tuple, [:binary, :integer]}}
+      assert quoted_pattern({<<foo::integer>>, foo}) == {:ok, {:tuple, 2, [:binary, :integer]}}
+      assert quoted_pattern({<<foo::binary>>, foo}) == {:ok, {:tuple, 2, [:binary, :binary]}}
+      assert quoted_pattern({<<foo::utf8>>, foo}) == {:ok, {:tuple, 2, [:binary, :integer]}}
 
       assert {:error, {:unable_unify, {:binary, :integer, _}}} =
                quoted_pattern(<<foo::binary-0, foo::integer>>)
@@ -200,24 +200,24 @@ defmodule Module.Types.PatternTest do
 
     test "variables" do
       assert quoted_pattern(foo) == {:ok, {:var, 0}}
-      assert quoted_pattern({foo}) == {:ok, {:tuple, [{:var, 0}]}}
-      assert quoted_pattern({foo, bar}) == {:ok, {:tuple, [{:var, 0}, {:var, 1}]}}
+      assert quoted_pattern({foo}) == {:ok, {:tuple, 1, [{:var, 0}]}}
+      assert quoted_pattern({foo, bar}) == {:ok, {:tuple, 2, [{:var, 0}, {:var, 1}]}}
 
       assert quoted_pattern(_) == {:ok, :dynamic}
-      assert quoted_pattern({_ = 123, _}) == {:ok, {:tuple, [:integer, :dynamic]}}
+      assert quoted_pattern({_ = 123, _}) == {:ok, {:tuple, 2, [:integer, :dynamic]}}
     end
 
     test "assignment" do
       assert quoted_pattern(x = y) == {:ok, {:var, 0}}
       assert quoted_pattern(x = 123) == {:ok, :integer}
-      assert quoted_pattern({foo}) == {:ok, {:tuple, [{:var, 0}]}}
-      assert quoted_pattern({x = y}) == {:ok, {:tuple, [{:var, 0}]}}
+      assert quoted_pattern({foo}) == {:ok, {:tuple, 1, [{:var, 0}]}}
+      assert quoted_pattern({x = y}) == {:ok, {:tuple, 1, [{:var, 0}]}}
 
       assert quoted_pattern(x = y = 123) == {:ok, :integer}
       assert quoted_pattern(x = 123 = y) == {:ok, :integer}
       assert quoted_pattern(123 = x = y) == {:ok, :integer}
 
-      assert {:error, {:unable_unify, {{:tuple, [var: 0]}, {:var, 0}, _}}} =
+      assert {:error, {:unable_unify, {{:tuple, 1, [var: 0]}, {:var, 0}, _}}} =
                quoted_pattern({x} = x)
     end
   end
@@ -258,7 +258,7 @@ defmodule Module.Types.PatternTest do
       assert quoted_head([x = y, y = z, z = :foo]) ==
                {:ok, [{:atom, :foo}, {:atom, :foo}, {:atom, :foo}]}
 
-      assert {:error, {:unable_unify, {{:tuple, [var: 1]}, {:var, 0}, _}}} =
+      assert {:error, {:unable_unify, {{:tuple, 1, [var: 1]}, {:var, 0}, _}}} =
                quoted_head([{x} = y, {y} = x])
     end
 
diff --git a/lib/elixir/test/elixir/module/types/types_test.exs b/lib/elixir/test/elixir/module/types/types_test.exs
index 8e940bd2440..6edc1ca0dcc 100644
--- a/lib/elixir/test/elixir/module/types/types_test.exs
+++ b/lib/elixir/test/elixir/module/types/types_test.exs
@@ -4,43 +4,6 @@ defmodule Module.Types.TypesTest do
   use ExUnit.Case, async: true
   alias Module.Types
 
-  test "format_type/1" do
-    assert Types.format_type(:binary, false) == "binary()"
-    assert Types.format_type({:atom, true}, false) == "true"
-    assert Types.format_type({:atom, :atom}, false) == ":atom"
-    assert Types.format_type({:list, :binary}, false) == "[binary()]"
-    assert Types.format_type({:tuple, []}, false) == "{}"
-    assert Types.format_type({:tuple, [:integer]}, false) == "{integer()}"
-
-    assert Types.format_type({:map, []}, true) == "map()"
-    assert Types.format_type({:map, [{:required, {:atom, :foo}, :atom}]}, true) == "map()"
-
-    assert Types.format_type({:map, []}, false) ==
-             "%{}"
-
-    assert Types.format_type({:map, [{:required, {:atom, :foo}, :atom}]}, false) ==
-             "%{foo: atom()}"
-
-    assert Types.format_type({:map, [{:required, :integer, :atom}]}, false) ==
-             "%{integer() => atom()}"
-
-    assert Types.format_type({:map, [{:optional, :integer, :atom}]}, false) ==
-             "%{optional(integer()) => atom()}"
-
-    assert Types.format_type({:map, [{:optional, {:atom, :foo}, :atom}]}, false) ==
-             "%{optional(:foo) => atom()}"
-
-    assert Types.format_type({:map, [{:required, {:atom, :__struct__}, {:atom, Struct}}]}, false) ==
-             "%Struct{}"
-
-    assert Types.format_type(
-             {:map,
-              [{:required, {:atom, :__struct__}, {:atom, Struct}}, {:required, :integer, :atom}]},
-             false
-           ) ==
-             "%Struct{integer() => atom()}"
-  end
-
   test "expr_to_string/1" do
     assert Types.expr_to_string({1, 2}) == "{1, 2}"
     assert Types.expr_to_string(quote(do: Foo.bar(arg))) == "Foo.bar(arg)"