From a2f17becfec8266612b0995a2d0155a5eca7a4fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 8 Mar 2026 16:27:14 +0100
Subject: [PATCH 1/4] Add subtype optimizations to eager literal difference

---
 lib/elixir/lib/module/types/descr.ex | 215 ++++++++++++++++-----------
 1 file changed, 128 insertions(+), 87 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 43e9446e9d6..1011037a0a0 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -2258,15 +2258,20 @@ defmodule Module.Types.Descr do
         do: :bdd_bot,
         else: bdd_leaf(list1, difference(last1, last2))
     else
-      bdd_difference(bdd1, bdd2, &list_leaf_disjoint?/2)
+      bdd_difference(bdd1, bdd2, &list_leaf_compare/2)
     end
   end
 
   defp list_difference(bdd1, bdd2),
-    do: bdd_difference(bdd1, bdd2, &list_leaf_disjoint?/2)
+    do: bdd_difference(bdd1, bdd2, &list_leaf_compare/2)
 
-  defp list_leaf_disjoint?(bdd_leaf(list1, last1), bdd_leaf(list2, last2)),
-    do: disjoint?(list1, list2) or disjoint?(last1, last2)
+  defp list_leaf_compare(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
+    if disjoint?(list1, list2) or disjoint?(last1, last2) do
+      :disjoint
+    else
+      :none
+    end
+  end
 
   defp list_empty?(@non_empty_list_top), do: false
 
@@ -2969,13 +2974,13 @@ defmodule Module.Types.Descr do
         end
 
       _ when is_atom(tag) and is_atom(neg_tag) ->
-        case map_difference_strategy(fields, neg_fields, tag, neg_tag, :all_equal) do
-          :all_equal when tag == neg_tag or neg_tag == :open ->
-            :bdd_bot
-
+        case map_difference_strategy(fields, neg_fields, tag, neg_tag) do
           :disjoint ->
             bdd_leaf(tag, fields)
 
+          :left_subtype_of_right ->
+            :bdd_bot
+
           {:one_key_difference, key, v1, v2} ->
             t_diff = difference(fields_get(fields, key, v1), v2)
 
@@ -2985,38 +2990,28 @@ defmodule Module.Types.Descr do
               bdd_leaf(tag, fields_store(key, t_diff, fields))
             end
 
-          :left_subtype_of_right ->
-            :bdd_bot
-
           _ ->
             bdd_difference(map1, map2)
         end
 
       _ ->
-        bdd_difference(map1, map2, &map_leaf_disjoint?/2)
+        bdd_difference(map1, map2, &map_leaf_compare/2)
     end
   end
 
   defp map_difference(bdd_leaf(:open, []), bdd2),
     do: bdd_negation(bdd2)
 
-  defp map_difference(bdd1, bdd2),
-    do: bdd_difference(bdd1, bdd2, &map_leaf_disjoint?/2)
-
-  defp map_leaf_disjoint?(bdd_leaf(_tag1, fields1), bdd_leaf(_tag2, fields2)) do
-    disjoint_structs?(fields1, fields2)
+  defp map_difference(bdd1, bdd2) do
+    bdd_difference(bdd1, bdd2, &map_leaf_compare/2)
   end
 
-  defp disjoint_structs?(fields1, fields2) do
-    case {fields_find(:__struct__, fields1), fields_find(:__struct__, fields2)} do
-      {{:ok, %{atom: atom} = d1}, {:ok, d2}} when map_size(d1) == 1 ->
-        disjoint_atom_descr?(atom, d2)
-
-      {{:ok, d1}, {:ok, %{atom: atom} = d2}} when map_size(d2) == 1 ->
-        disjoint_atom_descr?(atom, d1)
-
-      _ ->
-        false
+  defp map_leaf_compare(bdd_leaf(tag, fields), bdd_leaf(neg_tag, neg_fields)) do
+    case map_difference_strategy(fields, neg_fields, tag, neg_tag) do
+      :disjoint -> :disjoint
+      :left_subtype_of_right -> :subtype
+      {:one_key_difference, _, v1, v2} -> if subtype?(v1, v2), do: :subtype, else: :none
+      _ -> :none
     end
   end
 
@@ -4361,10 +4356,7 @@ defmodule Module.Types.Descr do
       if empty_intersection? do
         {acc_fields, acc_negs}
       else
-        case map_difference_strategy(acc_fields, neg_fields, tag, neg_tag, :all_equal) do
-          :all_equal when tag == neg_tag or neg_tag == :open ->
-            {acc_fields, acc_negs}
-
+        case map_difference_strategy(acc_fields, neg_fields, tag, neg_tag) do
           {:one_key_difference, key, v1, v2} ->
             {fields_store(key, difference(v1, v2), acc_fields), acc_negs}
 
@@ -4378,13 +4370,27 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  defp map_difference_strategy([{k1, _} | t1], [{k2, _} | _] = l2, tag1, tag2, status)
+  defp map_difference_strategy(fields1, fields2, tag1, tag2) do
+    if is_atom(tag1) and is_atom(tag2) do
+      status = if tag1 == tag2 or tag2 == :open, do: :all_equal, else: :none
+      map_difference_strategy(fields1, fields2, tag1, tag2, status)
+    else
+      :none
+    end
+  end
+
+  defp map_difference_strategy([{k1, value} | t1], [{k2, _} | _] = l2, tag1, tag2, status)
        when k1 < k2 do
     # Left side has a key the right side does not have,
     # left can only be a subtype if the right side is open.
+    # If the right side is closed and the key is not optional, they are disjoint.
     case status do
-      _ when tag2 != :open ->
-        :none
+      _ when tag2 == :closed ->
+        if not is_optional_static(value) do
+          :disjoint
+        else
+          map_difference_strategy(t1, l2, tag1, tag2, :none)
+        end
 
       :all_equal ->
         map_difference_strategy(t1, l2, tag1, tag2, :left_subtype_of_right)
@@ -4402,11 +4408,15 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp map_difference_strategy([{k1, _} | _], [{k2, value} | _], tag1, _tag2, _status)
+  defp map_difference_strategy([{k1, _} | _] = l1, [{k2, value} | t2], tag1, tag2, _status)
        when k1 > k2 do
     # Right side has a key the left side does not have,
     # if left-side is closed, they are disjoint.
-    if tag1 == :closed and not is_optional_static(value), do: :disjoint, else: :none
+    if tag1 == :closed and not is_optional_static(value) do
+      :disjoint
+    else
+      map_difference_strategy(l1, t2, tag1, tag2, :none)
+    end
   end
 
   defp map_difference_strategy([{_, v} | t1], [{_, v} | t2], tag1, tag2, status) do
@@ -4430,20 +4440,19 @@ defmodule Module.Types.Descr do
             :none
           end
 
-        # all_equal or left_subtype_of_right
         _ ->
-          if subtype?(v1, v2),
+          if status in [:all_equal, :left_subtype_of_right] and subtype?(v1, v2),
             do: map_difference_strategy(t1, t2, tag1, tag2, :left_subtype_of_right),
-            else: :none
+            else: map_difference_strategy(t1, t2, tag1, tag2, :none)
       end
     end
   end
 
   defp map_difference_strategy([], [], _tag1, _tag2, status) do
-    status
+    if status == :all_equal, do: :left_subtype_of_right, else: status
   end
 
-  defp map_difference_strategy(_l1, l2, tag1, tag2, status) do
+  defp map_difference_strategy(l1, l2, tag1, tag2, status) do
     cond do
       tag2 == :open and l2 == [] ->
         case status do
@@ -4455,11 +4464,17 @@ defmodule Module.Types.Descr do
 
           :left_subtype_of_right ->
             :left_subtype_of_right
+
+          :none ->
+            :none
         end
 
       tag1 == :closed and l2 != [] and Enum.all?(l2, fn {_, v} -> not is_optional_static(v) end) ->
         :disjoint
 
+      tag2 == :closed and l1 != [] and Enum.all?(l1, fn {_, v} -> not is_optional_static(v) end) ->
+        :disjoint
+
       true ->
         :none
     end
@@ -4816,11 +4831,15 @@ defmodule Module.Types.Descr do
     do: bdd_negation(bdd2)
 
   defp tuple_difference(bdd1, bdd2),
-    do: bdd_difference(bdd1, bdd2, &tuple_leaf_disjoint?/2)
+    do: bdd_difference(bdd1, bdd2, &tuple_leaf_compare?/2)
 
-  defp tuple_leaf_disjoint?(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
-    mismatched_tuple_sizes?(tag1, elements1, tag2, elements2) or
-      disjoint_tagged_tuples?(elements1, elements2)
+  defp tuple_leaf_compare?(bdd_leaf(tag1, elements1), bdd_leaf(tag2, elements2)) do
+    if mismatched_tuple_sizes?(tag1, elements1, tag2, elements2) or
+         disjoint_tagged_tuples?(elements1, elements2) do
+      :disjoint
+    else
+      :none
+    end
   end
 
   # A very cheap check for tagged tuples
@@ -5593,65 +5612,87 @@ defmodule Module.Types.Descr do
   defp bdd_difference_union(i, u1, u2),
     do: bdd_difference(i, bdd_union(u1, u2))
 
-  # Optimize differences
-  #
-  # ## When D2 == :bottom
-  #
-  # We can rewrite the BDD format:
+  ## Optimize differences
+
+  # For the right-side being a leaf, we have:
   #
-  # B1 and not B2
-  # ((a1 and C1) or B1_no_C1) and not B2
-  # ((a1 and C1) and not B2) or (B1_no_C1 and not B2)
-  # (a1 and C1 and not ((a2 and C2) or U2)) or (B1_no_C1 and not B2)
-  # (a1 and C1 and not (a2 and C2) and not U2) or (B1_no_C1 and not B2)
-  # (a1 and C1 and not U2) or (B1_no_C1 and not B2)
-  # (a1 and C1 and not U2) or (U1 and not B2) or (not a1 and D1 and not B2)
+  #     ((a1 and C1) or U1 or (not a1 and D1)) and not a2
   #
-  # The last line is equivalent to the BDD:
-  # {a1, C1 and not U2, U1 and not B2, D1 and not B2}
+  # If disjoint?(a1, a2), we end up with:
   #
-  # ## When D2 != :bottom
+  #     (a1 and C1) or (U1 and not d2) or (not a1 and D1 and not a2)
   #
-  # We could rewrite it to use the same optimization as bdd_leaf_intersection.
-  # However, given differences of negations are not common and because
-  # bdd_leaf_intersection can be expensive for open maps, we skip this step for now.
+  # If subtype?(a1, a2), we end up with:
   #
-  # (B1) and not (B2)
-  # (B1) and not (B2_no_D2 or (not a2 and D2))
-  # (B1) and (not B2_no_D2 and (a2 or not D2))
-  # (B1) and (a2 or not D2) and not B2_no_D2
-  # ((B1 and a2) or (B1 and not D2)) and not B2_no_D2
+  #     (U1 and not d2) or (D1 and not a2)
+  defp bdd_difference({a1, c1, u1, d1} = bdd1, bdd_leaf(_, _) = bdd2, leaf_compare)
+       when is_tuple(bdd2) do
+    case leaf_compare.(a1, bdd2) do
+      :disjoint ->
+        bdd_union(
+          bdd_difference(u1, bdd2, leaf_compare),
+          bdd_difference({a1, :bdd_bot, :bdd_bot, d1}, bdd2)
+        )
+        |> bdd_union({a1, c1, :bdd_bot, :bdd_bot})
 
-  defp bdd_difference(bdd1, {_, _, _, d} = bdd2, _leaf_disjoint) when d != :bdd_bot do
-    bdd_difference(bdd1, bdd2)
-  end
+      :subtype ->
+        bdd_union(bdd_difference(u1, bdd2, leaf_compare), bdd_difference(d1, bdd2, leaf_compare))
 
-  defp bdd_difference(bdd_leaf(_, _) = bdd1, bdd2, leaf_disjoint)
-       when is_tuple(bdd2) do
-    {leaf, _, u, :bdd_bot} = bdd_expand(bdd2)
+      :none when a1 < bdd2 ->
+        {a1, bdd_difference(c1, bdd2, leaf_compare), bdd_difference(u1, bdd2, leaf_compare),
+         bdd_difference(d1, bdd2, leaf_compare)}
+        |> case do
+          {_, :bdd_bot, u, :bdd_bot} -> u
+          other -> other
+        end
 
-    case leaf_disjoint.(bdd1, leaf) do
-      true when u == :bdd_bot -> bdd1
-      true -> bdd_difference(bdd1, u, leaf_disjoint)
-      false -> bdd_difference(bdd1, bdd2)
+      :none ->
+        bdd_difference(bdd1, bdd2)
     end
   end
 
-  defp bdd_difference({a1, c1, u1, d1} = bdd1, bdd2, leaf_disjoint)
-       when is_tuple(bdd2) do
-    {a2, _c2, u2, :bdd_bot} = bdd_expand(bdd2)
+  # For the left-side being a leaf, we have:
+  #
+  #     a1 and not ((a2 and C2) or U2 or (not a2 and D2))
+  #     a1 and not (a2 and C2) and not U2 and (a2 or not D2)
+  #
+  # If disjoint?(a1, a2):
+  #
+  #     a1 and not (a2 and C2) = a1            (a2 and C2 is subset of a2, disjoint from a1)
+  #     a1 and (a2 or not D2) = a1 and not D2  (a1 and a2 = bottom)
+  #
+  # Result: a1 and not D2 and not U2
+  #
+  # If subtype?(a1, a2):
+  #
+  #     a1 and not (a2 and C2) = a1 and not C2 (a1 and not a2 = bottom)
+  #     a1 and (a2 or not D2) = a1             (a1 and a2 = a1)
+  #
+  # Result: a1 and not C2 and not U2
+  defp bdd_difference(bdd_leaf(_, _) = bdd1, bdd2, leaf_compare) when is_tuple(bdd2) do
+    {a2, c2, u2, d2} = bdd_expand(bdd2)
 
-    case leaf_disjoint.(a1, a2) do
-      true ->
-        {a1, bdd_difference(c1, u2, leaf_disjoint), bdd_difference(u1, bdd2, leaf_disjoint),
-         bdd_difference(d1, bdd2, leaf_disjoint)}
+    case leaf_compare.(bdd1, a2) do
+      :disjoint ->
+        bdd1 |> bdd_difference(u2, leaf_compare) |> bdd_difference(d2, leaf_compare)
+
+      :subtype ->
+        bdd1 |> bdd_difference(u2, leaf_compare) |> bdd_difference(c2, leaf_compare)
+
+      :none when a2 < bdd1 ->
+        {a2, bdd_difference(bdd1, bdd_union(c2, u2), leaf_compare), :bdd_bot,
+         bdd_difference(bdd1, bdd_union(d2, u2), leaf_compare)}
+        |> case do
+          {_, :bdd_bot, u, :bdd_bot} -> u
+          other -> other
+        end
 
-      false ->
+      :none ->
         bdd_difference(bdd1, bdd2)
     end
   end
 
-  defp bdd_difference(bdd1, bdd2, _leaf_disjoint) do
+  defp bdd_difference(bdd1, bdd2, _leaf_compare) do
     bdd_difference(bdd1, bdd2)
   end
 

From e14608d4c356f8f1c9c7f18ef77545364aaf0229 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 8 Mar 2026 18:42:36 +0100
Subject: [PATCH 2/4] Avoid nested differences

---
 lib/elixir/lib/module/types/apply.ex          |   4 +-
 lib/elixir/lib/module/types/of.ex             |  77 ++++--
 lib/elixir/lib/module/types/pattern.ex        | 258 +++++++++---------
 .../test/elixir/module/types/expr_test.exs    |   8 +-
 .../test/elixir/module/types/pattern_test.exs |  85 +++---
 5 files changed, 231 insertions(+), 201 deletions(-)

diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index 1e8d154dabc..07354ee02be 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -1486,9 +1486,9 @@ defmodule Module.Types.Apply do
     domain(domain, clauses)
   end
 
-  defp filter_domain({_type, domain, clauses}, expected, arity) do
+  defp filter_domain({_type, domain, clauses}, expected, _arity) do
     case filter_domain(clauses, expected, [], true) do
-      :none -> List.duplicate(term(), arity)
+      :none -> domain(domain, clauses)
       :all -> domain(domain, clauses)
       args -> Enum.zip_with(args, fn types -> Enum.reduce(types, &union/2) end)
     end
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index ba795ee20f1..354b1d260af 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -105,31 +105,62 @@ defmodule Module.Types.Of do
           context
       end
 
-    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
-        {:error, _} when allow_empty? ->
-          data = %{
-            data
-            | type: none(),
-              off_traces: new_trace(expr, none(), stack, off_traces)
-          }
-
-          {none(), %{context | vars: %{vars | version => data}}}
-
-        {:ok, new_type} when new_type != old_type ->
-          data = %{
-            data
-            | type: new_type,
-              off_traces: new_trace(expr, new_type, stack, off_traces)
-          }
-
-          {new_type, %{context | vars: %{vars | version => data}}}
-
-        _ ->
-          {old_type, context}
+    if match?(%{pattern_info: %{allow_empty?: _}}, context) do
+      if type not in [term(), dynamic()] and not is_map_key(data, :errored) do
+        new_type = intersection(old_type, type)
+
+        case empty?(new_type) do
+          true when allow_empty? ->
+            data = %{
+              data
+              | type: none(),
+                off_traces: new_trace(expr, none(), stack, off_traces)
+            }
+
+            {none(), %{context | vars: %{vars | version => data}}}
+
+          false when new_type != old_type ->
+            data = %{
+              data
+              | type: new_type,
+                off_traces: new_trace(expr, new_type, stack, off_traces)
+            }
+
+            {new_type, %{context | vars: %{vars | version => data}}}
+
+          _ ->
+            {old_type, context}
+        end
+      else
+        {old_type, context}
       end
     else
-      {old_type, context}
+      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
+          {:error, _} when allow_empty? ->
+            data = %{
+              data
+              | type: none(),
+                off_traces: new_trace(expr, none(), stack, off_traces)
+            }
+
+            {none(), %{context | vars: %{vars | version => data}}}
+
+          {:ok, new_type} when new_type != old_type ->
+            data = %{
+              data
+              | type: new_type,
+                off_traces: new_trace(expr, new_type, stack, off_traces)
+            }
+
+            {new_type, %{context | vars: %{vars | version => data}}}
+
+          _ ->
+            {old_type, context}
+        end
+      else
+        {old_type, context}
+      end
     end
   end
 
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index cb37cd15bba..a7ff57a3d29 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -194,7 +194,7 @@ defmodule Module.Types.Pattern do
   def of_head(patterns, guards, expected, previous, tag, meta, stack, original) do
     stack = %{stack | meta: meta}
 
-    {trees, precise?, context} =
+    {trees, precise?, args_types, context} =
       of_precise_head(patterns, guards, expected, previous, tag, stack, original)
 
     if context.failed and not empty_previous?(previous) and
@@ -202,17 +202,10 @@ defmodule Module.Types.Pattern do
       # If it failed, let's try to break it down to a better error message.
       # First we check if it fails without previous, if it doesn't, check if it is redundant.
       case of_precise_head(patterns, guards, expected, init_previous(), tag, stack, original) do
-        {other_trees, _, %{failed: true} = other_context} ->
+        {other_trees, _, _, %{failed: true} = other_context} ->
           {other_trees, previous, other_context}
 
-        {other_trees, _, other_context} ->
-          args_types =
-            Enum.map(other_trees, fn {tree, _, _} ->
-              tree
-              |> of_pattern_tree(stack, other_context)
-              |> upper_bound()
-            end)
-
+        {other_trees, _, args_types, other_context} ->
           if previous_subtype?(args_types, previous) do
             warning = {:redundant, tag, expected, args_types, previous, other_context}
             {other_trees, previous, warn(__MODULE__, warning, meta, stack, other_context)}
@@ -221,13 +214,6 @@ defmodule Module.Types.Pattern do
           end
       end
     else
-      args_types =
-        Enum.map(trees, fn {tree, _, _} ->
-          tree
-          |> of_pattern_tree(stack, context)
-          |> upper_bound()
-        end)
-
       cond do
         previous_subtype?(args_types, previous) ->
           warning = {:redundant, tag, expected, args_types, previous, context}
@@ -242,16 +228,63 @@ defmodule Module.Types.Pattern do
     end
   end
 
+  defp of_precise_head([], guards, _expected, _previous, _tag, stack, context) do
+    %{vars: vars} = context
+    {guard_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
+    {[], guard_precise?, [], of_changed(changed, stack, context)}
+  end
+
   defp of_precise_head(patterns, guards, expected, previous, tag, stack, context) do
     %{vars: vars} = context
+    context = init_pattern_info(context, [])
+
+    {trees, pattern_precise?, context} =
+      of_pattern_args_zip(patterns, expected, 0, [], true, stack, context)
 
-    case of_pattern_args(patterns, expected, previous, tag, stack, context) do
-      {trees, pattern_precise?, changed, context} ->
-        {guard_precise?, context} = of_guards(guards, changed, vars, stack, context)
-        {trees, pattern_precise? and guard_precise?, context}
+    {pattern_info, context} = pop_pattern_info(context)
+    {guard_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
+
+    with {:ok, types} <-
+           of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
+         fork_types = types,
+         fork_context = context,
+         fork_changed = changed,
+         {:ok, types} <-
+           of_pattern_previous(types, previous, trees, pattern_info, tag, stack, context),
+         {_types, changed, context} <-
+           of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
+      args_types =
+        if previous != [] do
+          {_types, fork_changed, fork_context} =
+            of_pattern_refine(fork_types, fork_changed, pattern_info, tag, stack, fork_context)
+
+          fork_context = of_changed(fork_changed, stack, fork_context)
+
+          Enum.map(trees, fn {tree, _, _} ->
+            tree
+            |> of_pattern_tree(stack, fork_context)
+            |> upper_bound()
+          end)
+        else
+          Enum.map(trees, fn {tree, _, _} ->
+            tree
+            |> of_pattern_tree(stack, context)
+            |> upper_bound()
+          end)
+        end
+
+      {trees, pattern_precise? and guard_precise?, args_types,
+       of_changed(changed, stack, context)}
+    else
+      {:error, context} ->
+        args_types =
+          Enum.map(trees, fn {tree, _, _} ->
+            tree
+            |> of_pattern_tree(stack, context)
+            |> upper_bound()
+          end)
 
-      {trees, context} ->
-        {trees, false, context}
+        {trees, false, args_types, context}
     end
   end
 
@@ -272,30 +305,6 @@ defmodule Module.Types.Pattern do
     []
   end
 
-  defp of_pattern_args([], [], _previous, _tag, _stack, context) do
-    {[], true, [], context}
-  end
-
-  defp of_pattern_args(patterns, expected, previous, tag, stack, context) do
-    context = init_pattern_info(context, [])
-
-    {trees, precise?, context} =
-      of_pattern_args_zip(patterns, expected, 0, [], true, stack, context)
-
-    {pattern_info, context} = pop_pattern_info(context)
-
-    with {:ok, types} <-
-           of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
-         {:ok, types} <-
-           of_pattern_previous(types, previous, trees, pattern_info, tag, stack, context),
-         {_types, changed, context} <-
-           of_pattern_refine(types, pattern_info, tag, stack, context) do
-      {trees, precise?, changed, context}
-    else
-      {:error, context} -> {trees, context}
-    end
-  end
-
   defp of_pattern_args_zip(
          [pattern | tail],
          [expected | types],
@@ -353,14 +362,17 @@ defmodule Module.Types.Pattern do
     {pattern_info, context} = pop_pattern_info(context)
     args = [{tree, expected, pattern}]
 
-    with {:ok, types} <- of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
-         {_types, changed, context} <-
-           of_pattern_refine(types, pattern_info, tag, stack, context) do
-      {_precise?, context} = of_guards(guards, changed, vars, stack, context)
-      context
+    with {:ok, types} <- of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context) do
+      {_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
+
+      with {_types, changed, context} <-
+             of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
+        of_changed(changed, stack, context)
+      else
+        {:error, context} -> context
+      end
     else
-      {:error, context} ->
-        context
+      {:error, context} -> context
     end
   end
 
@@ -382,10 +394,10 @@ defmodule Module.Types.Pattern do
     {:ok, Enum.reverse(acc)}
   end
 
-  defp of_pattern_refine(types, pattern_info, tag, stack, context) do
+  defp of_pattern_refine(types, changed \\ [], pattern_info, tag, stack, context) do
     pattern_info
     |> Enum.reverse()
-    |> Enum.reduce({[], context}, fn {version, _pinned, node}, {changed, context} ->
+    |> Enum.reduce({changed, context}, fn {version, _pinned, node}, {changed, context} ->
       %{var: var, expr: expr, root: root, path: path} = node
 
       {actual, index} =
@@ -1025,8 +1037,8 @@ defmodule Module.Types.Pattern do
   @atom_true atom([true])
   @atom_false atom([false])
 
-  defp of_guards([], changed, _vars, stack, context) do
-    {true, of_changed(changed, stack, context)}
+  defp of_guards([], changed, _vars, _stack, context) do
+    {true, changed, context}
   end
 
   defp of_guards(guards, changed, vars, stack, context) do
@@ -1040,7 +1052,7 @@ defmodule Module.Types.Pattern do
 
     {precise?, context} = of_guards(guards, stack, context)
     {%{vars: vars, changed: changed}, context} = pop_pattern_info(context)
-    {is_map(vars) and precise?, of_changed(Map.keys(changed), stack, context)}
+    {is_map(vars) and precise?, Map.keys(changed), context}
   end
 
   defp of_guards([guard], stack, context) do
@@ -1478,66 +1490,44 @@ defmodule Module.Types.Pattern do
     traces = collect_traces(args, context)
 
     message =
-      with {:case, meta, expr, type} <- info,
-           {:case, :||} <- meta[:type_check] do
-        if subtype?(type, atom([false, nil])) do
+      with {_op, meta, expr, type} <- info,
+           true <- previous_subtype?(expected, previous) do
+        if match?({:case, :||}, meta[:type_check]) do
           """
-          the following conditional expression will never succeed:
+          the right-hand side of || will always execute:
 
               #{expr_to_string(expr) |> indent(4)}
 
-          because it evaluates to:
+          because the left-hand side always evaluates to:
 
               #{to_quoted_string(type) |> indent(4)}
           """
         else
-          additional =
-            with {:case, meta, [_, _]} <- expr,
-                 {:case, :||} <- meta[:type_check] do
-              "(shown as ... below) "
-            else
-              _ -> ""
-            end
-
           """
-          the right-hand side of || #{additional}will never be executed:
+          the following clause cannot match because the previous clauses already matched all possible values:
 
-              #{expr_to_string({:||, [], [expr, {:..., [], []}]}) |> indent(4)}
+              #{args_to_string(args) |> indent(4)} ->
 
-          because the left-hand side always evaluates to:
+          it attempts to match on the result of:
+
+              #{expr_to_string(expr) |> indent(4)}
+
+          which has the already matched type:
 
               #{to_quoted_string(type) |> indent(4)}
           """
         end
       else
         _ ->
-          with {_op, _meta, expr, type} <- info,
-               true <- previous_subtype?(expected, previous) do
-            """
-            the following clause cannot match because the previous clauses already matched all possible values:
-
-                #{args_to_string(args) |> indent(4)} ->
-
-            it attempts to match on the result of:
-
-                #{expr_to_string(expr) |> indent(4)}
-
-            which has the already matched type:
-
-                #{to_quoted_string(type) |> indent(4)}
-            """
-          else
-            _ ->
-              """
-              the following clause is redundant:
+          """
+          the following clause is redundant:
 
-                  #{args_to_string(args) |> indent(4)} ->
+              #{args_to_string(args) |> indent(4)} ->
 
-              previous clauses have already matched on the following types:
+          previous clauses have already matched on the following types:
 
-                  #{previous_to_string(previous)}
-              """
-          end
+              #{previous_to_string(previous)}
+          """
       end
 
     %{
@@ -1616,37 +1606,59 @@ defmodule Module.Types.Pattern do
 
   defp badpattern({{op, meta, expr, type}, args}, _index) when op in [:case, :try_else] do
     with {:case, op} <- meta[:type_check] do
-      if op in [:and, :or] do
-        {first_message, second_message} =
-          case booleaness(type) do
-            {true, _} -> {" will always succeed", "because it evaluates to"}
-            {false, _} -> {" will never succeed", "because it evaluates to"}
-            :none -> {" will always fail", "because it evaluates to"}
-            _ -> {"", "will always evaluate to"}
-          end
+      message =
+        cond do
+          op == :|| ->
+            additional =
+              with {:case, meta, [_, _]} <- expr,
+                   {:case, :||} <- meta[:type_check] do
+                "(shown as ... below) "
+              else
+                _ -> ""
+              end
 
-        {expr,
-         """
-         the following conditional expression#{first_message}:
+            """
+            the right-hand side of || #{additional}will never be executed:
 
-             #{expr_to_string(expr) |> indent(4)}
+                #{expr_to_string({:||, [], [expr, {:..., [], []}]}) |> indent(4)}
 
-         #{second_message}:
+            because the left-hand side always evaluates to:
 
-             #{to_quoted_string(type) |> indent(4)}
-         """}
-      else
-        {expr,
-         """
-         the following conditional expression:
+                #{to_quoted_string(type) |> indent(4)}
+            """
 
-             #{expr_to_string(expr) |> indent(4)}
+          op in [:and, :or] ->
+            {first_message, second_message} =
+              case booleaness(type) do
+                {true, _} -> {" will always succeed", "because it evaluates to"}
+                {false, _} -> {" will never succeed", "because it evaluates to"}
+                :none -> {" will always fail", "because it evaluates to"}
+                _ -> {"", "will always evaluate to"}
+              end
 
-         will always evaluate to:
+            """
+            the following conditional expression#{first_message}:
 
-             #{to_quoted_string(type) |> indent(4)}
-         """}
-      end
+                #{expr_to_string(expr) |> indent(4)}
+
+            #{second_message}:
+
+                #{to_quoted_string(type) |> indent(4)}
+            """
+
+          true ->
+            """
+            the following conditional expression:
+
+                #{expr_to_string(expr) |> indent(4)}
+
+            will always evaluate to:
+
+                #{to_quoted_string(type) |> indent(4)}
+            """
+        end
+
+      {expr, message}
     else
       _ ->
         {args,
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index a5d7a829f6b..0fcbcad7b06 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -1974,7 +1974,7 @@ defmodule Module.Types.ExprTest do
     end
 
     test "|| reports violations" do
-      assert typewarn!([x = 123], x || true) |> elem(1) =~ """
+      assert typeerror!([x = 123], x || true) =~ """
              the right-hand side of || will never be executed:
 
                  x || ...
@@ -1985,7 +1985,7 @@ defmodule Module.Types.ExprTest do
 
              """
 
-      assert typewarn!([x = 123], System.get_env("foo") || x || true) |> elem(1) =~ """
+      assert typeerror!([x = 123], System.get_env("foo") || x || true) =~ """
              the right-hand side of || (shown as ... below) will never be executed:
 
                  System.get_env("foo") || x || ...
@@ -1997,11 +1997,11 @@ defmodule Module.Types.ExprTest do
              """
 
       assert typewarn!([x = false], x || true) |> elem(1) =~ """
-             the following conditional expression will never succeed:
+             the right-hand side of || will always execute:
 
                  x
 
-             because it evaluates to:
+             because the left-hand side always evaluates to:
 
                  dynamic(false)
              """
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 2a73eebf860..79063f03279 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -171,7 +171,7 @@ defmodule Module.Types.PatternTest do
 
              where "y" was given the type:
 
-                 # type: dynamic(atom())
+                 # type: atom()
                  # from: types_test.ex:LINE
                  is_atom(y)
              """
@@ -631,9 +631,9 @@ defmodule Module.Types.PatternTest do
 
              where "x" was given the type:
 
-                 # type: dynamic()
+                 # type: list(term())
                  # from: types_test.ex:LINE
-                 x
+                 length(x)
              """
     end
 
@@ -678,22 +678,17 @@ defmodule Module.Types.PatternTest do
       assert typecheck!([x = %{foo: :bar}], not x.bar, x) ==
                dynamic(open_map(foo: atom([:bar]), bar: atom([false])))
 
-      assert typeerror!([x = %Point{}], x.foo_bar, :ok) ==
-               ~l"""
-               unknown key .foo_bar in expression:
-
-                   x.foo_bar
-
-               the given type does not have the given key:
+      assert typeerror!([x = %Point{}], x.foo_bar, :ok) == ~l"""
+             the following pattern will never match:
 
-                   dynamic(%Point{x: term(), y: term(), z: term()})
+                 x = %Point{}
 
-               where "x" was given the type:
+             where "x" was given the type:
 
-                   # type: dynamic(%Point{})
-                   # from: types_test.ex:LINE-1
-                   x = %Point{}
-               """
+                 # type: %{..., foo_bar: true}
+                 # from: types_test.ex:LINE
+                 x.foo_bar
+             """
     end
 
     test "when checks" do
@@ -754,7 +749,7 @@ defmodule Module.Types.PatternTest do
 
              where "x" was given the type:
 
-                 # type: dynamic(atom() or binary())
+                 # type: atom() or binary()
                  # from: types_test.ex:LINE
                  is_binary(x) or is_atom(x)
              """
@@ -807,7 +802,7 @@ defmodule Module.Types.PatternTest do
 
                where "x" was given the type:
 
-                   # type: dynamic(atom() or binary())
+                   # type: atom() or binary()
                    # from: types_test.ex:LINE-1
                    :erlang.or(is_binary(x), is_atom(x))
                """
@@ -846,21 +841,17 @@ defmodule Module.Types.PatternTest do
                dynamic(tuple([list(term()), term()]))
     end
 
-    test "errors in guards" do
+    test "incompatible pattern and guards" do
       assert typeerror!([x = {}], is_integer(x), x) == ~l"""
-             this guard will never succeed:
-
-                 is_integer(x)
-
-             because it returns type:
+             the following pattern will never match:
 
-                 false
+                 x = {}
 
              where "x" was given the type:
 
-                 # type: dynamic({})
+                 # type: integer()
                  # from: types_test.ex:LINE
-                 x = {}
+                 is_integer(x)
              """
     end
   end
@@ -1014,43 +1005,39 @@ defmodule Module.Types.PatternTest do
 
     test "warnings" do
       assert typeerror!([x = {}], x == 0, x) =~ ~l"""
-             comparison between distinct types found:
-
-                 x == 0
-
-             given types:
-
-                 dynamic({}) == integer()
-             """
-
-      assert typeerror!([x = {}], x != 0, x) =~ ~l"""
-             comparison between distinct types found:
+             the following pattern will never match:
 
-                 x != 0
+                 x = {}
 
-             given types:
+             where "x" was given the type:
 
-                 dynamic({}) != integer()
+                 # type: float() or integer()
+                 # from: types_test.ex:LINE
+                 x == 0
              """
 
       assert typeerror!([x = {}], x == :foo, x) =~ ~l"""
-             comparison between distinct types found:
+             the following pattern will never match:
 
-                 x == :foo
+                 x = {}
 
-             given types:
+             where "x" was given the type:
 
-                 dynamic({}) == :foo
+                 # type: :foo
+                 # from: types_test.ex:LINE
+                 x == :foo
              """
 
       assert typeerror!([x = {}], not (x != :foo), x) =~ ~l"""
-             comparison between distinct types found:
+             the following pattern will never match:
 
-                 x != :foo
+                 x = {}
 
-             given types:
+             where "x" was given the type:
 
-                 dynamic({}) != :foo
+                 # type: :foo
+                 # from: types_test.ex:LINE
+                 x != :foo
              """
 
       # We cannot warn in this case because the inference itself will lead to disjoint types

From e193fd582a94e80a899d02a4dc3b4d083987cbf6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 8 Mar 2026 21:12:59 +0100
Subject: [PATCH 3/4] Refactor

---
 lib/elixir/lib/module/types/pattern.ex | 120 +++++++++++--------------
 1 file changed, 51 insertions(+), 69 deletions(-)

diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index a7ff57a3d29..93ade479d78 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -230,8 +230,8 @@ defmodule Module.Types.Pattern do
 
   defp of_precise_head([], guards, _expected, _previous, _tag, stack, context) do
     %{vars: vars} = context
-    {guard_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
-    {[], guard_precise?, [], of_changed(changed, stack, context)}
+    {guard_precise?, changed, context} = of_guards(guards, vars, stack, context)
+    {[], guard_precise?, [], of_changed(Map.keys(changed), stack, context)}
   end
 
   defp of_precise_head(patterns, guards, expected, previous, tag, stack, context) do
@@ -242,52 +242,39 @@ defmodule Module.Types.Pattern do
       of_pattern_args_zip(patterns, expected, 0, [], true, stack, context)
 
     {pattern_info, context} = pop_pattern_info(context)
-    {guard_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
+    {guard_precise?, changed, context} = of_guards(guards, vars, stack, context)
 
     with {:ok, types} <-
            of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
-         fork_types = types,
-         fork_context = context,
-         fork_changed = changed,
+         # We compute the args types before we do the intersection with previous clauses
+         args_types =
+           (with [_ | _] <- previous,
+                 {:ok, _types, context} <-
+                   of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
+              trees_to_args_types(trees, stack, context)
+            else
+              _ -> nil
+            end),
          {:ok, types} <-
            of_pattern_previous(types, previous, trees, pattern_info, tag, stack, context),
-         {_types, changed, context} <-
+         {:ok, _types, context} <-
            of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
-      args_types =
-        if previous != [] do
-          {_types, fork_changed, fork_context} =
-            of_pattern_refine(fork_types, fork_changed, pattern_info, tag, stack, fork_context)
-
-          fork_context = of_changed(fork_changed, stack, fork_context)
-
-          Enum.map(trees, fn {tree, _, _} ->
-            tree
-            |> of_pattern_tree(stack, fork_context)
-            |> upper_bound()
-          end)
-        else
-          Enum.map(trees, fn {tree, _, _} ->
-            tree
-            |> of_pattern_tree(stack, context)
-            |> upper_bound()
-          end)
-        end
-
-      {trees, pattern_precise? and guard_precise?, args_types,
-       of_changed(changed, stack, context)}
+      {trees, pattern_precise? and guard_precise?,
+       args_types || trees_to_args_types(trees, stack, context), context}
     else
       {:error, context} ->
-        args_types =
-          Enum.map(trees, fn {tree, _, _} ->
-            tree
-            |> of_pattern_tree(stack, context)
-            |> upper_bound()
-          end)
-
-        {trees, false, args_types, context}
+        {trees, false, trees_to_args_types(trees, stack, context), context}
     end
   end
 
+  defp trees_to_args_types(trees, stack, context) do
+    Enum.map(trees, fn {tree, _, _} ->
+      tree
+      |> of_pattern_tree(stack, context)
+      |> upper_bound()
+    end)
+  end
+
   @doc """
   Computes the domain from the pattern tree and expected types.
 
@@ -342,9 +329,9 @@ defmodule Module.Types.Pattern do
 
     with {:ok, types} <-
            of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
-         {[type], changed, context} <-
-           of_pattern_refine(types, pattern_info, tag, stack, context) do
-      {type, of_changed(changed, stack, context)}
+         {:ok, [type], context} <-
+           of_pattern_refine(types, %{}, pattern_info, tag, stack, context) do
+      {type, context}
     else
       {:error, context} -> {expected, context}
     end
@@ -361,16 +348,13 @@ defmodule Module.Types.Pattern do
 
     {pattern_info, context} = pop_pattern_info(context)
     args = [{tree, expected, pattern}]
+    {_precise?, changed, context} = of_guards(guards, vars, stack, context)
 
-    with {:ok, types} <- of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context) do
-      {_precise?, changed, context} = of_guards(guards, [], vars, stack, context)
-
-      with {_types, changed, context} <-
-             of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
-        of_changed(changed, stack, context)
-      else
-        {:error, context} -> context
-      end
+    with {:ok, types} <-
+           of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
+         {:ok, _types, context} <-
+           of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
+      context
     else
       {:error, context} -> context
     end
@@ -394,7 +378,7 @@ defmodule Module.Types.Pattern do
     {:ok, Enum.reverse(acc)}
   end
 
-  defp of_pattern_refine(types, changed \\ [], pattern_info, tag, stack, context) do
+  defp of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
     pattern_info
     |> Enum.reverse()
     |> Enum.reduce({changed, context}, fn {version, _pinned, node}, {changed, context} ->
@@ -425,13 +409,13 @@ defmodule Module.Types.Pattern do
             throw(badpattern_error(expr, index, tag, stack, context))
         end
 
-      {[version | changed], context}
+      {Map.put(changed, version, true), context}
     end)
   catch
     context -> {:error, error_vars(pattern_info, context)}
   else
     {changed, context} ->
-      {types, changed, context}
+      {:ok, types, of_changed(Map.keys(changed), stack, context)}
   end
 
   defp error_vars(pattern_info, context) do
@@ -531,13 +515,11 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  @doc """
-  Receives the pattern tree and the context and returns a concrete type.
-  """
-  def of_pattern_tree(descr, _stack, _context) when is_descr(descr),
+  # Receives the pattern tree and the context and returns a concrete type.
+  defp of_pattern_tree(descr, _stack, _context) when is_descr(descr),
     do: descr
 
-  def of_pattern_tree({:guard, name, polarity, guard, expr}, stack, context) do
+  defp of_pattern_tree({:guard, name, polarity, guard, expr}, stack, context) do
     {type, _context} = of_guard(guard, term(), expr, stack, context)
 
     # This logic mirrors the code in `Apply.compare`
@@ -553,25 +535,25 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  def of_pattern_tree({:tuple, entries}, stack, context) do
+  defp of_pattern_tree({:tuple, entries}, stack, context) do
     tuple(Enum.map(entries, &of_pattern_tree(&1, stack, context)))
   end
 
-  def of_pattern_tree({:open_map, static, dynamic}, stack, context) do
+  defp of_pattern_tree({:open_map, static, dynamic}, stack, context) do
     dynamic =
       Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, stack, context)} end)
 
     open_map(static ++ dynamic)
   end
 
-  def of_pattern_tree({:closed_map, static, dynamic}, stack, context) do
+  defp of_pattern_tree({:closed_map, static, dynamic}, stack, context) do
     dynamic =
       Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, stack, context)} end)
 
     closed_map(static ++ dynamic)
   end
 
-  def of_pattern_tree({:non_empty_list, [head | tail], suffix}, stack, context) do
+  defp of_pattern_tree({:non_empty_list, [head | tail], suffix}, stack, context) do
     tail
     |> Enum.reduce(
       of_pattern_tree(head, stack, context),
@@ -580,20 +562,20 @@ defmodule Module.Types.Pattern do
     |> non_empty_list(of_pattern_tree(suffix, stack, context))
   end
 
-  def of_pattern_tree({:intersection, entries}, stack, context) do
+  defp of_pattern_tree({:intersection, entries}, stack, context) do
     entries
     |> Enum.map(&of_pattern_tree(&1, stack, context))
     |> Enum.reduce(&intersection/2)
   end
 
-  def of_pattern_tree({:var, version}, _stack, context) do
+  defp of_pattern_tree({:var, version}, _stack, context) do
     case context do
       %{vars: %{^version => %{type: type}}} -> type
       _ -> term()
     end
   end
 
-  def of_pattern_tree(:key, _stack, _context) do
+  defp of_pattern_tree(:key, _stack, _context) do
     term()
   end
 
@@ -1037,22 +1019,22 @@ defmodule Module.Types.Pattern do
   @atom_true atom([true])
   @atom_false atom([false])
 
-  defp of_guards([], changed, _vars, _stack, context) do
-    {true, changed, context}
+  defp of_guards([], _vars, _stack, context) do
+    {true, %{}, context}
   end
 
-  defp of_guards(guards, changed, vars, stack, context) do
+  defp of_guards(guards, vars, stack, context) do
     context =
       init_pattern_info(context, %{
         allow_empty?: false,
         parent_version: nil,
         vars: vars,
-        changed: Map.from_keys(changed, [])
+        changed: %{}
       })
 
     {precise?, context} = of_guards(guards, stack, context)
     {%{vars: vars, changed: changed}, context} = pop_pattern_info(context)
-    {is_map(vars) and precise?, Map.keys(changed), context}
+    {is_map(vars) and precise?, changed, context}
   end
 
   defp of_guards([guard], stack, context) do

From eb1f6ed084847865367fc0888ba71ab5bd1556d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Valim?= <jose.valim@gmail.com>
Date: Sun, 8 Mar 2026 22:49:02 +0100
Subject: [PATCH 4/4] Refactor refine_body_var for guards

---
 lib/elixir/lib/module/types.ex         |  2 +-
 lib/elixir/lib/module/types/of.ex      | 37 +++++++++-----------------
 lib/elixir/lib/module/types/pattern.ex |  9 +++----
 3 files changed, 18 insertions(+), 30 deletions(-)

diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index 586a9584aa3..64f99907212 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -452,7 +452,7 @@ defmodule Module.Types do
       subpatterns: %{},
       # Variables that are specific to the current environment/conditional
       conditional_vars: nil,
-      # Track metadata specific to matches and guards
+      # Track metadata specific to patterns and guards
       pattern_info: nil,
       # If type checking has found an error/failure
       failed: false,
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index 354b1d260af..9b9610bfb75 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -86,13 +86,14 @@ defmodule Module.Types.Of do
   or if we are doing a guard analysis or occurrence typing.
   Returns `true` if there was a refinement, `false` otherwise.
   """
-  def refine_body_var(var_or_version, type, expr, stack, context, allow_empty? \\ false)
+  @skip_refinement_for [term(), dynamic()]
+  def refine_body_var(var_or_version, type, expr, stack, context)
 
-  def refine_body_var({_, meta, _}, type, expr, stack, context, allow_empty?) do
-    refine_body_var(Keyword.fetch!(meta, :version), type, expr, stack, context, allow_empty?)
+  def refine_body_var({_, meta, _}, type, expr, stack, context) do
+    refine_body_var(Keyword.fetch!(meta, :version), type, expr, stack, context)
   end
 
-  def refine_body_var(version, type, expr, stack, context, allow_empty?)
+  def refine_body_var(version, type, expr, stack, context)
       when is_integer(version) or is_reference(version) do
     %{vars: %{^version => %{type: old_type, off_traces: off_traces} = data} = vars} = context
 
@@ -105,12 +106,15 @@ defmodule Module.Types.Of do
           context
       end
 
-    if match?(%{pattern_info: %{allow_empty?: _}}, context) do
-      if type not in [term(), dynamic()] and not is_map_key(data, :errored) do
+    case context do
+      _ when type in @skip_refinement_for or is_map_key(data, :errored) ->
+        {old_type, context}
+
+      %{pattern_info: %{guard_context: guard_context}} ->
         new_type = intersection(old_type, type)
 
         case empty?(new_type) do
-          true when allow_empty? ->
+          true when guard_context == :orelse ->
             data = %{
               data
               | type: none(),
@@ -131,21 +135,9 @@ defmodule Module.Types.Of do
           _ ->
             {old_type, context}
         end
-      else
-        {old_type, context}
-      end
-    else
-      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
-          {:error, _} when allow_empty? ->
-            data = %{
-              data
-              | type: none(),
-                off_traces: new_trace(expr, none(), stack, off_traces)
-            }
-
-            {none(), %{context | vars: %{vars | version => data}}}
 
+      _ ->
+        case gradual?(old_type) and compatible_intersection(old_type, type) do
           {:ok, new_type} when new_type != old_type ->
             data = %{
               data
@@ -158,9 +150,6 @@ defmodule Module.Types.Of do
           _ ->
             {old_type, context}
         end
-      else
-        {old_type, context}
-      end
     end
   end
 
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 93ade479d78..4bf82e0c73a 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -1026,7 +1026,7 @@ defmodule Module.Types.Pattern do
   defp of_guards(guards, vars, stack, context) do
     context =
       init_pattern_info(context, %{
-        allow_empty?: false,
+        guard_context: :andalso,
         parent_version: nil,
         vars: vars,
         changed: %{}
@@ -1066,7 +1066,7 @@ defmodule Module.Types.Pattern do
   end
 
   defp enable_conditional_mode(%{pattern_info: pattern_info} = context) do
-    %{context | pattern_info: %{pattern_info | allow_empty?: true}, conditional_vars: %{}}
+    %{context | pattern_info: %{pattern_info | guard_context: :orelse}, conditional_vars: %{}}
   end
 
   defp maybe_badguard(type, guard, stack, context) do
@@ -1184,8 +1184,7 @@ defmodule Module.Types.Pattern do
     # and also when vars change, so we need to deal with all possibilities
     # for pattern_info.
     case context.pattern_info do
-      %{allow_empty?: allow_empty?, vars: vars, parent_version: parent_version, changed: changed} =
-          pattern_info ->
+      %{vars: vars, parent_version: parent_version, changed: changed} = pattern_info ->
         vars =
           is_map(vars) and not is_map_key(vars, version) and
             not list_subpattern?(version, context) and vars
@@ -1199,7 +1198,7 @@ defmodule Module.Types.Pattern do
             do: Of.track_var(version, [parent_version], [], context),
             else: context
 
-        Of.refine_body_var(version, expected, expr, stack, context, allow_empty?)
+        Of.refine_body_var(version, expected, expr, stack, context)
 
       list when is_list(list) ->
         node = path_node(expected, var, expr, [])