diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 1339a70e04..4fa5d83874 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2099,9 +2099,9 @@ defmodule Module.Types.Descr do
   defp list_hd_static(%{}), do: none()
 
   @doc """
-   Returns the tail of a list.
+  Returns the tail of a list.
 
-   For a `non_empty_list(t)`, the tail type is `list(t)`.
+  For a `non_empty_list(t)`, the tail type is `list(t)`.
   For an improper list `non_empty_list(t, s)`, the tail type is
   `list(t, s) or s` (either the rest of the list or the terminator)
   """
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 7c8e37f785..33cd84681a 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -580,6 +580,7 @@ defmodule Module.Types.Expr do
         _ ->
           expected = if structs == [], do: @exception, else: Enum.reduce(structs, &union/2)
           expr = {:__block__, [type_check: info], [expr]}
+          context = Of.declare_var(var, context)
           {_ok?, _type, context} = Of.refine_head_var(var, expected, expr, stack, context)
           context
       end
diff --git a/lib/elixir/lib/module/types/helpers.ex b/lib/elixir/lib/module/types/helpers.ex
index d090d8e7c0..e5b0e03903 100644
--- a/lib/elixir/lib/module/types/helpers.ex
+++ b/lib/elixir/lib/module/types/helpers.ex
@@ -148,7 +148,7 @@ defmodule Module.Types.Helpers do
           version = meta[:version]
 
           case vars do
-            %{^version => %{off_traces: off_traces, name: name, context: context}} ->
+            %{^version => %{off_traces: [_ | _] = off_traces, name: name, context: context}} ->
               {:ok,
                Map.put(versions, version, %{
                  type: :variable,
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index cec8fdcff0..9591dcc773 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -30,19 +30,40 @@ defmodule Module.Types.Of do
 
   @doc """
   Marks a variable with error.
+
+  This purposedly deletes all traces of the variable,
+  as it is often invoked when the cause for error is elsewhere.
+  """
+  def error_var({_var_name, meta, _var_context}, context) do
+    version = Keyword.fetch!(meta, :version)
+
+    update_in(context.vars[version], fn
+      %{errored: true} = data -> data
+      data -> Map.put(%{data | type: error_type(), off_traces: []}, :errored, true)
+    end)
+  end
+
+  @doc """
+  Declares a variable.
   """
-  def error_var(var, context) do
+  def declare_var(var, context) do
     {var_name, meta, var_context} = var
     version = Keyword.fetch!(meta, :version)
 
-    data = %{
-      type: error_type(),
-      name: var_name,
-      context: var_context,
-      off_traces: []
-    }
+    case context.vars do
+      %{^version => _} ->
+        context
+
+      vars ->
+        data = %{
+          type: term(),
+          name: var_name,
+          context: var_context,
+          off_traces: []
+        }
 
-    put_in(context.vars[version], data)
+        %{context | vars: Map.put(vars, version, data)}
+    end
   end
 
   @doc """
@@ -56,7 +77,7 @@ defmodule Module.Types.Of do
     version = Keyword.fetch!(meta, :version)
     %{vars: %{^version => %{type: old_type, off_traces: off_traces} = data} = vars} = context
 
-    if gradual?(old_type) and type not in [term(), dynamic()] do
+    if gradual?(old_type) and type not in [term(), dynamic()] and not is_map_key(data, :errored) do
       case compatible_intersection(old_type, type) do
         {:ok, new_type} when new_type != old_type ->
           data = %{
@@ -82,11 +103,13 @@ defmodule Module.Types.Of do
   because we want to refine types. Otherwise we should
   use compatibility.
   """
-  def refine_head_var(var, type, expr, stack, context) do
-    {var_name, meta, var_context} = var
+  def refine_head_var({_, meta, _}, type, expr, stack, context) do
     version = Keyword.fetch!(meta, :version)
 
     case context.vars do
+      %{^version => %{errored: true}} ->
+        {:ok, error_type(), context}
+
       %{^version => %{type: old_type, off_traces: off_traces} = data} = vars ->
         new_type = intersection(type, old_type)
 
@@ -96,26 +119,14 @@ defmodule Module.Types.Of do
             off_traces: new_trace(expr, type, stack, off_traces)
         }
 
-        context = %{context | vars: %{vars | version => data}}
-
-        # We need to return error otherwise it leads to cascading errors
         if empty?(new_type) do
-          {:error, error_type(),
-           error({:refine_head_var, old_type, type, var, context}, meta, stack, context)}
+          data = Map.put(%{data | type: error_type()}, :errored, true)
+          context = %{context | vars: %{vars | version => data}}
+          {:error, old_type, context}
         else
+          context = %{context | vars: %{vars | version => data}}
           {:ok, new_type, context}
         end
-
-      %{} = vars ->
-        data = %{
-          type: type,
-          name: var_name,
-          context: var_context,
-          off_traces: new_trace(expr, type, stack, [])
-        }
-
-        context = %{context | vars: Map.put(vars, version, data)}
-        {:ok, type, context}
     end
   end
 
@@ -546,23 +557,6 @@ defmodule Module.Types.Of do
     error(__MODULE__, warning, meta, stack, context)
   end
 
-  def format_diagnostic({:refine_head_var, old_type, new_type, var, context}) do
-    traces = collect_traces(var, context)
-
-    %{
-      details: %{typing_traces: traces},
-      message:
-        IO.iodata_to_binary([
-          """
-          incompatible types assigned to #{format_var(var)}:
-
-              #{to_quoted_string(old_type)} !~ #{to_quoted_string(new_type)}
-          """,
-          format_traces(traces)
-        ])
-    }
-  end
-
   def format_diagnostic({:badbinary, kind, meta, expr, expected_type, actual_type, context}) do
     type = if kind == :match, do: "matching", else: "construction"
     hints = if meta[:inferred_bitstring_spec], do: [:inferred_bitstring_spec], else: []
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index ecfca9fd64..3150f4ce1e 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -62,16 +62,20 @@ defmodule Module.Types.Pattern do
     {trees, context} = of_pattern_args_index(patterns, 0, [], stack, context)
     {pattern_info, context} = pop_pattern_info(context)
 
-    {_, context} =
-      of_pattern_recur(expected, tag, pattern_info, stack, context, fn types, changed, context ->
-        of_pattern_args_tree(trees, types, changed, 0, [], tag, stack, context)
-      end)
+    context =
+      case of_pattern_args_tree(trees, expected, 0, [], tag, stack, context) do
+        {:ok, types, context} ->
+          of_pattern_recur(types, tag, pattern_info, stack, context)
+
+        {:error, context} ->
+          error_vars(pattern_info, context)
+      end
 
     {trees, context}
   end
 
   defp of_pattern_args_index([pattern | tail], index, acc, stack, context) do
-    {tree, context} = of_pattern(pattern, [{:arg, index, pattern}], stack, context)
+    {tree, context} = of_pattern(pattern, [%{root: {:arg, index}, expr: pattern}], stack, context)
     acc = [{pattern, tree} | acc]
     of_pattern_args_index(tail, index + 1, acc, stack, context)
   end
@@ -82,7 +86,6 @@ defmodule Module.Types.Pattern do
   defp of_pattern_args_tree(
          [{pattern, tree} | tail],
          [type | expected_types],
-         [index | changed],
          index,
          acc,
          tag,
@@ -92,25 +95,11 @@ defmodule Module.Types.Pattern do
     with {:ok, type, context} <-
            of_pattern_intersect(tree, type, pattern, index, tag, stack, context) do
       acc = [type | acc]
-      of_pattern_args_tree(tail, expected_types, changed, index + 1, acc, tag, stack, context)
+      of_pattern_args_tree(tail, expected_types, index + 1, acc, tag, stack, context)
     end
   end
 
-  defp of_pattern_args_tree(
-         [_ | tail],
-         [type | expected_types],
-         changed,
-         index,
-         acc,
-         tag,
-         stack,
-         context
-       ) do
-    acc = [type | acc]
-    of_pattern_args_tree(tail, expected_types, changed, index + 1, acc, tag, stack, context)
-  end
-
-  defp of_pattern_args_tree([], [], [], _index, acc, _tag, _stack, context) do
+  defp of_pattern_args_tree([], [], _index, acc, _tag, _stack, context) do
     {:ok, Enum.reverse(acc), context}
   end
 
@@ -125,7 +114,7 @@ defmodule Module.Types.Pattern do
 
   def of_match(pattern, expected_fun, expr, stack, context) do
     context = init_pattern_info(context)
-    {tree, context} = of_pattern(pattern, [{:arg, 0, expr}], stack, context)
+    {tree, context} = of_pattern(pattern, [%{root: {:arg, 0}, expr: expr}], stack, context)
     {pattern_info, context} = pop_pattern_info(context)
     {expected, context} = expected_fun.(of_pattern_tree(tree, context), context)
     tag = {:match, expected}
@@ -147,7 +136,7 @@ defmodule Module.Types.Pattern do
 
   def of_generator(pattern, guards, expected, tag, expr, stack, context) do
     context = init_pattern_info(context)
-    {tree, context} = of_pattern(pattern, [{:arg, 0, expr}], stack, context)
+    {tree, context} = of_pattern(pattern, [%{root: {:arg, 0}, expr: expr}], stack, context)
     {pattern_info, context} = pop_pattern_info(context)
 
     {_, context} =
@@ -158,115 +147,164 @@ defmodule Module.Types.Pattern do
   end
 
   defp of_single_pattern_recur(expected, tag, tree, pattern_info, expr, stack, context) do
-    of_pattern_recur([expected], tag, pattern_info, stack, context, fn [type], [0], context ->
-      with {:ok, type, context} <-
-             of_pattern_intersect(tree, type, expr, 0, tag, stack, context) do
-        {:ok, [type], context}
-      end
-    end)
-  end
+    case of_pattern_intersect(tree, expected, expr, 0, tag, stack, context) do
+      {:ok, type, context} ->
+        {[type], of_pattern_recur([type], tag, pattern_info, stack, context)}
 
-  defp all_single_path?(vars, info, index) do
-    info
-    |> Map.get(index, [])
-    |> Enum.all?(fn version -> match?([_], Map.fetch!(vars, version)) end)
+      {:error, context} ->
+        {[expected], error_vars(pattern_info, context)}
+    end
   end
 
-  defp of_pattern_recur(types, tag, pattern_info, stack, context, callback) do
-    {vars, info, _counter} = pattern_info
-    changed = :lists.seq(0, length(types) - 1)
-
-    # If all variables in a given index have a single path,
-    # then there are no changes to propagate
-    unchangeable = for index <- changed, all_single_path?(vars, info, index), do: index
-    vars = Map.to_list(vars)
+  defp of_pattern_recur(types, tag, pattern_info, stack, context) do
+    {args_paths, vars_paths, vars_deps} = pattern_info
 
     try do
-      case callback.(types, changed, context) do
-        {:ok, types, context} ->
-          of_pattern_recur(types, unchangeable, vars, info, tag, stack, context, callback)
+      Enum.map_reduce(args_paths, context, fn {version, paths}, context ->
+        context =
+          Enum.reduce(paths, context, fn
+            %{var: var, expr: expr, root: {:arg, index}, path: path}, context ->
+              actual = Enum.fetch!(types, index)
 
-        {:error, context} ->
-          {types, error_vars(vars, context)}
-      end
+              case of_pattern_var(path, actual, context) do
+                {:ok, new_type} ->
+                  case Of.refine_head_var(var, new_type, expr, stack, context) do
+                    {:ok, _type, context} ->
+                      context
+
+                    {:error, old_type, error_context} ->
+                      if match_error?(var, new_type) do
+                        throw(badpattern_error(expr, index, tag, stack, context))
+                      else
+                        throw(badvar_error(var, old_type, new_type, stack, error_context))
+                      end
+                  end
+
+                :error ->
+                  throw(badpattern_error(expr, index, tag, stack, context))
+              end
+          end)
+
+        {version, context}
+      end)
     catch
-      {types, context} -> {types, error_vars(vars, context)}
+      context -> error_vars(pattern_info, context)
+    else
+      {changed, context} ->
+        context =
+          Enum.reduce(changed, context, fn version, context ->
+            {_, context} = of_pattern_var_dep(vars_paths, version, stack, context)
+            context
+          end)
+
+        of_pattern_var_deps(changed, vars_paths, vars_deps, stack, context)
     end
   end
 
-  defp of_pattern_recur(types, unchangeable, vars, info, tag, stack, context, callback) do
+  defp of_pattern_var_deps([], _vars_paths, _vars_deps, _stack, context) do
+    context
+  end
+
+  defp of_pattern_var_deps(previous_changed, vars_paths, vars_deps, stack, context) do
     {changed, context} =
-      Enum.reduce(vars, {[], context}, fn {version, paths}, {changed, context} ->
-        {var_changed?, context} =
+      previous_changed
+      |> Enum.reduce(%{}, fn version, acc ->
+        case vars_deps do
+          %{^version => deps} -> Map.merge(acc, deps)
+          %{} -> acc
+        end
+      end)
+      |> Map.keys()
+      |> Enum.reduce({[], context}, fn version, {changed, context} ->
+        {var_changed?, context} = of_pattern_var_dep(vars_paths, version, stack, context)
+
+        case var_changed? do
+          false -> {changed, context}
+          true -> {[version | changed], context}
+        end
+      end)
+
+    of_pattern_var_deps(changed, vars_paths, vars_deps, stack, context)
+  end
+
+  defp of_pattern_var_dep(vars_paths, version, stack, context) do
+    paths = Map.get(vars_paths, version, [])
+
+    case context.vars do
+      %{^version => %{type: old_type} = data} when not is_map_key(data, :errored) ->
+        try do
           Enum.reduce(paths, {false, context}, fn
-            [var, {:arg, index, expr} | path], {var_changed?, context} ->
-              actual = Enum.fetch!(types, index)
+            %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
+              actual = of_pattern_tree(root, context)
 
-              case of_pattern_var(path, actual, true, info, context) do
-                {type, reachable_var?} ->
+              case of_pattern_var(path, actual, context) do
+                {:ok, new_type} ->
                   # Optimization: if current type is already a subtype, there is nothing to refine.
-                  with %{^version => %{type: current_type}} <- context.vars,
-                       true <- subtype?(current_type, type) do
+                  if old_type != term() and subtype?(old_type, new_type) do
                     {var_changed?, context}
                   else
-                    _ ->
-                      case Of.refine_head_var(var, type, expr, stack, context) do
-                        {:ok, _type, context} -> {var_changed? or reachable_var?, context}
-                        {:error, _type, context} -> throw({types, context})
-                      end
+                    case Of.refine_head_var(var, new_type, expr, stack, context) do
+                      {:ok, _type, context} ->
+                        {true, context}
+
+                      {:error, _old_type, error_context} ->
+                        if match_error?(var, new_type) do
+                          throw(badmatch_error(var, expr, stack, context))
+                        else
+                          throw(badvar_error(var, old_type, new_type, stack, error_context))
+                        end
+                    end
                   end
 
                 :error ->
-                  throw({types, badpattern_error(expr, index, tag, stack, context)})
+                  throw(badmatch_error(var, expr, stack, context))
               end
           end)
-
-        case var_changed? do
-          false ->
-            {changed, context}
-
-          true ->
-            var_changed = Enum.map(paths, fn [_var, {:arg, index, _} | _] -> index end)
-            {var_changed ++ changed, context}
+        catch
+          context -> {false, context}
         end
-      end)
 
-    case :lists.usort(changed) -- unchangeable do
-      [] ->
-        {types, context}
+      _ ->
+        {false, context}
+    end
+  end
 
-      changed ->
-        case callback.(types, changed, context) do
-          # A simple structural comparison for optimization
-          {:ok, ^types, context} ->
-            {types, context}
+  defp error_vars({args_paths, vars_paths, _vars_deps}, context) do
+    callback = fn [%{var: var} | _paths], context ->
+      Of.error_var(var, context)
+    end
 
-          {:ok, types, context} ->
-            of_pattern_recur(types, unchangeable, vars, info, tag, stack, context, callback)
+    context = Enum.reduce(Map.values(args_paths), context, callback)
+    context = Enum.reduce(Map.values(vars_paths), context, callback)
+    context
+  end
 
-          {:error, context} ->
-            {types, error_vars(vars, context)}
-        end
-    end
+  defp match_error?({:match, _, __MODULE__}, _type), do: true
+  defp match_error?(_var, type), do: empty?(type)
+
+  defp badmatch_error(var, expr, stack, context) do
+    context = Of.error_var(var, context)
+    error(__MODULE__, {:badmatch, expr, context}, error_meta(expr, stack), stack, context)
   end
 
-  defp error_vars(vars, context) do
-    Enum.reduce(vars, context, fn {_version, [[var | _path] | _paths]}, context ->
-      Of.error_var(var, context)
-    end)
+  defp badvar_error(var, old_type, new_type, stack, context) do
+    error = {:badvar, old_type, new_type, var, context}
+    error(__MODULE__, error, error_meta(var, stack), stack, context)
   end
 
   defp badpattern_error(expr, index, tag, stack, context) do
-    meta =
-      if meta = get_meta(expr) do
-        meta ++ Keyword.take(stack.meta, [:generated, :line, :type_check])
-      else
-        stack.meta
-      end
-
+    meta = error_meta(expr, stack)
     error(__MODULE__, {:badpattern, meta, expr, index, tag, context}, meta, stack, context)
   end
 
+  defp error_meta(expr, stack) do
+    if meta = get_meta(expr) do
+      meta ++ Keyword.take(stack.meta, [:generated, :line, :type_check])
+    else
+      stack.meta
+    end
+  end
+
   defp of_pattern_intersect(tree, expected, expr, index, tag, stack, context) do
     actual = of_pattern_tree(tree, context)
     type = intersection(actual, expected)
@@ -278,46 +316,41 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  defp of_pattern_var([], type, reachable_var?, _info, _context) do
-    {type, reachable_var?}
+  defp of_pattern_var([], type, _context) do
+    {:ok, type}
   end
 
-  defp of_pattern_var([{:elem, index} | rest], type, reachable_var?, info, context)
+  defp of_pattern_var([{:elem, index} | rest], type, context)
        when is_integer(index) do
     case tuple_fetch(type, index) do
-      {_optional?, type} -> of_pattern_var(rest, type, reachable_var?, info, context)
+      {_optional?, type} -> of_pattern_var(rest, type, context)
       _reason -> :error
     end
   end
 
-  defp of_pattern_var([{:key, field} | rest], type, reachable_var?, info, context)
+  defp of_pattern_var([{:key, field} | rest], type, context)
        when is_atom(field) do
     case map_fetch_key(type, field) do
-      {_optional?, type} -> of_pattern_var(rest, type, reachable_var?, info, context)
+      {_optional?, type} -> of_pattern_var(rest, type, context)
       _reason -> :error
     end
   end
 
   # TODO: Implement domain key types
-  defp of_pattern_var([{:key, _key} | rest], _type, _reachable_var?, info, context) do
-    of_pattern_var(rest, dynamic(), false, info, context)
+  defp of_pattern_var([{:key, _key} | rest], _type, context) do
+    of_pattern_var(rest, dynamic(), context)
   end
 
-  defp of_pattern_var([{:head, counter} | rest], type, _reachable_var?, info, context) do
+  defp of_pattern_var([:head | rest], type, context) do
     case list_hd(type) do
-      {:ok, head} ->
-        tree = Map.fetch!(info, -counter)
-        type = intersection(of_pattern_tree(tree, context), head)
-        of_pattern_var(rest, type, false, info, context)
-
-      _ ->
-        :error
+      {:ok, head} -> of_pattern_var(rest, head, context)
+      _ -> :error
     end
   end
 
-  defp of_pattern_var([:tail | rest], type, reachable_var?, info, context) do
+  defp of_pattern_var([:tail | rest], type, context) do
     case list_tl(type) do
-      {:ok, tail} -> of_pattern_var(rest, tail, reachable_var?, info, context)
+      {:ok, tail} -> of_pattern_var(rest, tail, context)
       :badnonemptylist -> :error
     end
   end
@@ -373,8 +406,15 @@ defmodule Module.Types.Pattern do
   end
 
   def of_match_var(var, expected, expr, stack, context) when is_var(var) do
-    {_ok?, type, context} = Of.refine_head_var(var, expected, expr, stack, context)
-    {type, context}
+    context = Of.declare_var(var, context)
+
+    case Of.refine_head_var(var, expected, expr, stack, context) do
+      {:ok, type, context} ->
+        {type, context}
+
+      {:error, old_type, error_context} ->
+        {error_type(), badvar_error(var, old_type, expected, stack, error_context)}
+    end
   end
 
   def of_match_var({:<<>>, _meta, args}, _expected, _expr, stack, context) do
@@ -420,11 +460,27 @@ defmodule Module.Types.Pattern do
 
   # left = right
   defp of_pattern({:=, _meta, [_, _]} = match, path, stack, context) do
-    result =
+    {matches, version, var} =
       match
       |> unpack_match([])
-      |> Enum.reduce({[], [], context}, fn pattern, {static, dynamic, context} ->
-        {type, context} = of_pattern(pattern, path, stack, context)
+      |> Enum.split_while(&(not is_versioned_var(&1)))
+      |> case do
+        {matches, []} ->
+          version = make_ref()
+          {matches, version, {:match, [version: version], __MODULE__}}
+
+        {pre, [{_, meta, _} = var | post]} ->
+          version = Keyword.fetch!(meta, :version)
+          {pre ++ post, version, var}
+      end
+
+    # Pass the current path to build the current var
+    context = of_var(var, version, path, context)
+    root = %{root: {:var, version}, expr: match}
+
+    {static, dynamic, context} =
+      Enum.reduce(matches, {[], [], context}, fn pattern, {static, dynamic, context} ->
+        {type, context} = of_pattern(pattern, [root], stack, context)
 
         if is_descr(type) do
           {[type | static], dynamic, context}
@@ -433,20 +489,22 @@ defmodule Module.Types.Pattern do
         end
       end)
 
-    case result do
-      {[], dynamic, context} ->
-        {{:intersection, dynamic}, context}
-
-      {static, [], context} ->
-        {Enum.reduce(static, &intersection/2), context}
+    if dynamic == [] do
+      {Enum.reduce(static, &intersection/2), context}
+    else
+      # The dynamic parts have to be recomputed whenever they change
+      context = of_var(var, version, [%{root: {:intersection, dynamic}, expr: match}], context)
 
-      {static, dynamic, context} ->
+      # And everything else is also pushed as part of the argument intersection
+      if static == [] do
+        {{:intersection, dynamic}, context}
+      else
         {{:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}, context}
+      end
     end
   end
 
   # %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)
@@ -541,18 +599,44 @@ defmodule Module.Types.Pattern do
   end
 
   # var
-  defp of_pattern({name, meta, ctx} = var, reverse_path, _stack, context)
+  defp of_pattern({name, meta, ctx} = var, path, _stack, context)
        when is_atom(name) and is_atom(ctx) do
     version = Keyword.fetch!(meta, :version)
-    [{:arg, arg, _pattern} | _] = path = Enum.reverse(reverse_path)
-    {vars, info, counter} = context.pattern_info
-
-    paths = [[var | path] | Map.get(vars, version, [])]
-    vars = Map.put(vars, version, paths)
+    {{:var, version}, of_var(var, version, path, context)}
+  end
+
+  defp is_versioned_var({name, _meta, ctx}) when is_atom(name) and is_atom(ctx) and name != :_,
+    do: true
+
+  defp is_versioned_var(_), do: false
+
+  defp of_var(var, version, reverse_path, context) do
+    context = Of.declare_var(var, context)
+    {args_paths, vars_paths, vars_deps} = context.pattern_info
+    [%{root: root, expr: expr} | path] = Enum.reverse(reverse_path)
+    node = %{root: root, var: var, expr: expr, path: path}
+
+    pattern_info =
+      case root do
+        {:arg, _} ->
+          paths = [node | Map.get(args_paths, version, [])]
+          args_paths = Map.put(args_paths, version, paths)
+          {args_paths, vars_paths, vars_deps}
+
+        {:var, other} ->
+          paths = [node | Map.get(vars_paths, version, [])]
+          vars_paths = Map.put(vars_paths, version, paths)
+          vars_deps = Map.update(vars_deps, version, %{other => []}, &Map.put(&1, other, []))
+          vars_deps = Map.update(vars_deps, other, %{version => []}, &Map.put(&1, version, []))
+          {args_paths, vars_paths, vars_deps}
+
+        _ ->
+          paths = [node | Map.get(vars_paths, version, [])]
+          vars_paths = Map.put(vars_paths, version, paths)
+          {args_paths, vars_paths, vars_deps}
+      end
 
-    # Stores all variables used at any given argument
-    info = Map.update(info, arg, [version], &[version | &1])
-    {{:var, version}, %{context | pattern_info: {vars, info, counter}}}
+    %{context | pattern_info: pattern_info}
   end
 
   # TODO: Properly traverse domain keys
@@ -607,45 +691,26 @@ defmodule Module.Types.Pattern do
   # [prefix1, prefix2, prefix3], [prefix1, prefix2 | suffix]
   defp of_list(prefix, suffix, path, stack, context) do
     {suffix, context} = of_pattern(suffix, [:tail | path], stack, context)
-    {vars, info, counter} = context.pattern_info
-    context = %{context | pattern_info: {vars, info, counter + length(prefix)}}
-
-    {static, dynamic, info, context} =
-      Enum.reduce(prefix, {[], [], %{}, context}, fn
-        arg, {static, dynamic, info, context}
-        when is_number(arg) or is_atom(arg) or is_binary(arg) or arg == [] ->
-          {type, context} = of_pattern(arg, [], stack, context)
-          {[type | static], dynamic, info, context}
-
-        arg, {static, dynamic, info, context} ->
-          counter = map_size(info) + counter
-          {type, context} = of_pattern(arg, [{:head, counter} | path], stack, context)
-          info = Map.put(info, -counter, type)
-
-          if is_descr(type) do
-            {[type | static], dynamic, info, context}
-          else
-            {static, [type | dynamic], info, context}
-          end
-      end)
 
-    context =
-      if info != %{} do
-        update_in(context.pattern_info, fn {acc_vars, acc_info, acc_counter} ->
-          {acc_vars, Map.merge(acc_info, info), acc_counter}
-        end)
-      else
-        context
-      end
+    result =
+      Enum.reduce(prefix, {[], [], context}, fn arg, {static, dynamic, context} ->
+        {type, context} = of_pattern(arg, [:head | path], stack, context)
+
+        if is_descr(type) do
+          {[type | static], dynamic, context}
+        else
+          {static, [type | dynamic], context}
+        end
+      end)
 
-    case {static, dynamic} do
-      {static, []} when is_descr(suffix) ->
+    case result do
+      {static, [], context} when is_descr(suffix) ->
         {non_empty_list(Enum.reduce(static, &union/2), suffix), context}
 
-      {[], dynamic} ->
+      {[], dynamic, context} ->
         {{:non_empty_list, dynamic, suffix}, context}
 
-      {static, dynamic} ->
+      {static, dynamic, context} ->
         {{:non_empty_list, [Enum.reduce(static, &union/2) | dynamic], suffix}, context}
     end
   end
@@ -763,14 +828,49 @@ defmodule Module.Types.Pattern do
   # additional information about the number of variables in
   # arguments and list heads, and a counter used to compute
   # the number of list heads.
+  # TODO: Consider moving pattern_info into context.vars.
   defp init_pattern_info(context) do
-    %{context | pattern_info: {%{}, %{}, 1}}
+    %{context | pattern_info: {%{}, %{}, %{}}}
   end
 
   defp pop_pattern_info(%{pattern_info: pattern_info} = context) do
     {pattern_info, %{context | pattern_info: nil}}
   end
 
+  def format_diagnostic({:badmatch, expr, context}) do
+    traces = collect_traces(expr, context)
+
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          this match will never succeed due to incompatible types:
+
+              #{expr_to_string(expr) |> indent(4)}
+          """,
+          format_traces(traces)
+        ])
+    }
+  end
+
+  def format_diagnostic({:badvar, old_type, new_type, var, context}) do
+    traces = collect_traces(var, context)
+
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          incompatible types assigned to #{format_var(var)}:
+
+              #{to_quoted_string(old_type)} !~ #{to_quoted_string(new_type)}
+          """,
+          format_traces(traces)
+        ])
+    }
+  end
+
   def format_diagnostic({:badstruct, type, expr, context}) do
     traces = collect_traces(expr, context)
 
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 626c4c9147..8a3073e25b 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -51,27 +51,6 @@ defmodule Module.Types.PatternTest do
                """
     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:LINE-1
-                   a = :foo
-
-               where "b" was given the type:
-
-                   # type: dynamic(:bar)
-                   # from: types_test.ex:LINE-1
-                   b = :bar
-               """
-    end
-
     test "can be accessed even if they don't match" do
       assert typeerror!(
                (
@@ -117,20 +96,56 @@ defmodule Module.Types.PatternTest do
     end
 
     test "reports incompatible types" do
-      assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""
+      assert typeerror!([x = 123 = "123"], x) == ~l"""
+             the following pattern will never match:
+
+                 x = 123 = "123"
+             """
+
+      assert typeerror!([x = {:ok, _} = {:error, _, _}], x) == ~l"""
+             the following pattern will never match:
+
+                 x = {:ok, _} = {:error, _, _}
+             """
+
+      assert typeerror!([{x = {:ok, y} = {:error, z, w}}], {x, y, z, w}) == ~l"""
              the following pattern will never match:
 
-                 [_ | _] = x
+                 {x = {:ok, y} = {:error, z, w}}
+             """
+
+      assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) == ~l"""
+             incompatible types assigned to "a":
+
+                 dynamic(:foo) !~ dynamic(:bar)
+
+             where "a" was given the types:
+
+                 # type: dynamic(:foo)
+                 # from: types_test.ex:LINE
+                 a = :foo
+
+                 # type: dynamic(:bar)
+                 # from: types_test.ex:LINE
+                 a = b
+             """
 
-             because the right-hand side has type:
+      assert typeerror!([{x, _} = {y, _}, x = :foo, y = :bar], {x, y}) == ~l"""
+             this match will never succeed due to incompatible types:
 
-                 dynamic({:ok, term()})
+                 {x, _} = {y, _}
 
              where "x" was given the type:
 
-                 # type: dynamic({:ok, term()})
+                 # type: dynamic(:foo)
+                 # from: types_test.ex:LINE
+                 x = :foo
+
+             where "y" was given the type:
+
+                 # type: dynamic(:bar)
                  # from: types_test.ex:LINE
-                 x = {:ok, _}
+                 y = :bar
              """
     end
   end