diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index a4fcf190e07..a355f29fcd5 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -84,7 +84,9 @@ defmodule Module.Types do
       # A list of all warnings found so far
       warnings: [],
       # Information about all vars and their types
-      vars: %{}
+      vars: %{},
+      # Information about variables and arguments from patterns
+      pattern_info: nil
     }
   end
 end
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index c5fcc9a6493..79275ded3c8 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -38,6 +38,8 @@ defmodule Module.Types.Descr do
 
   # Type definitions
 
+  defguard is_descr(descr) when is_map(descr) or descr == :term
+
   def dynamic(), do: %{dynamic: :term}
   def none(), do: @none
   def term(), do: :term
@@ -55,8 +57,8 @@ defmodule Module.Types.Descr do
   def integer(), do: %{bitmap: @bit_integer}
   def float(), do: %{bitmap: @bit_float}
   def fun(), do: %{bitmap: @bit_fun}
-  def list(), do: %{bitmap: @bit_list}
-  def non_empty_list(), do: %{bitmap: @bit_non_empty_list}
+  def list(_arg), do: %{bitmap: @bit_list}
+  def non_empty_list(_arg, _tail \\ empty_list()), do: %{bitmap: @bit_non_empty_list}
   def open_map(), do: %{map: @map_top}
   def open_map(pairs), do: map_descr(:open, pairs)
   def open_tuple(elements), do: tuple_descr(:open, elements)
@@ -113,6 +115,8 @@ defmodule Module.Types.Descr do
   def term_type?(:term), do: true
   def term_type?(descr), do: subtype_static(unfolded_term(), Map.delete(descr, :dynamic))
 
+  def dynamic_term_type?(descr), do: descr == %{dynamic: :term}
+
   def gradual?(:term), do: false
   def gradual?(descr), do: is_map_key(descr, :dynamic)
 
@@ -133,6 +137,8 @@ defmodule Module.Types.Descr do
   """
   def union(:term, other) when not is_optional(other), do: :term
   def union(other, :term) when not is_optional(other), do: :term
+  def union(none, other) when none == %{}, do: other
+  def union(other, none) when none == %{}, do: other
 
   def union(left, right) do
     left = unfold(left)
@@ -166,6 +172,8 @@ defmodule Module.Types.Descr do
   """
   def intersection(:term, other) when not is_optional(other), do: other
   def intersection(other, :term) when not is_optional(other), do: other
+  def intersection(%{dynamic: :term}, other) when not is_optional(other), do: dynamic(other)
+  def intersection(other, %{dynamic: :term}) when not is_optional(other), do: dynamic(other)
 
   def intersection(left, right) do
     left = unfold(left)
@@ -385,6 +393,18 @@ defmodule Module.Types.Descr do
 
   ## Bitmaps
 
+  @doc """
+  Optimized version of `not empty?(intersection(empty_list(), type))`.
+  """
+  def empty_list_type?(:term), do: true
+  def empty_list_type?(%{dynamic: :term}), do: true
+
+  def empty_list_type?(%{dynamic: %{bitmap: bitmap}}) when (bitmap &&& @bit_empty_list) != 0,
+    do: true
+
+  def empty_list_type?(%{bitmap: bitmap}) when (bitmap &&& @bit_empty_list) != 0, do: true
+  def empty_list_type?(_), do: false
+
   @doc """
   Optimized version of `not empty?(intersection(binary(), type))`.
   """
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 2c195f074dd..8dfacd81e76 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -6,69 +6,63 @@ defmodule Module.Types.Expr do
 
   14 = length(Macro.Env.__info__(:struct))
 
+  aliases = list(tuple([atom(), atom()]))
+  functions_and_macros = list(tuple([atom(), list(tuple([atom(), integer()]))]))
+  list_of_modules = list(atom())
+
   @caller closed_map(
             __struct__: atom([Macro.Env]),
-            aliases: list(),
+            aliases: aliases,
             context: atom([:match, :guard, nil]),
-            context_modules: list(),
+            context_modules: list_of_modules,
             file: binary(),
             function: union(tuple(), atom([nil])),
-            functions: list(),
+            functions: functions_and_macros,
             lexical_tracker: union(pid(), atom([nil])),
             line: integer(),
-            macro_aliases: list(),
-            macros: list(),
+            macro_aliases: aliases,
+            macros: functions_and_macros,
             module: atom(),
-            requires: list(),
-            tracers: list(),
+            requires: list_of_modules,
+            tracers: list_of_modules,
             versioned_vars: open_map()
           )
 
   @atom_true atom([true])
   @exception open_map(__struct__: atom(), __exception__: @atom_true)
 
-  # of_expr/4 is public as it is called recursively from Of.binary
-  def of_expr(expr, expected_expr, stack, context) do
-    with {:ok, actual, context} <- of_expr(expr, stack, context) do
-      Of.intersect(actual, expected_expr, stack, context)
-    end
-  end
-
   # :atom
-  def of_expr(atom, _stack, context) when is_atom(atom) do
-    {:ok, atom([atom]), context}
-  end
+  def of_expr(atom, _stack, context) when is_atom(atom),
+    do: {:ok, atom([atom]), context}
 
   # 12
-  def of_expr(literal, _stack, context) when is_integer(literal) do
-    {:ok, integer(), context}
-  end
+  def of_expr(literal, _stack, context) when is_integer(literal),
+    do: {:ok, integer(), context}
 
   # 1.2
-  def of_expr(literal, _stack, context) when is_float(literal) do
-    {:ok, float(), context}
-  end
+  def of_expr(literal, _stack, context) when is_float(literal),
+    do: {:ok, float(), context}
 
   # "..."
-  def of_expr(literal, _stack, context) when is_binary(literal) do
-    {:ok, binary(), context}
-  end
+  def of_expr(literal, _stack, context) when is_binary(literal),
+    do: {:ok, binary(), context}
 
   # #PID<...>
-  def of_expr(literal, _stack, context) when is_pid(literal) do
-    {:ok, pid(), context}
-  end
+  def of_expr(literal, _stack, context) when is_pid(literal),
+    do: {:ok, pid(), context}
 
   # []
-  def of_expr([], _stack, context) do
-    {:ok, empty_list(), context}
-  end
+  def of_expr([], _stack, context),
+    do: {:ok, empty_list(), context}
 
-  # TODO: [expr, ...]
-  def of_expr(exprs, stack, context) when is_list(exprs) do
-    case map_reduce_ok(exprs, context, &of_expr(&1, stack, &2)) do
-      {:ok, _types, context} -> {:ok, non_empty_list(), context}
-      {:error, context} -> {:error, context}
+  # [expr, ...]
+  def of_expr(list, stack, context) when is_list(list) do
+    {prefix, suffix} = unpack_list(list, [])
+
+    with {:ok, prefix, context} <-
+           map_reduce_ok(prefix, context, &of_expr(&1, stack, &2)),
+         {:ok, suffix, context} <- of_expr(suffix, stack, context) do
+      {:ok, non_empty_list(Enum.reduce(prefix, &union/2), suffix), context}
     end
   end
 
@@ -84,27 +78,11 @@ defmodule Module.Types.Expr do
   def of_expr({:<<>>, _meta, args}, stack, context) do
     case Of.binary(args, :expr, stack, context) do
       {:ok, context} -> {:ok, binary(), context}
-      # It is safe to discard errors from binary inside expressions
+      # It is safe to discard errors from binaries, we can continue typechecking
       {:error, context} -> {:ok, binary(), context}
     end
   end
 
-  # TODO: left | []
-  def of_expr({:|, _meta, [left_expr, []]}, stack, context) do
-    of_expr(left_expr, stack, context)
-  end
-
-  # TODO: left | right
-  def of_expr({:|, _meta, [left_expr, right_expr]}, stack, context) do
-    case of_expr(left_expr, stack, context) do
-      {:ok, _left, context} ->
-        of_expr(right_expr, stack, context)
-
-      {:error, context} ->
-        {:error, context}
-    end
-  end
-
   def of_expr({:__CALLER__, _meta, var_context}, _stack, context)
       when is_atom(var_context) do
     {:ok, @caller, context}
@@ -113,7 +91,7 @@ defmodule Module.Types.Expr do
   # TODO: __STACKTRACE__
   def of_expr({:__STACKTRACE__, _meta, var_context}, _stack, context)
       when is_atom(var_context) do
-    {:ok, list(), context}
+    {:ok, list(term()), context}
   end
 
   # {...}
@@ -123,10 +101,10 @@ defmodule Module.Types.Expr do
     end
   end
 
-  # TODO: left = right
+  # left = right
   def of_expr({:=, _meta, [left_expr, right_expr]} = expr, stack, context) do
     with {:ok, right_type, context} <- of_expr(right_expr, stack, context) do
-      Pattern.of_match(left_expr, {right_type, expr}, stack, context)
+      Pattern.of_match(left_expr, right_type, expr, stack, context)
     end
   end
 
@@ -152,6 +130,7 @@ defmodule Module.Types.Expr do
                {:ok, {key, type}, context}
              end
            end),
+         # TODO: args_types could be an empty list
          {:ok, struct_type, context} <-
            Of.struct(module, args_types, :only_defaults, struct_meta, stack, context),
          {:ok, map_type, context} <- of_expr(map, stack, context) do
@@ -172,6 +151,7 @@ defmodule Module.Types.Expr do
 
   # %Struct{}
   def of_expr({:%, _, [module, {:%{}, _, args}]} = expr, stack, context) do
+    # TODO: We should not skip defaults
     Of.struct(expr, module, args, :skip_defaults, stack, context, &of_expr/3)
   end
 
@@ -359,7 +339,7 @@ defmodule Module.Types.Expr do
     {:ok, fun(), context}
   end
 
-  # TODO: call(arg)
+  # TODO: local_call(arg)
   def of_expr({fun, _meta, args}, stack, context)
       when is_atom(fun) and is_list(args) do
     with {:ok, _arg_types, context} <-
@@ -404,7 +384,7 @@ defmodule Module.Types.Expr do
             end
 
             {:ok, _type, context} =
-              Of.refine_var(var, {expected, expr}, formatter, stack, context)
+              Of.refine_var(var, expected, expr, formatter, stack, context)
 
             context
         end
@@ -426,7 +406,7 @@ defmodule Module.Types.Expr do
 
   defp for_clause({:<<>>, _, [{:<-, meta, [left, right]}]}, stack, context) do
     with {:ok, right_type, context} <- of_expr(right, stack, context),
-         {:ok, _pattern_type, context} <- Pattern.of_match(left, {binary(), left}, stack, context) do
+         {:ok, _pattern_type, context} <- Pattern.of_match(left, binary(), left, stack, context) do
       if binary_type?(right_type) do
         {:ok, context}
       else
@@ -539,7 +519,7 @@ defmodule Module.Types.Expr do
   ## Warning formatting
 
   def format_diagnostic({:badupdate, type, expr, expected_type, actual_type, context}) do
-    traces = Of.collect_traces(expr, context)
+    traces = collect_traces(expr, context)
 
     %{
       details: %{typing_traces: traces},
@@ -558,13 +538,13 @@ defmodule Module.Types.Expr do
 
               #{to_quoted_string(actual_type) |> indent(4)}
           """,
-          Of.format_traces(traces)
+          format_traces(traces)
         ])
     }
   end
 
   def format_diagnostic({:badbinary, type, expr, context}) do
-    traces = Of.collect_traces(expr, context)
+    traces = collect_traces(expr, context)
 
     %{
       details: %{typing_traces: traces},
@@ -579,7 +559,7 @@ defmodule Module.Types.Expr do
 
               #{to_quoted_string(type) |> indent(4)}
           """,
-          Of.format_traces(traces)
+          format_traces(traces)
         ])
     }
   end
diff --git a/lib/elixir/lib/module/types/helpers.ex b/lib/elixir/lib/module/types/helpers.ex
index 37307ae91cd..820c66aa0a2 100644
--- a/lib/elixir/lib/module/types/helpers.ex
+++ b/lib/elixir/lib/module/types/helpers.ex
@@ -2,6 +2,8 @@ defmodule Module.Types.Helpers do
   # AST and enumeration helpers.
   @moduledoc false
 
+  ## AST helpers
+
   @doc """
   Guard function to check if an AST node is a variable.
   """
@@ -14,6 +16,72 @@ defmodule Module.Types.Helpers do
     end
   end
 
+  @doc """
+  Unpacks a list into head elements and tail.
+  """
+  def unpack_list([{:|, _, [head, tail]}], acc), do: {Enum.reverse([head | acc]), tail}
+  def unpack_list([head], acc), do: {Enum.reverse([head | acc]), []}
+  def unpack_list([head | tail], acc), do: unpack_list(tail, [head | acc])
+
+  @doc """
+  Unpacks a match into several matches.
+  """
+  def unpack_match({:=, _, [left, right]}, acc),
+    do: unpack_match(left, unpack_match(right, acc))
+
+  def unpack_match(node, acc),
+    do: [node | acc]
+
+  @doc """
+  Returns the AST metadata.
+  """
+  def get_meta({_, meta, _}), do: meta
+  def get_meta(_other), do: []
+
+  ## Traversal helpers
+
+  @doc """
+  Like `Enum.reduce/3` but only continues while `fun` returns `{:ok, acc}`
+  and stops on `{:error, reason}`.
+  """
+  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)
+
+      {:error, reason} ->
+        {:error, reason}
+    end
+  end
+
+  defp do_reduce_ok([], acc, _fun), do: {:ok, acc}
+
+  @doc """
+  Like `Enum.map_reduce/3` but only continues while `fun` returns `{:ok, elem, acc}`
+  and stops on `{:error, reason}`.
+  """
+  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}
+
+  ## Warnings
+
   @doc """
   Formatted hints in typing errors.
   """
@@ -50,6 +118,116 @@ defmodule Module.Types.Helpers do
 
   defp hint, do: :elixir_errors.prefix(:hint)
 
+  @doc """
+  Collect traces from variables in expression.
+  """
+  def collect_traces(expr, %{vars: vars}) do
+    {_, versions} =
+      Macro.prewalk(expr, %{}, fn
+        {var_name, meta, var_context}, versions when is_atom(var_name) and is_atom(var_context) ->
+          version = meta[:version]
+
+          case vars do
+            %{^version => %{off_traces: [_ | _] = off_traces, name: name, context: context}} ->
+              {:ok,
+               Map.put(versions, version, %{
+                 type: :variable,
+                 name: name,
+                 context: context,
+                 traces: collect_var_traces(off_traces)
+               })}
+
+            _ ->
+              {:ok, versions}
+          end
+
+        node, versions ->
+          {node, versions}
+      end)
+
+    versions
+    |> Map.values()
+    |> Enum.sort_by(& &1.name)
+  end
+
+  defp collect_var_traces(traces) do
+    traces
+    |> Enum.reject(fn {_expr, _file, type, _formatter} ->
+      Module.Types.Descr.dynamic_term_type?(type)
+    end)
+    |> case do
+      [] -> traces
+      filtered -> filtered
+    end
+    |> Enum.reverse()
+    |> Enum.map(fn {expr, file, type, formatter} ->
+      meta = get_meta(expr)
+
+      {formatted_expr, formatter_hints} =
+        case formatter do
+          :default -> {expr_to_string(expr), []}
+          formatter -> formatter.(expr)
+        end
+
+      %{
+        file: file,
+        meta: meta,
+        formatted_expr: formatted_expr,
+        formatted_hints: format_hints(formatter_hints ++ expr_hints(expr)),
+        formatted_type: Module.Types.Descr.to_quoted_string(type)
+      }
+    end)
+    |> Enum.sort_by(&{&1.meta[:line], &1.meta[:column]})
+  end
+
+  @doc """
+  Format previously collected traces.
+  """
+  def format_traces(traces) do
+    Enum.map(traces, &format_trace/1)
+  end
+
+  defp format_trace(%{type: :variable, name: name, context: context, traces: traces}) do
+    traces =
+      for trace <- traces do
+        location =
+          trace.file
+          |> Path.relative_to_cwd()
+          |> Exception.format_file_line(trace.meta[:line])
+          |> String.replace_suffix(":", "")
+
+        [
+          """
+
+              # type: #{indent(trace.formatted_type, 4)}
+              # from: #{location}
+              \
+          """,
+          indent(trace.formatted_expr, 4),
+          ?\n,
+          trace.formatted_hints
+        ]
+      end
+
+    type_or_types = pluralize(traces, "type", "types")
+    ["\nwhere #{format_var(name, context)} was given the #{type_or_types}:\n" | traces]
+  end
+
+  @doc """
+  Formats a var for pretty printing.
+  """
+  def format_var({var, _, context}), do: format_var(var, context)
+  def format_var(var, nil), do: "\"#{var}\""
+  def format_var(var, context), do: "\"#{var}\" (context #{inspect(context)})"
+
+  defp pluralize([_], singular, _plural), do: singular
+  defp pluralize(_, _singular, plural), do: plural
+
+  defp expr_hints({:<<>>, [inferred_bitstring_spec: true] ++ _meta, _}),
+    do: [:inferred_bitstring_spec]
+
+  defp expr_hints(_), do: []
+
   @doc """
   Converts the given expression to a string,
   translating inlined Erlang calls back to Elixir.
@@ -74,12 +252,6 @@ defmodule Module.Types.Helpers do
     end
   end
 
-  @doc """
-  Returns the AST metadata.
-  """
-  def get_meta({_, meta, _}), do: meta
-  def get_meta(_other), do: []
-
   @doc """
   Indents new lines.
   """
@@ -88,7 +260,7 @@ defmodule Module.Types.Helpers do
   end
 
   @doc """
-  Emits a warnings.
+  Emits a warning.
   """
   def warn(module, warning, meta, stack, context) do
     if Keyword.get(meta, :generated, false) do
@@ -99,44 +271,4 @@ defmodule Module.Types.Helpers do
       %{context | warnings: [{module, warning, location} | context.warnings]}
     end
   end
-
-  @doc """
-  Like `Enum.reduce/3` but only continues while `fun` returns `{:ok, acc}`
-  and stops on `{:error, reason}`.
-  """
-  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)
-
-      {:error, reason} ->
-        {:error, reason}
-    end
-  end
-
-  defp do_reduce_ok([], acc, _fun), do: {:ok, acc}
-
-  @doc """
-  Like `Enum.map_reduce/3` but only continues while `fun` returns `{:ok, elem, acc}`
-  and stops on `{:error, reason}`.
-  """
-  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/of.ex b/lib/elixir/lib/module/types/of.ex
index b97d3ab4f8b..6fb22053aea 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -29,7 +29,7 @@ defmodule Module.Types.Of do
   @doc """
   Refines the type of a variable.
   """
-  def refine_var(var, {type, expr}, formatter \\ :default, stack, context) do
+  def refine_var(var, type, expr, formatter \\ :default, stack, context) do
     {var_name, meta, var_context} = var
     version = Keyword.fetch!(meta, :version)
 
@@ -175,18 +175,9 @@ defmodule Module.Types.Of do
   # against the struct types.
   # TODO: Use the struct default values to define the default types.
   def struct(struct, args_types, default_handling, meta, stack, context) do
-    context = remote(struct, :__struct__, 0, meta, stack, context)
-
-    info =
-      struct.__info__(:struct) ||
-        raise "expected #{inspect(struct)} to return struct metadata, but got none"
-
+    {info, context} = struct_info(struct, meta, stack, context)
     term = term()
-
-    defaults =
-      for %{field: field} <- info, field != :__struct__ do
-        {field, term}
-      end
+    defaults = for %{field: field} <- info, do: {field, term}
 
     pairs =
       case default_handling do
@@ -198,6 +189,19 @@ defmodule Module.Types.Of do
     {:ok, dynamic(closed_map(pairs)), context}
   end
 
+  @doc """
+  Returns `__info__(:struct)` information about a struct.
+  """
+  def struct_info(struct, meta, stack, context) do
+    context = remote(struct, :__struct__, 0, meta, stack, context)
+
+    info =
+      struct.__info__(:struct) ||
+        raise "expected #{inspect(struct)} to return struct metadata, but got none"
+
+    {info, context}
+  end
+
   ## Binary
 
   @doc """
@@ -240,14 +244,21 @@ defmodule Module.Types.Of do
   end
 
   defp binary_segment({:"::", meta, [left, right]}, kind, args, stack, context) do
-    expected_type = specifier_type(kind, right)
+    type = specifier_type(kind, right)
     expr = {:<<>>, meta, args}
 
     result =
       case kind do
-        :pattern -> Module.Types.Pattern.of_pattern(left, {expected_type, expr}, stack, context)
-        :guard -> Module.Types.Pattern.of_guard(left, {expected_type, expr}, stack, context)
-        :expr -> Module.Types.Expr.of_expr(left, {expected_type, expr}, stack, context)
+        :match ->
+          Module.Types.Pattern.of_match_var(left, type, expr, stack, context)
+
+        :guard ->
+          Module.Types.Pattern.of_guard(left, type, expr, stack, context)
+
+        :expr ->
+          with {:ok, actual, context} <- Module.Types.Expr.of_expr(left, stack, context) do
+            intersect(actual, type, expr, stack, context)
+          end
       end
 
     with {:ok, _type, context} <- result do
@@ -256,10 +267,10 @@ defmodule Module.Types.Of do
   end
 
   defp specifier_type(kind, {:-, _, [left, _right]}), do: specifier_type(kind, left)
-  defp specifier_type(:pattern, {:utf8, _, _}), do: @integer
-  defp specifier_type(:pattern, {:utf16, _, _}), do: @integer
-  defp specifier_type(:pattern, {:utf32, _, _}), do: @integer
-  defp specifier_type(:pattern, {:float, _, _}), do: @float
+  defp specifier_type(:match, {:utf8, _, _}), do: @integer
+  defp specifier_type(:match, {:utf16, _, _}), do: @integer
+  defp specifier_type(:match, {:utf32, _, _}), do: @integer
+  defp specifier_type(:match, {:float, _, _}), do: @float
   defp specifier_type(_kind, {:float, _, _}), do: @integer_or_float
   defp specifier_type(_kind, {:utf8, _, _}), do: @integer_or_binary
   defp specifier_type(_kind, {:utf16, _, _}), do: @integer_or_binary
@@ -277,15 +288,17 @@ defmodule Module.Types.Of do
 
   defp specifier_size(:expr, {:size, _, [arg]}, expr, stack, context)
        when not is_integer(arg) do
-    case Module.Types.Expr.of_expr(arg, {integer(), expr}, stack, context) do
-      {:ok, _, context} -> context
+    with {:ok, actual, context} <- Module.Types.Expr.of_expr(arg, stack, context),
+         {:ok, _, context} <- intersect(actual, integer(), expr, stack, context) do
+      context
+    else
       {:error, context} -> context
     end
   end
 
   defp specifier_size(_pattern_or_guard, {:size, _, [arg]}, expr, stack, context)
        when not is_integer(arg) do
-    case Module.Types.Pattern.of_guard(arg, {integer(), expr}, stack, context) do
+    case Module.Types.Pattern.of_guard(arg, integer(), expr, stack, context) do
       {:ok, _, context} -> context
       {:error, context} -> context
     end
@@ -450,7 +463,7 @@ defmodule Module.Types.Of do
   @doc """
   Intersects two types and emit an incompatible warning if empty.
   """
-  def intersect(actual, {expected, expr}, stack, context) do
+  def intersect(actual, expected, expr, stack, context) do
     type = intersection(actual, expected)
 
     if empty?(type) do
@@ -477,101 +490,6 @@ defmodule Module.Types.Of do
     warn(__MODULE__, warning, meta, stack, context)
   end
 
-  ## Traces
-
-  def collect_traces(expr, %{vars: vars}) do
-    {_, versions} =
-      Macro.prewalk(expr, %{}, fn
-        {var_name, meta, var_context}, versions when is_atom(var_name) and is_atom(var_context) ->
-          version = meta[:version]
-
-          case vars do
-            %{^version => %{off_traces: [_ | _] = off_traces, name: name, context: context}} ->
-              {:ok,
-               Map.put(versions, version, %{
-                 type: :variable,
-                 name: name,
-                 context: context,
-                 traces: collect_var_traces(off_traces)
-               })}
-
-            _ ->
-              {:ok, versions}
-          end
-
-        node, versions ->
-          {node, versions}
-      end)
-
-    versions
-    |> Map.values()
-    |> Enum.sort_by(& &1.name)
-  end
-
-  defp collect_var_traces(traces) do
-    traces
-    |> Enum.reverse()
-    |> Enum.map(fn {expr, file, type, formatter} ->
-      meta = get_meta(expr)
-
-      {formatted_expr, formatter_hints} =
-        case formatter do
-          :default -> {expr_to_string(expr), []}
-          formatter -> formatter.(expr)
-        end
-
-      %{
-        file: file,
-        meta: meta,
-        formatted_expr: formatted_expr,
-        formatted_hints: format_hints(formatter_hints ++ expr_hints(expr)),
-        formatted_type: to_quoted_string(type)
-      }
-    end)
-  end
-
-  def format_traces(traces) do
-    Enum.map(traces, &format_trace/1)
-  end
-
-  defp format_trace(%{type: :variable, name: name, context: context, traces: traces}) do
-    traces =
-      for trace <- traces do
-        location =
-          trace.file
-          |> Path.relative_to_cwd()
-          |> Exception.format_file_line(trace.meta[:line])
-          |> String.replace_suffix(":", "")
-
-        [
-          """
-
-              # type: #{indent(trace.formatted_type, 4)}
-              # from: #{location}
-              \
-          """,
-          indent(trace.formatted_expr, 4),
-          ?\n,
-          trace.formatted_hints
-        ]
-      end
-
-    type_or_types = pluralize(traces, "type", "types")
-    ["\nwhere #{format_var(name, context)} was given the #{type_or_types}:\n" | traces]
-  end
-
-  defp format_var({var, _, context}), do: format_var(var, context)
-  defp format_var(var, nil), do: "\"#{var}\""
-  defp format_var(var, context), do: "\"#{var}\" (context #{inspect(context)})"
-
-  defp pluralize([_], singular, _plural), do: singular
-  defp pluralize(_, _singular, plural), do: plural
-
-  defp expr_hints({:<<>>, [inferred_bitstring_spec: true] ++ _meta, _}),
-    do: [:inferred_bitstring_spec]
-
-  defp expr_hints(_), do: []
-
   ## Warning formatting
 
   def format_diagnostic({:refine_var, old_type, new_type, var, context}) do
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 0701a2c107b..ef2786d0861 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -8,213 +8,556 @@ defmodule Module.Types.Pattern do
 
   @doc """
   Handles patterns and guards at once.
+
+  The algorithm works as follows:
+
+  1. First we traverse the patterns and build a pattern tree
+     (which tells how to compute the type of a pattern) alongside
+     the variable trees (which tells us how to compute the type
+     of a variable).
+
+  2. Then we traverse the pattern tree and compute the intersection
+     between the pattern and the expected types (which is currently dynamic).
+
+  3. Then we compute the values for each variable.
+
+  4. Then we refine the variables inside guards. If any variable
+     is refined, we restart at step 2.
+
   """
   # TODO: The expected types for patterns/guards must always given as arguments.
-  # Meanwhile, it is hardcoded to dynamic.
+  # TODO: Perform full guard inference
   def of_head(patterns, guards, meta, stack, context) do
-    pattern_stack = %{stack | meta: meta}
+    stack = %{stack | meta: meta}
+    dynamic = dynamic()
+    expected_types = Enum.map(patterns, fn _ -> dynamic end)
 
-    with {:ok, types, context} <-
-           map_reduce_ok(patterns, context, &of_pattern(&1, pattern_stack, &2)),
+    with {:ok, _trees, types, context} <-
+           of_pattern_args(patterns, expected_types, stack, context),
          {:ok, _, context} <-
-           map_reduce_ok(guards, context, &of_guard(&1, {@guard, &1}, stack, &2)),
-         do: {:ok, types, context}
+           map_reduce_ok(guards, context, &of_guard(&1, @guard, &1, stack, &2)) do
+      {:ok, types, context}
+    end
+  end
+
+  defp of_pattern_args([], [], _stack, context) do
+    {:ok, [], context}
+  end
+
+  defp of_pattern_args(patterns, expected_types, stack, context) do
+    context = %{context | pattern_info: {%{}, %{}}}
+    changed = :lists.seq(0, length(patterns) - 1)
+
+    with {:ok, trees, context} <-
+           of_pattern_args_index(patterns, expected_types, 0, [], stack, context),
+         {:ok, types, context} <-
+           of_pattern_recur(expected_types, changed, stack, context, fn types, changed, context ->
+             of_pattern_args_tree(trees, types, changed, 0, [], stack, context)
+           end) do
+      {:ok, trees, types, context}
+    end
+  end
+
+  defp of_pattern_args_index(
+         [pattern | tail],
+         [type | expected_types],
+         index,
+         acc,
+         stack,
+         context
+       ) do
+    with {:ok, tree, context} <-
+           of_pattern(pattern, [{:arg, index, type, pattern}], stack, context) do
+      acc = [{pattern, tree} | acc]
+      of_pattern_args_index(tail, expected_types, index + 1, acc, stack, context)
+    end
+  end
+
+  defp of_pattern_args_index([], [], _index, acc, _stack, context),
+    do: {:ok, Enum.reverse(acc), context}
+
+  defp of_pattern_args_tree(
+         [{pattern, tree} | tail],
+         [type | expected_types],
+         [index | changed],
+         index,
+         acc,
+         stack,
+         context
+       ) do
+    with {:ok, type, context} <- of_pattern_intersect(tree, type, pattern, stack, context) do
+      of_pattern_args_tree(tail, expected_types, changed, index + 1, [type | acc], stack, context)
+    end
+  end
+
+  defp of_pattern_args_tree(
+         [_ | tail],
+         [type | expected_types],
+         changed,
+         index,
+         acc,
+         stack,
+         context
+       ) do
+    of_pattern_args_tree(tail, expected_types, changed, index + 1, [type | acc], stack, context)
+  end
+
+  defp of_pattern_args_tree([], [], [], _index, acc, _stack, context) do
+    {:ok, Enum.reverse(acc), context}
   end
 
   @doc """
   Return the type and typing context of a pattern expression with
-  the given {expected, expr} pair or an error in case of a typing conflict.
+  the given expected and expr or an error in case of a typing conflict.
   """
-  def of_match(expr, expected_expr, stack, context) do
-    of_pattern(expr, expected_expr, stack, context)
+  def of_match(pattern, expected, expr, stack, context) do
+    context = %{context | pattern_info: {%{}, %{}}}
+
+    with {:ok, tree, context} <-
+           of_pattern(pattern, [{:arg, 0, expected, expr}], stack, context),
+         {:ok, [type], context} <-
+           of_pattern_recur([expected], [0], stack, context, fn [type], [0], context ->
+             with {:ok, type, context} <- of_pattern_intersect(tree, type, expr, stack, context) do
+               {:ok, [type], context}
+             end
+           end) do
+      {:ok, type, context}
+    end
   end
 
-  ## Patterns
-  # of_pattern is public as it is called recursively from Of.binary
+  defp of_pattern_recur(types, changed, stack, context, callback) do
+    %{pattern_info: {pattern_vars, pattern_args}} = context
+    context = %{context | pattern_info: nil}
+    pattern_vars = Map.to_list(pattern_vars)
+    of_pattern_recur(types, changed, pattern_vars, pattern_args, stack, context, callback)
+  end
+
+  defp of_pattern_recur(types, [], _vars, _args, _stack, context, _callback) do
+    {:ok, types, context}
+  end
+
+  defp of_pattern_recur(types, changed, vars, args, stack, context, callback) do
+    with {:ok, types, %{vars: context_vars} = context} <- callback.(types, changed, context) do
+      result =
+        reduce_ok(vars, {[], context}, fn {version, paths}, {changed, context} ->
+          current_type = context_vars[version][:type]
+
+          result =
+            reduce_ok(paths, {false, context}, fn
+              [var, {:arg, index, expected, expr} | path], {var_changed?, context} ->
+                actual = Enum.fetch!(types, index)
+
+                case of_pattern_var(path, actual) do
+                  {:ok, type} ->
+                    with {:ok, type, context} <- Of.refine_var(var, type, expr, stack, context) do
+                      {:ok, {var_changed? or current_type != type, context}}
+                    end
+
+                  :error ->
+                    {:error, Of.incompatible_warn(expr, expected, actual, stack, context)}
+                end
+            end)
+
+          with {:ok, {var_changed?, context}} <- result do
+            case var_changed? do
+              false ->
+                {:ok, {changed, context}}
+
+              true ->
+                case paths do
+                  # A single change, check if there are other variables in this index.
+                  [[_var, {:arg, index, _, _} | _]] ->
+                    case args do
+                      %{^index => true} -> {:ok, {[index | changed], context}}
+                      %{^index => false} -> {:ok, {changed, context}}
+                    end
+
+                  # Several changes, we have to recompute all indexes.
+                  _ ->
+                    var_changed = Enum.map(paths, fn [_var, {:arg, index, _, _} | _] -> index end)
+                    {:ok, {var_changed ++ changed, context}}
+                end
+            end
+          end
+        end)
 
-  # TODO: Remove the hardcoding of dynamic
-  # TODO: Remove this function
-  def of_pattern(expr, stack, context) do
-    of_pattern(expr, {dynamic(), expr}, stack, context)
+      with {:ok, {changed, context}} <- result do
+        of_pattern_recur(types, :lists.usort(changed), vars, args, stack, context, callback)
+      end
+    end
   end
 
-  # left = right
-  # TODO: Track variables and handle nesting
-  def of_pattern({:=, _meta, [left_expr, right_expr]}, {expected, expr}, stack, context) do
-    case {is_var(left_expr), is_var(right_expr)} do
-      {true, false} ->
-        with {:ok, type, context} <- of_pattern(right_expr, {expected, expr}, stack, context) do
-          of_pattern(left_expr, {type, expr}, stack, context)
-        end
+  defp of_pattern_intersect(tree, expected, expr, stack, context) do
+    actual = of_pattern_tree(tree, context)
 
-      {false, true} ->
-        with {:ok, type, context} <- of_pattern(left_expr, {expected, expr}, stack, context) do
-          of_pattern(right_expr, {type, expr}, stack, context)
-        end
+    case Of.intersect(actual, expected, expr, stack, context) do
+      {:ok, type, context} ->
+        {:ok, type, context}
 
-      {_, _} ->
-        with {:ok, _, context} <- of_pattern(left_expr, {expected, expr}, stack, context),
-             {:ok, _, context} <- of_pattern(right_expr, {expected, expr}, stack, context),
-             do: {:ok, dynamic(), context}
+      {:error, intersection_context} ->
+        if empty?(actual) do
+          meta = get_meta(expr) || stack.meta
+          {:error, warn(__MODULE__, {:invalid_pattern, expr, context}, meta, stack, context)}
+        else
+          {:error, intersection_context}
+        end
     end
   end
 
-  # %var{...} and %^var{...}
-  def of_pattern(
-        {:%, _meta, [struct_var, {:%{}, _meta2, args}]} = expr,
-        expected_expr,
-        stack,
-        context
-      )
-      when not is_atom(struct_var) do
-    with {:ok, struct_type, context} <-
-           of_struct_var(struct_var, {atom(), expr}, stack, context),
-         {:ok, map_type, context} <-
-           of_open_map(args, [__struct__: struct_type], expected_expr, stack, context),
-         {_, struct_type} = map_fetch(map_type, :__struct__),
-         {:ok, _struct_type, context} <-
-           of_pattern(struct_var, {struct_type, expr}, stack, context) do
-      {:ok, map_type, context}
+  defp of_pattern_var([], type) do
+    {:ok, type}
+  end
+
+  defp of_pattern_var([{:elem, index} | rest], type) when is_integer(index) do
+    case tuple_fetch(type, index) do
+      {_optional?, type} -> of_pattern_var(rest, type)
+      _reason -> :error
     end
   end
 
-  # %Struct{...}
-  def of_pattern({:%, _meta, [module, {:%{}, _, args}]} = expr, expected_expr, stack, context)
-      when is_atom(module) do
-    with {:ok, actual, context} <-
-           Of.struct(expr, module, args, :merge_defaults, stack, context, &of_pattern/3) do
-      Of.intersect(actual, expected_expr, stack, context)
+  defp of_pattern_var([{:key, field} | rest], type) when is_atom(field) do
+    case map_fetch(type, field) do
+      {_optional?, type} -> of_pattern_var(rest, type)
+      _reason -> :error
     end
   end
 
-  # %{...}
-  def of_pattern({:%{}, _meta, args}, expected_expr, stack, context) do
-    of_open_map(args, [], expected_expr, stack, context)
+  # TODO: Implement domain key types
+  defp of_pattern_var([{:key, _key} | rest], _type) do
+    of_pattern_var(rest, dynamic())
   end
 
-  # <<...>>>
-  def of_pattern({:<<>>, _meta, args}, _expected_expr, stack, context) do
-    case Of.binary(args, :pattern, stack, context) do
-      {:ok, context} -> {:ok, binary(), context}
-      {:error, context} -> {:error, context}
+  # TODO: This should intersect with the head of the list.
+  defp of_pattern_var([:head | rest], _type) do
+    of_pattern_var(rest, dynamic())
+  end
+
+  # TODO: This should intersect with the list itself and its tail.
+  defp of_pattern_var([:tail | rest], _type) do
+    of_pattern_var(rest, dynamic())
+  end
+
+  defp of_pattern_tree(descr, _context) when is_descr(descr),
+    do: descr
+
+  defp of_pattern_tree({:tuple, entries}, context) do
+    tuple(Enum.map(entries, &of_pattern_tree(&1, context)))
+  end
+
+  defp of_pattern_tree({:open_map, static, dynamic}, context) do
+    dynamic = Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, context)} end)
+    open_map(static ++ dynamic)
+  end
+
+  defp of_pattern_tree({:closed_map, static, dynamic}, context) do
+    dynamic = Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, context)} end)
+    closed_map(static ++ dynamic)
+  end
+
+  defp of_pattern_tree({:non_empty_list, [head | tail], suffix}, context) do
+    tail
+    |> Enum.reduce(of_pattern_tree(head, context), &union(of_pattern_tree(&1, context), &2))
+    |> non_empty_list(of_pattern_tree(suffix, context))
+  end
+
+  defp of_pattern_tree({:intersection, entries}, context) do
+    entries
+    |> Enum.map(&of_pattern_tree(&1, context))
+    |> Enum.reduce(&intersection/2)
+  end
+
+  defp of_pattern_tree({:var, version}, context) do
+    case context do
+      %{vars: %{^version => %{type: type}}} -> type
+      _ -> term()
     end
   end
 
-  # _
-  def of_pattern({:_, _meta, _var_context}, {expected, _expr}, _stack, context) do
+  @doc """
+  Function used to assign a type to a variable. Used by %struct{}
+  and binary patterns.
+  """
+  def of_match_var({:^, _, [var]}, expected, expr, stack, context) do
+    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+  end
+
+  def of_match_var({:_, _, _}, expected, _expr, _stack, context) do
     {:ok, expected, context}
   end
 
-  # var
-  def of_pattern(var, expected_expr, stack, context) when is_var(var) do
-    Of.refine_var(var, expected_expr, stack, context)
+  def of_match_var(var, expected, expr, stack, context) when is_var(var) do
+    Of.refine_var(var, expected, expr, stack, context)
   end
 
-  def of_pattern(expr, expected_expr, stack, context) do
-    of_shared(expr, expected_expr, stack, context, &of_pattern/4)
+  def of_match_var(ast, expected, expr, stack, context) do
+    of_match(ast, expected, expr, stack, context)
   end
 
-  # TODO: Track variables inside the map (mirror it with %var{} handling)
-  defp of_open_map(args, extra, expected_expr, stack, context) do
+  ## Patterns
+
+  # :atom
+  defp of_pattern(atom, _path, _stack, context) when is_atom(atom),
+    do: {:ok, atom([atom]), context}
+
+  # 12
+  defp of_pattern(literal, _path, _stack, context) when is_integer(literal),
+    do: {:ok, integer(), context}
+
+  # 1.2
+  defp of_pattern(literal, _path, _stack, context) when is_float(literal),
+    do: {:ok, float(), context}
+
+  # "..."
+  defp of_pattern(literal, _path, _stack, context) when is_binary(literal),
+    do: {:ok, binary(), context}
+
+  # []
+  defp of_pattern([], _path, _stack, context),
+    do: {:ok, empty_list(), context}
+
+  # [expr, ...]
+  defp of_pattern(list, path, stack, context) when is_list(list) do
+    {prefix, suffix} = unpack_list(list, [])
+    of_list(prefix, suffix, path, stack, context)
+  end
+
+  # {left, right}
+  defp of_pattern({left, right}, path, stack, context) do
+    of_tuple([left, right], path, stack, context)
+  end
+
+  # left = right
+  defp of_pattern({:=, _meta, [_, _]} = match, path, stack, context) do
     result =
-      reduce_ok(args, {[], context}, fn {key, value}, {fields, context} ->
-        with {:ok, value_type, context} <- of_pattern(value, stack, context) do
-          if is_atom(key) do
-            {:ok, {[{key, value_type} | fields], context}}
+      match
+      |> unpack_match([])
+      |> reduce_ok({[], [], context}, fn pattern, {static, dynamic, context} ->
+        with {:ok, type, context} <- of_pattern(pattern, path, stack, context) do
+          if is_descr(type) do
+            {:ok, {[type | static], dynamic, context}}
           else
-            {:ok, {fields, context}}
+            {:ok, {static, [type | dynamic], context}}
           end
         end
       end)
 
-    with {:ok, {fields, context}} <- result do
-      Of.intersect(open_map(extra ++ fields), expected_expr, stack, context)
+    with {:ok, acc} <- result do
+      case acc do
+        {[], dynamic, context} ->
+          {:ok, {:intersection, dynamic}, context}
+
+        {static, [], context} ->
+          {:ok, Enum.reduce(static, &intersection/2), context}
+
+        {static, dynamic, context} ->
+          {:ok, {:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}, context}
+      end
     end
   end
 
-  ## Guards
-  # of_guard is public as it is called recursively from Of.binary
+  # %Struct{...}
+  # TODO: Once we support typed structs, we need to type check them here.
+  defp of_pattern({:%, meta, [struct, {:%{}, _, args}]}, path, stack, context)
+       when is_atom(struct) do
+    {info, context} = Of.struct_info(struct, meta, stack, context)
+
+    result =
+      map_reduce_ok(args, context, fn {key, value}, context ->
+        with {:ok, value_type, context} <- of_pattern(value, [{:key, key} | path], stack, context) do
+          {:ok, {key, value_type}, context}
+        end
+      end)
+
+    with {:ok, pairs, context} <- result do
+      pairs = Map.new(pairs)
+      term = term()
+      static = [__struct__: atom([struct])]
+      dynamic = []
 
-  # TODO: Remove the hardcoding of dynamic
-  # TODO: Remove this function
-  def of_guard(expr, stack, context) do
-    of_guard(expr, {dynamic(), expr}, stack, context)
+      {static, dynamic} =
+        Enum.reduce(info, {static, dynamic}, fn %{field: field}, {static, dynamic} ->
+          case pairs do
+            %{^field => value_type} when is_descr(value_type) ->
+              {[{field, value_type} | static], dynamic}
+
+            %{^field => value_type} ->
+              {static, [{field, value_type} | dynamic]}
+
+            _ ->
+              {[{field, term} | static], dynamic}
+          end
+        end)
+
+      if dynamic == [] do
+        {:ok, closed_map(static), context}
+      else
+        {:ok, {:closed_map, static, dynamic}, context}
+      end
+    end
   end
 
-  # %Struct{...}
-  def of_guard({:%, _, [module, {:%{}, _, args}]} = expr, _expected_expr, stack, context)
-      when is_atom(module) do
-    Of.struct(expr, module, args, :skip_defaults, stack, context, &of_guard/3)
+  # %var{...}
+  defp of_pattern({:%, _, [{name, _, ctx} = var, {:%{}, _, args}]}, path, stack, context)
+       when is_atom(name) and is_atom(ctx) and name != :_ do
+    with {:ok, var, context} <- of_pattern(var, [{:key, :__struct__} | path], stack, context) do
+      dynamic = [__struct__: {:intersection, [atom(), var]}]
+      of_open_map(args, [], dynamic, path, stack, context)
+    end
+  end
+
+  # %^var{...} and %_{...}
+  defp of_pattern(
+         {:%, _meta, [var, {:%{}, _meta2, args}]} = expr,
+         path,
+         stack,
+         context
+       ) do
+    with {:ok, refined, context} <- of_match_var(var, atom(), expr, stack, context) do
+      of_open_map(args, [__struct__: refined], [], path, stack, context)
+    end
   end
 
   # %{...}
-  def of_guard({:%{}, _meta, args}, _expected_expr, stack, context) do
-    Of.closed_map(args, stack, context, &of_guard/3)
+  defp of_pattern({:%{}, _meta, args}, path, stack, context) do
+    of_open_map(args, [], [], path, stack, context)
   end
 
-  # <<>>
-  def of_guard({:<<>>, _meta, args}, _expected_expr, stack, context) do
-    case Of.binary(args, :guard, stack, context) do
-      {:ok, context} -> {:ok, binary(), context}
-      # It is safe to discard errors from binary inside expressions
-      {:error, context} -> {:ok, binary(), context}
+  # <<...>>>
+  defp of_pattern({:<<>>, _meta, args}, _path, stack, context) do
+    with {:ok, context} <- Of.binary(args, :match, stack, context) do
+      {:ok, binary(), context}
     end
   end
 
-  # var.field
-  def of_guard({{:., _, [callee, key]}, _, []} = expr, _expected_expr, stack, context)
-      when not is_atom(callee) do
-    with {:ok, type, context} <- of_guard(callee, stack, context) do
-      Of.map_fetch(expr, type, key, stack, context)
-    end
+  # left ++ right
+  defp of_pattern({{:., _meta1, [:erlang, :++]}, _meta2, [left, right]}, path, stack, context) do
+    of_list(left, right, path, stack, context)
   end
 
-  # Remote
-  def of_guard({{:., _, [:erlang, function]}, _, args} = expr, _expected_expr, stack, context)
-      when is_atom(function) do
-    with {:ok, args_type, context} <-
-           map_reduce_ok(args, context, &of_guard(&1, stack, &2)) do
-      Of.apply(:erlang, function, args_type, expr, stack, context)
-    end
+  # {...}
+  defp of_pattern({:{}, _meta, args}, path, stack, context) do
+    of_tuple(args, path, stack, context)
+  end
+
+  # ^var
+  defp of_pattern({:^, _meta, [var]}, _path, _stack, context) do
+    {:ok, Of.var(var, context), context}
+  end
+
+  # _
+  defp of_pattern({:_, _meta, _var_context}, _path, _stack, context) do
+    {:ok, term(), context}
   end
 
   # var
-  def of_guard(var, expected_expr, stack, context) when is_var(var) do
-    # TODO: This should be ver refinement once we have inference in guards
-    # Of.refine_var(var, expected_expr, stack, context)
-    Of.intersect(Of.var(var, context), expected_expr, stack, context)
+  defp of_pattern({name, meta, ctx} = var, reverse_path, _stack, context)
+       when is_atom(name) and is_atom(ctx) do
+    version = Keyword.fetch!(meta, :version)
+    [{:arg, arg, _type, _pattern} | _] = path = Enum.reverse(reverse_path)
+    {vars, args} = context.pattern_info
+
+    paths = [[var | path] | Map.get(vars, version, [])]
+    vars = Map.put(vars, version, paths)
+
+    # Our goal here is to compute if an argument has more than one variable.
+    args =
+      case args do
+        %{^arg => false} -> %{args | arg => true}
+        %{^arg => true} -> args
+        %{} -> Map.put(args, arg, false)
+      end
+
+    {:ok, {:var, version}, %{context | pattern_info: {vars, args}}}
   end
 
-  def of_guard(expr, expected_expr, stack, context) do
-    of_shared(expr, expected_expr, stack, context, &of_guard/4)
+  # TODO: Properly traverse domain keys
+  # TODO: Properly handle pin operator in keys
+  defp of_open_map(args, static, dynamic, path, stack, context) do
+    result =
+      reduce_ok(args, {static, dynamic, context}, fn {key, value}, {static, dynamic, context} ->
+        with {:ok, value_type, context} <- of_pattern(value, [{:key, key} | path], stack, context) do
+          cond do
+            # Only atom keys become part of the type because the other keys are divisible
+            not is_atom(key) ->
+              {:ok, {static, dynamic, context}}
+
+            is_descr(value_type) ->
+              {:ok, {[{key, value_type} | static], dynamic, context}}
+
+            true ->
+              {:ok, {static, [{key, value_type} | dynamic], context}}
+          end
+        end
+      end)
+
+    with {:ok, {static, dynamic, context}} <- result do
+      case dynamic do
+        [] -> {:ok, open_map(static), context}
+        _ -> {:ok, {:open_map, static, dynamic}, context}
+      end
+    end
   end
 
-  ## Helpers
+  defp of_tuple(args, path, stack, context) do
+    result =
+      reduce_ok(args, {0, true, [], context}, fn arg, {index, static?, acc, context} ->
+        with {:ok, type, context} <- of_pattern(arg, [{:elem, index} | path], stack, context) do
+          {:ok, {index + 1, static? and is_descr(type), [type | acc], context}}
+        end
+      end)
 
-  defp of_struct_var({:_, _, _}, {expected, _expr}, _stack, context) do
-    {:ok, expected, context}
+    with {:ok, {_index, static?, entries, context}} <- result do
+      case static? do
+        true -> {:ok, tuple(Enum.reverse(entries)), context}
+        false -> {:ok, {:tuple, Enum.reverse(entries)}, context}
+      end
+    end
   end
 
-  defp of_struct_var({:^, _, [var]}, expected_expr, stack, context) do
-    Of.intersect(Of.var(var, context), expected_expr, stack, context)
+  # [] ++ []
+  defp of_list([], [], _path, _stack, context) do
+    {:ok, empty_list(), context}
   end
 
-  defp of_struct_var({_name, meta, _ctx}, expected_expr, stack, context) do
-    version = Keyword.fetch!(meta, :version)
+  # [] ++ suffix
+  defp of_list([], suffix, path, stack, context) do
+    of_pattern(suffix, path, stack, context)
+  end
 
-    case context do
-      %{vars: %{^version => %{type: type}}} ->
-        Of.intersect(type, expected_expr, stack, context)
+  # [prefix1, prefix2, prefix3], [prefix1, prefix2 | suffix]
+  defp of_list(prefix, suffix, path, stack, context) do
+    with {:ok, suffix, context} <- of_pattern(suffix, [:tail | path], stack, context) do
+      result =
+        reduce_ok(prefix, {[], [], context}, fn arg, {static, dynamic, context} ->
+          with {:ok, type, context} <- of_pattern(arg, [:head | path], stack, context) do
+            if is_descr(type) do
+              {:ok, {[type | static], dynamic, context}}
+            else
+              {:ok, {static, [type | dynamic], context}}
+            end
+          end
+        end)
+
+      with {:ok, acc} <- result do
+        case acc do
+          {static, [], context} when is_descr(suffix) ->
+            {:ok, non_empty_list(Enum.reduce(static, &union/2), suffix), context}
 
-      %{} ->
-        {:ok, elem(expected_expr, 0), context}
+          {[], dynamic, context} ->
+            {:ok, {:non_empty_list, dynamic, suffix}, context}
+
+          {static, dynamic, context} ->
+            {:ok, {:non_empty_list, [Enum.reduce(static, &union/2) | dynamic], suffix}, context}
+        end
+      end
     end
   end
 
-  ## Shared
+  ## Guards
+  # This function is public as it is invoked from Of.binary/4.
 
   # :atom
-  defp of_shared(atom, {expected, expr}, stack, context, _fun) when is_atom(atom) do
+  def of_guard(atom, expected, expr, stack, context) when is_atom(atom) do
     if atom_type?(expected, atom) do
       {:ok, atom([atom]), context}
     else
@@ -223,7 +566,7 @@ defmodule Module.Types.Pattern do
   end
 
   # 12
-  defp of_shared(literal, {expected, expr}, stack, context, _fun) when is_integer(literal) do
+  def of_guard(literal, expected, expr, stack, context) when is_integer(literal) do
     if integer_type?(expected) do
       {:ok, integer(), context}
     else
@@ -232,7 +575,7 @@ defmodule Module.Types.Pattern do
   end
 
   # 1.2
-  defp of_shared(literal, {expected, expr}, stack, context, _fun) when is_float(literal) do
+  def of_guard(literal, expected, expr, stack, context) when is_float(literal) do
     if float_type?(expected) do
       {:ok, float(), context}
     else
@@ -241,7 +584,7 @@ defmodule Module.Types.Pattern do
   end
 
   # "..."
-  defp of_shared(literal, {expected, expr}, stack, context, _fun) when is_binary(literal) do
+  def of_guard(literal, expected, expr, stack, context) when is_binary(literal) do
     if binary_type?(expected) do
       {:ok, binary(), context}
     else
@@ -250,68 +593,105 @@ defmodule Module.Types.Pattern do
   end
 
   # []
-  defp of_shared([], _expected_expr, _stack, context, _fun) do
-    {:ok, empty_list(), context}
+  def of_guard([], expected, expr, stack, context) do
+    if empty_list_type?(expected) do
+      {:ok, empty_list(), context}
+    else
+      {:error, Of.incompatible_warn(expr, expected, empty_list(), stack, context)}
+    end
   end
 
   # [expr, ...]
-  defp of_shared(exprs, _expected_expr, stack, context, fun) when is_list(exprs) do
-    case map_reduce_ok(exprs, context, &fun.(&1, {dynamic(), &1}, stack, &2)) do
-      {:ok, _types, context} -> {:ok, non_empty_list(), context}
-      {:error, reason} -> {:error, reason}
+  def of_guard(list, _expected, expr, stack, context) when is_list(list) do
+    {prefix, suffix} = unpack_list(list, [])
+
+    with {:ok, prefix, context} <-
+           map_reduce_ok(prefix, context, &of_guard(&1, dynamic(), expr, stack, &2)),
+         {:ok, suffix, context} <- of_guard(suffix, dynamic(), expr, stack, context) do
+      {:ok, non_empty_list(Enum.reduce(prefix, &union/2), suffix), context}
     end
   end
 
   # {left, right}
-  defp of_shared({left, right}, expected_expr, stack, context, fun) do
-    of_shared({:{}, [], [left, right]}, expected_expr, stack, context, fun)
+  def of_guard({left, right}, expected, expr, stack, context) do
+    of_guard({:{}, [], [left, right]}, expected, expr, stack, context)
   end
 
-  # ^var
-  defp of_shared({:^, _meta, [var]}, expected_expr, stack, context, _fun) do
-    # This is by definition a variable defined outside of this pattern, so we don't track it.
-    Of.intersect(Of.var(var, context), expected_expr, stack, context)
+  # %Struct{...}
+  def of_guard({:%, _, [module, {:%{}, _, args}]} = struct, _expected, _expr, stack, context)
+      when is_atom(module) do
+    fun = &of_guard(&1, dynamic(), struct, &2, &3)
+    Of.struct(struct, module, args, :skip_defaults, stack, context, fun)
   end
 
-  # left | []
-  defp of_shared({:|, _meta, [left_expr, []]}, _expected_expr, stack, context, fun) do
-    fun.(left_expr, {dynamic(), left_expr}, stack, context)
+  # %{...}
+  def of_guard({:%{}, _meta, args}, _expected, expr, stack, context) do
+    Of.closed_map(args, stack, context, &of_guard(&1, dynamic(), expr, &2, &3))
   end
 
-  # left | right
-  defp of_shared({:|, _meta, [left_expr, right_expr]}, _expected_expr, stack, context, fun) do
-    case fun.(left_expr, {dynamic(), left_expr}, stack, context) do
-      {:ok, _, context} ->
-        fun.(right_expr, {dynamic(), right_expr}, stack, context)
+  # <<>>
+  def of_guard({:<<>>, _meta, args}, expected, expr, stack, context) do
+    if binary_type?(expected) do
+      with {:ok, context} <- Of.binary(args, :guard, stack, context) do
+        {:ok, binary(), context}
+      end
+    else
+      {:error, Of.incompatible_warn(expr, expected, binary(), stack, context)}
+    end
+  end
 
-      {:error, reason} ->
-        {:error, reason}
+  # ^var
+  def of_guard({:^, _meta, [var]}, expected, expr, stack, context) do
+    # This is by definition a variable defined outside of this pattern, so we don't track it.
+    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+  end
+
+  # {...}
+  def of_guard({:{}, _meta, args}, _expected, expr, stack, context) do
+    with {:ok, types, context} <-
+           map_reduce_ok(args, context, &of_guard(&1, dynamic(), expr, stack, &2)) do
+      {:ok, tuple(types), context}
     end
   end
 
-  # left ++ right
-  defp of_shared(
-         {{:., _meta1, [:erlang, :++]}, _meta2, [left_expr, right_expr]},
-         _expected_expr,
-         stack,
-         context,
-         fun
-       ) do
-    # The left side is always a list
-    with {:ok, _, context} <- fun.(left_expr, {dynamic(), left_expr}, stack, context),
-         {:ok, _, context} <- fun.(right_expr, {dynamic(), right_expr}, stack, context) do
-      # TODO: Both lists can be empty, so this may be an empty list,
-      # so we return dynamic for now.
-      {:ok, dynamic(), context}
+  # var.field
+  def of_guard({{:., _, [callee, key]}, _, []} = map_fetch, _expected, expr, stack, context)
+      when not is_atom(callee) do
+    with {:ok, type, context} <- of_guard(callee, dynamic(), expr, stack, context) do
+      Of.map_fetch(map_fetch, type, key, stack, context)
     end
   end
 
-  # {...}
-  # TODO: Implement this
-  defp of_shared({:{}, _meta, exprs}, _expected_expr, stack, context, fun) do
-    case map_reduce_ok(exprs, context, &fun.(&1, {dynamic(), &1}, stack, &2)) do
-      {:ok, types, context} -> {:ok, tuple(types), context}
-      {:error, reason} -> {:error, reason}
+  # Remote
+  def of_guard({{:., _, [:erlang, function]}, _, args}, _expected, expr, stack, context)
+      when is_atom(function) do
+    with {:ok, args_type, context} <-
+           map_reduce_ok(args, context, &of_guard(&1, dynamic(), expr, stack, &2)) do
+      Of.apply(:erlang, function, args_type, expr, stack, context)
     end
   end
+
+  # var
+  def of_guard(var, expected, expr, stack, context) when is_var(var) do
+    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+  end
+
+  ## Helpers
+
+  def format_diagnostic({:invalid_pattern, expr, context}) do
+    traces = collect_traces(expr, context)
+
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          the following pattern will never match:
+
+              #{expr_to_string(expr) |> indent(4)}
+          """,
+          format_traces(traces)
+        ])
+    }
+  end
 end
diff --git a/lib/elixir/src/elixir.hrl b/lib/elixir/src/elixir.hrl
index 15db26813e6..c66aa6d41e8 100644
--- a/lib/elixir/src/elixir.hrl
+++ b/lib/elixir/src/elixir.hrl
@@ -6,24 +6,58 @@
 -define(remote(Ann, Module, Function, Args), {call, Ann, {remote, Ann, {atom, Ann, Module}, {atom, Ann, Function}}, Args}).
 
 -record(elixir_ex, {
-  caller=false,            %% stores if __CALLER__ is allowed
-  %% TODO: Remove warn and everywhere it is set in v2.0
-  prematch=raise,          %% {Read, Counter, {bitsize, Original} | none} | warn | raise | pin
-  stacktrace=false,        %% stores if __STACKTRACE__ is allowed
-  unused={#{}, 0},         %% a map of unused vars and a version counter for vars
-  runtime_modules=[],      %% a list of modules defined in functions (runtime)
-  vars={#{}, false}        %% a tuple with maps of read and optional write current vars
+  %% Stores if __CALLER__ is allowed
+  caller=false,
+  %% Stores the variables available before a match.
+  %% May be one of:
+  %%
+  %%   * {Read, Cycle :: #{}, Meta :: Counter | {bitsize, Original}}
+  %%   * pin
+  %%   * none.
+  %%
+  %% The cycle is used to detect cyclic dependencies between
+  %% variables in a match.
+  %%
+  %% The bitsize is used when dealing with bitstring modifiers,
+  %% as they allow guards but also support the pin operator.
+  prematch=none,
+  %% Stores if __STACKTRACE__ is allowed
+  stacktrace=false,
+  %% A map of unused vars and a version counter for vars
+  unused={#{}, 0},
+  %% A list of modules defined in functions (runtime)
+  runtime_modules=[],
+  %% A tuple with maps of read and optional write current vars.
+  %% Read variables is all defined variables. Write variables
+  %% stores the variables that have been made available (written
+  %% to) but cannot be currently read. This is used in two occasions:
+  %%
+  %%   * To store variables graphs inside = in patterns
+  %%
+  %%   * To store variables defined inside calls. For example,
+  %%     if you write foo(a = 123), the value of `a` cannot be
+  %%     read in the following argument, only after the call
+  %%
+  vars={#{}, false}
 }).
 
 -record(elixir_erl, {
-  context=nil,             %% can be match, guards or nil
-  extra=nil,               %% extra information about the context, like pin_guard and map_key
-  caller=false,            %% when true, it means caller was invoked
-  var_names=#{},           %% maps of defined variables and their alias
-  extra_guards=[],         %% extra guards from args expansion
-  counter=#{},             %% a map counting the variables defined
-  expand_captures=false,   %% a boolean to control if captures should be expanded
-  stacktrace=nil           %% holds information about the stacktrace variable
+  %% Can be match, guards or nil
+  context=nil,
+  %% Extra information about the context, like pin_guard and map_key
+  extra=nil,
+  %% When true, it means caller was invoked
+  caller=false,
+  %% Maps of defined variables and their alias
+  var_names=#{},
+  %% Extra guards from args expansion
+  extra_guards=[],
+  %% A map counting the variables defined
+  counter=#{},
+  %% A boolean to control if captures should be expanded
+  expand_captures=false,
+  %% Holds information about the stacktrace variable
+  stacktrace=nil
 }).
 
 -record(elixir_tokenizer, {
diff --git a/lib/elixir/src/elixir_bitstring.erl b/lib/elixir/src/elixir_bitstring.erl
index e392ed68cad..4a92a9827a3 100644
--- a/lib/elixir/src/elixir_bitstring.erl
+++ b/lib/elixir/src/elixir_bitstring.erl
@@ -31,7 +31,7 @@ expand(Meta, Args, S, E, RequireSize) ->
 expand(_BitstrMeta, _Fun, [], Acc, S, E, Alignment, _RequireSize) ->
   {lists:reverse(Acc), Alignment, S, E};
 expand(BitstrMeta, Fun, [{'::', Meta, [Left, Right]} | T], Acc, S, E, Alignment, RequireSize) ->
-  {ELeft, {SL, OriginalS}, EL} = expand_expr(Meta, Left, Fun, S, E),
+  {ELeft, {SL, OriginalS}, EL} = expand_expr(Left, Fun, S, E),
 
   MatchOrRequireSize = RequireSize or is_match_size(T, EL),
   EType = expr_type(ELeft),
@@ -46,7 +46,7 @@ expand(BitstrMeta, Fun, [{'::', Meta, [Left, Right]} | T], Acc, S, E, Alignment,
   expand(BitstrMeta, Fun, T, EAcc, {SS, OriginalS}, ES, alignment(Alignment, EAlignment), RequireSize);
 expand(BitstrMeta, Fun, [H | T], Acc, S, E, Alignment, RequireSize) ->
   Meta = extract_meta(H, BitstrMeta),
-  {ELeft, {SS, OriginalS}, ES} = expand_expr(Meta, H, Fun, S, E),
+  {ELeft, {SS, OriginalS}, ES} = expand_expr(H, Fun, S, E),
 
   MatchOrRequireSize = RequireSize or is_match_size(T, ES),
   EType = expr_type(ELeft),
@@ -136,19 +136,14 @@ compute_alignment(_, _, _) -> unknown.
 %% If we are inside a match/guard, we inline interpolations explicitly,
 %% otherwise they are inlined by elixir_rewrite.erl.
 
-expand_expr(_Meta, {{'.', _, [Mod, to_string]}, _, [Arg]} = AST, Fun, S, #{context := Context} = E)
+expand_expr({{'.', _, [Mod, to_string]}, _, [Arg]} = AST, Fun, S, #{context := Context} = E)
     when Context /= nil, (Mod == 'Elixir.Kernel') orelse (Mod == 'Elixir.String.Chars') ->
   case Fun(Arg, S, E) of
     {EBin, SE, EE} when is_binary(EBin) -> {EBin, SE, EE};
     _ -> Fun(AST, S, E) % Let it raise
   end;
-expand_expr(Meta, Component, Fun, S, E) ->
-  case Fun(Component, S, E) of
-    {EComponent, _, ErrorE} when is_list(EComponent); is_atom(EComponent) ->
-      file_error(Meta, ErrorE, ?MODULE, {invalid_literal, EComponent});
-    {_, _, _} = Expanded ->
-      Expanded
-  end.
+expand_expr(Component, Fun, S, E) ->
+  Fun(Component, S, E).
 
 %% Expands and normalizes types of a bitstring.
 
@@ -273,9 +268,9 @@ expand_spec_arg(Expr, S, _OriginalS, E) when is_atom(Expr); is_integer(Expr) ->
   {Expr, S, E};
 expand_spec_arg(Expr, S, OriginalS, #{context := match} = E) ->
   %% We can only access variables that are either on prematch or not in original
-  #elixir_ex{prematch={PreRead, PreCounter, _} = OldPre} = S,
+  #elixir_ex{prematch={PreRead, PreCycle, _} = OldPre} = S,
   #elixir_ex{vars={OriginalRead, _}} = OriginalS,
-  NewPre = {PreRead, PreCounter, {bitsize, OriginalRead}},
+  NewPre = {PreRead, PreCycle, {bitsize, OriginalRead}},
   {EExpr, SE, EE} = elixir_expand:expand(Expr, S#elixir_ex{prematch=NewPre}, E#{context := guard}),
   {EExpr, SE#elixir_ex{prematch=OldPre}, EE#{context := match}};
 expand_spec_arg(Expr, S, OriginalS, E) ->
@@ -397,8 +392,6 @@ format_error(bittype_unit) ->
   "integer and float types require a size specifier if the unit specifier is given";
 format_error({bittype_float_size, Other}) ->
   io_lib:format("float requires size*unit to be 16, 32, or 64 (default), got: ~p", [Other]);
-format_error({invalid_literal, Literal}) ->
-  io_lib:format("invalid literal ~ts in <<>>", ['Elixir.Macro':to_string(Literal)]);
 format_error({undefined_bittype, Expr}) ->
   io_lib:format("unknown bitstring specifier: ~ts", ['Elixir.Macro':to_string(Expr)]);
 format_error({unknown_bittype, Name}) ->
diff --git a/lib/elixir/src/elixir_clauses.erl b/lib/elixir/src/elixir_clauses.erl
index b55f58e6bd8..40f191cd77a 100644
--- a/lib/elixir/src/elixir_clauses.erl
+++ b/lib/elixir/src/elixir_clauses.erl
@@ -1,26 +1,153 @@
 %% Handle code related to args, guard and -> matching for case,
 %% fn, receive and friends. try is handled in elixir_try.
 -module(elixir_clauses).
--export([match/5, clause/6, def/3, head/3,
+-export([parallel_match/4, match/6, clause/6, def/3, head/4,
          'case'/4, 'receive'/4, 'try'/4, 'cond'/4, with/4,
          format_error/1]).
 -import(elixir_errors, [file_error/4, file_warn/4]).
 -include("elixir.hrl").
 
-match(Fun, Expr, AfterS, _BeforeS, #{context := match} = E) ->
-  Fun(Expr, AfterS, E);
-match(Fun, Expr, AfterS, BeforeS, E) ->
+%% Deal with parallel matches and loops in variables
+
+parallel_match(Meta, Expr, S, #{context := match} = E) ->
+  #elixir_ex{vars={_Read, Write}} = S,
+  Matches = unpack_match(Expr, Meta, []),
+
+  {[{_, EHead} | ETail], EWrites, SM, EM} =
+    lists:foldl(fun({EMeta, Match}, {AccMatches, AccWrites, SI, EI}) ->
+      #elixir_ex{vars={Read, _Write}} = SI,
+      {EMatch, SM, EM} = elixir_expand:expand(Match, SI#elixir_ex{vars={Read, #{}}}, EI),
+      #elixir_ex{vars={_, EWrite}} = SM,
+      {[{EMeta, EMatch} | AccMatches], [EWrite | AccWrites], SM, EM}
+    end, {[], [], S, E}, Matches),
+
+  EMatch =
+    lists:foldl(fun({EMeta, EMatch}, Acc) ->
+      {'=', EMeta, [EMatch, Acc]}
+    end, EHead, ETail),
+
+  #elixir_ex{vars={VRead, _}, prematch={PRead, Cycles, PInfo}} = SM,
+  {PCycles, PWrites} = store_cycles(EWrites, Cycles, #{}),
+  VWrite = (Write /= false) andalso elixir_env:merge_vars(Write, PWrites),
+  {EMatch, SM#elixir_ex{vars={VRead, VWrite}, prematch={PRead, PCycles, PInfo}}, EM}.
+
+unpack_match({'=', Meta, [Left, Right]}, _Meta, Acc) ->
+  unpack_match(Left, Meta, unpack_match(Right, Meta, Acc));
+unpack_match(Node, Meta, Acc) ->
+  [{Meta, Node} | Acc].
+
+store_cycles([Write | Writes], {Cycles, SkipList}, Acc) ->
+  %% Compute the variables this parallel pattern depends on
+  DependsOn = lists:foldl(fun maps:merge/2, Acc, Writes),
+
+  %% For each variable on a sibling, we store it inside the graph (Cycles).
+  %% The graph will by definition have at least one degree cycles. We need
+  %% to find variables which depend on each other more than once (tagged as
+  %% error below) and also all second-degree (or later) cycles. In other
+  %% words, take this code:
+  %%
+  %%     {x = y, x = {:ok, y}} = expr()
+  %%
+  %% The first parallel match will say we store the following cycle:
+  %%
+  %%     #{{x,nil} => #{{y,nil} => 1}, {y,nil} => #{{x,nil} => 0}}
+  %%
+  %% That's why one degree cycles are allowed. However, once we go
+  %% over the next parallel pattern, we will have:
+  %%
+  %%     #{{x,nil} => #{{y,nil} => error}, {y,nil} => #{{x,nil} => error}}
+  %%
+  AccCycles =
+    maps:fold(fun(Pair, _, AccCycles) ->
+      maps:update_with(Pair, fun(Current) ->
+        maps:merge_with(fun(_, _, _) -> error end, Current, DependsOn)
+      end, DependsOn, AccCycles)
+    end, Cycles, Write),
+
+  %% The SkipList keeps variables that are seen as defined together by other
+  %% nodes. Those must be skipped on the graph traversal, as they will always
+  %% contain cycles between them. For example:
+  %%
+  %%     {{a} = b} = c = expr()
+  %%
+  %% In the example above, c sees "a" and "b" as defined together and therefore
+  %% one should not point to the other when looking for cycles.
+  AccSkipList =
+    case map_size(DependsOn) > 1 of
+      true -> [DependsOn | SkipList];
+      false -> SkipList
+    end,
+
+  store_cycles(Writes, {AccCycles, AccSkipList}, maps:merge(Acc, Write));
+store_cycles([], Cycles, Acc) ->
+  {Cycles, Acc}.
+
+validate_cycles({Cycles, SkipList}, Meta, Expr, E) ->
+  maps:fold(fun(Current, _DependsOn, Seen) ->
+    recur_cycles(Cycles, Current, root, Seen, SkipList, Meta, Expr, E)
+  end, #{}, Cycles).
+
+recur_cycles(Cycles, Current, Source, Seen, SkipList, Meta, Expr, E) ->
+  case is_map_key(Current, Seen) of
+    true ->
+      Seen;
+
+    false ->
+      case maps:get(Current, Cycles) of
+        #{Current := _} ->
+          file_error(Meta, E, ?MODULE, {recursive, [Current], Expr});
+
+        DependsOn ->
+          maps:fold(fun
+            (Key, error, _See) ->
+              file_error(Meta, E, ?MODULE, {recursive, [Current, Key], Expr});
+
+            %% Never go back to the node that we came from (as we can always one hop).
+            (Key, _, AccSeen) when Key =:= Source ->
+              AccSeen;
+
+            (Key, _, AccSeen) ->
+              Fun = fun
+                (#{Current := _, Key := _}) -> true;
+                (#{}) -> false
+              end,
+
+              case lists:any(Fun, SkipList) of
+                true ->
+                  AccSeen;
+
+                false when is_map_key(Key, Seen) ->
+                  file_error(Meta, E, ?MODULE, {recursive, [Current | maps:keys(Seen)], Expr});
+
+                false ->
+                  recur_cycles(Cycles, Key, Current, AccSeen, SkipList, Meta, Expr, E)
+              end
+          end, maps:put(Current, true, Seen), DependsOn)
+      end
+  end.
+
+%% Match
+
+match(Fun, Meta, Expr, AfterS, BeforeS, #{context := nil} = E) ->
   #elixir_ex{vars=Current, unused={_, Counter} = Unused} = AfterS,
   #elixir_ex{vars={Read, _}, prematch=Prematch} = BeforeS,
 
   CallS = BeforeS#elixir_ex{
-    prematch={Read, Counter, none},
+    prematch={Read, {#{}, []}, Counter},
     unused=Unused,
     vars=Current
   },
 
   CallE = E#{context := match},
-  {EExpr, #elixir_ex{vars=NewCurrent, unused=NewUnused}, EE} = Fun(Expr, CallS, CallE),
+  {EExpr, SE, EE} = Fun(Expr, CallS, CallE),
+
+  #elixir_ex{
+    vars=NewCurrent,
+    unused=NewUnused,
+    prematch={_, Cycles, _}
+  } = SE,
+
+  validate_cycles(Cycles, Meta, {match, Expr}, E),
 
   EndS = AfterS#elixir_ex{
     prematch=Prematch,
@@ -32,36 +159,31 @@ match(Fun, Expr, AfterS, BeforeS, E) ->
   {EExpr, EndS, EndE}.
 
 def({Meta, Args, Guards, Body}, S, E) ->
-  {EArgs, SA, EA} = elixir_expand:expand_args(Args, S#elixir_ex{prematch={#{}, 0, none}}, E#{context := match}),
-  {EGuards, SG, EG} = guard(Guards, SA#elixir_ex{prematch=raise}, EA#{context := guard}),
-  Prematch = elixir_config:get(on_undefined_variable),
-  {EBody, SB, EB} = elixir_expand:expand(Body, SG#elixir_ex{prematch=Prematch}, EG#{context := nil}),
+  {EArgs, SA, EA} = elixir_expand:expand_args(Args, S#elixir_ex{prematch={#{}, {#{}, []}, 0}}, E#{context := match}),
+  #elixir_ex{prematch={_, Cycles, _}} = SA,
+  validate_cycles(Cycles, Meta, {?key(E, function), Args}, E),
+  {EGuards, SG, EG} = guard(Guards, SA#elixir_ex{prematch=none}, EA#{context := guard}),
+  {EBody, SB, EB} = elixir_expand:expand(Body, SG, EG#{context := nil}),
   elixir_env:check_unused_vars(SB, EB),
   {Meta, EArgs, EGuards, EBody}.
 
-clause(Meta, Kind, Fun, {'->', ClauseMeta, [_, _]} = Clause, S, E) when is_function(Fun, 4) ->
-  clause(Meta, Kind, fun(X, SA, EA) -> Fun(ClauseMeta, X, SA, EA) end, Clause, S, E);
 clause(_Meta, _Kind, Fun, {'->', Meta, [Left, Right]}, S, E) ->
-  {ELeft, SL, EL}  = Fun(Left, S, E),
+  {ELeft, SL, EL}  = case is_function(Fun, 4) of
+    true -> Fun(Meta, Left, S, E);
+    false -> Fun(Left, S, E)
+  end,
   {ERight, SR, ER} = elixir_expand:expand(Right, SL, EL),
   {{'->', Meta, [ELeft, ERight]}, SR, ER};
 clause(Meta, Kind, _Fun, _, _, E) ->
   file_error(Meta, E, ?MODULE, {bad_or_missing_clauses, Kind}).
 
-head([{'when', Meta, [_ | _] = All}], S, E) ->
+head(Meta, [{'when', WhenMeta, [_ | _] = All}], S, E) ->
   {Args, Guard} = elixir_utils:split_last(All),
-  Prematch = S#elixir_ex.prematch,
-
-  {{EArgs, EGuard}, SG, EG} =
-    match(fun(ok, SM, EM) ->
-      {EArgs, SA, EA} = elixir_expand:expand_args(Args, SM, EM),
-      {EGuard, SG, EG} = guard(Guard, SA#elixir_ex{prematch=Prematch}, EA#{context := guard}),
-      {{EArgs, EGuard}, SG, EG}
-    end, ok, S, S, E),
-
-  {[{'when', Meta, EArgs ++ [EGuard]}], SG, EG};
-head(Args, S, E) ->
-  match(fun elixir_expand:expand_args/3, Args, S, S, E).
+  {EArgs, SA, EA} = match(fun elixir_expand:expand_args/3, Meta, Args, S, S, E),
+  {EGuard, SG, EG} = guard(Guard, SA, EA#{context := guard}),
+  {[{'when', WhenMeta, EArgs ++ [EGuard]}], SG, EG#{context := nil}};
+head(Meta, Args, S, E) ->
+  match(fun elixir_expand:expand_args/3, Meta, Args, S, S, E).
 
 guard({'when', Meta, [Left, Right]}, S, E) ->
   {ELeft, SL, EL}  = guard(Left, S, E),
@@ -100,7 +222,7 @@ warn_zero_length_guard(_, _) ->
   {Case, SA, E}.
 
 expand_case(Meta, {'do', _} = Do, S, E) ->
-  Fun = expand_head(Meta, 'case', 'do'),
+  Fun = expand_head('case', 'do'),
   expand_clauses(Meta, 'case', Fun, Do, S, E);
 expand_case(Meta, {Key, _}, _S, E) ->
   file_error(Meta, E, ?MODULE, {unexpected_option, 'case', Key}).
@@ -142,7 +264,7 @@ expand_cond(Meta, {Key, _}, _S, E) ->
 expand_receive(_Meta, {'do', {'__block__', _, []}} = Do, S, _E) ->
   {Do, S};
 expand_receive(Meta, {'do', _} = Do, S, E) ->
-  Fun = expand_head(Meta, 'receive', 'do'),
+  Fun = expand_head('receive', 'do'),
   expand_clauses(Meta, 'receive', Fun, Do, S, E);
 expand_receive(Meta, {'after', [_]} = After, S, E) ->
   Fun = expand_one(Meta, 'receive', 'after', fun elixir_expand:expand_args/3),
@@ -173,7 +295,7 @@ with(Meta, Args, S, E) ->
 expand_with({'<-', Meta, [Left, Right]}, {S, E, HasMatch}) ->
   {ERight, SR, ER} = elixir_expand:expand(Right, S, E),
   SM = elixir_env:reset_read(SR, S),
-  {[ELeft], SL, EL} = head([Left], SM, ER),
+  {[ELeft], SL, EL} = head(Meta, [Left], SM, ER),
   NewHasMatch =
     case ELeft of
       {Var, _, Ctx} when is_atom(Var), is_atom(Ctx) -> HasMatch;
@@ -200,7 +322,7 @@ expand_with_else(Meta, Opts, S, E, HasMatch) ->
         HasMatch -> ok;
         true -> file_warn(Meta, ?key(E, file), ?MODULE, unmatchable_else_in_with)
       end,
-      Fun = expand_head(Meta, 'with', 'else'),
+      Fun = expand_head('with', 'else'),
       {EPair, SE} = expand_clauses(Meta, 'with', Fun, Pair, S, E),
       {[EPair], RestOpts, SE};
     false ->
@@ -242,7 +364,7 @@ expand_try(_Meta, {'after', Expr}, S, E) ->
   {EExpr, SE, EE} = elixir_expand:expand(Expr, elixir_env:reset_unused_vars(S), E),
   {{'after', EExpr}, elixir_env:merge_and_check_unused_vars(SE, S, EE)};
 expand_try(Meta, {'else', _} = Else, S, E) ->
-  Fun = expand_head(Meta, 'try', 'else'),
+  Fun = expand_head('try', 'else'),
   expand_clauses(Meta, 'try', Fun, Else, S, E);
 expand_try(Meta, {'catch', _} = Catch, S, E) ->
   expand_clauses_with_stacktrace(Meta, fun expand_catch/4, Catch, S, E);
@@ -260,10 +382,10 @@ expand_clauses_with_stacktrace(Meta, Fun, Clauses, S, E) ->
 expand_catch(Meta, [{'when', _, [_, _, _, _ | _]}], _, E) ->
   Error = {wrong_number_of_args_for_clause, "one or two args", origin(Meta, 'try'), 'catch'},
   file_error(Meta, E, ?MODULE, Error);
-expand_catch(_Meta, [_] = Args, S, E) ->
-  head(Args, S, E);
-expand_catch(_Meta, [_, _] = Args, S, E) ->
-  head(Args, S, E);
+expand_catch(Meta, [_] = Args, S, E) ->
+  head(Meta, Args, S, E);
+expand_catch(Meta, [_, _] = Args, S, E) ->
+  head(Meta, Args, S, E);
 expand_catch(Meta, _, _, E) ->
   Error = {wrong_number_of_args_for_clause, "one or two args", origin(Meta, 'try'), 'catch'},
   file_error(Meta, E, ?MODULE, Error).
@@ -280,21 +402,21 @@ expand_rescue(Meta, _, _, E) ->
   file_error(Meta, E, ?MODULE, Error).
 
 %% rescue var
-expand_rescue({Name, _, Atom} = Var, S, E) when is_atom(Name), is_atom(Atom) ->
-  match(fun elixir_expand:expand/3, Var, S, S, E);
+expand_rescue({Name, Meta, Atom} = Var, S, E) when is_atom(Name), is_atom(Atom) ->
+  match(fun elixir_expand:expand/3, Meta, Var, S, S, E);
 
 %% rescue Alias => _ in [Alias]
 expand_rescue({'__aliases__', _, [_ | _]} = Alias, S, E) ->
   expand_rescue({in, [], [{'_', [], ?key(E, module)}, Alias]}, S, E);
 
 %% rescue var in _
-expand_rescue({in, _, [{Name, _, VarContext} = Var, {'_', _, UnderscoreContext}]}, S, E)
+expand_rescue({in, _, [{Name, Meta, VarContext} = Var, {'_', _, UnderscoreContext}]}, S, E)
     when is_atom(Name), is_atom(VarContext), is_atom(UnderscoreContext) ->
-  match(fun elixir_expand:expand/3, Var, S, S, E);
+  match(fun elixir_expand:expand/3, Meta, Var, S, S, E);
 
 %% rescue var in (list() or atom())
 expand_rescue({in, Meta, [Left, Right]}, S, E) ->
-  {ELeft, SL, EL}  = match(fun elixir_expand:expand/3, Left, S, S, E),
+  {ELeft, SL, EL}  = match(fun elixir_expand:expand/3, Meta, Left, S, S, E),
   {ERight, SR, ER} = elixir_expand:expand(Right, SL, EL),
 
   case ELeft of
@@ -325,13 +447,13 @@ normalize_rescue(Other) ->
 
 %% Expansion helpers
 
-expand_head(Meta, Kind, Key) ->
+expand_head(Kind, Key) ->
   fun
-    ([{'when', _, [_, _, _ | _]}], _, E) ->
+    (Meta, [{'when', _, [_, _, _ | _]}], _, E) ->
       file_error(Meta, E, ?MODULE, {wrong_number_of_args_for_clause, "one argument", Kind, Key});
-    ([_] = Args, S, E) ->
-      head(Args, S, E);
-    (_, _, E) ->
+    (Meta, [_] = Args, S, E) ->
+      head(Meta, Args, S, E);
+    (Meta, _, _, E) ->
       file_error(Meta, E, ?MODULE, {wrong_number_of_args_for_clause, "one argument", Kind, Key})
   end.
 
@@ -385,6 +507,29 @@ origin(Meta, Default) ->
     false -> Default
   end.
 
+format_error({recursive, Vars, TypeExpr}) ->
+  Code =
+    case TypeExpr of
+      {match, Expr} -> 'Elixir.Macro':to_string(Expr);
+      {{Name, _Arity}, Args} -> 'Elixir.Macro':to_string({Name, [], Args})
+    end,
+
+  Message =
+    case lists:map(fun({Name, Context}) -> elixir_utils:var_info(Name, Context) end, lists:sort(Vars)) of
+      [Var] ->
+        io_lib:format("the variable ~ts is defined in function of itself", [Var]);
+      [Var1, Var2] ->
+        io_lib:format("the variable ~ts is defined recursively in function of ~ts", [Var1, Var2]);
+      [Head | Tail] ->
+        List = lists:foldl(fun(X, Acc) -> [Acc, $,, $\s, X] end, Head, Tail),
+        io_lib:format("the following variables form a cycle: ~ts", [List])
+    end,
+
+  io_lib:format(
+    "recursive variable definition in patterns:~n~n    ~ts~n~n~ts",
+    [Code, Message]
+  );
+
 format_error({bad_or_missing_clauses, {Kind, Key}}) ->
   io_lib:format("expected -> clauses for :~ts in \"~ts\"", [Key, Kind]);
 format_error({bad_or_missing_clauses, Kind}) ->
diff --git a/lib/elixir/src/elixir_env.erl b/lib/elixir/src/elixir_env.erl
index 372303199fc..ff24f6ef3df 100644
--- a/lib/elixir/src/elixir_env.erl
+++ b/lib/elixir/src/elixir_env.erl
@@ -1,10 +1,10 @@
 -module(elixir_env).
 -include("elixir.hrl").
 -export([
-  new/0, to_caller/1, with_vars/2, reset_vars/1, env_to_ex/1,
+  new/0, to_caller/1, merge_vars/2, with_vars/2, reset_vars/1, env_to_ex/1,
   reset_unused_vars/1, check_unused_vars/2, merge_and_check_unused_vars/3, calculate_span/2,
   trace/2, format_error/1,
-  reset_read/2, prepare_write/1, close_write/2
+  reset_read/2, prepare_write/1, prepare_write/2, close_write/2
 ]).
 
 new() ->
@@ -50,13 +50,12 @@ reset_vars(Env) ->
 env_to_ex(#{context := match, versioned_vars := Vars}) ->
   Counter = map_size(Vars),
   #elixir_ex{
-    prematch={Vars, Counter, none},
+    prematch={Vars, {#{}, []}, Counter},
     vars={Vars, false},
     unused={#{}, Counter}
   };
 env_to_ex(#{versioned_vars := Vars}) ->
   #elixir_ex{
-    prematch=elixir_config:get(on_undefined_variable),
     vars={Vars, false},
     unused={#{}, map_size(Vars)}
   }.
@@ -66,6 +65,11 @@ env_to_ex(#{versioned_vars := Vars}) ->
 reset_read(#elixir_ex{vars={_, Write}} = S, #elixir_ex{vars={Read, _}}) ->
   S#elixir_ex{vars={Read, Write}}.
 
+prepare_write(S, #{context := nil}) ->
+  prepare_write(S);
+prepare_write(S, _) ->
+  S.
+
 prepare_write(#elixir_ex{vars={Read, _}} = S) ->
   S#elixir_ex{vars={Read, Read}}.
 
diff --git a/lib/elixir/src/elixir_expand.erl b/lib/elixir/src/elixir_expand.erl
index df555f96a55..0319225d82c 100644
--- a/lib/elixir/src/elixir_expand.erl
+++ b/lib/elixir/src/elixir_expand.erl
@@ -5,11 +5,13 @@
 
 %% =
 
+expand({'=', Meta, [_, _]} = Expr, S, #{context := match} = E) ->
+  elixir_clauses:parallel_match(Meta, Expr, S, E);
+
 expand({'=', Meta, [Left, Right]}, S, E) ->
   assert_no_guard_scope(Meta, "=", S, E),
   {ERight, SR, ER} = expand(Right, S, E),
-  {ELeft, SL, EL} = elixir_clauses:match(fun expand/3, Left, SR, S, ER),
-  refute_parallel_bitstring_match(ELeft, ERight, E, ?key(E, context) == match),
+  {ELeft, SL, EL} = elixir_clauses:match(fun expand/3, Meta, Left, SR, S, ER),
   {{'=', Meta, [ELeft, ERight]}, SL, EL};
 
 %% Literal operators
@@ -329,7 +331,7 @@ expand({'_', Meta, Kind} = Var, S, #{context := Context} = E) when is_atom(Kind)
 
 expand({Name, Meta, Kind}, S, #{context := match} = E) when is_atom(Name), is_atom(Kind) ->
   #elixir_ex{
-    prematch={_, PrematchVersion, _},
+    prematch={_, _, PrematchVersion},
     unused={Unused, Version},
     vars={Read, Write}
   } = S,
@@ -341,8 +343,9 @@ expand({Name, Meta, Kind}, S, #{context := match} = E) when is_atom(Name), is_at
     #{Pair := VarVersion} when VarVersion >= PrematchVersion ->
       maybe_warn_underscored_var_repeat(Meta, Name, Kind, E),
       NewUnused = var_used(Pair, Meta, VarVersion, Unused),
+      NewWrite = (Write /= false) andalso Write#{Pair => Version},
       Var = {Name, [{version, VarVersion} | Meta], Kind},
-      {Var, S#elixir_ex{unused={NewUnused, Version}}, E};
+      {Var, S#elixir_ex{vars={Read, NewWrite}, unused={NewUnused, Version}}, E};
 
     %% Variable is being overridden now
     #{Pair := _} ->
@@ -369,17 +372,20 @@ expand({Name, Meta, Kind}, S, E) when is_atom(Name), is_atom(Kind) ->
     case Read of
       #{Pair := CurrentVersion} ->
         case Prematch of
-          {Pre, _Counter, {bitsize, Original}} ->
+          {Pre, _Cycle, {bitsize, Original}} ->
             if
               map_get(Pair, Pre) /= CurrentVersion ->
                 {ok, CurrentVersion};
+
               is_map_key(Pair, Pre) ->
                 %% TODO: Enable this warning on Elixir v1.19
                 %% TODO: Remove me on Elixir 2.0
                 %% elixir_errors:file_warn(Meta, E, ?MODULE, {unpinned_bitsize_var, Name, Kind}),
                 {ok, CurrentVersion};
+
               not is_map_key(Pair, Original) ->
                 {ok, CurrentVersion};
+
               true ->
                 raise
             end;
@@ -389,7 +395,12 @@ expand({Name, Meta, Kind}, S, E) when is_atom(Name), is_atom(Kind) ->
         end;
 
       _ ->
-        Prematch
+        case E of
+          #{context := guard} -> raise;
+          #{} when S#elixir_ex.prematch =:= pin -> pin;
+          %% TODO: Remove fallback on on_undefined_variable
+          _ -> elixir_config:get(on_undefined_variable)
+        end
     end,
 
   case Result of
@@ -417,7 +428,7 @@ expand({Name, Meta, Kind}, S, E) when is_atom(Name), is_atom(Kind) ->
           function_error(Meta, E, ?MODULE, {undefined_var_pin, Name, Kind}),
           {{Name, Meta, Kind}, S, E};
 
-        _ ->
+        _ when Error == raise ->
           SpanMeta =  elixir_env:calculate_span(Meta, Name),
           function_error(SpanMeta, E, ?MODULE, {undefined_var, Name, Kind}),
           {{Name, SpanMeta, Kind}, S, E}
@@ -431,7 +442,7 @@ expand({Atom, Meta, Args}, S, E) when is_atom(Atom), is_list(Meta), is_list(Args
 
   elixir_dispatch:dispatch_import(Meta, Atom, Args, S, E, fun
     ({AR, AF}) ->
-      expand_remote(AR, Meta, AF, Meta, Args, S, elixir_env:prepare_write(S), E);
+      expand_remote(AR, Meta, AF, Meta, Args, S, elixir_env:prepare_write(S, E), E);
 
     (local) ->
       expand_local(Meta, Atom, Args, S, E)
@@ -441,7 +452,7 @@ expand({Atom, Meta, Args}, S, E) when is_atom(Atom), is_list(Meta), is_list(Args
 
 expand({{'.', DotMeta, [Left, Right]}, Meta, Args}, S, E)
     when (is_tuple(Left) orelse is_atom(Left)), is_atom(Right), is_list(Meta), is_list(Args) ->
-  {ELeft, SL, EL} = expand(Left, elixir_env:prepare_write(S), E),
+  {ELeft, SL, EL} = expand(Left, elixir_env:prepare_write(S, E), E),
 
   elixir_dispatch:dispatch_require(Meta, ELeft, Right, Args, S, EL, fun(AR, AF) ->
     expand_remote(AR, DotMeta, AF, Meta, Args, S, SL, EL)
@@ -700,9 +711,6 @@ maybe_warn_deprecated_super_in_gen_server_callback(Meta, Function, SuperMeta, E)
       ok
   end.
 
-context_info(Kind) when Kind == nil; is_integer(Kind) -> "";
-context_info(Kind) -> io_lib:format(" (context ~ts)", [elixir_aliases:inspect(Kind)]).
-
 should_warn(Meta) ->
   lists:keyfind(generated, 1, Meta) /= {generated, true}.
 
@@ -819,7 +827,7 @@ expand_for_do_block(Meta, [{'->', _, _} | _] = Clauses, S, E, {reduce, _}) ->
       SReset = elixir_env:reset_unused_vars(SA),
 
       {EClause, SAcc, EAcc} =
-        elixir_clauses:clause(Meta, fn, fun elixir_clauses:head/3, Clause, SReset, E),
+        elixir_clauses:clause(Meta, fn, fun elixir_clauses:head/4, Clause, SReset, E),
 
       {EClause, elixir_env:merge_and_check_unused_vars(SAcc, SA, EAcc)};
 
@@ -859,7 +867,7 @@ expand_local(Meta, Name, Args, S, #{module := Module, function := Function, cont
       module_error(Meta, E, ?MODULE, {invalid_local_invocation, "match", {Name, Meta, Args}});
 
     guard ->
-      module_error(Meta, E, ?MODULE, {invalid_local_invocation, guard_context(S), {Name, Meta, Args}});
+      module_error(Meta, E, ?MODULE, {invalid_local_invocation, elixir_utils:guard_info(S), {Name, Meta, Args}});
 
     nil ->
       Arity = length(Args),
@@ -879,20 +887,27 @@ expand_remote(Receiver, DotMeta, Right, Meta, Args, S, SL, #{context := Context}
   if
     Context =:= guard, is_tuple(Receiver) ->
       (lists:keyfind(no_parens, 1, Meta) /= {no_parens, true}) andalso
-        function_error(Meta, E, ?MODULE, {parens_map_lookup, Receiver, Right, guard_context(S)}),
+        function_error(Meta, E, ?MODULE, {parens_map_lookup, Receiver, Right, elixir_utils:guard_info(S)}),
 
       {{{'.', DotMeta, [Receiver, Right]}, Meta, []}, SL, E};
 
-    true ->
+    Context =:= nil ->
       AttachedMeta = attach_runtime_module(Receiver, Meta, S, E),
       {EArgs, {SA, _}, EA} = mapfold(fun expand_arg/3, {SL, S}, E, Args),
+      Rewritten = elixir_rewrite:rewrite(Receiver, DotMeta, Right, AttachedMeta, EArgs),
+      {Rewritten, elixir_env:close_write(SA, S), EA};
 
-      case rewrite(Context, Receiver, DotMeta, Right, AttachedMeta, EArgs, S) of
-        {ok, Rewritten} ->
-          {Rewritten, elixir_env:close_write(SA, S), EA};
+    true ->
+      case {Receiver, Right, Args} of
+        {erlang, '+', [Arg]} when is_number(Arg) -> {+Arg, SL, E};
+        {erlang, '-', [Arg]} when is_number(Arg) -> {-Arg, SL, E};
+        _ ->
+          {EArgs, SA, EA} = mapfold(fun expand/3, SL, E, Args),
 
-        {error, Error} ->
-          file_error(Meta, E, elixir_rewrite, Error)
+          case elixir_rewrite:Context(Receiver, DotMeta, Right, Meta, EArgs, S) of
+            {ok, Rewritten} -> {Rewritten, SA, EA};
+            {error, Error} -> file_error(Meta, E, elixir_rewrite, Error)
+          end
       end
   end;
 expand_remote(Receiver, DotMeta, Right, Meta, Args, _, _, E) ->
@@ -905,16 +920,6 @@ attach_runtime_module(Receiver, Meta, S, _E) ->
     false -> Meta
   end.
 
-% Signed numbers can be rewritten no matter the context
-rewrite(_, erlang, _, '+', _, [Arg], _S) when is_number(Arg) -> {ok, Arg};
-rewrite(_, erlang, _, '-', _, [Arg], _S) when is_number(Arg) -> {ok, -Arg};
-rewrite(match, Receiver, DotMeta, Right, Meta, EArgs, _S) ->
-  elixir_rewrite:match_rewrite(Receiver, DotMeta, Right, Meta, EArgs);
-rewrite(guard, Receiver, DotMeta, Right, Meta, EArgs, S) ->
-  elixir_rewrite:guard_rewrite(Receiver, DotMeta, Right, Meta, EArgs, guard_context(S));
-rewrite(_, Receiver, DotMeta, Right, Meta, EArgs, _S) ->
-  {ok, elixir_rewrite:rewrite(Receiver, DotMeta, Right, Meta, EArgs)}.
-
 %% Lexical helpers
 
 expand_opts(Meta, Kind, Allowed, Opts, S, E) ->
@@ -986,7 +991,7 @@ expand_aliases({'__aliases__', Meta, List} = Alias, S, E, Report) ->
 expand_for_generator({'<-', Meta, [Left, Right]}, S, E) ->
   {ERight, SR, ER} = expand(Right, S, E),
   SM = elixir_env:reset_read(SR, S),
-  {[ELeft], SL, EL} = elixir_clauses:head([Left], SM, ER),
+  {[ELeft], SL, EL} = elixir_clauses:head(Meta, [Left], SM, ER),
   {{'<-', Meta, [ELeft, ERight]}, SL, EL};
 expand_for_generator({'<<>>', Meta, Args} = X, S, E) when is_list(Args) ->
   case elixir_utils:split_last(Args) of
@@ -995,7 +1000,7 @@ expand_for_generator({'<<>>', Meta, Args} = X, S, E) when is_list(Args) ->
       SM = elixir_env:reset_read(SR, S),
       {ELeft, SL, EL} = elixir_clauses:match(fun(BArg, BS, BE) ->
         elixir_bitstring:expand(Meta, BArg, BS, BE, true)
-      end, LeftStart ++ [LeftEnd], SM, SM, ER),
+      end, Meta, LeftStart ++ [LeftEnd], SM, SM, ER),
       {{'<<>>', Meta, [{'<-', OpMeta, [ELeft, ERight]}]}, SL, EL};
     _ ->
       expand(X, S, E)
@@ -1012,45 +1017,6 @@ assert_generator_start(Meta, _, E) ->
 
 %% Assertions
 
-refute_parallel_bitstring_match({'<<>>', _, _}, {'<<>>', Meta, _} = Arg, E, true) ->
-  file_error(Meta, E, ?MODULE, {parallel_bitstring_match, Arg});
-refute_parallel_bitstring_match(Left, {'=', _Meta, [MatchLeft, MatchRight]}, E, Parallel) ->
-  refute_parallel_bitstring_match(Left, MatchLeft, E, true),
-  refute_parallel_bitstring_match(Left, MatchRight, E, Parallel);
-refute_parallel_bitstring_match([_ | _] = Left, [_ | _] = Right, E, Parallel) ->
-  refute_parallel_bitstring_match_each(Left, Right, E, Parallel);
-refute_parallel_bitstring_match({Left1, Left2}, {Right1, Right2}, E, Parallel) ->
-  refute_parallel_bitstring_match_each([Left1, Left2], [Right1, Right2], E, Parallel);
-refute_parallel_bitstring_match({'{}', _, Args1}, {'{}', _, Args2}, E, Parallel) ->
-  refute_parallel_bitstring_match_each(Args1, Args2, E, Parallel);
-refute_parallel_bitstring_match({'%{}', _, Args1}, {'%{}', _, Args2}, E, Parallel) ->
-  refute_parallel_bitstring_match_map_field(lists:sort(Args1), lists:sort(Args2), E, Parallel);
-refute_parallel_bitstring_match({'%', _, [_, Args]}, Right, E, Parallel) ->
-  refute_parallel_bitstring_match(Args, Right, E, Parallel);
-refute_parallel_bitstring_match(Left, {'%', _, [_, Args]}, E, Parallel) ->
-  refute_parallel_bitstring_match(Left, Args, E, Parallel);
-refute_parallel_bitstring_match(_Left, _Right, _E, _Parallel) ->
-  ok.
-
-refute_parallel_bitstring_match_each([Arg1 | Rest1], [Arg2 | Rest2], E, Parallel) ->
-  refute_parallel_bitstring_match(Arg1, Arg2, E, Parallel),
-    refute_parallel_bitstring_match_each(Rest1, Rest2, E, Parallel);
-refute_parallel_bitstring_match_each(_List1, _List2, _E, _Parallel) ->
-  ok.
-
-refute_parallel_bitstring_match_map_field([{Key, Val1} | Rest1], [{Key, Val2} | Rest2], E, Parallel) ->
-  refute_parallel_bitstring_match(Val1, Val2, E, Parallel),
-  refute_parallel_bitstring_match_map_field(Rest1, Rest2, E, Parallel);
-refute_parallel_bitstring_match_map_field([Field1 | Rest1] = Args1, [Field2 | Rest2] = Args2, E, Parallel) ->
-  case Field1 > Field2 of
-    true ->
-      refute_parallel_bitstring_match_map_field(Args1, Rest2, E, Parallel);
-    false ->
-      refute_parallel_bitstring_match_map_field(Rest1, Args2, E, Parallel)
-  end;
-refute_parallel_bitstring_match_map_field(_Args1, _Args2, _E, _Parallel) ->
-  ok.
-
 assert_module_scope(Meta, Kind, #{module := nil, file := File}) ->
   file_error(Meta, File, ?MODULE, {invalid_expr_in_scope, "module", Kind});
 assert_module_scope(_Meta, _Kind, #{module:=Module}) -> Module.
@@ -1067,8 +1033,8 @@ assert_no_match_scope(Meta, Kind, #{context := match, file := File}) ->
 assert_no_match_scope(_Meta, _Kind, _E) -> ok.
 assert_no_guard_scope(Meta, Kind, S, #{context := guard, file := File}) ->
   Key =
-    case S#elixir_ex.prematch of
-      {_, _, {bitsize, _}}  -> invalid_expr_in_bitsize;
+    case S of
+      #elixir_ex{prematch={_, _, {bitsize, _}}}  -> invalid_expr_in_bitsize;
       _ -> invalid_expr_in_guard
     end,
   file_error(Meta, File, ?MODULE, {Key, Kind});
@@ -1092,9 +1058,6 @@ assert_no_underscore_clause_in_cond(_Other, _E) ->
 
 %% Errors
 
-guard_context(#elixir_ex{prematch={_, _, {bitsize, _}}}) -> "bitstring size specifier";
-guard_context(_) -> "guard".
-
 format_error(invalid_match_on_zero_float) ->
   "pattern matching on 0.0 is equivalent to matching only on +0.0 from Erlang/OTP 27+. Instead you must match on +0.0 or -0.0";
 format_error({useless_literal, Term}) ->
@@ -1170,10 +1133,10 @@ format_error({pin_outside_of_match, Arg}) ->
 format_error(unbound_underscore) ->
   "invalid use of _. _ can only be used inside patterns to ignore values and cannot be used in expressions. Make sure you are inside a pattern or change it accordingly";
 format_error({undefined_var, Name, Kind}) ->
-  io_lib:format("undefined variable \"~ts\"~ts", [Name, context_info(Kind)]);
+  io_lib:format("undefined variable ~ts", [elixir_utils:var_info(Name, Kind)]);
 format_error({undefined_var_pin, Name, Kind}) ->
-  Message = "undefined variable ^~ts. No variable \"~ts\"~ts has been defined before the current pattern",
-  io_lib:format(Message, [Name, Name, context_info(Kind)]);
+  Message = "undefined variable ^~ts. No variable ~ts has been defined before the current pattern",
+  io_lib:format(Message, [Name, elixir_utils:var_info(Name, Kind)]);
 format_error(underscore_in_cond) ->
   "invalid use of _ inside \"cond\". If you want the last clause to always match, "
     "you probably meant to use: true ->";
@@ -1242,15 +1205,15 @@ format_error({options_are_not_keyword, Kind, Opts}) ->
 format_error({undefined_function, Name, Args}) ->
   io_lib:format("undefined function ~ts/~B (there is no such import)", [Name, length(Args)]);
 format_error({unpinned_bitsize_var, Name, Kind}) ->
-  io_lib:format("the variable \"~ts\"~ts is accessed inside size(...) of a bitstring "
+  io_lib:format("the variable ~ts is accessed inside size(...) of a bitstring "
                 "but it was defined outside of the match. You must precede it with the "
-                "pin operator", [Name, context_info(Kind)]);
+                "pin operator", [elixir_utils:var_info(Name, Kind)]);
 format_error({underscored_var_repeat, Name, Kind}) ->
-  io_lib:format("the underscored variable \"~ts\"~ts appears more than once in a "
+  io_lib:format("the underscored variable ~ts appears more than once in a "
                 "match. This means the pattern will only match if all \"~ts\" bind "
                 "to the same value. If this is the intended behaviour, please "
                 "remove the leading underscore from the variable name, otherwise "
-                "give the variables different names", [Name, context_info(Kind), Name]);
+                "give the variables different names", [elixir_utils:var_info(Name, Kind), Name]);
 format_error({underscored_var_access, Name}) ->
   io_lib:format("the underscored variable \"~ts\" is used after being set. "
                 "A leading underscore indicates that the value of the variable "
@@ -1282,8 +1245,4 @@ format_error({parens_map_lookup, Map, Field, Context}) ->
 format_error({super_in_genserver, {Name, Arity}}) ->
   io_lib:format("calling super for GenServer callback ~ts/~B is deprecated", [Name, Arity]);
 format_error('__cursor__') ->
-  "reserved special form __cursor__ cannot be expanded, it is used exclusively to annotate ASTs";
-format_error({parallel_bitstring_match, Expr}) ->
-  Message =
-    "binary patterns cannot be matched in parallel using \"=\", excess pattern: ~ts",
-  io_lib:format(Message, ['Elixir.Macro':to_string(Expr)]).
+  "reserved special form __cursor__ cannot be expanded, it is used exclusively to annotate ASTs".
\ No newline at end of file
diff --git a/lib/elixir/src/elixir_fn.erl b/lib/elixir/src/elixir_fn.erl
index 4dbb25983f2..668b201909d 100644
--- a/lib/elixir/src/elixir_fn.erl
+++ b/lib/elixir/src/elixir_fn.erl
@@ -14,7 +14,7 @@ expand(Meta, Clauses, S, E) when is_list(Clauses) ->
         SReset = elixir_env:reset_unused_vars(SA),
 
         {EClause, SAcc, EAcc} =
-          elixir_clauses:clause(Meta, fn, fun elixir_clauses:head/3, Clause, SReset, E),
+          elixir_clauses:clause(Meta, fn, fun elixir_clauses:head/4, Clause, SReset, E),
 
         {EClause, elixir_env:merge_and_check_unused_vars(SAcc, SA, EAcc)}
     end
diff --git a/lib/elixir/src/elixir_rewrite.erl b/lib/elixir/src/elixir_rewrite.erl
index 83f62704f07..516c6abc706 100644
--- a/lib/elixir/src/elixir_rewrite.erl
+++ b/lib/elixir/src/elixir_rewrite.erl
@@ -1,6 +1,6 @@
 -module(elixir_rewrite).
 -compile({inline, [inner_inline/4, inner_rewrite/5]}).
--export([erl_to_ex/3, inline/3, rewrite/5, match_rewrite/5, guard_rewrite/6, format_error/1]).
+-export([erl_to_ex/3, inline/3, rewrite/5, match/6, guard/6, format_error/1]).
 -include("elixir.hrl").
 
 %% Convenience variables
@@ -237,6 +237,8 @@ rewrite(?string_chars, DotMeta, to_string, Meta, [Arg]) ->
     true -> Arg;
     false -> {{'.', DotMeta, [?string_chars, to_string]}, Meta, [Arg]}
   end;
+rewrite(erlang, _, '+', _, [Arg]) when is_number(Arg) -> +Arg;
+rewrite(erlang, _, '-', _, [Arg]) when is_number(Arg) -> -Arg;
 rewrite(Receiver, DotMeta, Right, Meta, Args) ->
   {EReceiver, ERight, EArgs} = inner_rewrite(ex_to_erl, DotMeta, Receiver, Right, Args),
   {{'.', DotMeta, [EReceiver, ERight]}, Meta, EArgs}.
@@ -306,11 +308,11 @@ increment(Meta, Other) ->
 %% The allowed operations are very limited.
 %% The Kernel operators are already inlined by now, we only need to
 %% care about Erlang ones.
-match_rewrite(erlang, _, '++', Meta, [Left, Right]) ->
+match(erlang, _, '++', Meta, [Left, Right], _S) ->
   try {ok, static_append(Left, Right, Meta)}
   catch impossible -> {error, {invalid_match_append, Left}}
   end;
-match_rewrite(Receiver, _, Right, _, Args) ->
+match(Receiver, _, Right, _, Args, _S) ->
   {error, {invalid_match, Receiver, Right, length(Args)}}.
 
 static_append([], Right, _Meta) -> Right;
@@ -326,14 +328,14 @@ static_append(_, _, _) -> throw(impossible).
 %% Guard rewrite is similar to regular rewrite, except
 %% it also verifies the resulting function is supported in
 %% guard context - only certain BIFs and operators are.
-guard_rewrite(Receiver, DotMeta, Right, Meta, Args, Context) ->
+guard(Receiver, DotMeta, Right, Meta, Args, S) ->
   case inner_rewrite(ex_to_erl, DotMeta, Receiver, Right, Args) of
     {erlang, RRight, RArgs} ->
       case allowed_guard(RRight, length(RArgs)) of
         true -> {ok, {{'.', DotMeta, [erlang, RRight]}, Meta, RArgs}};
-        false -> {error, {invalid_guard, Receiver, Right, length(Args), Context}}
+        false -> {error, {invalid_guard, Receiver, Right, length(Args), elixir_utils:guard_info(S)}}
       end;
-    _ -> {error, {invalid_guard, Receiver, Right, length(Args), Context}}
+    _ -> {error, {invalid_guard, Receiver, Right, length(Args), elixir_utils:guard_info(S)}}
   end.
 
 %% erlang:is_record/2-3 are compiler guards in Erlang which we
diff --git a/lib/elixir/src/elixir_utils.erl b/lib/elixir/src/elixir_utils.erl
index 539300f2bea..96d61fefa01 100644
--- a/lib/elixir/src/elixir_utils.erl
+++ b/lib/elixir/src/elixir_utils.erl
@@ -6,12 +6,20 @@
   characters_to_list/1, characters_to_binary/1, relative_to_cwd/1,
   macro_name/1, returns_boolean/1, caller/4, meta_keep/1,
   read_file_type/1, read_file_type/2, read_link_type/1, read_posix_mtime_and_size/1,
-  change_posix_time/2, change_universal_time/2,
-  guard_op/2, extract_splat_guards/1, extract_guards/1,
+  change_posix_time/2, change_universal_time/2, var_info/2,
+  guard_op/2, guard_info/1, extract_splat_guards/1, extract_guards/1,
   erlang_comparison_op_to_elixir/1, erl_fa_to_elixir_fa/2, jaro_similarity/2]).
 -include("elixir.hrl").
 -include_lib("kernel/include/file.hrl").
 
+var_info(Name, Kind) when Kind == nil; is_integer(Kind) ->
+  io_lib:format("\"~ts\"", [Name]);
+var_info(Name, Kind) ->
+  io_lib:format("\"~ts\" (context ~ts)", [Name, elixir_aliases:inspect(Kind)]).
+
+guard_info(#elixir_ex{prematch={_, _, {bitsize, _}}}) -> "bitstring size specifier";
+guard_info(_) -> "guard".
+
 macro_name(Macro) ->
   list_to_atom("MACRO-" ++ atom_to_list(Macro)).
 
diff --git a/lib/elixir/test/elixir/kernel/binary_test.exs b/lib/elixir/test/elixir/kernel/binary_test.exs
index dcb80f5c418..458b517d6c7 100644
--- a/lib/elixir/test/elixir/kernel/binary_test.exs
+++ b/lib/elixir/test/elixir/kernel/binary_test.exs
@@ -192,12 +192,6 @@ defmodule Kernel.BinaryTest do
     assert_compile_error(message, fn ->
       Code.eval_string(~s[<<"foo"::float>>])
     end)
-
-    message = "invalid literal ~c\"foo\""
-
-    assert_compile_error(message, fn ->
-      Code.eval_string(~s[<<'foo'::binary>>])
-    end)
   end
 
   @bitstring <<"foo", 16::4>>
diff --git a/lib/elixir/test/elixir/kernel/errors_test.exs b/lib/elixir/test/elixir/kernel/errors_test.exs
index fae71633ca7..8a6a4a76fbb 100644
--- a/lib/elixir/test/elixir/kernel/errors_test.exs
+++ b/lib/elixir/test/elixir/kernel/errors_test.exs
@@ -144,6 +144,22 @@ defmodule Kernel.ErrorsTest do
     )
   end
 
+  test "recursive variables on definition" do
+    assert_compile_error(
+      [
+        "nofile:2:7: ",
+        "recursive variable definition in patterns:",
+        "foo(x = y, y = z, z = x)",
+        "the following variables form a cycle: \"x\", \"y\", \"z\""
+      ],
+      ~c"""
+      defmodule Kernel.ErrorsTest.RecursiveVars do
+        def foo(x = y, y = z, z = x), do: {x, y, z}
+      end
+      """
+    )
+  end
+
   test "function without definition" do
     assert_compile_error(
       ["nofile:2:7: ", "implementation not provided for predefined def foo/0"],
@@ -463,7 +479,7 @@ defmodule Kernel.ErrorsTest do
 
   test "invalid case clauses" do
     assert_compile_error(
-      ["nofile:1:1", "expected one argument for :do clauses (->) in \"case\""],
+      ["nofile:1:37", "expected one argument for :do clauses (->) in \"case\""],
       ~c"case nil do 0, z when not is_nil(z) -> z end"
     )
   end
diff --git a/lib/elixir/test/elixir/kernel/expansion_test.exs b/lib/elixir/test/elixir/kernel/expansion_test.exs
index 1767c6a9b21..67f41e8aa13 100644
--- a/lib/elixir/test/elixir/kernel/expansion_test.exs
+++ b/lib/elixir/test/elixir/kernel/expansion_test.exs
@@ -188,6 +188,63 @@ defmodule Kernel.ExpansionTest do
       assert output == quote(do: _ = 1)
       assert Macro.Env.vars(env) == []
     end
+
+    test "errors on directly recursive definitions" do
+      assert_compile_error(
+        ~r"""
+        recursive variable definition in patterns:
+
+            x = x
+
+        the variable "x" \(context Kernel.ExpansionTest\) is defined in function of itself
+        """,
+        fn -> expand(quote(do: (x = x) = :ok)) end
+      )
+
+      assert_compile_error(
+        ~r"""
+        recursive variable definition in patterns:
+
+            \{x = \{:ok, x\}\}
+
+        the variable "x" \(context Kernel.ExpansionTest\) is defined in function of itself
+        """,
+        fn -> expand(quote(do: {x = {:ok, x}} = :ok)) end
+      )
+
+      assert_compile_error(
+        ~r"""
+        recursive variable definition in patterns:
+
+            \{\{x, y\} = \{y, x\}\}
+
+        the variable "x" \(context Kernel.ExpansionTest\) is defined in function of itself
+        """,
+        fn -> expand(quote(do: {{x, y} = {y, x}} = :ok)) end
+      )
+
+      assert_compile_error(
+        ~r"""
+        recursive variable definition in patterns:
+
+            \{\{:x, y\} = \{x, :y\}, x = y\}
+
+        the variable "x" \(context Kernel.ExpansionTest\) is defined recursively in function of "y" \(context Kernel.ExpansionTest\)
+        """,
+        fn -> expand(quote(do: {{:x, y} = {x, :y}, x = y} = :ok)) end
+      )
+
+      assert_compile_error(
+        ~r"""
+        recursive variable definition in patterns:
+
+            \{x = y, y = z, z = x\}
+
+        the following variables form a cycle: "x" \(context Kernel.ExpansionTest\), "y" \(context Kernel.ExpansionTest\), "z" \(context Kernel.ExpansionTest\)
+        """,
+        fn -> expand(quote(do: {x = y, y = z, z = x} = :ok)) end
+      )
+    end
   end
 
   describe "environment macros" do
@@ -2286,81 +2343,9 @@ defmodule Kernel.ExpansionTest do
                quote(do: <<foo::integer>> = baz = <<bar()::integer>>)
                |> clean_bit_modifiers()
 
-      assert expand(quote(do: <<foo>> = {<<baz>>} = bar())) |> clean_meta([:alignment]) ==
-               quote(do: <<foo::integer>> = {<<baz::integer>>} = bar())
+      assert expand(quote(do: <<foo>> = <<bar>> = baz)) |> clean_meta([:alignment]) ==
+               quote(do: <<foo::integer>> = <<bar::integer>> = baz())
                |> clean_bit_modifiers()
-
-      message = ~r"binary patterns cannot be matched in parallel using \"=\""
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: <<foo>> = <<baz>> = bar()))
-      end)
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: <<foo>> = qux = <<baz>> = bar()))
-      end)
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: {<<foo>>} = {qux} = {<<baz>>} = bar()))
-      end)
-
-      assert expand(quote(do: {:foo, <<foo>>} = {<<baz>>, :baz} = bar()))
-
-      # two-element tuples are special cased
-      assert_compile_error(message, fn ->
-        expand(quote(do: {:foo, <<foo>>} = {:foo, <<baz>>} = bar()))
-      end)
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: %{foo: <<foo>>} = %{baz: <<qux>>, foo: <<baz>>} = bar()))
-      end)
-
-      assert expand(quote(do: %{foo: <<foo>>} = %{baz: <<baz>>} = bar()))
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: %_{foo: <<foo>>} = %_{foo: <<baz>>} = bar()))
-      end)
-
-      assert expand(quote(do: %_{foo: <<foo>>} = %_{baz: <<baz>>} = bar()))
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: %_{foo: <<foo>>} = %{foo: <<baz>>} = bar()))
-      end)
-
-      assert expand(quote(do: %_{foo: <<foo>>} = %{baz: <<baz>>} = bar()))
-
-      assert_compile_error(message, fn ->
-        code =
-          quote do
-            case bar() do
-              <<foo>> = <<baz>> -> nil
-            end
-          end
-
-        expand(code)
-      end)
-
-      assert_compile_error(message, fn ->
-        code =
-          quote do
-            case bar() do
-              <<foo>> = qux = <<baz>> -> nil
-            end
-          end
-
-        expand(code)
-      end)
-
-      assert_compile_error(message, fn ->
-        code =
-          quote do
-            case bar() do
-              [<<foo>>] = [<<baz>>] -> nil
-            end
-          end
-
-        expand(code)
-      end)
     end
 
     test "nested match" do
@@ -2812,16 +2797,6 @@ defmodule Kernel.ExpansionTest do
       end)
     end
 
-    test "raises for invalid literals" do
-      assert_compile_error(~r"invalid literal :foo in <<>>", fn ->
-        expand(quote(do: <<:foo>>))
-      end)
-
-      assert_compile_error(~r"invalid literal \[\] in <<>>", fn ->
-        expand(quote(do: <<[]::size(8)>>))
-      end)
-    end
-
     test "raises on binary fields with size in matches" do
       assert expand(quote(do: <<x::binary-size(3), y::binary>> = "foobar"))
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 1cf3417503a..8159111fcc3 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -37,7 +37,7 @@ defmodule Module.Types.DescrTest do
         float(),
         binary(),
         open_map(),
-        non_empty_list(),
+        non_empty_list(term()),
         empty_list(),
         tuple(),
         fun(),
@@ -445,9 +445,9 @@ defmodule Module.Types.DescrTest do
              |> difference(tuple([integer(), term(), atom()]))
              |> tuple_fetch(2) == {false, integer()}
 
-      assert tuple([integer(), atom(), union(union(atom(), integer()), list())])
+      assert tuple([integer(), atom(), union(union(atom(), integer()), list(term()))])
              |> difference(tuple([integer(), term(), atom()]))
-             |> difference(open_tuple([term(), atom(), list()]))
+             |> difference(open_tuple([term(), atom(), list(term())]))
              |> tuple_fetch(2) == {false, integer()}
 
       assert tuple([integer(), atom(), integer()])
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 51dc33701a3..7bb60a146a8 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -20,7 +20,6 @@ defmodule Module.Types.ExprTest do
     assert typecheck!(0.0) == float()
     assert typecheck!("foo") == binary()
     assert typecheck!([]) == empty_list()
-    assert typecheck!([1, 2]) == non_empty_list()
     assert typecheck!(%{}) == closed_map([])
     assert typecheck!(& &1) == fun()
     assert typecheck!(fn -> :ok end) == fun()
@@ -30,6 +29,14 @@ defmodule Module.Types.ExprTest do
     assert typecheck!([x = 1], generated(x)) == dynamic()
   end
 
+  describe "lists" do
+    test "creating lists" do
+      assert typecheck!([1, 2]) == non_empty_list(integer())
+      assert typecheck!([1, 2 | 3]) == non_empty_list(integer(), integer())
+      assert typecheck!([1, 2 | [3, 4]]) == non_empty_list(integer())
+    end
+  end
+
   describe "funs" do
     test "incompatible" do
       assert typewarn!([%x{}], x.(1, 2)) ==
@@ -229,7 +236,7 @@ defmodule Module.Types.ExprTest do
                 where "y" was given the type:
 
                     # type: dynamic()
-                    # from: types_test.ex:208
+                    # from: types_test.ex:LINE-2
                     y
                 """}
     end
@@ -339,11 +346,11 @@ defmodule Module.Types.ExprTest do
 
                 but got type:
 
-                    :foo
+                    dynamic(:foo)
 
                 where "x" was given the type:
 
-                    # type: :foo
+                    # type: dynamic(:foo)
                     # from: types_test.ex:LINE-2
                     x = :foo
                 """}
@@ -419,13 +426,13 @@ defmodule Module.Types.ExprTest do
 
   describe "comparison" do
     test "works across numbers" do
-      assert typecheck!([x = 123, y = 456.0], min(x, y)) == union(integer(), float())
+      assert typecheck!([x = 123, y = 456.0], min(x, y)) == dynamic(union(integer(), float()))
       assert typecheck!([x = 123, y = 456.0], x < y) == boolean()
     end
 
     test "warns when comparison is constant" do
       assert typewarn!([x = :foo, y = 321], min(x, y)) ==
-               {union(integer(), atom([:foo])),
+               {dynamic(union(integer(), atom([:foo]))),
                 ~l"""
                 comparison between incompatible types found:
 
@@ -433,7 +440,7 @@ defmodule Module.Types.ExprTest do
 
                 where "x" was given the type:
 
-                    # type: :foo
+                    # type: dynamic(:foo)
                     # from: types_test.ex:LINE-2
                     x = :foo
 
@@ -458,13 +465,13 @@ defmodule Module.Types.ExprTest do
 
                 where "mod" was given the type:
 
-                    # type: Kernel
+                    # type: dynamic(Kernel)
                     # from: types_test.ex:LINE-2
                     mod = Kernel
 
                 where "x" was given the type:
 
-                    # type: :foo
+                    # type: dynamic(:foo)
                     # from: types_test.ex:LINE-2
                     x = :foo
 
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 04dcb5d1dba..a4ff0b469a7 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -8,8 +8,8 @@ defmodule Module.Types.PatternTest do
 
   describe "variables" do
     test "captures variables from simple assignment in head" do
-      assert typecheck!([x = :foo], x) == atom([:foo])
-      assert typecheck!([:foo = x], x) == atom([:foo])
+      assert typecheck!([x = :foo], x) == dynamic(atom([:foo]))
+      assert typecheck!([:foo = x], x) == dynamic(atom([:foo]))
     end
 
     test "captures variables from simple assignment in =" do
@@ -20,6 +20,31 @@ defmodule Module.Types.PatternTest do
                )
              ) == atom([:foo])
     end
+
+    test "refines information across patterns" do
+      assert typecheck!([%y{}, %x{}, x = y, x = Point], y) == dynamic(atom([Point]))
+    end
+
+    test "errors on conflicting refinements" do
+      assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) ==
+               ~l"""
+               the following pattern will never match:
+
+                   a = b
+
+               where "a" was given the type:
+
+                   # type: dynamic(:foo)
+                   # from: types_test.ex:29
+                   a = :foo
+
+               where "b" was given the type:
+
+                   # type: dynamic(:bar)
+                   # from: types_test.ex:29
+                   b = :bar
+               """
+    end
   end
 
   describe "structs" do
@@ -32,7 +57,7 @@ defmodule Module.Types.PatternTest do
       assert typecheck!([x = %_{}], x) == dynamic(open_map(__struct__: atom()))
 
       assert typecheck!([x = %m{}, m = Point], x) ==
-               dynamic(open_map(__struct__: atom()))
+               dynamic(open_map(__struct__: atom([Point])))
 
       assert typecheck!([m = Point, x = %m{}], x) ==
                dynamic(open_map(__struct__: atom([Point])))
@@ -60,7 +85,7 @@ defmodule Module.Types.PatternTest do
     end
 
     test "fields in guards" do
-      assert typewarn!([x = %Point{}], [x.foo_bar], :ok) ==
+      assert typewarn!([x = %Point{}], x.foo_bar, :ok) ==
                {atom([:ok]),
                 ~l"""
                 unknown key .foo_bar in expression:
@@ -84,7 +109,40 @@ defmodule Module.Types.PatternTest do
     end
 
     test "fields in guards" do
-      assert typecheck!([x = %{foo: :bar}], [x.bar], x) == dynamic(open_map(foo: atom([:bar])))
+      assert typecheck!([x = %{foo: :bar}], x.bar, x) == dynamic(open_map(foo: atom([:bar])))
+    end
+  end
+
+  describe "tuples" do
+    test "in patterns" do
+      assert typecheck!([x = {:ok, 123}], x) == dynamic(tuple([atom([:ok]), integer()]))
+      assert typecheck!([{:x, y} = {x, :y}], {x, y}) == dynamic(tuple([atom([:x]), atom([:y])]))
+    end
+  end
+
+  describe "lists" do
+    test "in patterns" do
+      assert typecheck!([x = [1, 2, 3]], x) ==
+               dynamic(non_empty_list(integer()))
+
+      assert typecheck!([x = [1, 2, 3 | y], y = :foo], x) ==
+               dynamic(non_empty_list(integer(), atom([:foo])))
+
+      assert typecheck!([x = [1, 2, 3 | y], y = [1.0, 2.0, 3.0]], x) ==
+               dynamic(non_empty_list(union(integer(), float())))
+    end
+
+    test "in patterns through ++" do
+      assert typecheck!([x = [] ++ []], x) == dynamic(empty_list())
+
+      assert typecheck!([x = [] ++ y, y = :foo], x) ==
+               dynamic(atom([:foo]))
+
+      assert typecheck!([x = [1, 2, 3] ++ y, y = :foo], x) ==
+               dynamic(non_empty_list(integer(), atom([:foo])))
+
+      assert typecheck!([x = [1, 2, 3] ++ y, y = [1.0, 2.0, 3.0]], x) ==
+               dynamic(non_empty_list(union(integer(), float())))
     end
   end
 
@@ -160,4 +218,20 @@ defmodule Module.Types.PatternTest do
                 """}
     end
   end
+
+  describe "inference" do
+    test "refines information across patterns" do
+      result = [
+        dynamic(open_map(__struct__: atom([Point]))),
+        dynamic(open_map(__struct__: atom([Point]))),
+        dynamic(atom([Point])),
+        dynamic(atom([Point]))
+      ]
+
+      assert typeinfer!([%y{}, %x{}, x = y, x = Point]) == result
+      assert typeinfer!([%x{}, %y{}, x = y, x = Point]) == result
+      assert typeinfer!([%y{}, %x{}, x = y, y = Point]) == result
+      assert typeinfer!([%x{}, %y{}, x = y, y = Point]) == result
+    end
+  end
 end
diff --git a/lib/elixir/test/elixir/module/types/type_helper.exs b/lib/elixir/test/elixir/module/types/type_helper.exs
index 85fc2c20685..28b3b0b1128 100644
--- a/lib/elixir/test/elixir/module/types/type_helper.exs
+++ b/lib/elixir/test/elixir/module/types/type_helper.exs
@@ -8,10 +8,20 @@ defmodule TypeHelper do
   alias Module.Types
   alias Module.Types.{Pattern, Expr, Descr}
 
+  @doc """
+  Main helper for inferring the given pattern + guards.
+  """
+  defmacro typeinfer!(patterns \\ [], guards \\ true) do
+    quote do
+      unquote(typeinfer(patterns, guards, __CALLER__))
+      |> TypeHelper.__typecheck__!()
+    end
+  end
+
   @doc """
   Main helper for checking the given AST type checks without warnings.
   """
-  defmacro typecheck!(patterns \\ [], guards \\ [], body) do
+  defmacro typecheck!(patterns \\ [], guards \\ true, body) do
     quote do
       unquote(typecheck(patterns, guards, body, __CALLER__))
       |> TypeHelper.__typecheck__!()
@@ -21,7 +31,7 @@ defmodule TypeHelper do
   @doc """
   Main helper for checking the given AST type checks errors.
   """
-  defmacro typeerror!(patterns \\ [], guards \\ [], body) do
+  defmacro typeerror!(patterns \\ [], guards \\ true, body) do
     quote do
       unquote(typecheck(patterns, guards, body, __CALLER__))
       |> TypeHelper.__typeerror__!()
@@ -31,7 +41,7 @@ defmodule TypeHelper do
   @doc """
   Main helper for checking the given AST type warns.
   """
-  defmacro typewarn!(patterns \\ [], guards \\ [], body) do
+  defmacro typewarn!(patterns \\ [], guards \\ true, body) do
     quote do
       unquote(typecheck(patterns, guards, body, __CALLER__))
       |> TypeHelper.__typewarn__!()
@@ -41,7 +51,7 @@ defmodule TypeHelper do
   @doc """
   Main helper for checking the diagnostic of a given AST.
   """
-  defmacro typediag!(patterns \\ [], guards \\ [], body) do
+  defmacro typediag!(patterns \\ [], guards \\ true, body) do
     quote do
       unquote(typecheck(patterns, guards, body, __CALLER__))
       |> TypeHelper.__typediag__!()
@@ -83,17 +93,29 @@ defmodule TypeHelper do
     {type, message}
   end
 
+  @doc """
+  Building block for typeinferring a given AST.
+  """
+  def typeinfer(patterns, guards, env) do
+    {patterns, guards, :ok} = expand_and_unpack(patterns, guards, :ok, env)
+
+    quote do
+      TypeHelper.__typeinfer__(
+        unquote(Macro.escape(patterns)),
+        unquote(Macro.escape(guards))
+      )
+    end
+  end
+
+  def __typeinfer__(patterns, guards) do
+    Pattern.of_head(patterns, guards, [], new_stack(), new_context())
+  end
+
   @doc """
   Building block for typechecking a given AST.
   """
   def typecheck(patterns, guards, body, env) do
-    fun =
-      quote do
-        fn unquote(patterns) when unquote(guards) -> unquote(body) end
-      end
-
-    {ast, _, _} = :elixir_expand.expand(fun, :elixir_env.env_to_ex(env), env)
-    {:fn, _, [{:->, _, [[{:when, _, [patterns, guards]}], body]}]} = ast
+    {patterns, guards, body} = expand_and_unpack(patterns, guards, body, env)
 
     quote do
       TypeHelper.__typecheck__(
@@ -113,6 +135,18 @@ defmodule TypeHelper do
     end
   end
 
+  defp expand_and_unpack(patterns, guards, body, env) do
+    fun =
+      quote do
+        fn unquote_splicing(patterns) when unquote(guards) -> unquote(body) end
+      end
+
+    {ast, _, _} = :elixir_expand.expand(fun, :elixir_env.env_to_ex(env), env)
+    {:fn, _, [{:->, _, [[{:when, _, args}], body]}]} = ast
+    {patterns, guards} = Enum.split(args, -1)
+    {patterns, guards, body}
+  end
+
   defp new_stack() do
     Types.stack("types_test.ex", TypesTest, {:test, 0}, [], Module.ParallelChecker.test_cache())
   end