Add inference of function head to find function clauses that will never match (#9270)

7 files changed, 1432 insertions, 24 deletions

diff --git a/lib/elixir/lib/module/checker.ex b/lib/elixir/lib/module/checker.ex
index 48ad15523..e61bf48e7 100644
--- a/lib/elixir/lib/module/checker.ex
+++ b/lib/elixir/lib/module/checker.ex
@@ -5,8 +5,14 @@ defmodule Module.Checker do
 
   def verify(module, cache) do
     case prepare_module(module) do
-      {:ok, map} -> {build_chunk(map), warnings(map, cache)}
-      :error -> {nil, []}
+      {:ok, map} ->
+        undefined_and_deprecation_warnings = undefined_and_deprecation_warnings(map, cache)
+        {types, infer_warnings} = infer_definitions(map)
+        warnings = infer_warnings ++ undefined_and_deprecation_warnings
+        {build_chunk(map, types), emit_warnings(warnings)}
+
+      :error ->
+        {nil, []}
     end
   end
 
@@ -41,21 +47,23 @@ defmodule Module.Checker do
   defp checker_chunk(binary) do
     with {:ok, {_, [{'ExCk', chunk}]}} <- :beam_lib.chunks(binary, ['ExCk']),
          {:elixir_checker_v1, contents} <- :erlang.binary_to_term(chunk) do
-      deprecated = Enum.map(contents.exports, fn {fun, {_kind, reason}} -> {fun, reason} end)
+      deprecated = Enum.map(contents.exports, fn {fun, map} -> {fun, map.deprecated_reason} end)
       {:ok, %{deprecated: deprecated, no_warn_undefined: contents.no_warn_undefined}}
     else
       _ -> :error
     end
   end
 
-  defp build_chunk(map) do
+  defp build_chunk(map, types) do
     exports = ParallelChecker.definitions_to_exports(map.definitions)
     deprecated = :maps.from_list(map.deprecated)
+    types = :maps.from_list(types)
 
     exports =
       Enum.map(exports, fn {function, kind} ->
-        reason = :maps.get(function, deprecated, nil)
-        {function, {kind, reason}}
+        deprecated_reason = :maps.get(function, deprecated, nil)
+        type = :maps.get(function, types, nil)
+        {function, %{kind: kind, deprecated_reason: deprecated_reason, type: type}}
       end)
 
     contents = %{
@@ -66,7 +74,24 @@ defmodule Module.Checker do
     {'ExCk', :erlang.term_to_binary({:elixir_checker_v1, contents})}
   end
 
-  defp warnings(map, cache) do
+  defp infer_definitions(map) do
+    results = Module.Types.infer_definitions(map.file, map.module, map.definitions)
+
+    Enum.reduce(results, {[], []}, fn
+      {function, {:ok, type_and_context}}, {types, warnings} ->
+        type =
+          Enum.map(type_and_context, fn {type, context} ->
+            Module.Types.lift_types(type, context)
+          end)
+
+        {[{function, type} | types], warnings}
+
+      {_function, {:error, reason}}, {types, warnings} ->
+        {types, [reason | warnings]}
+    end)
+  end
+
+  defp undefined_and_deprecation_warnings(map, cache) do
     no_warn_undefined = map.no_warn_undefined ++ Code.get_compiler_option(:no_warn_undefined)
 
     state = %{
@@ -83,7 +108,6 @@ defmodule Module.Checker do
     state.warnings
     |> merge_warnings()
     |> sort_warnings()
-    |> emit_warnings()
   end
 
   defp check_definitions(definitions, state) do
@@ -210,25 +234,25 @@ defmodule Module.Checker do
   defp warn(meta, state, warning) do
     {fun, arity} = state.function
     location = {state.file, meta[:line], {state.module, fun, arity}}
-    %{state | warnings: [{warning, location} | state.warnings]}
+    %{state | warnings: [{__MODULE__, warning, location} | state.warnings]}
   end
 
   defp merge_warnings(warnings) do
-    Enum.reduce(warnings, %{}, fn {warning, location}, acc ->
+    Enum.reduce(warnings, %{}, fn {module, warning, location}, acc ->
       locations = MapSet.new([location])
-      Map.update(acc, warning, locations, &MapSet.put(&1, location))
+      Map.update(acc, {module, warning}, locations, &MapSet.put(&1, location))
     end)
   end
 
   defp sort_warnings(warnings) do
     warnings
-    |> Enum.map(fn {warning, locations} -> {warning, Enum.sort(locations)} end)
+    |> Enum.map(fn {{module, warning}, locations} -> {module, warning, Enum.sort(locations)} end)
     |> Enum.sort()
   end
 
   defp emit_warnings(warnings) do
-    Enum.flat_map(warnings, fn {warning, locations} ->
-      message = format_warning(warning)
+    Enum.flat_map(warnings, fn {module, warning, locations} ->
+      message = module.format_warning(warning)
       print_warning([message, ?\n, format_locations(locations)])
 
       Enum.map(locations, fn {file, line, _mfa} ->
@@ -237,7 +261,7 @@ defmodule Module.Checker do
     end)
   end
 
-  defp format_warning({:undefined_module, module, fun, arity}) do
+  def format_warning({:undefined_module, module, fun, arity}) do
     [
       Exception.format_mfa(module, fun, arity),
       " is undefined (module ",
@@ -246,7 +270,7 @@ defmodule Module.Checker do
     ]
   end
 
-  defp format_warning({:undefined_function, module, fun, arity, exports}) do
+  def format_warning({:undefined_function, module, fun, arity, exports}) do
     [
       Exception.format_mfa(module, fun, arity),
       " is undefined or private",
@@ -254,7 +278,7 @@ defmodule Module.Checker do
     ]
   end
 
-  defp format_warning({:deprecated, module, fun, arity, reason}) do
+  def format_warning({:deprecated, module, fun, arity, reason}) do
     [
       Exception.format_mfa(module, fun, arity),
       " is deprecated. ",
@@ -262,7 +286,7 @@ defmodule Module.Checker do
     ]
   end
 
-  defp format_warning({:unrequired_module, module, fun, arity}) do
+  def format_warning({:unrequired_module, module, fun, arity}) do
     [
       "you must require ",
       inspect(module),
diff --git a/lib/elixir/lib/module/parallel_checker.ex b/lib/elixir/lib/module/parallel_checker.ex
index 323b159aa..9f502a406 100644
--- a/lib/elixir/lib/module/parallel_checker.ex
+++ b/lib/elixir/lib/module/parallel_checker.ex
@@ -286,8 +286,8 @@ defmodule Module.ParallelChecker do
 
   defp cache_chunk(ets, module, exports) do
     exports =
-      Enum.map(exports, fn {{fun, arity}, {kind, deprecated}} ->
-        :ets.insert(ets, {{:export, {module, fun, arity}}, kind, deprecated})
+      Enum.map(exports, fn {{fun, arity}, %{kind: kind, deprecated_reason: reason}} ->
+        :ets.insert(ets, {{:export, {module, fun, arity}}, kind, reason})
 
         {{fun, arity}, kind}
       end)
diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
new file mode 100644
index 000000000..e6e1c8cd4
--- /dev/null
+++ b/lib/elixir/lib/module/types.ex
@@ -0,0 +1,959 @@
+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
+
+  @doc """
+  Infer function definitions' types.
+  """
+  def infer_definitions(file, module, defs) do
+    Enum.map(defs, fn {{fun, _arity} = function, kind, meta, clauses} ->
+      context = context(file, module, function)
+
+      types =
+        map_ok(clauses, fn {_meta, params, guards, _body} ->
+          def_expr = {kind, meta, [guards_to_expr(guards, {fun, [], params})]}
+
+          expr_stack(def_expr, context, fn context ->
+            of_clause(params, guards, context)
+          end)
+        end)
+
+      {function, types}
+    end)
+  end
+
+  @doc false
+  def of_clause(params, guards, context) do
+    with {:ok, types, context} <- map_reduce_ok(params, context, &of_pattern/2),
+         {:ok, context} <- of_guard(guards_to_or(guards), context),
+         do: {:ok, types, context}
+  end
+
+  @doc false
+  def context(file, module, function) do
+    %{
+      # File of module
+      file: file,
+      # Module of definitions
+      module: module,
+      # Current function
+      function: function,
+      # Expression variable to type variable
+      vars: %{},
+      # Type variable to expression variable
+      types_to_vars: %{},
+      # Type variable to type
+      types: %{},
+      # Trace of all variables that have been refined to a type,
+      # including the type they were refined to, why, and where
+      traces: %{},
+      # Stack of variables we have refined during unification,
+      # used for creating relevant traces
+      unify_stack: [],
+      # Stack of expression we have recursed through during inference,
+      # used for tracing
+      expr_stack: [],
+      # Counter to give type variables unique names
+      counter: 0
+    }
+  end
+
+  @doc """
+  Lifts type variables to their infered types from the context.
+  """
+  def lift_types(types, context) do
+    context = %{
+      types: context.types,
+      quantified_types: %{},
+      quantified_counter: 0
+    }
+
+    {types, _context} = Enum.map_reduce(types, context, &do_lift_type/2)
+    types
+  end
+
+  @doc false
+  def lift_type(type, context) do
+    context = %{
+      types: context.types,
+      quantified_types: %{},
+      quantified_counter: 0
+    }
+
+    {type, _context} = do_lift_type(type, context)
+    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
+
+  # TODO: Remove this and let multiple when be treated as multiple clauses,
+  #       meaning they will be intersection types
+  defp guards_to_or([]) do
+    []
+  end
+
+  defp guards_to_or(guards) 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
+
+  defp guards_to_expr([guard | guards], left) do
+    guards_to_expr(guards, {:when, [], [left, guard]})
+  end
+
+  ## VARIABLE QUANTIFICATION
+
+  # Lift type variable to its infered types from the context
+  defp do_lift_type({:var, var}, context) do
+    case :maps.find(var, context.quantified_types) do
+      {:ok, quantified_var} ->
+        {{:var, quantified_var}, context}
+
+      :error ->
+        case :maps.find(var, context.types) do
+          {:ok, :unbound} ->
+            new_quantified_var(var, context)
+
+          {:ok, type} ->
+            # Remove visited types to avoid infinite loops
+            # then restore after we are done recursing on vars
+            types = context.types
+            context = %{context | types: :maps.remove(var, context.types)}
+            {type, context} = do_lift_type(type, context)
+            {type, %{context | types: types}}
+
+          :error ->
+            new_quantified_var(var, context)
+        end
+    end
+  end
+
+  defp do_lift_type({:tuple, types}, context) do
+    {types, context} = Enum.map_reduce(types, context, &do_lift_type/2)
+    {{:tuple, types}, context}
+  end
+
+  defp do_lift_type({:map, pairs}, context) do
+    {pairs, context} =
+      Enum.map_reduce(pairs, context, fn {key, value}, context ->
+        {key, context} = do_lift_type(key, context)
+        {value, context} = do_lift_type(value, context)
+        {{key, value}, context}
+      end)
+
+    {{:map, pairs}, context}
+  end
+
+  defp do_lift_type({:cons, left, right}, context) do
+    {left, context} = do_lift_type(left, context)
+    {right, context} = do_lift_type(right, context)
+    {{:cons, left, right}, context}
+  end
+
+  defp do_lift_type(other, context) do
+    {other, context}
+  end
+
+  defp new_quantified_var(original_var, context) do
+    types = :maps.put(original_var, context.quantified_counter, context.quantified_types)
+    counter = context.quantified_counter + 1
+
+    type = {:var, context.quantified_counter}
+    context = %{context | quantified_types: types, quantified_counter: counter}
+    {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
+    [
+      "function clause will never match, found incompatibility:\n\n    ",
+      format_type(left),
+      " !~ ",
+      format_type(right),
+      "\n\n",
+      format_expr(expr),
+      format_traces(traces),
+      "Conflict found at"
+    ]
+  end
+
+  defp format_expr(nil) do
+    []
+  end
+
+  defp format_expr(expr) do
+    [
+      "in expression:\n\n    ",
+      expr_to_string(expr),
+      "\n\n"
+    ]
+  end
+
+  defp format_traces([]) do
+    []
+  end
+
+  defp format_traces(traces) do
+    Enum.map(traces, fn
+      {var, {:type, type, expr, location}} ->
+        [
+          "where \"",
+          Macro.to_string(var),
+          "\" was given the type ",
+          Module.Types.format_type(type),
+          " in:\n\n    # ",
+          format_location(location),
+          "    ",
+          expr_to_string(expr),
+          "\n\n"
+        ]
+
+      {var1, {:var, var2, expr, location}} ->
+        [
+          "where \"",
+          Macro.to_string(var1),
+          "\" was given the same type as \"",
+          Macro.to_string(var2),
+          "\" in:\n\n    # ",
+          format_location(location),
+          "    ",
+          expr_to_string(expr),
+          "\n\n"
+        ]
+    end)
+  end
+
+  defp format_location({file, line}) do
+    file = Path.relative_to_cwd(file)
+    line = if line, do: [Integer.to_string(line)], else: []
+    [file, ?:, line, ?\n]
+  end
+
+  @doc false
+  def format_type({:tuple, types}) do
+    "{#{Enum.map_join(types, ", ", &format_type/1)}}"
+  end
+
+  def format_type({:cons, left, :null}) do
+    "[#{format_type(left)}]"
+  end
+
+  def format_type({:cons, left, right}) do
+    "[#{format_type(left)} | #{format_type(right)}]"
+  end
+
+  def format_type({:literal, literal}) do
+    inspect(literal)
+  end
+
+  def format_type(:null) do
+    "[]"
+  end
+
+  def format_type(atom) when is_atom(atom) do
+    "#{atom}()"
+  end
+
+  def format_type({:var, index}) do
+    "var#{index}"
+  end
+
+  defp expr_to_string(expr) do
+    expr
+    |> rewrite_guard()
+    |> Macro.to_string()
+  end
+
+  defp rewrite_guard(guard) do
+    Macro.prewalk(guard, fn
+      {{:., _, [:erlang, :element]}, _, [{{:., _, [:erlang, :+]}, _, [int, 1]}, arg]} ->
+        {:elem, [], [arg, int]}
+
+      {{:., _, [:erlang, :element]}, _, [int, arg]} when is_integer(int) ->
+        {:elem, [], [arg, int - 1]}
+
+      {:., _, [:erlang, call]} ->
+        rewrite_guard_call(call)
+
+      other ->
+        other
+    end)
+  end
+
+  defp rewrite_guard_call(:orelse), do: :or
+  defp rewrite_guard_call(:andalso), do: :and
+  defp rewrite_guard_call(:"=<"), do: :<=
+  defp rewrite_guard_call(:"/="), do: :!=
+  defp rewrite_guard_call(:"=:="), do: :===
+  defp rewrite_guard_call(:"=/="), do: :!==
+
+  defp rewrite_guard_call(op) when op in [:band, :bor, :bnot, :bsl, :bsr, :bxor],
+    do: {:., [], [Bitwise, op]}
+
+  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/src/elixir_compiler.erl b/lib/elixir/src/elixir_compiler.erl
index 9918f6e60..f23165a34 100644
--- a/lib/elixir/src/elixir_compiler.erl
+++ b/lib/elixir/src/elixir_compiler.erl
@@ -148,6 +148,7 @@ 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.ex">>,
    <<"lib/elixir/lib/kernel/typespec.ex">>,
    <<"lib/elixir/lib/kernel/utils.ex">>,
    <<"lib/elixir/lib/exception.ex">>,
diff --git a/lib/elixir/test/elixir/module/checker_test.exs b/lib/elixir/test/elixir/module/checker_test.exs
index 8a507d505..973129d93 100644
--- a/lib/elixir/test/elixir/module/checker_test.exs
+++ b/lib/elixir/test/elixir/module/checker_test.exs
@@ -30,9 +30,9 @@ defmodule Module.CheckerTest do
       contents = read_chunk(modules[A])
 
       assert contents.exports == [
-               {{:c, 0}, {:def, nil}},
-               {{:d, 0}, {:defmacro, nil}},
-               {{:e, 0}, {:def, "oops"}}
+               {{:c, 0}, %{deprecated_reason: nil, kind: :def, type: [[]]}},
+               {{:d, 0}, %{deprecated_reason: nil, kind: :defmacro, type: [[]]}},
+               {{:e, 0}, %{deprecated_reason: "oops", kind: :def, type: [[]]}}
              ]
     end
   end
@@ -620,6 +620,188 @@ defmodule Module.CheckerTest do
     end
   end
 
+  describe "function header inference" do
+    test "warns on literals" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def a(var = 123, var = "abc"), do: var
+        end
+        """
+      }
+
+      warning = """
+      warning: function clause will never match, found incompatibility:
+
+          binary() !~ integer()
+
+      in expression:
+
+          def(a(var = 123, var = "abc"))
+
+      where "var" was given the type binary() in:
+
+          # a.ex:2
+          var = "abc"
+
+      where "var" was given the type integer() in:
+
+          # a.ex:2
+          var = 123
+
+      Conflict found at
+        a.ex:2: A.a/2
+
+      """
+
+      assert_warnings(files, warning)
+    end
+
+    test "warns on binary patterns" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def a(<<var::integer, var::binary>>), do: var
+        end
+        """
+      }
+
+      warning = """
+      warning: function clause will never match, found incompatibility:
+
+          binary() !~ integer()
+
+      in expression:
+
+          <<var::integer(), var::binary()>>
+
+      where "var" was given the type binary() in:
+
+          # a.ex:2
+          var :: binary()
+
+      where "var" was given the type integer() in:
+
+          # a.ex:2
+          var :: integer()
+
+      Conflict found at
+        a.ex:2: A.a/1
+
+      """
+
+      assert_warnings(files, warning)
+    end
+
+    test "warns on recursive patterns" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def a({var} = var), do: var
+        end
+        """
+      }
+
+      warning = """
+      warning: function clause will never match, found incompatibility:
+
+          {var0} !~ var0
+
+      in expression:
+
+          {var} = var
+
+      where "var" was given the type {var0} in:
+
+          # a.ex:2
+          {var} = var
+
+      Conflict found at
+        a.ex:2: A.a/1
+
+      """
+
+      assert_warnings(files, warning)
+    end
+
+    test "warns on guards" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def a(var) when is_integer(var) and is_binary(var), do: var
+        end
+        """
+      }
+
+      warning = """
+      warning: function clause will never match, found incompatibility:
+
+          binary() !~ integer()
+
+      in expression:
+
+          is_integer(var) and is_binary(var)
+
+      where "var" was given the type binary() in:
+
+          # a.ex:2
+          is_binary(var)
+
+      where "var" was given the type integer() in:
+
+          # a.ex:2
+          is_integer(var)
+
+      Conflict found at
+        a.ex:2: A.a/1
+
+      """
+
+      assert_warnings(files, warning)
+    end
+
+    test "warns on guards with multiple variables" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def a(x = y) when is_integer(x) and is_binary(y), do: {x, y}
+        end
+        """
+      }
+
+      warning = """
+      warning: function clause will never match, found incompatibility:
+
+          binary() !~ integer()
+
+      in expression:
+
+          def(a(x = y) when is_integer(x) and is_binary(y))
+
+      where "x" was given the type integer() in:
+
+          # a.ex:2
+          is_integer(x)
+
+      where "y" was given the type binary() in:
+
+          # a.ex:2
+          is_binary(y)
+
+      where "y" was given the same type as "x" in:
+
+          # a.ex:2
+          x = y
+
+      Conflict found at
+        a.ex:2: A.a/1
+
+      """
+
+      assert_warnings(files, warning)
+    end
+  end
+
   defp assert_warnings(files, expected) when is_binary(expected) do
     assert capture_compile_warnings(files) == expected
   end
diff --git a/lib/elixir/test/elixir/module/types_test.exs b/lib/elixir/test/elixir/module/types_test.exs
new file mode 100644
index 000000000..b34c31e40
--- /dev/null
+++ b/lib/elixir/test/elixir/module/types_test.exs
@@ -0,0 +1,241 @@
+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
+
+  defmacrop quoted_clause(exprs) do
+    quote do
+      Types.of_clause(unquote(Macro.escape(exprs)), [], new_context())
+      |> lift_result()
+    end
+  end
+
+  defmacrop quoted_clause(exprs, guards) do
+    quote do
+      Types.of_clause(unquote(Macro.escape(exprs)), unquote(Macro.escape(guards)), new_context())
+      |> lift_result()
+    end
+  end
+
+  defp new_context() do
+    Types.context("types_test.ex", TypesTest, {:test, 0})
+  end
+
+  defp lift_result({:ok, types, context}) when is_list(types) 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}]}
+      assert quoted_clause([foo]) == {:ok, [{:var, 0}]}
+    end
+
+    test "assignment" do
+      assert quoted_clause([x = y, x = y]) == {:ok, [{:var, 0}, {:var, 0}]}
+      assert quoted_clause([x = y, y = x]) == {:ok, [{:var, 0}, {:var, 0}]}
+
+      assert quoted_clause([x = :foo, x = y, y = z]) ==
+               {:ok, [{:literal, :foo}, {:literal, :foo}, {:literal, :foo}]}
+
+      assert quoted_clause([x = y, y = :foo, y = z]) ==
+               {:ok, [{:literal, :foo}, {:literal, :foo}, {:literal, :foo}]}
+
+      assert quoted_clause([x = y, y = z, z = :foo]) ==
+               {:ok, [{:literal, :foo}, {:literal, :foo}, {:literal, :foo}]}
+
+      assert {:error, {{:unable_unify, {:tuple, [var: 1]}, {:var, 0}, _, _}, _}} =
+               quoted_clause([{x} = y, {y} = x])
+    end
+
+    test "guards" do
+      assert quoted_clause([x], [:erlang.is_binary(x)]) == {:ok, [:binary]}
+
+      assert quoted_clause([x, y], [:erlang.andalso(:erlang.is_binary(x), :erlang.is_atom(y))]) ==
+               {:ok, [:binary, :atom]}
+
+      assert quoted_clause([x], [:erlang.orelse(:erlang.is_binary(x), :erlang.is_atom(x))]) ==
+               {:ok, [{:union, [:binary, :atom]}]}
+
+      assert quoted_clause([x, x], [:erlang.is_integer(x)]) == {:ok, [:integer, :integer]}
+
+      assert quoted_clause([x = 123], [:erlang.is_integer(x)]) == {:ok, [:integer]}
+
+      assert quoted_clause([x], [:erlang.orelse(:erlang.is_boolean(x), :erlang.is_atom(x))]) ==
+               {:ok, [:atom]}
+
+      assert quoted_clause([x], [:erlang.orelse(:erlang.is_atom(x), :erlang.is_boolean(x))]) ==
+               {:ok, [:atom]}
+
+      assert quoted_clause([x], [:erlang.andalso(:erlang.is_boolean(x), :erlang.is_atom(x))]) ==
+               {:ok, [:boolean]}
+
+      assert quoted_clause([x], [:erlang.andalso(:erlang.is_atom(x), :erlang.is_boolean(x))]) ==
+               {:ok, [:boolean]}
+
+      assert quoted_clause([x, x = y, y = z], [:erlang.is_atom(x)]) ==
+               {:ok, [:atom, :atom, :atom]}
+
+      assert quoted_clause([x = y, y, y = z], [:erlang.is_atom(y)]) ==
+               {:ok, [:atom, :atom, :atom]}
+
+      assert quoted_clause([x = y, y = z, z], [:erlang.is_atom(z)]) ==
+               {:ok, [:atom, :atom, :atom]}
+
+      assert {:error, {{:unable_unify, :integer, :binary, _, _}, _}} =
+               quoted_clause([x], [:erlang.andalso(:erlang.is_binary(x), :erlang.is_integer(x))])
+    end
+
+    test "map" do
+      assert quoted_clause([%{true: false} = foo, %{} = foo]) ==
+               {:ok,
+                [
+                  {:map, [{{:literal, true}, {:literal, false}}]},
+                  {:map, [{{:literal, true}, {:literal, false}}]}
+                ]}
+
+      assert quoted_clause([%{true: bool}], [:erlang.is_boolean(bool)]) ==
+               {:ok,
+                [
+                  {:map, [{{:literal, true}, :boolean}]}
+                ]}
+
+      assert quoted_clause([%{true: true} = foo, %{false: false} = foo]) ==
+               {:ok,
+                [
+                  {:map,
+                   [{{:literal, false}, {:literal, false}}, {{:literal, true}, {:literal, true}}]},
+                  {:map,
+                   [{{:literal, false}, {:literal, false}}, {{:literal, true}, {:literal, true}}]}
+                ]}
+
+      assert {:error, {{:unable_unify, {:literal, true}, {:literal, false}, _, _}, _}} =
+               quoted_clause([%{true: false} = foo, %{true: true} = foo])
+    end
+  end
+
+  test "format_type/1" do
+    assert Types.format_type(:binary) == "binary()"
+    assert Types.format_type({:literal, true}) == "true"
+    assert Types.format_type({:literal, :atom}) == ":atom"
+    assert Types.format_type({:cons, :binary, :null}) == "[binary()]"
+    assert Types.format_type({:cons, :binary, :binary}) == "[binary() | binary()]"
+    assert Types.format_type({:tuple, []}) == "{}"
+    assert Types.format_type({:tuple, [:integer]}) == "{integer()}"
+  end
+end
diff --git a/lib/elixir/test/elixir/protocol/consolidation_test.exs b/lib/elixir/test/elixir/protocol/consolidation_test.exs
index 1d0630961..9337b058c 100644
--- a/lib/elixir/test/elixir/protocol/consolidation_test.exs
+++ b/lib/elixir/test/elixir/protocol/consolidation_test.exs
@@ -117,7 +117,8 @@ defmodule Protocol.ConsolidationTest do
 
     {:ok, {Sample, [{'ExCk', check_bin}]}} = :beam_lib.chunks(@sample_binary, ['ExCk'])
     assert {:elixir_checker_v1, contents} = :erlang.binary_to_term(check_bin)
-    assert {{:ok, 1}, {:def, "Reason"}} in contents.exports
+    export_info = %{deprecated_reason: "Reason", kind: :def, type: [[var: 0]]}
+    assert {{:ok, 1}, export_info} in contents.exports
   end
 
   test "consolidation keeps source" do