Split Module.Types and add unit tests (#9303)

6 files changed, 1063 insertions, 772 deletions

diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index e6e1c8cd4..11b7472b7 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -1,14 +1,8 @@
 defmodule Module.Types do
   @moduledoc false
 
-  defmacrop is_var(expr) do
-    quote do
-      is_tuple(unquote(expr)) and
-        tuple_size(unquote(expr)) == 3 and
-        is_atom(elem(unquote(expr), 0)) and
-        is_atom(elem(unquote(expr), 2))
-    end
-  end
+  import Module.Types.Helpers
+  import Module.Types.Infer, only: [of_guard: 2, of_pattern: 2]
 
   @doc """
   Infer function definitions' types.
@@ -92,138 +86,7 @@ defmodule Module.Types do
     type
   end
 
-  ## INFERENCE
-
-  @doc false
-  # :atom
-  def of_pattern(atom, context) when is_atom(atom) do
-    {:ok, {:literal, atom}, context}
-  end
-
-  # 12
-  def of_pattern(literal, context) when is_integer(literal) do
-    {:ok, :integer, context}
-  end
-
-  # 1.2
-  def of_pattern(literal, context) when is_float(literal) do
-    {:ok, :float, context}
-  end
-
-  # "..."
-  def of_pattern(literal, context) when is_binary(literal) do
-    {:ok, :binary, context}
-  end
-
-  # <<...>>>
-  def of_pattern({:<<>>, _meta, args} = expr, context) do
-    expr_stack(expr, context, fn context ->
-      case reduce_ok(args, context, &of_binary/2) do
-        {:ok, context} -> {:ok, :binary, context}
-        {:error, reason} -> {:error, reason}
-      end
-    end)
-  end
-
-  # [left | right]
-  def of_pattern([{:|, _meta, [left_expr, right_expr]}] = expr, context) do
-    expr_stack(expr, context, fn context ->
-      with {:ok, left, context} <- of_pattern(left_expr, context),
-           {:ok, right, context} <- of_pattern(right_expr, context),
-           do: {:ok, {:cons, left, right}, context}
-    end)
-  end
-
-  # [left, right]
-  def of_pattern([left_expr | right_expr] = expr, context) do
-    expr_stack(expr, context, fn context ->
-      with {:ok, left, context} <- of_pattern(left_expr, context),
-           {:ok, right, context} <- of_pattern(right_expr, context),
-           do: {:ok, {:cons, left, right}, context}
-    end)
-  end
-
-  # []
-  def of_pattern([], context) do
-    {:ok, :null, context}
-  end
-
-  # _
-  def of_pattern({:_, _meta, atom}, context) when is_atom(atom) do
-    {:ok, :dynamic, context}
-  end
-
-  # var
-  def of_pattern(var, context) when is_var(var) do
-    {type, context} = new_var(var, context)
-    {:ok, type, context}
-  end
-
-  # {left, right}
-  def of_pattern({left, right}, context) do
-    of_pattern({:{}, [], [left, right]}, context)
-  end
-
-  # {...}
-  def of_pattern({:{}, _meta, exprs} = expr, context) do
-    expr_stack(expr, context, fn context ->
-      case map_reduce_ok(exprs, context, &of_pattern/2) do
-        {:ok, types, context} -> {:ok, {:tuple, types}, context}
-        {:error, reason} -> {:error, reason}
-      end
-    end)
-  end
-
-  # left = right
-  def of_pattern({:=, _meta, [left_expr, right_expr]} = expr, context) do
-    expr_stack(expr, context, fn context ->
-      with {:ok, left_type, context} <- of_pattern(left_expr, context),
-           {:ok, right_type, context} <- of_pattern(right_expr, context),
-           do: start_unify(left_type, right_type, context)
-    end)
-  end
-
-  # %{...}
-  def of_pattern({:%{}, _meta, args} = expr, context) do
-    result =
-      expr_stack(expr, context, fn context ->
-        map_reduce_ok(args, context, fn {key, value}, context ->
-          with {:ok, key_type, context} <- of_pattern(key, context),
-               {:ok, value_type, context} <- of_pattern(value, context),
-               do: {:ok, {key_type, value_type}, context}
-        end)
-      end)
-
-    case result do
-      {:ok, pairs, context} -> {:ok, {:map, pairs}, context}
-      {:error, reason} -> {:error, reason}
-    end
-  end
-
-  def of_pattern({:%, _meta, _args}, context) do
-    {:ok, {:map, []}, context}
-  end
-
-  defp of_guard(guard, context) do
-    expr_stack(guard, context, fn context ->
-      # Flatten `foo and bar` to list of type constraints
-      reduce_ok(flatten_binary_op(:and, guard), context, fn guard, context ->
-        # Flatten `foo or bar` to later build a union
-        union = Enum.map(flatten_binary_op(:or, guard), &type_guard/1)
-
-        # Only use group of guards using a single variable
-        with {:ok, args, guard_types} <- unzip_ok(union),
-             [_arg] <- Enum.uniq(Enum.map(args, &remove_meta/1)) do
-          expr_stack(guard, context, fn context ->
-            union = to_union(guard_types, context)
-            unify_guard(hd(args), union, context)
-          end)
-        else
-          _ -> {:ok, context}
-        end
-      end)
-    end)
-  end
+  ## GUARDS
 
   # TODO: Remove this and let multiple when be treated as multiple clauses,
   #       meaning they will be intersection types
@@ -235,389 +98,6 @@ defmodule Module.Types do
     Enum.reduce(guards, fn guard, acc -> {{:., [], [:erlang, :orelse]}, [], [guard, acc]} end)
   end
 
-  defp flatten_binary_op(:and, {{:., _, [:erlang, :andalso]}, _, [left, right]}) do
-    flatten_binary_op(:and, left) ++ flatten_binary_op(:and, right)
-  end
-
-  defp flatten_binary_op(:or, {{:., _, [:erlang, :orelse]}, _, [left, right]}) do
-    flatten_binary_op(:or, left) ++ flatten_binary_op(:or, right)
-  end
-
-  defp flatten_binary_op(_op, other) do
-    [other]
-  end
-
-  defp unify_guard(arg, guard_type, context) when is_var(arg) do
-    # TODO: It is incorrect to use of_pattern/2 but it helps for simplicity now
-    with {:ok, arg_type, context} <- of_pattern(arg, context),
-         {:ok, _, context} <- start_unify(arg_type, guard_type, context),
-         do: {:ok, context}
-  end
-
-  defp unify_guard(_arg, _guard_type, context) do
-    {:ok, context}
-  end
-
-  # Unimplemented guards:
-  # !=/2 !==/2 </2 <=/2 >/2 >=/2 ==/2 ===/2 not/1
-  # */2 +/1 +/2 -/1 -/2 //2
-  # abs/2 ceil/1 floor/1 round/1 trunc/1
-  # elem/2 hd/1 in/2 length/1 map_size/1 tl/1 tuple_size/1
-  # is_function/1 is_function/2 is_list/1 is_number/1 is_pid/1 is_port/1 is_reference/1 is_tuple/1
-  # node/1 self/1
-  # binary_part/3 bit_size/1 byte_size/1 div/2 rem/2 node/0
-
-  @type_guards %{
-    is_atom: :atom,
-    is_binary: :binary,
-    is_bitstring: :binary,
-    is_boolean: :boolean,
-    is_float: :float,
-    is_integer: :integer,
-    is_map: {:map, []}
-  }
-
-  defp type_guard({{:., _, [:erlang, guard]}, _, [arg]}) do
-    case :maps.find(guard, @type_guards) do
-      {:ok, type} -> {:ok, arg, type}
-      :error -> {:error, :unknown_guard}
-    end
-  end
-
-  defp type_guard(_other), do: {:error, :unknown_guard}
-
-  # binary-pattern :: specifier
-  defp of_binary({:"::", _meta, [expr, specifiers]} = full_expr, context) do
-    specifiers = List.flatten(collect_specifiers(specifiers))
-
-    expected_type =
-      cond do
-        :integer in specifiers -> :integer
-        :float in specifiers -> :float
-        :bits in specifiers -> :binary
-        :bitstring in specifiers -> :binary
-        :bytes in specifiers -> :binary
-        :binary in specifiers -> :binary
-        :utf8 in specifiers -> :integer
-        :utf16 in specifiers -> :integer
-        :utf32 in specifiers -> :integer
-        true -> :integer
-      end
-
-    expr_stack(full_expr, context, fn context ->
-      with {:ok, type, context} <- of_pattern(expr, context),
-           {:ok, _type, context} <- start_unify(type, expected_type, context),
-           do: {:ok, context}
-    end)
-  end
-
-  # binary-pattern
-  defp of_binary(expr, context) do
-    case of_pattern(expr, context) do
-      {:ok, type, context} when type in [:integer, :float, :binary] ->
-        {:ok, context}
-
-      {:ok, type, _context} ->
-        {:error, {:invalid_binary_type, type}}
-
-      {:error, reason} ->
-        {:error, reason}
-    end
-  end
-
-  # Push expr to stack inside fun and pop after fun
-  # The expression stack is used for
-  defp expr_stack(expr, context, fun) do
-    expr_stack = context.expr_stack
-
-    case fun.(%{context | expr_stack: [expr | context.expr_stack]}) do
-      {:ok, context} -> {:ok, %{context | expr_stack: expr_stack}}
-      {:ok, type, context} -> {:ok, type, %{context | expr_stack: expr_stack}}
-      {:error, reason} -> {:error, reason}
-    end
-  end
-
-  ## UNIFICATION
-
-  defp start_unify(left, right, context) do
-    case unify(left, right, context) do
-      {:ok, type, context} -> {:ok, type, %{context | unify_stack: []}}
-      {:error, reason} -> {:error, reason}
-    end
-  end
-
-  defp unify(type, {:var, var}, context) do
-    case :maps.get(var, context.types) do
-      :unbound ->
-        context = refine_var(var, type, context)
-        context = push_unify_stack(var, context)
-
-        if recursive_type?(type, [], context) do
-          error({:unable_unify, type, {:var, var}}, context)
-        else
-          {:ok, {:var, var}, context}
-        end
-
-      var_type ->
-        # Only add trace if the variable wasn't already "expanded"
-        context =
-          if variable_expanded?(var, context) do
-            context
-          else
-            trace_var(var, type, context)
-          end
-
-        context = push_unify_stack(var, context)
-
-        case unify(type, var_type, context) do
-          {:ok, var_type, context} ->
-            context = refine_var(var, var_type, context)
-            {:ok, {:var, var}, context}
-
-          {:error, reason} ->
-            {:error, reason}
-        end
-    end
-  end
-
-  defp unify({:var, var}, type, context) do
-    unify(type, {:var, var}, context)
-  end
-
-  defp unify({:tuple, lefts}, {:tuple, rights}, context)
-       when length(lefts) == length(rights) do
-    result =
-      map_reduce_ok(Enum.zip(lefts, rights), context, fn {left, right}, context ->
-        unify(left, right, context)
-      end)
-
-    case result do
-      {:ok, types, context} -> {:ok, {:tuple, types}, context}
-      {:error, reason} -> {:error, reason}
-    end
-  end
-
-  defp unify({:cons, left_left, left_right}, {:cons, right_left, right_right}, context) do
-    with {:ok, left, context} <- unify(left_left, right_left, context),
-         {:ok, right, context} <- unify(left_right, right_right, context),
-         do: {:ok, {:cons, left, right}, context}
-  end
-
-  defp unify({:map, left_pairs}, {:map, right_pairs}, context) do
-    # Since maps in patterns only support literal keys (excluding maps)
-    # we can do exact type match without subtype checking
-
-    unique_right_pairs =
-      Enum.reject(right_pairs, fn {key, _value} ->
-        :lists.keyfind(key, 1, left_pairs)
-      end)
-
-    unique_pairs = left_pairs ++ unique_right_pairs
-
-    # Build union of all unique key-value pairs between the maps
-    result =
-      map_reduce_ok(unique_pairs, context, fn {left_key, left_value}, context ->
-        case :lists.keyfind(left_key, 1, right_pairs) do
-          {^left_key, right_value} ->
-            case unify(left_value, right_value, context) do
-              {:ok, value, context} -> {:ok, {left_key, value}, context}
-              {:error, reason} -> {:error, reason}
-            end
-
-          false ->
-            {:ok, {left_key, left_value}, context}
-        end
-      end)
-
-    case result do
-      {:ok, pairs, context} -> {:ok, {:map, pairs}, context}
-      {:error, reason} -> {:error, reason}
-    end
-  end
-
-  defp unify(:dynamic, right, context) do
-    {:ok, right, context}
-  end
-
-  defp unify(left, :dynamic, context) do
-    {:ok, left, context}
-  end
-
-  defp unify(left, right, context) do
-    cond do
-      subtype?(left, right, context) -> {:ok, left, context}
-      subtype?(right, left, context) -> {:ok, right, context}
-      true -> error({:unable_unify, left, right}, context)
-    end
-  end
-
-  # Check unify stack to see if variable was already expanded
-  defp variable_expanded?(var, context) do
-    Enum.any?(context.unify_stack, &variable_same?(var, &1, context))
-  end
-
-  # Find if two variables are the same or point to the other
-  defp variable_same?(same, same, _context) do
-    true
-  end
-
-  defp variable_same?(left, right, context) do
-    case :maps.find(left, context.types) do
-      {:ok, {:var, new_left}} ->
-        variable_same?(new_left, right, context)
-
-      _ ->
-        case :maps.find(right, context.types) do
-          {:ok, {:var, new_right}} -> variable_same?(left, new_right, context)
-          :error -> false
-        end
-    end
-  end
-
-  defp push_unify_stack(var, context) do
-    %{context | unify_stack: [var | context.unify_stack]}
-  end
-
-  defp new_var(var, context) do
-    case :maps.find(var_name(var), context.vars) do
-      {:ok, type} ->
-        {type, context}
-
-      :error ->
-        type = {:var, context.counter}
-        vars = :maps.put(var_name(var), type, context.vars)
-        types_to_vars = :maps.put(context.counter, var, context.types_to_vars)
-        types = :maps.put(context.counter, :unbound, context.types)
-        traces = :maps.put(context.counter, [], context.traces)
-        counter = context.counter + 1
-
-        context = %{
-          context
-          | vars: vars,
-            types_to_vars: types_to_vars,
-            types: types,
-            traces: traces,
-            counter: counter
-        }
-
-        {type, context}
-    end
-  end
-
-  defp refine_var(var, type, context) do
-    types = :maps.put(var, type, context.types)
-    trace_var(var, type, %{context | types: types})
-  end
-
-  defp trace_var(var, type, context) do
-    line = get_meta(hd(context.expr_stack))[:line]
-    trace = {type, context.expr_stack, {context.file, line}}
-    traces = :maps.update_with(var, &[trace | &1], context.traces)
-    %{context | traces: traces}
-  end
-
-  defp var_name({name, _meta, context}), do: {name, context}
-
-  # Check if a variable is recursive and incompatible with itself
-  # Bad: `{var} = var`
-  # Good: `x = y; y = z; z = x`
-  defp recursive_type?({:var, var} = parent, parents, context) do
-    case :maps.get(var, context.types) do
-      :unbound ->
-        false
-
-      type ->
-        if type in parents do
-          not Enum.all?(parents, &match?({:var, _}, &1))
-        else
-          recursive_type?(type, [parent | parents], context)
-        end
-    end
-  end
-
-  defp recursive_type?({:cons, left, right} = parent, parents, context) do
-    recursive_type?(left, [parent | parents], context) or
-      recursive_type?(right, [parent | parents], context)
-  end
-
-  defp recursive_type?({:tuple, types} = parent, parents, context) do
-    Enum.any?(types, &recursive_type?(&1, [parent | parents], context))
-  end
-
-  defp recursive_type?({:map, pairs} = parent, parents, context) do
-    Enum.any?(pairs, fn {key, value} ->
-      recursive_type?(key, [parent | parents], context) or
-        recursive_type?(value, [parent | parents], context)
-    end)
-  end
-
-  defp recursive_type?(_other, _parents, _context) do
-    false
-  end
-
-  # Collect binary type specifiers,
-  # from `<<pattern::integer-size(10)>>` collect `integer`
-  defp collect_specifiers({:-, _meta, [left, right]}) do
-    [collect_specifiers(left), collect_specifiers(right)]
-  end
-
-  defp collect_specifiers({specifier, _meta, []}) do
-    [specifier]
-  end
-
-  defp collect_specifiers({name, _meta, context}) when is_atom(name) and is_atom(context) do
-    [name]
-  end
-
-  defp collect_specifiers(_other) do
-    []
-  end
-
-  defp subtype?({:literal, boolean}, :boolean, _context) when is_boolean(boolean), do: true
-  defp subtype?({:literal, atom}, :atom, _context) when is_atom(atom), do: true
-  defp subtype?(:boolean, :atom, _context), do: true
-  defp subtype?({:tuple, _}, :tuple, _context), do: true
-
-  # TODO: Lift unions to unify/3?
-  defp subtype?({:union, left_types}, {:union, _} = right_union, context) do
-    Enum.all?(left_types, &subtype?(&1, right_union, context))
-  end
-
-  defp subtype?(left, {:union, right_types}, context) do
-    Enum.any?(right_types, &subtype?(left, &1, context))
-  end
-
-  defp subtype?(left, right, _context), do: left == right
-
-  defp to_union(types, context) when types != [] do
-    if :dynamic in types do
-      :dynamic
-    else
-      # Filter subtypes
-      # `boolean() | atom()` => `atom()`
-      # `:foo | atom()` => `atom()`
-      # Does not unify `true | false` => `boolean()`
-      case unique_super_types(types, context) do
-        [type] -> type
-        types -> {:union, types}
-      end
-    end
-  end
-
-  defp unique_super_types([type | types], context) do
-    types = Enum.reject(types, &subtype?(&1, type, context))
-
-    if Enum.any?(types, &subtype?(type, &1, context)) do
-      unique_super_types(types, context)
-    else
-      [type | unique_super_types(types, context)]
-    end
-  end
-
-  defp unique_super_types([], _context) do
-    []
-  end
-
   defp guards_to_expr([], left) do
     left
   end
@@ -688,68 +168,6 @@ defmodule Module.Types do
     {type, context}
   end
 
-  ## ERROR GENERATION
-
-  # Collect relevant information from context and traces to report error
-  defp error({:unable_unify, left, right}, context) do
-    {fun, arity} = context.function
-    line = get_meta(hd(context.expr_stack))[:line]
-    location = {context.file, line, {context.module, fun, arity}}
-
-    traces = type_traces(context)
-    common_expr = common_super_expr(traces)
-    traces = simplify_traces(traces, context)
-
-    {:error, {__MODULE__, {:unable_unify, left, right, common_expr, traces}, [location]}}
-  end
-
-  # Collect relevant traces from context.traces using context.unify_stack
-  defp type_traces(context) do
-    stack = Enum.uniq(context.unify_stack)
-
-    Enum.flat_map(stack, fn var_index ->
-      case :maps.find(var_index, context.traces) do
-        {:ok, traces} ->
-          expr_var = :maps.get(var_index, context.types_to_vars)
-          Enum.map(traces, &{expr_var, &1})
-
-        _other ->
-          []
-      end
-    end)
-  end
-
-  # Only use last expr from trace and tag if trace is for
-  # a concrete type or type variable
-  defp simplify_traces(traces, context) do
-    Enum.flat_map(traces, fn {var, {type, [expr | _], location}} ->
-      case type do
-        {:var, var_index} ->
-          var2 = :maps.get(var_index, context.types_to_vars)
-          [{var, {:var, var2, expr, location}}]
-
-        _ ->
-          [{var, {:type, type, expr, location}}]
-      end
-    end)
-  end
-
-  # Find first common super expression among all traces
-  defp common_super_expr([]) do
-    nil
-  end
-
-  defp common_super_expr([{_var, {_type, expr_stack, _location}} | traces]) do
-    Enum.find_value(expr_stack, fn expr ->
-      common? =
-        Enum.all?(traces, fn {_var, {_type, expr_stack, _location}} -> expr in expr_stack end)
-
-      if common? do
-        expr
-      end
-    end)
-  end
-
   ## ERROR FORMATTING
 
   def format_warning({:unable_unify, left, right, expr, traces}) do
@@ -830,6 +248,16 @@ defmodule Module.Types do
     "[#{format_type(left)} | #{format_type(right)}]"
   end
 
+  def format_type({:map, pairs}) do
+    case List.keytake(pairs, :__struct__, 0) do
+      {{:__struct__, struct}, pairs} ->
+        "%#{inspect(struct)}{#{format_map_pairs(pairs)}}"
+
+      nil ->
+        "%{#{format_map_pairs(pairs)}}"
+    end
+  end
+
   def format_type({:literal, literal}) do
     inspect(literal)
   end
@@ -846,6 +274,12 @@ defmodule Module.Types do
     "var#{index}"
   end
 
+  defp format_map_pairs(pairs) do
+    Enum.map_join(pairs, ", ", fn {left, right} ->
+      "#{format_type(left)} => #{format_type(right)}"
+    end)
+  end
+
   defp expr_to_string(expr) do
     expr
     |> rewrite_guard()
@@ -880,80 +314,4 @@ defmodule Module.Types do
 
   defp rewrite_guard_call(op) when op in [:xor, :element, :size], do: {:., [], [:erlang, op]}
   defp rewrite_guard_call(op), do: op
-
-  ## HELPERS
-
-  defp remove_meta({fun, meta, args}) when is_list(meta), do: {fun, [], args}
-  defp remove_meta(other), do: other
-
-  defp get_meta({_fun, meta, _args}) when is_list(meta), do: meta
-  defp get_meta(_other), do: []
-
-  defp unzip_ok(list) do
-    do_unzip_ok(list, [], [])
-  end
-
-  defp do_unzip_ok([{:ok, head1, head2} | tail], acc1, acc2) do
-    do_unzip_ok(tail, [head1 | acc1], [head2 | acc2])
-  end
-
-  defp do_unzip_ok([{:error, reason} | _tail], _acc1, _acc2), do: {:error, reason}
-
-  defp do_unzip_ok([], acc1, acc2), do: {:ok, Enum.reverse(acc1), Enum.reverse(acc2)}
-
-  defp map_ok(list, fun) do
-    do_map_ok(list, [], fun)
-  end
-
-  defp do_map_ok([head | tail], acc, fun) do
-    case fun.(head) do
-      {:ok, elem} ->
-        do_map_ok(tail, [elem | acc], fun)
-
-      result when elem(result, 0) == :ok ->
-        result = Tuple.delete_at(result, 0)
-        do_map_ok(tail, [result | acc], fun)
-
-      {:error, reason} ->
-        {:error, reason}
-    end
-  end
-
-  defp do_map_ok([], acc, _fun), do: {:ok, Enum.reverse(acc)}
-
-  defp reduce_ok(list, acc, fun) do
-    do_reduce_ok(list, acc, fun)
-  end
-
-  defp do_reduce_ok([head | tail], acc, fun) do
-    case fun.(head, acc) do
-      {:ok, acc} ->
-        do_reduce_ok(tail, acc, fun)
-
-      result when elem(result, 0) == :ok ->
-        result = Tuple.delete_at(result, 0)
-        do_reduce_ok(tail, result, fun)
-
-      {:error, reason} ->
-        {:error, reason}
-    end
-  end
-
-  defp do_reduce_ok([], acc, _fun), do: {:ok, acc}
-
-  defp map_reduce_ok(list, acc, fun) do
-    do_map_reduce_ok(list, {[], acc}, fun)
-  end
-
-  defp do_map_reduce_ok([head | tail], {list, acc}, fun) do
-    case fun.(head, acc) do
-      {:ok, elem, acc} ->
-        do_map_reduce_ok(tail, {[elem | list], acc}, fun)
-
-      {:error, reason} ->
-        {:error, reason}
-    end
-  end
-
-  defp do_map_reduce_ok([], {list, acc}, _fun), do: {:ok, Enum.reverse(list), acc}
 end
diff --git a/lib/elixir/lib/module/types/helpers.ex b/lib/elixir/lib/module/types/helpers.ex
new file mode 100644
index 000000000..15ed2dfaa
--- /dev/null
+++ b/lib/elixir/lib/module/types/helpers.ex
@@ -0,0 +1,83 @@
+defmodule Module.Types.Helpers do
+  @moduledoc false
+
+  # Push expr to stack inside fun and pop after fun
+  # The expression stack is used for
+  def expr_stack(expr, context, fun) do
+    expr_stack = context.expr_stack
+
+    case fun.(%{context | expr_stack: [expr | context.expr_stack]}) do
+      {:ok, context} -> {:ok, %{context | expr_stack: expr_stack}}
+      {:ok, type, context} -> {:ok, type, %{context | expr_stack: expr_stack}}
+      {:error, reason} -> {:error, reason}
+    end
+  end
+
+  def reduce_ok(list, acc, fun) do
+    do_reduce_ok(list, acc, fun)
+  end
+
+  defp do_reduce_ok([head | tail], acc, fun) do
+    case fun.(head, acc) do
+      {:ok, acc} ->
+        do_reduce_ok(tail, acc, fun)
+
+      result when elem(result, 0) == :ok ->
+        result = Tuple.delete_at(result, 0)
+        do_reduce_ok(tail, result, fun)
+
+      {:error, reason} ->
+        {:error, reason}
+    end
+  end
+
+  defp do_reduce_ok([], acc, _fun), do: {:ok, acc}
+
+  def unzip_ok(list) do
+    do_unzip_ok(list, [], [])
+  end
+
+  defp do_unzip_ok([{:ok, head1, head2} | tail], acc1, acc2) do
+    do_unzip_ok(tail, [head1 | acc1], [head2 | acc2])
+  end
+
+  defp do_unzip_ok([{:error, reason} | _tail], _acc1, _acc2), do: {:error, reason}
+
+  defp do_unzip_ok([], acc1, acc2), do: {:ok, Enum.reverse(acc1), Enum.reverse(acc2)}
+
+  def map_ok(list, fun) do
+    do_map_ok(list, [], fun)
+  end
+
+  defp do_map_ok([head | tail], acc, fun) do
+    case fun.(head) do
+      {:ok, elem} ->
+        do_map_ok(tail, [elem | acc], fun)
+
+      result when elem(result, 0) == :ok ->
+        result = Tuple.delete_at(result, 0)
+        do_map_ok(tail, [result | acc], fun)
+
+      {:error, reason} ->
+        {:error, reason}
+    end
+  end
+
+  defp do_map_ok([], acc, _fun), do: {:ok, Enum.reverse(acc)}
+
+  def map_reduce_ok(list, acc, fun) do
+    do_map_reduce_ok(list, {[], acc}, fun)
+  end
+
+  defp do_map_reduce_ok([head | tail], {list, acc}, fun) do
+    case fun.(head, acc) do
+      {:ok, elem, acc} ->
+        do_map_reduce_ok(tail, {[elem | list], acc}, fun)
+
+      {:error, reason} ->
+        {:error, reason}
+    end
+  end
+
+  defp do_map_reduce_ok([], {list, acc}, _fun), do: {:ok, Enum.reverse(list), acc}
+end
diff --git a/lib/elixir/lib/module/types/infer.ex b/lib/elixir/lib/module/types/infer.ex
new file mode 100644
index 000000000..ade413a35
--- /dev/null
+++ b/lib/elixir/lib/module/types/infer.ex
@@ -0,0 +1,583 @@
+defmodule Module.Types.Infer do
+  @moduledoc false
+
+  import Module.Types.Helpers
+
+  defmacrop is_var(expr) do
+    quote do
+      is_tuple(unquote(expr)) and
+        tuple_size(unquote(expr)) == 3 and
+        is_atom(elem(unquote(expr), 0)) and
+        is_atom(elem(unquote(expr), 2))
+    end
+  end
+
+  # :atom
+  def of_pattern(atom, context) when is_atom(atom) do
+    {:ok, {:literal, atom}, context}
+  end
+
+  # 12
+  def of_pattern(literal, context) when is_integer(literal) do
+    {:ok, :integer, context}
+  end
+
+  # 1.2
+  def of_pattern(literal, context) when is_float(literal) do
+    {:ok, :float, context}
+  end
+
+  # "..."
+  def of_pattern(literal, context) when is_binary(literal) do
+    {:ok, :binary, context}
+  end
+
+  # <<...>>>
+  def of_pattern({:<<>>, _meta, args} = expr, context) do
+    expr_stack(expr, context, fn context ->
+      case reduce_ok(args, context, &of_binary/2) do
+        {:ok, context} -> {:ok, :binary, context}
+        {:error, reason} -> {:error, reason}
+      end
+    end)
+  end
+
+  # [left | right]
+  def of_pattern([{:|, _meta, [left_expr, right_expr]}] = expr, context) do
+    expr_stack(expr, context, fn context ->
+      with {:ok, left, context} <- of_pattern(left_expr, context),
+           {:ok, right, context} <- of_pattern(right_expr, context),
+           do: {:ok, {:cons, left, right}, context}
+    end)
+  end
+
+  # [left, right]
+  def of_pattern([left_expr | right_expr] = expr, context) do
+    expr_stack(expr, context, fn context ->
+      with {:ok, left, context} <- of_pattern(left_expr, context),
+           {:ok, right, context} <- of_pattern(right_expr, context),
+           do: {:ok, {:cons, left, right}, context}
+    end)
+  end
+
+  # []
+  def of_pattern([], context) do
+    {:ok, :null, context}
+  end
+
+  # _
+  def of_pattern({:_, _meta, atom}, context) when is_atom(atom) do
+    {:ok, :dynamic, context}
+  end
+
+  # var
+  def of_pattern(var, context) when is_var(var) do
+    {type, context} = new_var(var, context)
+    {:ok, type, context}
+  end
+
+  # {left, right}
+  def of_pattern({left, right}, context) do
+    of_pattern({:{}, [], [left, right]}, context)
+  end
+
+  # {...}
+  def of_pattern({:{}, _meta, exprs} = expr, context) do
+    expr_stack(expr, context, fn context ->
+      case map_reduce_ok(exprs, context, &of_pattern/2) do
+        {:ok, types, context} -> {:ok, {:tuple, types}, context}
+        {:error, reason} -> {:error, reason}
+      end
+    end)
+  end
+
+  # left = right
+  def of_pattern({:=, _meta, [left_expr, right_expr]} = expr, context) do
+    expr_stack(expr, context, fn context ->
+      with {:ok, left_type, context} <- of_pattern(left_expr, context),
+           {:ok, right_type, context} <- of_pattern(right_expr, context),
+           do: unify(left_type, right_type, context)
+    end)
+  end
+
+  # %{...}
+  def of_pattern({:%{}, _meta, args} = expr, context) do
+    result =
+      expr_stack(expr, context, fn context ->
+        map_reduce_ok(args, context, fn {key, value}, context ->
+          with {:ok, key_type, context} <- of_pattern(key, context),
+               {:ok, value_type, context} <- of_pattern(value, context),
+               do: {:ok, {key_type, value_type}, context}
+        end)
+      end)
+
+    case result do
+      {:ok, pairs, context} -> {:ok, {:map, pairs}, context}
+      {:error, reason} -> {:error, reason}
+    end
+  end
+
+  # TODO: structs
+  def of_pattern({:%, _meta, _args}, context) do
+    {:ok, {:map, []}, context}
+  end
+
+  def of_guard(guard, context) do
+    expr_stack(guard, context, fn context ->
+      # Flatten `foo and bar` to list of type constraints
+      reduce_ok(flatten_binary_op(:and, guard), context, fn guard, context ->
+        # Flatten `foo or bar` to later build a union
+        union = Enum.map(flatten_binary_op(:or, guard), &type_guard/1)
+
+        # Only use group of guards using a single variable
+        with {:ok, args, guard_types} <- unzip_ok(union),
+             [_arg] <- Enum.uniq(Enum.map(args, &remove_meta/1)) do
+          expr_stack(guard, context, fn context ->
+            union = to_union(guard_types, context)
+            unify_guard(hd(args), union, context)
+          end)
+        else
+          _ -> {:ok, context}
+        end
+      end)
+    end)
+  end
+
+  defp flatten_binary_op(:and, {{:., _, [:erlang, :andalso]}, _, [left, right]}) do
+    flatten_binary_op(:and, left) ++ flatten_binary_op(:and, right)
+  end
+
+  defp flatten_binary_op(:or, {{:., _, [:erlang, :orelse]}, _, [left, right]}) do
+    flatten_binary_op(:or, left) ++ flatten_binary_op(:or, right)
+  end
+
+  defp flatten_binary_op(_op, other) do
+    [other]
+  end
+
+  defp unify_guard(arg, guard_type, context) when is_var(arg) do
+    # TODO: It is incorrect to use of_pattern/2 but it helps for simplicity now
+    with {:ok, arg_type, context} <- of_pattern(arg, context),
+         {:ok, _, context} <- unify(arg_type, guard_type, context),
+         do: {:ok, context}
+  end
+
+  defp unify_guard(_arg, _guard_type, context) do
+    {:ok, context}
+  end
+
+  # Unimplemented guards:
+  # !=/2 !==/2 </2 <=/2 >/2 >=/2 ==/2 ===/2 not/1
+  # */2 +/1 +/2 -/1 -/2 //2
+  # abs/2 ceil/1 floor/1 round/1 trunc/1
+  # elem/2 hd/1 in/2 length/1 map_size/1 tl/1 tuple_size/1
+  # is_function/1 is_function/2 is_list/1 is_number/1 is_pid/1 is_port/1 is_reference/1 is_tuple/1
+  # node/1 self/1
+  # binary_part/3 bit_size/1 byte_size/1 div/2 rem/2 node/0
+
+  @type_guards %{
+    is_atom: :atom,
+    is_binary: :binary,
+    is_bitstring: :binary,
+    is_boolean: :boolean,
+    is_float: :float,
+    is_integer: :integer,
+    is_map: {:map, []}
+  }
+
+  defp type_guard({{:., _, [:erlang, guard]}, _, [arg]}) do
+    case :maps.find(guard, @type_guards) do
+      {:ok, type} -> {:ok, arg, type}
+      :error -> {:error, :unknown_guard}
+    end
+  end
+
+  defp type_guard(_other), do: {:error, :unknown_guard}
+
+  # binary-pattern :: specifier
+  defp of_binary({:"::", _meta, [expr, specifiers]} = full_expr, context) do
+    specifiers = List.flatten(collect_specifiers(specifiers))
+
+    expected_type =
+      cond do
+        :integer in specifiers -> :integer
+        :float in specifiers -> :float
+        :bits in specifiers -> :binary
+        :bitstring in specifiers -> :binary
+        :bytes in specifiers -> :binary
+        :binary in specifiers -> :binary
+        :utf8 in specifiers -> :integer
+        :utf16 in specifiers -> :integer
+        :utf32 in specifiers -> :integer
+        true -> :integer
+      end
+
+    expr_stack(full_expr, context, fn context ->
+      with {:ok, type, context} <- of_pattern(expr, context),
+           {:ok, _type, context} <- unify(type, expected_type, context),
+           do: {:ok, context}
+    end)
+  end
+
+  # binary-pattern
+  defp of_binary(expr, context) do
+    case of_pattern(expr, context) do
+      {:ok, type, context} when type in [:integer, :float, :binary] ->
+        {:ok, context}
+
+      {:ok, type, _context} ->
+        {:error, {:invalid_binary_type, type}}
+
+      {:error, reason} ->
+        {:error, reason}
+    end
+  end
+
+  # Collect binary type specifiers,
+  # from `<<pattern::integer-size(10)>>` collect `integer`
+  defp collect_specifiers({:-, _meta, [left, right]}) do
+    [collect_specifiers(left), collect_specifiers(right)]
+  end
+
+  defp collect_specifiers({specifier, _meta, []}) do
+    [specifier]
+  end
+
+  defp collect_specifiers({name, _meta, context}) when is_atom(name) and is_atom(context) do
+    [name]
+  end
+
+  defp collect_specifiers(_other) do
+    []
+  end
+
+  ## UNIFICATION
+
+  def unify(left, right, context) do
+    case do_unify(left, right, context) do
+      {:ok, type, context} -> {:ok, type, %{context | unify_stack: []}}
+      {:error, reason} -> {:error, reason}
+    end
+  end
+
+  defp do_unify(type, {:var, var}, context) do
+    case :maps.get(var, context.types) do
+      :unbound ->
+        context = refine_var(var, type, context)
+        context = push_unify_stack(var, context)
+
+        if recursive_type?(type, [], context) do
+          error({:unable_unify, type, {:var, var}}, context)
+        else
+          {:ok, {:var, var}, context}
+        end
+
+      var_type ->
+        # Only add trace if the variable wasn't already "expanded"
+        context =
+          if variable_expanded?(var, context) do
+            context
+          else
+            trace_var(var, type, context)
+          end
+
+        context = push_unify_stack(var, context)
+
+        case do_unify(type, var_type, context) do
+          {:ok, var_type, context} ->
+            context = refine_var(var, var_type, context)
+            {:ok, {:var, var}, context}
+
+          {:error, reason} ->
+            {:error, reason}
+        end
+    end
+  end
+
+  defp do_unify({:var, var}, type, context) do
+    do_unify(type, {:var, var}, context)
+  end
+
+  defp do_unify({:tuple, lefts}, {:tuple, rights}, context)
+       when length(lefts) == length(rights) do
+    result =
+      map_reduce_ok(Enum.zip(lefts, rights), context, fn {left, right}, context ->
+        do_unify(left, right, context)
+      end)
+
+    case result do
+      {:ok, types, context} -> {:ok, {:tuple, types}, context}
+      {:error, reason} -> {:error, reason}
+    end
+  end
+
+  defp do_unify({:cons, left_left, left_right}, {:cons, right_left, right_right}, context) do
+    with {:ok, left, context} <- do_unify(left_left, right_left, context),
+         {:ok, right, context} <- do_unify(left_right, right_right, context),
+         do: {:ok, {:cons, left, right}, context}
+  end
+
+  defp do_unify({:map, left_pairs}, {:map, right_pairs}, context) do
+    # Since maps in patterns only support literal keys (excluding maps)
+    # we can do exact type match without subtype checking
+
+    unique_right_pairs =
+      Enum.reject(right_pairs, fn {key, _value} ->
+        :lists.keyfind(key, 1, left_pairs)
+      end)
+
+    unique_pairs = left_pairs ++ unique_right_pairs
+
+    # Build union of all unique key-value pairs between the maps
+    result =
+      map_reduce_ok(unique_pairs, context, fn {left_key, left_value}, context ->
+        case :lists.keyfind(left_key, 1, right_pairs) do
+          {^left_key, right_value} ->
+            case do_unify(left_value, right_value, context) do
+              {:ok, value, context} -> {:ok, {left_key, value}, context}
+              {:error, reason} -> {:error, reason}
+            end
+
+          false ->
+            {:ok, {left_key, left_value}, context}
+        end
+      end)
+
+    case result do
+      {:ok, pairs, context} -> {:ok, {:map, pairs}, context}
+      {:error, reason} -> {:error, reason}
+    end
+  end
+
+  defp do_unify(:dynamic, right, context) do
+    {:ok, right, context}
+  end
+
+  defp do_unify(left, :dynamic, context) do
+    {:ok, left, context}
+  end
+
+  defp do_unify(left, right, context) do
+    cond do
+      subtype?(left, right, context) -> {:ok, left, context}
+      subtype?(right, left, context) -> {:ok, right, context}
+      true -> error({:unable_unify, left, right}, context)
+    end
+  end
+
+  # Check unify stack to see if variable was already expanded
+  defp variable_expanded?(var, context) do
+    Enum.any?(context.unify_stack, &variable_same?(var, &1, context))
+  end
+
+  # Find if two variables are the same or point to the other
+  defp variable_same?(same, same, _context) do
+    true
+  end
+
+  defp variable_same?(left, right, context) do
+    case :maps.find(left, context.types) do
+      {:ok, {:var, new_left}} ->
+        variable_same?(new_left, right, context)
+
+      _ ->
+        case :maps.find(right, context.types) do
+          {:ok, {:var, new_right}} -> variable_same?(left, new_right, context)
+          _ -> false
+        end
+    end
+  end
+
+  defp push_unify_stack(var, context) do
+    %{context | unify_stack: [var | context.unify_stack]}
+  end
+
+  def new_var(var, context) do
+    case :maps.find(var_name(var), context.vars) do
+      {:ok, type} ->
+        {type, context}
+
+      :error ->
+        type = {:var, context.counter}
+        vars = :maps.put(var_name(var), type, context.vars)
+        types_to_vars = :maps.put(context.counter, var, context.types_to_vars)
+        types = :maps.put(context.counter, :unbound, context.types)
+        traces = :maps.put(context.counter, [], context.traces)
+        counter = context.counter + 1
+
+        context = %{
+          context
+          | vars: vars,
+            types_to_vars: types_to_vars,
+            types: types,
+            traces: traces,
+            counter: counter
+        }
+
+        {type, context}
+    end
+  end
+
+  defp refine_var(var, type, context) do
+    types = :maps.put(var, type, context.types)
+    trace_var(var, type, %{context | types: types})
+  end
+
+  defp trace_var(var, type, context) do
+    line = get_meta(hd(context.expr_stack))[:line]
+    trace = {type, context.expr_stack, {context.file, line}}
+    traces = :maps.update_with(var, &[trace | &1], context.traces)
+    %{context | traces: traces}
+  end
+
+  defp var_name({name, _meta, context}), do: {name, context}
+
+  # Check if a variable is recursive and incompatible with itself
+  # Bad: `{var} = var`
+  # Good: `x = y; y = z; z = x`
+  defp recursive_type?({:var, var} = parent, parents, context) do
+    case :maps.get(var, context.types) do
+      :unbound ->
+        false
+
+      type ->
+        if type in parents do
+          not Enum.all?(parents, &match?({:var, _}, &1))
+        else
+          recursive_type?(type, [parent | parents], context)
+        end
+    end
+  end
+
+  defp recursive_type?({:cons, left, right} = parent, parents, context) do
+    recursive_type?(left, [parent | parents], context) or
+      recursive_type?(right, [parent | parents], context)
+  end
+
+  defp recursive_type?({:tuple, types} = parent, parents, context) do
+    Enum.any?(types, &recursive_type?(&1, [parent | parents], context))
+  end
+
+  defp recursive_type?({:map, pairs} = parent, parents, context) do
+    Enum.any?(pairs, fn {key, value} ->
+      recursive_type?(key, [parent | parents], context) or
+        recursive_type?(value, [parent | parents], context)
+    end)
+  end
+
+  defp recursive_type?(_other, _parents, _context) do
+    false
+  end
+
+  def subtype?({:literal, boolean}, :boolean, _context) when is_boolean(boolean), do: true
+  def subtype?({:literal, atom}, :atom, _context) when is_atom(atom), do: true
+  def subtype?(:boolean, :atom, _context), do: true
+  def subtype?({:tuple, _}, :tuple, _context), do: true
+
+  # TODO: Lift unions to unify/3?
+  def subtype?({:union, left_types}, {:union, _} = right_union, context) do
+    Enum.all?(left_types, &subtype?(&1, right_union, context))
+  end
+
+  def subtype?(left, {:union, right_types}, context) do
+    Enum.any?(right_types, &subtype?(left, &1, context))
+  end
+
+  def subtype?(left, right, _context), do: left == right
+
+  def to_union(types, context) when types != [] do
+    if :dynamic in types do
+      # NOTE: Or filter away dynamic()?
+      :dynamic
+    else
+      case unique_super_types(types, context) do
+        [type] -> type
+        types -> {:union, types}
+      end
+    end
+  end
+
+  # Filter subtypes
+  # `boolean() | atom()` => `atom()`
+  # `:foo | atom()` => `atom()`
+  # Does not unify `true | false` => `boolean()`
+  defp unique_super_types([type | types], context) do
+    types = Enum.reject(types, &subtype?(&1, type, context))
+
+    if Enum.any?(types, &subtype?(type, &1, context)) do
+      unique_super_types(types, context)
+    else
+      [type | unique_super_types(types, context)]
+    end
+  end
+
+  defp unique_super_types([], _context) do
+    []
+  end
+
+  # Collect relevant information from context and traces to report error
+  defp error({:unable_unify, left, right}, context) do
+    {fun, arity} = context.function
+    line = get_meta(hd(context.expr_stack))[:line]
+    location = {context.file, line, {context.module, fun, arity}}
+
+    traces = type_traces(context)
+    common_expr = common_super_expr(traces)
+    traces = simplify_traces(traces, context)
+
+    {:error, {Module.Types, {:unable_unify, left, right, common_expr, traces}, [location]}}
+  end
+
+  # Collect relevant traces from context.traces using context.unify_stack
+  defp type_traces(context) do
+    stack = Enum.uniq(context.unify_stack)
+
+    Enum.flat_map(stack, fn var_index ->
+      case :maps.find(var_index, context.traces) do
+        {:ok, traces} ->
+          expr_var = :maps.get(var_index, context.types_to_vars)
+          Enum.map(traces, &{expr_var, &1})
+
+        _other ->
+          []
+      end
+    end)
+  end
+
+  # Only use last expr from trace and tag if trace is for
+  # a concrete type or type variable
+  defp simplify_traces(traces, context) do
+    Enum.flat_map(traces, fn {var, {type, [expr | _], location}} ->
+      case type do
+        {:var, var_index} ->
+          var2 = :maps.get(var_index, context.types_to_vars)
+          [{var, {:var, var2, expr, location}}]
+
+        _ ->
+          [{var, {:type, type, expr, location}}]
+      end
+    end)
+  end
+
+  # Find first common super expression among all traces
+  defp common_super_expr([]) do
+    nil
+  end
+
+  defp common_super_expr([{_var, {_type, expr_stack, _location}} | traces]) do
+    Enum.find_value(expr_stack, fn expr ->
+      common? =
+        Enum.all?(traces, fn {_var, {_type, expr_stack, _location}} -> expr in expr_stack end)
+
+      if common? do
+        expr
+      end
+    end)
+  end
+
+  defp remove_meta({fun, meta, args}) when is_list(meta), do: {fun, [], args}
+  defp remove_meta(other), do: other
+
+  defp get_meta({_fun, meta, _args}) when is_list(meta), do: meta
+  defp get_meta(_other), do: []
+end
diff --git a/lib/elixir/src/elixir_compiler.erl b/lib/elixir/src/elixir_compiler.erl
index f23165a34..6272f0cc5 100644
--- a/lib/elixir/src/elixir_compiler.erl
+++ b/lib/elixir/src/elixir_compiler.erl
@@ -148,6 +148,8 @@ bootstrap_main() ->
    <<"lib/elixir/lib/module/checker.ex">>,
    <<"lib/elixir/lib/module/locals_tracker.ex">>,
    <<"lib/elixir/lib/module/parallel_checker.ex">>,
+   <<"lib/elixir/lib/module/types/helpers.ex">>,
+   <<"lib/elixir/lib/module/types/infer.ex">>,
    <<"lib/elixir/lib/module/types.ex">>,
    <<"lib/elixir/lib/kernel/typespec.ex">>,
    <<"lib/elixir/lib/kernel/utils.ex">>,
diff --git a/lib/elixir/test/elixir/module/types/infer_test.exs b/lib/elixir/test/elixir/module/types/infer_test.exs
new file mode 100644
index 000000000..228ea667c
--- /dev/null
+++ b/lib/elixir/test/elixir/module/types/infer_test.exs
@@ -0,0 +1,369 @@
+Code.require_file("../../test_helper.exs", __DIR__)
+
+defmodule Module.Types.InferTest do
+  use ExUnit.Case, async: true
+  import Module.Types.Infer
+  alias Module.Types
+
+  defmacrop quoted_pattern(expr) do
+    quote do
+      of_pattern(unquote(Macro.escape(expr)), new_context())
+      |> lift_result()
+    end
+  end
+
+  defp unify_lift(left, right, context \\ new_context()) do
+    unify(left, right, context)
+    |> lift_result()
+  end
+
+  defp new_context() do
+    %{
+      Types.context("types_test.ex", TypesTest, {:test, 0})
+      | expr_stack: [{:foo, [], nil}]
+    }
+  end
+
+  defp lift_result({:ok, type, context}) do
+    {:ok, Types.lift_type(type, context)}
+  end
+
+  defp lift_result({:error, {Types, reason, location}}) do
+    {:error, {reason, location}}
+  end
+
+  describe "of_pattern/2" do
+    test "error location" do
+      assert {:error, {{:unable_unify, :binary, :integer, expr, traces}, location}} =
+               quoted_pattern(<<foo::integer, foo::binary>>)
+
+      assert location == [{"types_test.ex", 38, {TypesTest, :test, 0}}]
+
+      assert {:<<>>, _,
+              [
+                {:"::", _, [{:foo, _, nil}, {:integer, _, nil}]},
+                {:"::", _, [{:foo, _, nil}, {:binary, _, nil}]}
+              ]} = expr
+
+      assert [
+               {{:foo, _, nil},
+                {:type, :binary, {:"::", _, [{:foo, _, nil}, {:binary, _, nil}]},
+                 {"types_test.ex", 38}}},
+               {{:foo, _, nil},
+                {:type, :integer, {:"::", _, [{:foo, _, nil}, {:integer, _, nil}]},
+                 {"types_test.ex", 38}}}
+             ] = traces
+    end
+
+    test "literal" do
+      assert quoted_pattern(true) == {:ok, {:literal, true}}
+      assert quoted_pattern(false) == {:ok, {:literal, false}}
+      assert quoted_pattern(:foo) == {:ok, {:literal, :foo}}
+      assert quoted_pattern(0) == {:ok, :integer}
+      assert quoted_pattern(0.0) == {:ok, :float}
+      assert quoted_pattern("foo") == {:ok, :binary}
+    end
+
+    test "list" do
+      assert quoted_pattern([]) == {:ok, :null}
+      assert quoted_pattern([123]) == {:ok, {:cons, :integer, :null}}
+      assert quoted_pattern([123 | []]) == {:ok, {:cons, :integer, :null}}
+      assert quoted_pattern([123 | 456]) == {:ok, {:cons, :integer, :integer}}
+
+      assert quoted_pattern([123, 456 | 789]) ==
+               {:ok, {:cons, :integer, {:cons, :integer, :integer}}}
+    end
+
+    test "tuple" do
+      assert quoted_pattern({}) == {:ok, {:tuple, []}}
+      assert quoted_pattern({:a}) == {:ok, {:tuple, [{:literal, :a}]}}
+      assert quoted_pattern({:a, 123}) == {:ok, {:tuple, [{:literal, :a}, :integer]}}
+    end
+
+    test "map" do
+      assert quoted_pattern(%{}) == {:ok, {:map, []}}
+      assert quoted_pattern(%{a: :b}) == {:ok, {:map, [{{:literal, :a}, {:literal, :b}}]}}
+      assert quoted_pattern(%{123 => a}) == {:ok, {:map, [{:integer, {:var, 0}}]}}
+
+      assert {:error, {{:unable_unify, {:literal, :foo}, :integer, _, _}, _}} =
+               quoted_pattern(%{a: a = 123, b: a = :foo})
+    end
+
+    test "binary" do
+      assert quoted_pattern(<<"foo"::binary>>) == {:ok, :binary}
+      assert quoted_pattern(<<123::integer>>) == {:ok, :binary}
+      assert quoted_pattern(<<foo::integer>>) == {:ok, :binary}
+
+      assert quoted_pattern({<<foo::integer>>, foo}) == {:ok, {:tuple, [:binary, :integer]}}
+      assert quoted_pattern({<<foo::binary>>, foo}) == {:ok, {:tuple, [:binary, :binary]}}
+
+      assert {:error, {{:unable_unify, :integer, :binary, _, _}, _}} =
+               quoted_pattern(<<123::binary>>)
+
+      assert {:error, {{:unable_unify, :binary, :integer, _, _}, _}} =
+               quoted_pattern(<<"foo"::integer>>)
+
+      assert {:error, {{:unable_unify, :integer, :binary, _, _}, _}} =
+               quoted_pattern(<<foo::binary, foo::integer>>)
+    end
+
+    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(_) == {:ok, :dynamic}
+      assert quoted_pattern({_ = 123, _}) == {:ok, {:tuple, [: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(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}, _, _}, _}} =
+               quoted_pattern({x} = x)
+    end
+  end
+
+  describe "unify/3" do
+    test "literal" do
+      assert unify_lift({:literal, :foo}, {:literal, :foo}) == {:ok, {:literal, :foo}}
+
+      assert {:error, {{:unable_unify, {:literal, :foo}, {:literal, :bar}, _, _}, _}} =
+               unify_lift({:literal, :foo}, {:literal, :bar})
+    end
+
+    test "type" do
+      assert unify_lift(:integer, :integer) == {:ok, :integer}
+      assert unify_lift(:binary, :binary) == {:ok, :binary}
+      assert unify_lift(:atom, :atom) == {:ok, :atom}
+      assert unify_lift(:boolean, :boolean) == {:ok, :boolean}
+
+      assert {:error, {{:unable_unify, :integer, :boolean, _, _}, _}} =
+               unify_lift(:integer, :boolean)
+    end
+
+    test "subtype" do
+      assert unify_lift(:boolean, :atom) == {:ok, :boolean}
+      assert unify_lift(:atom, :boolean) == {:ok, :boolean}
+      assert unify_lift(:boolean, {:literal, true}) == {:ok, {:literal, true}}
+      assert unify_lift({:literal, true}, :boolean) == {:ok, {:literal, true}}
+      assert unify_lift(:atom, {:literal, true}) == {:ok, {:literal, true}}
+      assert unify_lift({:literal, true}, :atom) == {:ok, {:literal, true}}
+    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 {:error, {{:unable_unify, {:tuple, [:integer]}, {:tuple, []}, _, _}, _}} =
+               unify_lift({:tuple, [:integer]}, {:tuple, []})
+
+      assert {:error, {{:unable_unify, :integer, :atom, _, _}, _}} =
+               unify_lift({:tuple, [:integer]}, {:tuple, [:atom]})
+    end
+
+    test "cons" do
+      assert unify_lift({:cons, :integer, :integer}, {:cons, :integer, :integer}) ==
+               {:ok, {:cons, :integer, :integer}}
+
+      assert unify_lift({:cons, :boolean, :atom}, {:cons, :atom, :boolean}) ==
+               {:ok, {:cons, :boolean, :boolean}}
+
+      assert {:error, {{:unable_unify, :atom, :integer, _, _}, _}} =
+               unify_lift({:cons, :integer, :atom}, {:cons, :integer, :integer})
+
+      assert {:error, {{:unable_unify, :atom, :integer, _, _}, _}} =
+               unify_lift({:cons, :atom, :integer}, {:cons, :integer, :integer})
+    end
+
+    test "map" do
+      assert unify_lift({:map, []}, {:map, []}) == {:ok, {:map, []}}
+
+      assert unify_lift({:map, [{:integer, :atom}]}, {:map, []}) ==
+               {:ok, {:map, [{:integer, :atom}]}}
+
+      assert unify_lift({:map, []}, {:map, [{:integer, :atom}]}) ==
+               {:ok, {:map, [{:integer, :atom}]}}
+
+      assert unify_lift({:map, [{:integer, :atom}]}, {:map, [{:integer, :atom}]}) ==
+               {:ok, {:map, [{:integer, :atom}]}}
+
+      assert unify_lift({:map, [{:integer, :atom}]}, {:map, [{:atom, :integer}]}) ==
+               {:ok, {:map, [{:integer, :atom}, {:atom, :integer}]}}
+
+      assert unify_lift(
+               {:map, [{{:literal, :foo}, :boolean}]},
+               {:map, [{{:literal, :foo}, :atom}]}
+             ) ==
+               {:ok, {:map, [{{:literal, :foo}, :boolean}]}}
+
+      assert {:error, {{:unable_unify, :integer, :atom, _, _}, _}} =
+               unify_lift(
+                 {:map, [{{:literal, :foo}, :integer}]},
+                 {:map, [{{:literal, :foo}, :atom}]}
+               )
+    end
+
+    test "union" do
+      assert unify_lift({:union, []}, {:union, []}) == {:ok, {:union, []}}
+      assert unify_lift({:union, [:integer]}, {:union, [:integer]}) == {:ok, {:union, [:integer]}}
+
+      assert unify_lift({:union, [:integer, :atom]}, {:union, [:integer, :atom]}) ==
+               {:ok, {:union, [:integer, :atom]}}
+
+      assert unify_lift({:union, [:integer, :atom]}, {:union, [:atom, :integer]}) ==
+               {:ok, {:union, [:integer, :atom]}}
+
+      assert unify_lift({:union, [:atom]}, {:union, [:boolean]}) == {:ok, {:union, [:boolean]}}
+      assert unify_lift({:union, [:boolean]}, {:union, [:atom]}) == {:ok, {:union, [:boolean]}}
+
+      assert {:error, {{:unable_unify, {:union, [:integer]}, {:union, [:atom]}, _, _}, _}} =
+               unify_lift({:union, [:integer]}, {:union, [:atom]})
+    end
+
+    test "dynamic" do
+      assert unify_lift({:literal, :foo}, :dynamic) == {:ok, {:literal, :foo}}
+      assert unify_lift(:dynamic, {:literal, :foo}) == {:ok, {:literal, :foo}}
+      assert unify_lift(:integer, :dynamic) == {:ok, :integer}
+      assert unify_lift(:dynamic, :integer) == {:ok, :integer}
+    end
+
+    test "vars" do
+      assert {{:var, 0}, var_context} = new_var({:foo, [], nil}, new_context())
+      assert {{:var, 1}, var_context} = new_var({:bar, [], nil}, var_context)
+
+      assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, var_context)
+      assert Types.lift_type({:var, 0}, context) == :integer
+
+      assert {:ok, {:var, 0}, context} = unify(:integer, {:var, 0}, var_context)
+      assert Types.lift_type({:var, 0}, context) == :integer
+
+      assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, var_context)
+      assert {:var, _} = Types.lift_type({:var, 0}, context)
+      assert {:var, _} = Types.lift_type({:var, 1}, context)
+
+      assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, var_context)
+      assert {:ok, {:var, 1}, context} = unify({:var, 1}, :integer, context)
+      assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, context)
+
+      assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, var_context)
+      assert {:ok, {:var, 1}, context} = unify({:var, 1}, :integer, context)
+      assert {:ok, {:var, _}, context} = unify({:var, 1}, {:var, 0}, context)
+
+      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, :binary, :integer, _, _}, _}} =
+               unify_lift({:var, 0}, {:var, 1}, context)
+
+      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({:var, 1}, {:var, 0}, context)
+    end
+
+    test "vars inside tuples" do
+      assert {{:var, 0}, var_context} = new_var({:foo, [], nil}, new_context())
+      assert {{:var, 1}, var_context} = new_var({:bar, [], nil}, var_context)
+
+      assert {:ok, {:tuple, [{:var, 0}]}, context} =
+               unify({:tuple, [{:var, 0}]}, {:tuple, [: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, {:var, 1}, context} = unify({:var, 1}, {:tuple, [{:var, 0}]}, var_context)
+      assert {:ok, {:var, 0}, context} = unify({:var, 0}, :integer, context)
+      assert Types.lift_type({:var, 1}, context) == {:tuple, [: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, :binary, :integer, _, _}, _}} =
+               unify_lift({:tuple, [{:var, 0}]}, {:tuple, [{:var, 1}]}, context)
+    end
+
+    # TODO: Vars inside unions
+
+    test "recursive type" do
+      assert {{:var, 0}, var_context} = new_var({:foo, [], nil}, new_context())
+      assert {{:var, 1}, var_context} = new_var({:bar, [], nil}, var_context)
+      assert {{:var, 2}, var_context} = new_var({:baz, [], nil}, var_context)
+
+      assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, var_context)
+      assert {:ok, {:var, _}, context} = unify({:var, 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 {:ok, {:var, _}, context} = unify({:var, 2}, {:var, 0}, context)
+
+      assert {:ok, {:var, _}, context} = unify({:var, 0}, {:var, 1}, var_context)
+
+      assert {:error, {{:unable_unify, {:tuple, [var: 0]}, {:var, 0}, _, _}, _}} =
+               unify_lift({:var, 1}, {:tuple, [{: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, {:tuple, [var: 0]}, {:var, 0}, _, _}, _}} =
+               unify_lift({:var, 2}, {:tuple, [{:var, 0}]}, context)
+    end
+  end
+
+  test "subtype?/3" do
+    assert subtype?({:literal, :foo}, :atom, new_context())
+    assert subtype?({:literal, true}, :boolean, new_context())
+    assert subtype?({:literal, true}, :atom, new_context())
+    assert subtype?(:boolean, :atom, new_context())
+
+    refute subtype?(:integer, :binary, new_context())
+    refute subtype?(:atom, {:literal, :foo}, new_context())
+    refute subtype?(:boolean, {:literal, true}, new_context())
+    refute subtype?(:atom, {:literal, true}, new_context())
+    refute subtype?(:atom, :boolean, new_context())
+  end
+
+  test "to_union/2" do
+    assert to_union([:atom], new_context()) == :atom
+    assert to_union([:integer, :integer], new_context()) == :integer
+    assert to_union([:boolean, :atom], new_context()) == :atom
+    assert to_union([{:literal, :foo}, :boolean, :atom], new_context()) == :atom
+
+    assert to_union([:binary, :atom], new_context()) == {:union, [:binary, :atom]}
+    assert to_union([:atom, :binary, :atom], new_context()) == {:union, [:atom, :binary]}
+
+    assert to_union([{:literal, :foo}, :binary, :atom], new_context()) ==
+             {:union, [:binary, :atom]}
+
+    assert {{:var, 0}, var_context} = new_var({:foo, [], nil}, new_context())
+    assert to_union([{:var, 0}], var_context) == {:var, 0}
+
+    # TODO: Add missing tests that uses variables and higher rank types.
+    #       We may have to change, to_union to use unify, check the return
+    #       type and throw away the returned context instead of using subtype?
+    #       since subtype? is incomplete when it comes to variables and higher
+    #       rank types.
+
+    # assert {:ok, {:var, _}, context} = unify({:var, 0}, :integer, var_context)
+    # assert to_union([{:var, 0}, :integer], context) == :integer
+
+    assert to_union([{:tuple, [:integer]}, {:tuple, [:integer]}], new_context()) ==
+             {:tuple, [:integer]}
+
+    # assert to_union([{:tuple, [:boolean]}, {:tuple, [:atom]}], new_context()) == {:tuple, [:atom]}
+  end
+end
diff --git a/lib/elixir/test/elixir/module/types_test.exs b/lib/elixir/test/elixir/module/types_test.exs
index b34c31e40..1120a8e23 100644
--- a/lib/elixir/test/elixir/module/types_test.exs
+++ b/lib/elixir/test/elixir/module/types_test.exs
@@ -1,15 +1,8 @@
 Code.require_file("../test_helper.exs", __DIR__)
 
 defmodule Module.TypesTest do
-  alias Module.Types
   use ExUnit.Case, async: true
-
-  defmacrop quoted_pattern(expr) do
-    quote do
-      Types.of_pattern(unquote(Macro.escape(expr)), new_context())
-      |> lift_result()
-    end
-  end
+  alias Module.Types
 
   defmacrop quoted_clause(exprs) do
     quote do
@@ -33,113 +26,10 @@ defmodule Module.TypesTest do
     {:ok, Types.lift_types(types, context)}
   end
 
-  defp lift_result({:ok, type, context}) do
-    {:ok, Types.lift_type(type, context)}
-  end
-
   defp lift_result({:error, {Types, reason, location}}) do
     {:error, {reason, location}}
   end
 
-  describe "of_pattern/2" do
-    test "error location" do
-      assert {:error, {{:unable_unify, :binary, :integer, expr, traces}, location}} =
-               quoted_pattern(<<foo::integer, foo::binary>>)
-
-      assert location == [{"types_test.ex", 47, {TypesTest, :test, 0}}]
-
-      assert {:<<>>, _,
-              [
-                {:"::", _, [{:foo, _, nil}, {:integer, _, nil}]},
-                {:"::", _, [{:foo, _, nil}, {:binary, _, nil}]}
-              ]} = expr
-
-      assert [
-               {{:foo, _, nil},
-                {:type, :binary, {:"::", _, [{:foo, _, nil}, {:binary, _, nil}]},
-                 {"types_test.ex", 47}}},
-               {{:foo, _, nil},
-                {:type, :integer, {:"::", _, [{:foo, _, nil}, {:integer, _, nil}]},
-                 {"types_test.ex", 47}}}
-             ] = traces
-    end
-
-    test "literals" do
-      assert quoted_pattern(true) == {:ok, {:literal, true}}
-      assert quoted_pattern(false) == {:ok, {:literal, false}}
-      assert quoted_pattern(:foo) == {:ok, {:literal, :foo}}
-      assert quoted_pattern(0) == {:ok, :integer}
-      assert quoted_pattern(0.0) == {:ok, :float}
-      assert quoted_pattern("foo") == {:ok, :binary}
-    end
-
-    test "list" do
-      assert quoted_pattern([]) == {:ok, :null}
-      assert quoted_pattern([123]) == {:ok, {:cons, :integer, :null}}
-      assert quoted_pattern([123 | []]) == {:ok, {:cons, :integer, :null}}
-      assert quoted_pattern([123 | 456]) == {:ok, {:cons, :integer, :integer}}
-
-      assert quoted_pattern([123, 456 | 789]) ==
-               {:ok, {:cons, :integer, {:cons, :integer, :integer}}}
-    end
-
-    test "tuple" do
-      assert quoted_pattern({}) == {:ok, {:tuple, []}}
-      assert quoted_pattern({:a}) == {:ok, {:tuple, [{:literal, :a}]}}
-      assert quoted_pattern({:a, 123}) == {:ok, {:tuple, [{:literal, :a}, :integer]}}
-    end
-
-    test "map" do
-      assert quoted_pattern(%{}) == {:ok, {:map, []}}
-      assert quoted_pattern(%{a: :b}) == {:ok, {:map, [{{:literal, :a}, {:literal, :b}}]}}
-      assert quoted_pattern(%{123 => a}) == {:ok, {:map, [{:integer, {:var, 0}}]}}
-
-      assert {:error, {{:unable_unify, {:literal, :foo}, :integer, _, _}, _}} =
-               quoted_pattern(%{a: a = 123, b: a = :foo})
-    end
-
-    test "binary" do
-      assert quoted_pattern(<<"foo"::binary>>) == {:ok, :binary}
-      assert quoted_pattern(<<123::integer>>) == {:ok, :binary}
-      assert quoted_pattern(<<foo::integer>>) == {:ok, :binary}
-
-      assert quoted_pattern({<<foo::integer>>, foo}) == {:ok, {:tuple, [:binary, :integer]}}
-      assert quoted_pattern({<<foo::binary>>, foo}) == {:ok, {:tuple, [:binary, :binary]}}
-
-      assert {:error, {{:unable_unify, :integer, :binary, _, _}, _}} =
-               quoted_pattern(<<123::binary>>)
-
-      assert {:error, {{:unable_unify, :binary, :integer, _, _}, _}} =
-               quoted_pattern(<<"foo"::integer>>)
-
-      assert {:error, {{:unable_unify, :integer, :binary, _, _}, _}} =
-               quoted_pattern(<<foo::binary, foo::integer>>)
-    end
-
-    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(_) == {:ok, :dynamic}
-      assert quoted_pattern({_ = 123, _}) == {:ok, {:tuple, [: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(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}, _, _}, _}} =
-               quoted_pattern({x} = x)
-    end
-  end
-
   describe "of_clause/2" do
     test "various" do
       assert quoted_clause([true]) == {:ok, [{:literal, true}]}
@@ -237,5 +127,11 @@ defmodule Module.TypesTest do
     assert Types.format_type({:cons, :binary, :binary}) == "[binary() | binary()]"
     assert Types.format_type({:tuple, []}) == "{}"
     assert Types.format_type({:tuple, [:integer]}) == "{integer()}"
+    assert Types.format_type({:map, []}) == "%{}"
+    assert Types.format_type({:map, [{:integer, :atom}]}) == "%{integer() => atom()}"
+    assert Types.format_type({:map, [{:__struct__, Struct}]}) == "%Struct{}"
+
+    assert Types.format_type({:map, [{:__struct__, Struct}, {:integer, :atom}]}) ==
+             "%Struct{integer() => atom()}"
   end
 end