From 6e0414bed98dc97ce77aa112aa2c1e127d89b88c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sat, 27 Dec 2025 17:42:09 +0100
Subject: [PATCH 01/13] Start tracking variable dependencies

---
 lib/elixir/lib/module/types/pattern.ex | 279 ++++++++++++++-----------
 1 file changed, 156 insertions(+), 123 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index ecfca9fd642..abde745adb6 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -166,44 +166,79 @@ defmodule Module.Types.Pattern do
     end)
   end
 
-  defp all_single_path?(vars, info, index) do
-    info
-    |> Map.get(index, [])
-    |> Enum.all?(fn version -> match?([_], Map.fetch!(vars, version)) end)
-  end
-
   defp of_pattern_recur(types, tag, pattern_info, stack, context, callback) do
-    {vars, info, _counter} = pattern_info
+    {args_paths, vars_paths, vars_deps} = 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)
-
     try do
+      # TODO: Remove this callback
       case callback.(types, changed, context) do
         {:ok, types, context} ->
-          of_pattern_recur(types, unchangeable, vars, info, tag, stack, context, callback)
+          {changed, context} =
+            Enum.reduce(args_paths, {[], context}, fn {version, paths}, {changed, context} ->
+              {var_changed?, context} =
+                Enum.reduce(paths, {false, context}, fn
+                  [var, {:arg, index, expr} | path], {var_changed?, context} ->
+                    actual = Enum.fetch!(types, index)
+
+                    case of_pattern_var(path, actual, context) do
+                      {:ok, 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
+                          {var_changed?, context}
+                        else
+                          _ ->
+                            case Of.refine_head_var(var, type, expr, stack, context) do
+                              {:ok, _type, context} -> {true, context}
+                              {:error, _type, context} -> throw({types, context})
+                            end
+                        end
+
+                      :error ->
+                        throw({types, badpattern_error(expr, index, tag, stack, context)})
+                    end
+                end)
+
+              case var_changed? do
+                true -> {[version | changed], context}
+                false -> {changed, context}
+              end
+            end)
+
+          try do
+            {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
+          catch
+            {:error, context} -> {types, error_vars(vars_paths, context)}
+          end
 
         {:error, context} ->
-          {types, error_vars(vars, context)}
+          {types, error_vars(vars_paths, context)}
       end
     catch
-      {types, context} -> {types, error_vars(vars, context)}
+      {types, context} -> {types, error_vars(vars_paths, 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, _tag, _stack, context) do
+    context
+  end
+
+  defp of_pattern_var_deps(previous_changed, vars_paths, vars_deps, tag, stack, context) do
     {changed, context} =
-      Enum.reduce(vars, {[], context}, fn {version, paths}, {changed, context} ->
+      Enum.reduce(previous_changed, {[], context}, fn version, {changed, context} ->
+        paths = Map.get(vars_paths, version, [])
+
         {var_changed?, context} =
           Enum.reduce(paths, {false, context}, fn
-            [var, {:arg, index, expr} | path], {var_changed?, context} ->
-              actual = Enum.fetch!(types, index)
-
-              case of_pattern_var(path, actual, true, info, context) do
-                {type, reachable_var?} ->
+            [var, tree | path], {var_changed?, context} ->
+              # TODO: temporary
+              expr = var
+              index = 0
+              actual = of_pattern_tree(tree, context)
+
+              case of_pattern_var(path, actual, context) do
+                {:ok, 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
@@ -211,48 +246,42 @@ defmodule Module.Types.Pattern do
                   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})
+                        {:ok, _type, context} -> {true, context}
+                        {:error, _type, context} -> throw({:error, context})
                       end
                   end
 
                 :error ->
-                  throw({types, badpattern_error(expr, index, tag, stack, context)})
+                  throw({:error, badpattern_error(expr, index, tag, 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}
+          false -> {changed, context}
+          true -> {[version | changed], context}
         end
       end)
 
-    case :lists.usort(changed) -- unchangeable do
-      [] ->
-        {types, context}
-
-      changed ->
-        case callback.(types, changed, context) do
-          # A simple structural comparison for optimization
-          {:ok, ^types, context} ->
-            {types, context}
-
-          {:ok, types, context} ->
-            of_pattern_recur(types, unchangeable, vars, info, tag, stack, context, callback)
-
-          {:error, context} ->
-            {types, error_vars(vars, context)}
-        end
-    end
+    changed
+    |> Enum.reduce(%{}, fn version, acc ->
+      case vars_deps do
+        %{^version => deps} -> Map.merge(acc, deps)
+        %{} -> acc
+      end
+    end)
+    |> Map.keys()
+    |> Kernel.--(previous_changed)
+    |> of_pattern_var_deps(vars_paths, vars_deps, tag, stack, context)
   end
 
-  defp error_vars(vars, context) do
-    Enum.reduce(vars, context, fn {_version, [[var | _path] | _paths]}, context ->
-      Of.error_var(var, context)
+  defp error_vars(vars_paths, context) do
+    Enum.reduce(vars_paths, context, fn {version, [[var | _path] | _paths]}, context ->
+      # TODO: ew
+      if is_integer(version) do
+        Of.error_var(var, context)
+      else
+        context
+      end
     end)
   end
 
@@ -278,46 +307,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
@@ -420,11 +444,26 @@ defmodule Module.Types.Pattern do
 
   # left = right
   defp of_pattern({:=, _meta, [_, _]} = match, path, stack, context) do
-    result =
+    {match, 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_var(&1)))
+      |> case do
+        {match, []} ->
+          version = make_ref()
+          {match, version, {:temp, [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_pattern(var, path, stack, context)
+
+    {static, dynamic, context} =
+      Enum.reduce(match, {[], [], context}, fn pattern, {static, dynamic, context} ->
+        {type, context} = of_pattern(pattern, [{:var, version}], stack, context)
 
         if is_descr(type) do
           {[type | static], dynamic, context}
@@ -433,16 +472,15 @@ defmodule Module.Types.Pattern do
         end
       end)
 
-    case result do
-      {[], dynamic, context} ->
-        {{:intersection, dynamic}, context}
-
-      {static, [], context} ->
-        {Enum.reduce(static, &intersection/2), context}
+    intersection =
+      cond do
+        static == [] -> {:intersection, dynamic}
+        dynamic == [] -> Enum.reduce(static, &intersection/2)
+        true -> {:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}
+      end
 
-      {static, dynamic, context} ->
-        {{:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}, context}
-    end
+    # But also build the new path with the intersection
+    of_pattern(var, [intersection], stack, context)
   end
 
   # %Struct{...}
@@ -544,15 +582,29 @@ defmodule Module.Types.Pattern do
   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, _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)
+    {args_paths, vars_paths, vars_deps} = context.pattern_info
+
+    pattern_info =
+      case Enum.reverse(reverse_path) do
+        [{:arg, _index, _pattern} | _] = path ->
+          paths = [[var | path] | Map.get(args_paths, version, [])]
+          args_paths = Map.put(args_paths, version, paths)
+          {args_paths, vars_paths, vars_deps}
+
+        [{:var, other} | _] = path ->
+          paths = [[var | path] | 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}
+
+        path ->
+          paths = [[var | path] | 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}}}
+    {{:var, version}, %{context | pattern_info: pattern_info}}
   end
 
   # TODO: Properly traverse domain keys
@@ -607,45 +659,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)
 
-    case {static, dynamic} do
-      {static, []} when is_descr(suffix) ->
+        if is_descr(type) do
+          {[type | static], dynamic, context}
+        else
+          {static, [type | dynamic], context}
+        end
+      end)
+
+    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
@@ -764,7 +797,7 @@ defmodule Module.Types.Pattern do
   # arguments and list heads, and a counter used to compute
   # the number of list heads.
   defp init_pattern_info(context) do
-    %{context | pattern_info: {%{}, %{}, 1}}
+    %{context | pattern_info: {%{}, %{}, %{}}}
   end
 
   defp pop_pattern_info(%{pattern_info: pattern_info} = context) do

From a8911a08a8ebeff7a33112cea14420733be067e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sat, 27 Dec 2025 19:04:02 +0100
Subject: [PATCH 02/13] Progress

---
 lib/elixir/lib/module/types/pattern.ex | 113 ++++++++++---------------
 1 file changed, 45 insertions(+), 68 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index abde745adb6..87665d0d3c5 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -63,9 +63,13 @@ defmodule Module.Types.Pattern do
     {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)
+      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} ->
+          {expected, error_vars(pattern_info, context)}
+      end
 
     {trees, 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
 
@@ -158,65 +147,54 @@ 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)
+    case of_pattern_intersect(tree, expected, expr, 0, tag, stack, context) do
+      {:ok, type, context} ->
+        of_pattern_recur([type], tag, pattern_info, stack, context)
+
+      {:error, context} ->
+        {[expected], error_vars(pattern_info, context)}
+    end
   end
 
-  defp of_pattern_recur(types, tag, pattern_info, stack, context, callback) do
+  defp of_pattern_recur(types, tag, pattern_info, stack, context) do
     {args_paths, vars_paths, vars_deps} = pattern_info
-    changed = :lists.seq(0, length(types) - 1)
 
     try do
-      # TODO: Remove this callback
-      case callback.(types, changed, context) do
-        {:ok, types, context} ->
-          {changed, context} =
-            Enum.reduce(args_paths, {[], context}, fn {version, paths}, {changed, context} ->
-              {var_changed?, context} =
-                Enum.reduce(paths, {false, context}, fn
-                  [var, {:arg, index, expr} | path], {var_changed?, context} ->
-                    actual = Enum.fetch!(types, index)
-
-                    case of_pattern_var(path, actual, context) do
-                      {:ok, 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
-                          {var_changed?, context}
-                        else
-                          _ ->
-                            case Of.refine_head_var(var, type, expr, stack, context) do
-                              {:ok, _type, context} -> {true, context}
-                              {:error, _type, context} -> throw({types, context})
-                            end
+      {changed, context} =
+        Enum.reduce(args_paths, {[], context}, fn {version, paths}, {changed, context} ->
+          {var_changed?, context} =
+            Enum.reduce(paths, {false, context}, fn
+              [var, {:arg, index, expr} | path], {var_changed?, context} ->
+                actual = Enum.fetch!(types, index)
+
+                case of_pattern_var(path, actual, context) do
+                  {:ok, 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
+                      {var_changed?, context}
+                    else
+                      _ ->
+                        case Of.refine_head_var(var, type, expr, stack, context) do
+                          {:ok, _type, context} -> {true, context}
+                          {:error, _type, context} -> throw({types, context})
                         end
-
-                      :error ->
-                        throw({types, badpattern_error(expr, index, tag, stack, context)})
                     end
-                end)
 
-              case var_changed? do
-                true -> {[version | changed], context}
-                false -> {changed, context}
-              end
+                  :error ->
+                    throw({types, badpattern_error(expr, index, tag, stack, context)})
+                end
             end)
 
-          try do
-            {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
-          catch
-            {:error, context} -> {types, error_vars(vars_paths, context)}
+          case var_changed? do
+            true -> {[version | changed], context}
+            false -> {changed, context}
           end
+        end)
 
-        {:error, context} ->
-          {types, error_vars(vars_paths, context)}
-      end
+      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
     catch
-      {types, context} -> {types, error_vars(vars_paths, context)}
+      {types, context} -> {types, error_vars(pattern_info, context)}
     end
   end
 
@@ -270,11 +248,10 @@ defmodule Module.Types.Pattern do
       end
     end)
     |> Map.keys()
-    |> Kernel.--(previous_changed)
     |> of_pattern_var_deps(vars_paths, vars_deps, tag, stack, context)
   end
 
-  defp error_vars(vars_paths, context) do
+  defp error_vars({_args_paths, vars_paths, _vars_deps}, context) do
     Enum.reduce(vars_paths, context, fn {version, [[var | _path] | _paths]}, context ->
       # TODO: ew
       if is_integer(version) do

From 5994bfc0e2f48113318effbbe7906dff8fd96a3b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 28 Dec 2025 19:13:01 +0100
Subject: [PATCH 03/13] Slow progress

---
 lib/elixir/lib/module/types/descr.ex          |  4 +-
 lib/elixir/lib/module/types/pattern.ex        | 87 +++++++++----------
 .../test/elixir/module/types/pattern_test.exs | 16 ++++
 3 files changed, 59 insertions(+), 48 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 1339a70e043..4fa5d838748 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/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 87665d0d3c5..ded81ea56e2 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -75,7 +75,7 @@ defmodule Module.Types.Pattern do
   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
@@ -114,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}
@@ -136,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} =
@@ -161,24 +161,17 @@ defmodule Module.Types.Pattern do
 
     try do
       {changed, context} =
-        Enum.reduce(args_paths, {[], context}, fn {version, paths}, {changed, context} ->
-          {var_changed?, context} =
-            Enum.reduce(paths, {false, context}, fn
-              [var, {:arg, index, expr} | path], {var_changed?, context} ->
+        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)
 
                 case of_pattern_var(path, actual, context) do
                   {:ok, 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
-                      {var_changed?, context}
-                    else
-                      _ ->
-                        case Of.refine_head_var(var, type, expr, stack, context) do
-                          {:ok, _type, context} -> {true, context}
-                          {:error, _type, context} -> throw({types, context})
-                        end
+                    case Of.refine_head_var(var, type, expr, stack, context) do
+                      {:ok, _type, context} -> context
+                      {:error, _type, context} -> throw({types, context})
                     end
 
                   :error ->
@@ -186,10 +179,7 @@ defmodule Module.Types.Pattern do
                 end
             end)
 
-          case var_changed? do
-            true -> {[version | changed], context}
-            false -> {changed, context}
-          end
+          {version, context}
         end)
 
       {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
@@ -209,11 +199,9 @@ defmodule Module.Types.Pattern do
 
         {var_changed?, context} =
           Enum.reduce(paths, {false, context}, fn
-            [var, tree | path], {var_changed?, context} ->
-              # TODO: temporary
-              expr = var
+            %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
               index = 0
-              actual = of_pattern_tree(tree, context)
+              actual = of_pattern_tree(root, context)
 
               case of_pattern_var(path, actual, context) do
                 {:ok, type} ->
@@ -251,15 +239,14 @@ defmodule Module.Types.Pattern do
     |> of_pattern_var_deps(vars_paths, vars_deps, tag, stack, context)
   end
 
-  defp error_vars({_args_paths, vars_paths, _vars_deps}, context) do
-    Enum.reduce(vars_paths, context, fn {version, [[var | _path] | _paths]}, context ->
-      # TODO: ew
-      if is_integer(version) do
-        Of.error_var(var, context)
-      else
-        context
-      end
-    end)
+  defp error_vars({args_paths, vars_paths, _vars_deps}, context) do
+    callback = fn {_, [%{var: var} | _paths]}, context ->
+      Of.error_var(var, context)
+    end
+
+    context = Enum.reduce(args_paths, context, callback)
+    context = Enum.reduce(vars_paths, context, callback)
+    context
   end
 
   defp badpattern_error(expr, index, tag, stack, context) do
@@ -436,11 +423,12 @@ defmodule Module.Types.Pattern do
       end
 
     # Pass the current path to build the current var
-    {_, context} = of_pattern(var, path, stack, context)
+    {expr, context} = of_var(var, version, path, context)
+    root = %{root: {:var, version}, expr: expr}
 
     {static, dynamic, context} =
       Enum.reduce(match, {[], [], context}, fn pattern, {static, dynamic, context} ->
-        {type, context} = of_pattern(pattern, [{:var, version}], stack, context)
+        {type, context} = of_pattern(pattern, [root], stack, context)
 
         if is_descr(type) do
           {[type | static], dynamic, context}
@@ -457,7 +445,7 @@ defmodule Module.Types.Pattern do
       end
 
     # But also build the new path with the intersection
-    of_pattern(var, [intersection], stack, context)
+    of_pattern(var, [%{root: intersection, expr: expr}], stack, context)
   end
 
   # %Struct{...}
@@ -556,32 +544,39 @@ 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)
+    {_, context} = of_var(var, version, path, context)
+    {{:var, version}, context}
+  end
+
+  defp of_var(var, version, reverse_path, context) do
     {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 Enum.reverse(reverse_path) do
-        [{:arg, _index, _pattern} | _] = path ->
-          paths = [[var | path] | Map.get(args_paths, version, [])]
+      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} | _] = path ->
-          paths = [[var | path] | Map.get(vars_paths, version, [])]
+        {: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}
 
-        path ->
-          paths = [[var | path] | Map.get(vars_paths, version, [])]
+        _ ->
+          paths = [node | Map.get(vars_paths, version, [])]
           vars_paths = Map.put(vars_paths, version, paths)
           {args_paths, vars_paths, vars_deps}
       end
 
-    {{:var, version}, %{context | pattern_info: pattern_info}}
+    {expr, %{context | pattern_info: pattern_info}}
   end
 
   # TODO: Properly traverse domain keys
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 626c4c91478..104dc3f9f8a 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -117,6 +117,22 @@ defmodule Module.Types.PatternTest do
     end
 
     test "reports incompatible types" do
+      assert typeerror!([x = {:ok, _} = {:error, _, _}], x) == ~l"""
+             the following pattern will never match:
+
+                 [_ | _] = x
+
+             because the right-hand side has type:
+
+                 dynamic({:ok, term()})
+
+             where "x" was given the type:
+
+                 # type: dynamic({:ok, term()})
+                 # from: types_test.ex:LINE
+                 x = {:ok, _}
+             """
+
       assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""
              the following pattern will never match:
 

From 72f26464f07d91dd37ba81da228212a33906b104 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 28 Dec 2025 19:40:51 +0100
Subject: [PATCH 04/13] More progress

---
 lib/elixir/lib/module/types/pattern.ex | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index ded81ea56e2..5b145aa1fa0 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -437,15 +437,20 @@ defmodule Module.Types.Pattern do
         end
       end)
 
-    intersection =
-      cond do
-        static == [] -> {:intersection, dynamic}
-        dynamic == [] -> Enum.reduce(static, &intersection/2)
-        true -> {:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}
-      end
+    if dynamic == [] do
+      {Enum.reduce(static, &intersection/2), context}
+    else
+      # The dynamic parts have to be recomputed whenever they change
+      {var, context} =
+        of_pattern(var, [%{root: {:intersection, dynamic}, expr: expr}], stack, context)
 
-    # But also build the new path with the intersection
-    of_pattern(var, [%{root: intersection, expr: expr}], stack, context)
+      # But the static parts we push down as part of the argument intersection
+      if static == [] do
+        {var, context}
+      else
+        {{:intersection, [var, Enum.reduce(static, &intersection/2)]}, context}
+      end
+    end
   end
 
   # %Struct{...}

From 39494ca56abaaf2f9ba8a63a83060f9f39f4dfd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 28 Dec 2025 22:47:10 +0100
Subject: [PATCH 05/13] More refine var

---
 lib/elixir/lib/module/types/of.ex      | 20 +---------
 lib/elixir/lib/module/types/pattern.ex | 53 +++++++++++++++++++++-----
 2 files changed, 45 insertions(+), 28 deletions(-)

diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index cec8fdcff02..ccb12687cbd 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -100,8 +100,7 @@ defmodule Module.Types.Of do
 
         # 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)}
+          {:error, old_type, context}
         else
           {:ok, new_type, context}
         end
@@ -546,23 +545,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 5b145aa1fa0..4671b02b0b4 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -170,8 +170,11 @@ defmodule Module.Types.Pattern do
                 case of_pattern_var(path, actual, context) do
                   {:ok, type} ->
                     case Of.refine_head_var(var, type, expr, stack, context) do
-                      {:ok, _type, context} -> context
-                      {:error, _type, context} -> throw({types, context})
+                      {:ok, _type, context} ->
+                        context
+
+                      {:error, old_type, context} ->
+                        throw({types, refine_error(var, old_type, type, stack, context)})
                     end
 
                   :error ->
@@ -182,7 +185,11 @@ defmodule Module.Types.Pattern do
           {version, context}
         end)
 
-      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
+      try do
+        {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
+      catch
+        {:error, context} -> {types, context}
+      end
     catch
       {types, context} -> {types, error_vars(pattern_info, context)}
     end
@@ -212,8 +219,11 @@ defmodule Module.Types.Pattern do
                   else
                     _ ->
                       case Of.refine_head_var(var, type, expr, stack, context) do
-                        {:ok, _type, context} -> {true, context}
-                        {:error, _type, context} -> throw({:error, context})
+                        {:ok, _type, context} ->
+                          {true, context}
+
+                        {:error, old_type, context} ->
+                          throw({:error, refine_error(var, old_type, type, stack, context)})
                       end
                   end
 
@@ -249,6 +259,10 @@ defmodule Module.Types.Pattern do
     context
   end
 
+  defp refine_error({_, meta, _} = var, old_type, type, stack, context) do
+    error(__MODULE__, {:badvar, old_type, type, var, context}, meta, stack, context)
+  end
+
   defp badpattern_error(expr, index, tag, stack, context) do
     meta =
       if meta = get_meta(expr) do
@@ -361,8 +375,13 @@ 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}
+    case Of.refine_head_var(var, expected, expr, stack, context) do
+      {:ok, type, context} ->
+        {type, context}
+
+      {:error, old_type, context} ->
+        {error_type(), refine_error(var, old_type, expected, stack, context)}
+    end
   end
 
   def of_match_var({:<<>>, _meta, args}, _expected, _expr, stack, context) do
@@ -415,7 +434,7 @@ defmodule Module.Types.Pattern do
       |> case do
         {match, []} ->
           version = make_ref()
-          {match, version, {:temp, [version: version], __MODULE__}}
+          {match, version, {:match, [version: version], __MODULE__}}
 
         {pre, [{_, meta, _} = var | post]} ->
           version = Keyword.fetch!(meta, :version)
@@ -454,7 +473,6 @@ defmodule Module.Types.Pattern do
   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)
@@ -781,6 +799,23 @@ defmodule Module.Types.Pattern do
     {pattern_info, %{context | pattern_info: nil}}
   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)
 

From a7164bd0dc1cc3747899a050bf1d1850b2513602 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 28 Dec 2025 22:57:02 +0100
Subject: [PATCH 06/13] More progress

---
 lib/elixir/lib/module/types/pattern.ex        | 10 +++--
 .../test/elixir/module/types/pattern_test.exs | 40 ++++++++++++-------
 2 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 4671b02b0b4..770f2dae028 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -188,7 +188,7 @@ defmodule Module.Types.Pattern do
       try do
         {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
       catch
-        {:error, context} -> {types, context}
+        {:error, context} -> {types, error_vars(pattern_info, context)}
       end
     catch
       {types, context} -> {types, error_vars(pattern_info, context)}
@@ -250,15 +250,16 @@ defmodule Module.Types.Pattern do
   end
 
   defp error_vars({args_paths, vars_paths, _vars_deps}, context) do
-    callback = fn {_, [%{var: var} | _paths]}, context ->
+    callback = fn [%{var: var} | _paths], context ->
       Of.error_var(var, context)
     end
 
-    context = Enum.reduce(args_paths, context, callback)
-    context = Enum.reduce(vars_paths, context, callback)
+    context = Enum.reduce(Map.values(args_paths), context, callback)
+    context = Enum.reduce(Map.values(vars_paths), context, callback)
     context
   end
 
+  # TODO: May pass the expression as well for more context
   defp refine_error({_, meta, _} = var, old_type, type, stack, context) do
     error(__MODULE__, {:badvar, old_type, type, var, context}, meta, stack, context)
   end
@@ -799,6 +800,7 @@ defmodule Module.Types.Pattern do
     {pattern_info, %{context | pattern_info: nil}}
   end
 
+  # TODO: Deal when new_type is none()
   def format_diagnostic({:badvar, old_type, new_type, var, context}) do
     traces = collect_traces(var, context)
 
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 104dc3f9f8a..d00850e1992 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -54,21 +54,19 @@ defmodule Module.Types.PatternTest do
     test "errors on conflicting refinements" do
       assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) ==
                ~l"""
-               the following pattern will never match:
+               incompatible types assigned to "a":
 
-                   a = b
+                   dynamic(:foo) !~ dynamic(:bar)
 
-               where "a" was given the type:
+               where "a" was given the types:
 
                    # type: dynamic(:foo)
-                   # from: types_test.ex:LINE-1
+                   # from: types_test.ex:55
                    a = :foo
 
-               where "b" was given the type:
-
                    # type: dynamic(:bar)
-                   # from: types_test.ex:LINE-1
-                   b = :bar
+                   # from: types_test.ex:55
+                   a = b
                """
     end
 
@@ -120,17 +118,31 @@ defmodule Module.Types.PatternTest do
       assert typeerror!([x = {:ok, _} = {:error, _, _}], x) == ~l"""
              the following pattern will never match:
 
-                 [_ | _] = x
+                 x = {:ok, _} = {:error, _, _}
+             """
 
-             because the right-hand side has type:
+      assert typeerror!([x = {:ok, y} = {:error, z, w}], {x, y, z, w}) == ~l"""
+             incompatible types assigned to "x":
 
-                 dynamic({:ok, term()})
+                 dynamic() !~ none()
 
              where "x" was given the type:
 
-                 # type: dynamic({:ok, term()})
-                 # from: types_test.ex:LINE
-                 x = {:ok, _}
+                 # type: none()
+                 # from: types_test.ex:124
+                 x = {:ok, y} = {:error, z, w}
+             """
+
+      assert typeerror!([{:ok, y} = {:error, z, w}], {y, z, w}) == ~l"""
+             incompatible types assigned to "match" (context Module.Types.Pattern):
+
+                 dynamic() !~ none()
+
+             where "match" (context Module.Types.Pattern) was given the type:
+
+                 # type: none()
+                 # from: types_test.ex:136
+                 {:ok, y} = {:error, z, w}
              """
 
       assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""

From 303031c81c0522ae69831b8529e7eec8aba8bc69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 28 Dec 2025 23:16:40 +0100
Subject: [PATCH 07/13] Add failing test

---
 lib/elixir/test/elixir/module/types/pattern_test.exs | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index d00850e1992..39968ab3c34 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -114,6 +114,13 @@ defmodule Module.Types.PatternTest do
              ) == dynamic(tuple([atom([:foo]), integer()]))
     end
 
+    test "parallel match with map" do
+      assert typecheck!(
+               [%{key: value} = context = %{key: %{}}],
+               {context, value}
+             ) == dynamic(tuple([atom([:foo]), integer()]))
+    end
+
     test "reports incompatible types" do
       assert typeerror!([x = {:ok, _} = {:error, _, _}], x) == ~l"""
              the following pattern will never match:
@@ -129,7 +136,7 @@ defmodule Module.Types.PatternTest do
              where "x" was given the type:
 
                  # type: none()
-                 # from: types_test.ex:124
+                 # from: types_test.ex:LINE
                  x = {:ok, y} = {:error, z, w}
              """
 
@@ -141,7 +148,7 @@ defmodule Module.Types.PatternTest do
              where "match" (context Module.Types.Pattern) was given the type:
 
                  # type: none()
-                 # from: types_test.ex:136
+                 # from: types_test.ex:LINE
                  {:ok, y} = {:error, z, w}
              """
 

From 551de4fc6c1adddef00045bc328352834446e09f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Mon, 29 Dec 2025 12:27:01 +0100
Subject: [PATCH 08/13] All green

---
 lib/elixir/lib/module/types/pattern.ex        | 99 ++++++++++---------
 .../test/elixir/module/types/pattern_test.exs | 30 +++---
 2 files changed, 66 insertions(+), 63 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 770f2dae028..6dc7594446c 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -185,12 +185,15 @@ defmodule Module.Types.Pattern do
           {version, context}
         end)
 
-      try do
-        {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
-      catch
-        {:error, context} -> {types, error_vars(pattern_info, context)}
-      end
+      context =
+        Enum.reduce(changed, context, fn version, context ->
+          {_, context} = of_pattern_var_dep(vars_paths, version, tag, stack, context)
+          context
+        end)
+
+      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
     catch
+      {:error, context} -> {types, error_vars(pattern_info, context)}
       {types, context} -> {types, error_vars(pattern_info, context)}
     end
   end
@@ -201,36 +204,16 @@ defmodule Module.Types.Pattern do
 
   defp of_pattern_var_deps(previous_changed, vars_paths, vars_deps, tag, stack, context) do
     {changed, context} =
-      Enum.reduce(previous_changed, {[], context}, fn version, {changed, context} ->
-        paths = Map.get(vars_paths, version, [])
-
-        {var_changed?, context} =
-          Enum.reduce(paths, {false, context}, fn
-            %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
-              index = 0
-              actual = of_pattern_tree(root, context)
-
-              case of_pattern_var(path, actual, context) do
-                {:ok, 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
-                    {var_changed?, context}
-                  else
-                    _ ->
-                      case Of.refine_head_var(var, type, expr, stack, context) do
-                        {:ok, _type, context} ->
-                          {true, context}
-
-                        {:error, old_type, context} ->
-                          throw({:error, refine_error(var, old_type, type, stack, context)})
-                      end
-                  end
-
-                :error ->
-                  throw({:error, badpattern_error(expr, index, tag, stack, context)})
-              end
-          end)
+      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, tag, stack, context)
 
         case var_changed? do
           false -> {changed, context}
@@ -238,15 +221,38 @@ defmodule Module.Types.Pattern do
         end
       end)
 
-    changed
-    |> Enum.reduce(%{}, fn version, acc ->
-      case vars_deps do
-        %{^version => deps} -> Map.merge(acc, deps)
-        %{} -> acc
-      end
+    of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)
+  end
+
+  defp of_pattern_var_dep(vars_paths, version, tag, stack, context) do
+    paths = Map.get(vars_paths, version, [])
+
+    Enum.reduce(paths, {false, context}, fn
+      %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
+        index = 0
+        actual = of_pattern_tree(root, context)
+
+        case of_pattern_var(path, actual, context) do
+          {:ok, 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
+              {var_changed?, context}
+            else
+              _ ->
+                case Of.refine_head_var(var, type, expr, stack, context) do
+                  {:ok, _type, context} ->
+                    {true, context}
+
+                  {:error, old_type, context} ->
+                    throw({:error, refine_error(var, old_type, type, stack, context)})
+                end
+            end
+
+          :error ->
+            throw({:error, badpattern_error(expr, index, tag, stack, context)})
+        end
     end)
-    |> Map.keys()
-    |> of_pattern_var_deps(vars_paths, vars_deps, tag, stack, context)
   end
 
   defp error_vars({args_paths, vars_paths, _vars_deps}, context) do
@@ -431,7 +437,7 @@ defmodule Module.Types.Pattern do
     {match, version, var} =
       match
       |> unpack_match([])
-      |> Enum.split_while(&(not is_var(&1)))
+      |> Enum.split_while(&(not is_versioned_var(&1)))
       |> case do
         {match, []} ->
           version = make_ref()
@@ -575,6 +581,11 @@ defmodule Module.Types.Pattern do
     {{:var, version}, 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
     {args_paths, vars_paths, vars_deps} = context.pattern_info
     [%{root: root, expr: expr} | path] = Enum.reverse(reverse_path)
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 39968ab3c34..c568b48ffec 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -52,22 +52,21 @@ defmodule Module.Types.PatternTest do
     end
 
     test "errors on conflicting refinements" do
-      assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) ==
-               ~l"""
-               incompatible types assigned to "a":
+      assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) == ~l"""
+             incompatible types assigned to "a":
 
-                   dynamic(:foo) !~ dynamic(:bar)
+                 dynamic(:foo) !~ dynamic(:bar)
 
-               where "a" was given the types:
+             where "a" was given the types:
 
-                   # type: dynamic(:foo)
-                   # from: types_test.ex:55
-                   a = :foo
+                 # type: dynamic(:foo)
+                 # from: types_test.ex:LINE
+                 a = :foo
 
-                   # type: dynamic(:bar)
-                   # from: types_test.ex:55
-                   a = b
-               """
+                 # type: dynamic(:bar)
+                 # from: types_test.ex:LINE
+                 a = b
+             """
     end
 
     test "can be accessed even if they don't match" do
@@ -114,13 +113,6 @@ defmodule Module.Types.PatternTest do
              ) == dynamic(tuple([atom([:foo]), integer()]))
     end
 
-    test "parallel match with map" do
-      assert typecheck!(
-               [%{key: value} = context = %{key: %{}}],
-               {context, value}
-             ) == dynamic(tuple([atom([:foo]), integer()]))
-    end
-
     test "reports incompatible types" do
       assert typeerror!([x = {:ok, _} = {:error, _, _}], x) == ~l"""
              the following pattern will never match:

From 1bd258d3846ea3306ef916c988b3e9ced0e75412 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Mon, 29 Dec 2025 13:58:26 +0100
Subject: [PATCH 09/13] Progress

---
 lib/elixir/lib/module/types/helpers.ex        |   2 +-
 lib/elixir/lib/module/types/of.ex             |  44 +++++--
 lib/elixir/lib/module/types/pattern.ex        | 121 +++++++++++-------
 .../test/elixir/module/types/pattern_test.exs |   8 +-
 4 files changed, 112 insertions(+), 63 deletions(-)

diff --git a/lib/elixir/lib/module/types/helpers.ex b/lib/elixir/lib/module/types/helpers.ex
index d090d8e7c0a..e5b0e039038 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 ccb12687cbd..6fde95a8399 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -31,18 +31,36 @@ defmodule Module.Types.Of do
   @doc """
   Marks a variable with error.
   """
-  def error_var(var, context) do
+  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()}, :errored, true)
+    end)
+  end
+
+  @doc """
+  Declares a variable.
+  """
+  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
 
-    put_in(context.vars[version], data)
+      vars ->
+        data = %{
+          type: term(),
+          name: var_name,
+          context: var_context,
+          off_traces: []
+        }
+
+        %{context | vars: Map.put(vars, version, data)}
+    end
   end
 
   @doc """
@@ -56,7 +74,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 = %{
@@ -87,6 +105,9 @@ defmodule Module.Types.Of 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,12 +117,11 @@ 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
+          context = %{context | vars: %{vars | version => Map.put(data, :errored, true)}}
           {:error, old_type, context}
         else
+          context = %{context | vars: %{vars | version => data}}
           {:ok, new_type, context}
         end
 
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 6dc7594446c..c73bf7e6736 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -174,7 +174,7 @@ defmodule Module.Types.Pattern do
                         context
 
                       {:error, old_type, context} ->
-                        throw({types, refine_error(var, old_type, type, stack, context)})
+                        throw({types, badvar_error(var, old_type, type, expr, stack, context)})
                     end
 
                   :error ->
@@ -187,22 +187,21 @@ defmodule Module.Types.Pattern do
 
       context =
         Enum.reduce(changed, context, fn version, context ->
-          {_, context} = of_pattern_var_dep(vars_paths, version, tag, stack, context)
+          {_, context} = of_pattern_var_dep(vars_paths, version, stack, context)
           context
         end)
 
-      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)}
+      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, stack, context)}
     catch
-      {:error, context} -> {types, error_vars(pattern_info, context)}
       {types, context} -> {types, error_vars(pattern_info, context)}
     end
   end
 
-  defp of_pattern_var_deps([], _vars_paths, _vars_deps, _tag, _stack, context) 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, tag, stack, context) do
+  defp of_pattern_var_deps(previous_changed, vars_paths, vars_deps, stack, context) do
     {changed, context} =
       previous_changed
       |> Enum.reduce(%{}, fn version, acc ->
@@ -213,7 +212,7 @@ defmodule Module.Types.Pattern do
       end)
       |> Map.keys()
       |> Enum.reduce({[], context}, fn version, {changed, context} ->
-        {var_changed?, context} = of_pattern_var_dep(vars_paths, version, tag, stack, context)
+        {var_changed?, context} = of_pattern_var_dep(vars_paths, version, stack, context)
 
         case var_changed? do
           false -> {changed, context}
@@ -221,38 +220,45 @@ defmodule Module.Types.Pattern do
         end
       end)
 
-    of_pattern_var_deps(changed, vars_paths, vars_deps, tag, stack, context)
+    of_pattern_var_deps(changed, vars_paths, vars_deps, stack, context)
   end
 
-  defp of_pattern_var_dep(vars_paths, version, tag, stack, context) do
+  defp of_pattern_var_dep(vars_paths, version, stack, context) do
     paths = Map.get(vars_paths, version, [])
 
-    Enum.reduce(paths, {false, context}, fn
-      %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
-        index = 0
-        actual = of_pattern_tree(root, context)
-
-        case of_pattern_var(path, actual, context) do
-          {:ok, 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
-              {var_changed?, context}
-            else
-              _ ->
-                case Of.refine_head_var(var, type, expr, stack, context) do
-                  {:ok, _type, context} ->
-                    {true, context}
-
-                  {:error, old_type, context} ->
-                    throw({:error, refine_error(var, old_type, type, stack, context)})
-                end
-            end
+    case context.vars do
+      %{^version => %{type: current_type} = data} when not is_map_key(data, :errored) ->
+        try do
+          Enum.reduce(paths, {false, context}, fn
+            %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
+              actual = of_pattern_tree(root, context)
+
+              case of_pattern_var(path, actual, context) do
+                {:ok, type} ->
+                  # Optimization: if current type is already a subtype, there is nothing to refine.
+                  if current_type != term() and subtype?(current_type, type) do
+                    {var_changed?, context}
+                  else
+                    case Of.refine_head_var(var, type, expr, stack, context) do
+                      {:ok, _type, context} ->
+                        {true, context}
 
-          :error ->
-            throw({:error, badpattern_error(expr, index, tag, stack, context)})
+                      {:error, _, context} ->
+                        throw(badvar_error(var, current_type, type, expr, stack, context))
+                    end
+                  end
+
+                :error ->
+                  throw(badmatch_error(expr, stack, Of.error_var(var, context)))
+              end
+          end)
+        catch
+          context -> {false, context}
         end
-    end)
+
+      _ ->
+        {false, context}
+    end
   end
 
   defp error_vars({args_paths, vars_paths, _vars_deps}, context) do
@@ -265,22 +271,34 @@ defmodule Module.Types.Pattern do
     context
   end
 
-  # TODO: May pass the expression as well for more context
-  defp refine_error({_, meta, _} = var, old_type, type, stack, context) do
-    error(__MODULE__, {:badvar, old_type, type, var, context}, meta, stack, context)
+  defp badmatch_error(expr, stack, context) do
+    error(__MODULE__, {:badmatch, expr, context}, error_meta(expr, 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])
+  defp badvar_error({var_name, _, var_context} = var, old_type, new_type, expr, stack, context) do
+    error =
+      if var_name == :match and var_context == __MODULE__ do
+        {:badmatch, expr, context}
       else
-        stack.meta
+        {:badvar, old_type, new_type, var, context}
       end
 
+    error(__MODULE__, error, error_meta(var, stack), stack, context)
+  end
+
+  defp badpattern_error(expr, index, tag, stack, context) do
+    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)
@@ -387,7 +405,7 @@ defmodule Module.Types.Pattern do
         {type, context}
 
       {:error, old_type, context} ->
-        {error_type(), refine_error(var, old_type, expected, stack, context)}
+        {error_type(), badvar_error(var, old_type, expected, expr, stack, context)}
     end
   end
 
@@ -587,6 +605,7 @@ defmodule Module.Types.Pattern do
   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}
@@ -811,7 +830,23 @@ defmodule Module.Types.Pattern do
     {pattern_info, %{context | pattern_info: nil}}
   end
 
-  # TODO: Deal when new_type is none()
+  def format_diagnostic({:badmatch, expr, context}) do
+    traces = collect_traces(expr, context)
+
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          incompatible types in expression:
+
+              #{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)
 
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index c568b48ffec..21589006caf 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -133,14 +133,8 @@ defmodule Module.Types.PatternTest do
              """
 
       assert typeerror!([{:ok, y} = {:error, z, w}], {y, z, w}) == ~l"""
-             incompatible types assigned to "match" (context Module.Types.Pattern):
+             incompatible types in expression:
 
-                 dynamic() !~ none()
-
-             where "match" (context Module.Types.Pattern) was given the type:
-
-                 # type: none()
-                 # from: types_test.ex:LINE
                  {:ok, y} = {:error, z, w}
              """
 

From 0581d88644a1f61146f20eacc6682521f3130e15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Mon, 29 Dec 2025 15:48:33 +0100
Subject: [PATCH 10/13] More precision in error messages

---
 lib/elixir/lib/module/types/of.ex             |   8 +-
 lib/elixir/lib/module/types/pattern.ex        | 110 +++++++++---------
 .../test/elixir/module/types/pattern_test.exs |  16 +--
 3 files changed, 72 insertions(+), 62 deletions(-)

diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index 6fde95a8399..9fb46a67705 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -30,13 +30,16 @@ 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()}, :errored, true)
+      data -> Map.put(%{data | type: error_type(), off_traces: []}, :errored, true)
     end)
   end
 
@@ -118,7 +121,8 @@ defmodule Module.Types.Of do
         }
 
         if empty?(new_type) do
-          context = %{context | vars: %{vars | version => Map.put(data, :errored, true)}}
+          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}}
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index c73bf7e6736..b59685ef97e 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -62,13 +62,13 @@ defmodule Module.Types.Pattern do
     {trees, context} = of_pattern_args_index(patterns, 0, [], stack, context)
     {pattern_info, context} = pop_pattern_info(context)
 
-    {_, context} =
+    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} ->
-          {expected, error_vars(pattern_info, context)}
+          error_vars(pattern_info, context)
       end
 
     {trees, context}
@@ -149,7 +149,7 @@ defmodule Module.Types.Pattern do
   defp of_single_pattern_recur(expected, tag, tree, pattern_info, expr, stack, context) do
     case of_pattern_intersect(tree, expected, expr, 0, tag, stack, context) do
       {:ok, type, context} ->
-        of_pattern_recur([type], tag, pattern_info, stack, context)
+        {[type], of_pattern_recur([type], tag, pattern_info, stack, context)}
 
       {:error, context} ->
         {[expected], error_vars(pattern_info, context)}
@@ -160,40 +160,44 @@ defmodule Module.Types.Pattern do
     {args_paths, vars_paths, vars_deps} = pattern_info
 
     try do
-      {changed, context} =
-        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)
-
-                case of_pattern_var(path, actual, context) do
-                  {:ok, type} ->
-                    case Of.refine_head_var(var, type, expr, stack, context) do
-                      {:ok, _type, context} ->
-                        context
-
-                      {:error, old_type, context} ->
-                        throw({types, badvar_error(var, old_type, type, expr, stack, context)})
-                    end
-
-                  :error ->
-                    throw({types, badpattern_error(expr, index, tag, stack, context)})
-                end
-            end)
+      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)
 
-          {version, 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
 
-      context =
-        Enum.reduce(changed, context, fn version, context ->
-          {_, context} = of_pattern_var_dep(vars_paths, version, stack, context)
-          context
-        end)
+                :error ->
+                  throw(badpattern_error(expr, index, tag, stack, context))
+              end
+          end)
 
-      {types, of_pattern_var_deps(changed, vars_paths, vars_deps, stack, context)}
+        {version, context}
+      end)
     catch
-      {types, context} -> {types, error_vars(pattern_info, 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
 
@@ -227,29 +231,33 @@ defmodule Module.Types.Pattern do
     paths = Map.get(vars_paths, version, [])
 
     case context.vars do
-      %{^version => %{type: current_type} = data} when not is_map_key(data, :errored) ->
+      %{^version => %{type: old_type} = data} when not is_map_key(data, :errored) ->
         try do
           Enum.reduce(paths, {false, context}, fn
             %{var: var, expr: expr, root: root, path: path}, {var_changed?, context} ->
               actual = of_pattern_tree(root, context)
 
               case of_pattern_var(path, actual, context) do
-                {:ok, type} ->
+                {:ok, new_type} ->
                   # Optimization: if current type is already a subtype, there is nothing to refine.
-                  if current_type != term() and 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
+                    case Of.refine_head_var(var, new_type, expr, stack, context) do
                       {:ok, _type, context} ->
                         {true, context}
 
-                      {:error, _, context} ->
-                        throw(badvar_error(var, current_type, type, expr, stack, 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(badmatch_error(expr, stack, Of.error_var(var, context)))
+                  throw(badmatch_error(var, expr, stack, context))
               end
           end)
         catch
@@ -271,18 +279,16 @@ defmodule Module.Types.Pattern do
     context
   end
 
-  defp badmatch_error(expr, stack, context) do
+  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 badvar_error({var_name, _, var_context} = var, old_type, new_type, expr, stack, context) do
-    error =
-      if var_name == :match and var_context == __MODULE__ do
-        {:badmatch, expr, context}
-      else
-        {:badvar, old_type, new_type, 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
 
@@ -404,8 +410,8 @@ defmodule Module.Types.Pattern do
       {:ok, type, context} ->
         {type, context}
 
-      {:error, old_type, context} ->
-        {error_type(), badvar_error(var, old_type, expected, expr, stack, context)}
+      {:error, old_type, error_context} ->
+        {error_type(), badvar_error(var, old_type, expected, stack, error_context)}
     end
   end
 
@@ -838,7 +844,7 @@ defmodule Module.Types.Pattern do
       message:
         IO.iodata_to_binary([
           """
-          incompatible types in expression:
+          this match will never succeed due to incompatible types:
 
               #{expr_to_string(expr) |> indent(4)}
           """,
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 21589006caf..139620395fb 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -114,6 +114,12 @@ defmodule Module.Types.PatternTest do
     end
 
     test "reports incompatible types" do
+      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:
 
@@ -121,19 +127,13 @@ defmodule Module.Types.PatternTest do
              """
 
       assert typeerror!([x = {:ok, y} = {:error, z, w}], {x, y, z, w}) == ~l"""
-             incompatible types assigned to "x":
+             this match will never succeed due to incompatible types:
 
-                 dynamic() !~ none()
-
-             where "x" was given the type:
-
-                 # type: none()
-                 # from: types_test.ex:LINE
                  x = {:ok, y} = {:error, z, w}
              """
 
       assert typeerror!([{:ok, y} = {:error, z, w}], {y, z, w}) == ~l"""
-             incompatible types in expression:
+             this match will never succeed due to incompatible types:
 
                  {:ok, y} = {:error, z, w}
              """

From 1a58437b346be12ce4b7bff3836376b38b09a17c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Mon, 29 Dec 2025 19:17:29 +0100
Subject: [PATCH 11/13] Surface errors earlier whenever possible

---
 lib/elixir/lib/module/types/pattern.ex        | 26 ++++-----
 .../test/elixir/module/types/pattern_test.exs | 58 +++++++++----------
 2 files changed, 38 insertions(+), 46 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index b59685ef97e..becf56c4e8f 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -458,14 +458,14 @@ defmodule Module.Types.Pattern do
 
   # left = right
   defp of_pattern({:=, _meta, [_, _]} = match, path, stack, context) do
-    {match, version, var} =
+    {matches, version, var} =
       match
       |> unpack_match([])
       |> Enum.split_while(&(not is_versioned_var(&1)))
       |> case do
-        {match, []} ->
+        {matches, []} ->
           version = make_ref()
-          {match, version, {:match, [version: version], __MODULE__}}
+          {matches, version, {:match, [version: version], __MODULE__}}
 
         {pre, [{_, meta, _} = var | post]} ->
           version = Keyword.fetch!(meta, :version)
@@ -473,11 +473,11 @@ defmodule Module.Types.Pattern do
       end
 
     # Pass the current path to build the current var
-    {expr, context} = of_var(var, version, path, context)
-    root = %{root: {:var, version}, expr: expr}
+    context = of_var(var, version, path, context)
+    root = %{root: {:var, version}, expr: match}
 
     {static, dynamic, context} =
-      Enum.reduce(match, {[], [], context}, fn pattern, {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
@@ -491,14 +491,13 @@ defmodule Module.Types.Pattern do
       {Enum.reduce(static, &intersection/2), context}
     else
       # The dynamic parts have to be recomputed whenever they change
-      {var, context} =
-        of_pattern(var, [%{root: {:intersection, dynamic}, expr: expr}], stack, context)
+      context = of_var(var, version, [%{root: {:intersection, dynamic}, expr: match}], context)
 
-      # But the static parts we push down as part of the argument intersection
+      # And everything else is also pushed as part of the argument intersection
       if static == [] do
-        {var, context}
+        {{:intersection, dynamic}, context}
       else
-        {{:intersection, [var, Enum.reduce(static, &intersection/2)]}, context}
+        {{:intersection, [Enum.reduce(static, &intersection/2) | dynamic]}, context}
       end
     end
   end
@@ -601,8 +600,7 @@ defmodule Module.Types.Pattern do
   defp of_pattern({name, meta, ctx} = var, path, _stack, context)
        when is_atom(name) and is_atom(ctx) do
     version = Keyword.fetch!(meta, :version)
-    {_, context} = of_var(var, version, path, context)
-    {{:var, version}, context}
+    {{: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 != :_,
@@ -636,7 +634,7 @@ defmodule Module.Types.Pattern do
           {args_paths, vars_paths, vars_deps}
       end
 
-    {expr, %{context | pattern_info: pattern_info}}
+    %{context | pattern_info: pattern_info}
   end
 
   # TODO: Properly traverse domain keys
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 139620395fb..8a3073e25b3 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -51,24 +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"""
-             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
-             """
-    end
-
     test "can be accessed even if they don't match" do
       assert typeerror!(
                (
@@ -126,32 +108,44 @@ defmodule Module.Types.PatternTest do
                  x = {:ok, _} = {:error, _, _}
              """
 
-      assert typeerror!([x = {:ok, y} = {:error, z, w}], {x, y, z, w}) == ~l"""
-             this match will never succeed due to incompatible types:
+      assert typeerror!([{x = {:ok, y} = {:error, z, w}}], {x, y, z, w}) == ~l"""
+             the following pattern will never match:
 
-                 x = {:ok, y} = {:error, z, w}
+                 {x = {:ok, y} = {:error, z, w}}
              """
 
-      assert typeerror!([{:ok, y} = {:error, z, w}], {y, z, w}) == ~l"""
-             this match will never succeed due to incompatible types:
+      assert typeerror!([a = b, a = :foo, b = :bar], {a, b}) == ~l"""
+             incompatible types assigned to "a":
 
-                 {:ok, y} = {:error, z, w}
-             """
+                 dynamic(:foo) !~ dynamic(:bar)
 
-      assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""
-             the following pattern will never match:
+             where "a" was given the types:
 
-                 [_ | _] = x
+                 # 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

From e2b3119d9d2a7a0fb778d870c47859b815ff97c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Mon, 29 Dec 2025 20:37:58 +0100
Subject: [PATCH 12/13] Always declare vars upfront

---
 lib/elixir/lib/module/types/expr.ex    |  1 +
 lib/elixir/lib/module/types/of.ex      | 14 +-------------
 lib/elixir/lib/module/types/pattern.ex |  2 ++
 3 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 7c8e37f7850..33cd84681a2 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/of.ex b/lib/elixir/lib/module/types/of.ex
index 9fb46a67705..9591dcc7735 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -103,8 +103,7 @@ 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
@@ -128,17 +127,6 @@ defmodule Module.Types.Of do
           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
 
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index becf56c4e8f..7e248a7afcb 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -406,6 +406,8 @@ defmodule Module.Types.Pattern do
   end
 
   def of_match_var(var, expected, expr, stack, context) when is_var(var) do
+    context = Of.declare_var(var, context)
+
     case Of.refine_head_var(var, expected, expr, stack, context) do
       {:ok, type, context} ->
         {type, context}

From cdd69909109ceafd994dd334981b2f2fa58a6c0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Tue, 30 Dec 2025 10:10:54 +0100
Subject: [PATCH 13/13] TODO

---
 lib/elixir/lib/module/types/pattern.ex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 7e248a7afcb..3150f4ce1e9 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -828,6 +828,7 @@ 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: {%{}, %{}, %{}}}
   end