From 9d3945bfa3f29197c74e686408ccc5d7ad134740 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Wed, 25 Feb 2026 17:17:10 +0100
Subject: [PATCH 1/6] Implement gradual function domains and tighten function
 application

Add fun_domain/1 to compute function domains for static, dynamic, and mixed function types, including explicit :badfun and {:badarity, ...} outcomes when domain extraction is not well-defined.

Refine gradual function application internals by separating static and dynamic normalization paths, documenting behavior for purely dynamic and mixed cases, and clarifying domain/compatibility handling.

Expand descr tests with gradual-application edge cases and a dedicated fun_domain test suite covering static, dynamic, mixed, and arity-error scenarios.
---
 lib/elixir/lib/module/types/descr.ex          | 188 ++++++++++++++----
 .../test/elixir/module/types/descr_test.exs   | 144 ++++++++++++++
 2 files changed, 297 insertions(+), 35 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e1958e95ac8..401a653994a 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1294,7 +1294,7 @@ defmodule Module.Types.Descr do
 
   ## Function application formula for dynamic types
 
-      τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) ∨ (dynamic(upper_bound(τ) ◦ lower_bound(τ′)))
+      τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) ∨ (dynamic(upper_bound(τ) ◦ upper_bound(τ′)))
 
   Where:
 
@@ -1302,7 +1302,8 @@ defmodule Module.Types.Descr do
   - τ′ are the arguments
   - ◦ is function application
 
-  For more details, see Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf
+  For more details, see Section 13.2 of
+  https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf
 
   ## Examples
 
@@ -1340,11 +1341,81 @@ defmodule Module.Types.Descr do
     end
   end
 
+  def fun_domain(:term), do: :badfun
+
+  def fun_domain(fun) do
+    case :maps.take(:dynamic, fun) do
+      :error ->
+        if fun_only?(fun) do
+          with {:ok, arity} <- fun_single_arity(fun) do
+            case fun_normalize(fun, arity) do
+              {:ok, domain, _arrows} -> {:ok, domain}
+              error -> error
+            end
+          end
+        else
+          :badfun
+        end
+
+      {fun_dynamic, fun_static} ->
+        cond do
+          fun_static == %{} and dynamic_fun_top?(fun_dynamic) ->
+            {:ok, dynamic()}
+
+          fun_only?(fun_static) ->
+            with {:ok, arity} <- fun_single_arity_pair(fun_static, fun_dynamic) do
+              case fun_normalize_both(fun_static, fun_dynamic, arity) do
+                {:ok, domain, _static_arrows, _dynamic_arrows} -> {:ok, domain}
+                error -> error
+              end
+            end
+
+          true ->
+            :badfun
+        end
+    end
+  end
+
+  defp fun_single_arity(%{fun: {:union, bdds}}) do
+    case :maps.keys(bdds) do
+      [arity] -> {:ok, arity}
+      arities -> {:badarity, arities}
+    end
+  end
+
+  defp fun_single_arity(_), do: {:badarity, []}
+
+  defp fun_single_arity_pair(fun_static, fun_dynamic) do
+    arities = Enum.uniq(fun_arities_of(fun_static) ++ fun_arities_of(fun_dynamic))
+
+    case arities do
+      [arity] -> {:ok, arity}
+      [] -> {:badarity, []}
+      arities -> {:badarity, arities}
+    end
+  end
+
+  defp fun_arities_of(%{fun: {:union, bdds}}), do: :maps.keys(bdds)
+  defp fun_arities_of(_), do: []
+
   defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
   defp dynamic_fun_top?(:term), do: true
   defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
   defp dynamic_fun_top?(_), do: false
 
+  # Gradual function application algorithm.
+  #
+  # 1. Domain check against the extended gradual domain (see fun_normalize_both/3):
+  #    - If the argument is a subtype of the domain, proceed to application.
+  #    - Otherwise, in gradual mode, check compatibility (see below). If
+  #      compatible, the application may succeed at runtime but we have no
+  #      static information about the result, so we return dynamic().
+  #    - Otherwise, error.
+  # 2. Compute the application result in three cases:
+  #    - Fully static: apply static arrows to the arguments directly.
+  #    - Purely dynamic function (no static arrows): wrap the result of
+  #      applying dynamic arrows to upper-bounded arguments in dynamic().
+  #    - Mixed: union the static result with the dynamic-wrapped dynamic result.
   defp fun_apply_with_strategy(fun_static, fun_dynamic, arguments) do
     args_domain = args_to_domain(arguments)
     static? = fun_dynamic == nil and Enum.all?(arguments, fn arg -> not gradual?(arg) end)
@@ -1356,6 +1427,18 @@ defmodule Module.Types.Descr do
         Enum.any?(arguments, &empty?/1) ->
           {:badarg, domain_to_flat_args(domain, arity)}
 
+        # The domain here is the extended gradual domain computed by
+        # fun_normalize_both/3. If the argument does not satisfy it, we
+        # check compatibility before rejecting.
+        #
+        # Compatibility has two cases to avoid a degenerate situation.
+        # If the argument is purely dynamic (e.g. dynamic() and bool()),
+        # its static part (lower bound) is none(). We do not want
+        # none() <= domain to trivially succeed, because that would mean
+        # "a diverging argument is accepted by any function", which is true but
+        # useless. So when the static part is empty, we instead check
+        # that the upper bound overlaps with the domain. When the static
+        # part is non-empty, we check it is a subtype of the domain.
         not subtype?(args_domain, domain) ->
           if static? or not compatible?(args_domain, domain),
             do: {:badarg, domain_to_flat_args(domain, arity)},
@@ -1365,12 +1448,27 @@ defmodule Module.Types.Descr do
           {:ok, fun_apply_static(arguments, static_arrows)}
 
         static_arrows == [] ->
-          # TODO: We need to validate this within the theory
+          # Purely dynamic function (e.g. dynamic() and (integer() -> integer())).
+          # There are no static arrows, so the general mixed formula simplifies:
+          # applying none() to anything yields none(), so the static branch
+          # vanishes and only the dynamic branch remains.
+          # The result is wrapped in dynamic(), so it is safe regardless of argument precision.
+          # If the upper-bounded arguments escape the domain, fun_apply_static returns term(),
+          # and dynamic(term()) = dynamic(), which brings back to the compatible case.
           arguments = Enum.map(arguments, &upper_bound/1)
           {:ok, dynamic(fun_apply_static(arguments, dynamic_arrows))}
 
         true ->
-          # For dynamic cases, combine static and dynamic results
+          # Mixed case: union of the static and dynamic results.
+          # static_arrows (lower materialization) contain only arrows that are
+          # guaranteed to exist at runtime. Static guarantees about the result
+          # come from these alone.
+          # dynamic_arrows (upper materialization) include dynamically uncertain
+          # arrows, so their result is wrapped in dynamic().
+          # We use upper_bound on the arguments for both branches. This is sound
+          # because the dynamic branch wraps its result in dynamic().
+          # It is more strict and informative than using lower_bound in the static part,
+          # as it amounts to assuming the worst case of using the statically present arrows.
           arguments = Enum.map(arguments, &upper_bound/1)
 
           {:ok,
@@ -1382,6 +1480,28 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # Normalizes a gradual function type into static and dynamic arrow
+  # components, and computes the extended gradual domain.
+  #
+  # The extended gradual domain is:
+  #   dom(upper_bound and fun_top) or dynamic(dom(lower_bound))
+  #
+  # fun_normalize/3 implicitly performs the "and fun_top" projection
+  # because it only looks at the :fun component, so any non-function
+  # parts of the type are automatically discarded.
+  #
+  # Fallback cases:
+  #
+  # - Static normalization succeeds but dynamic fails (e.g. the dynamic
+  #   part has no arrows at the given arity): we discard the dynamic
+  #   arrows and use the static arrows for both branches, degenerating
+  #   to the fully static case. This is sound because ignoring unusable
+  #   dynamic information cannot produce incorrect static results.
+  #
+  # - Static normalization fails (:badfun): only the dynamic arrows
+  #   contribute. The domain becomes dom(upper_bound) or dynamic(),
+  #   reflecting that the lower bound has no function type at this arity.
+  #   The application proceeds as purely dynamic (static_arrows = []).
   defp fun_normalize_both(fun_static, fun_dynamic, arity) do
     case fun_normalize(fun_static, arity) do
       {:ok, static_domain, static_arrows} when fun_dynamic == nil ->
@@ -1394,6 +1514,7 @@ defmodule Module.Types.Descr do
             {:ok, domain, static_arrows, dynamic_arrows}
 
           _ ->
+            # Dynamic normalization failed: fall back to static-only.
             {:ok, static_domain, static_arrows, static_arrows}
         end
 
@@ -1456,6 +1577,13 @@ defmodule Module.Types.Descr do
 
   defp fun_normalize(%{}, _arity), do: :badfun
 
+  # Applies a static function type to arguments by reducing over the
+  # function's DNF clauses. Each clause is an intersection of arrows,
+  # processed by aux_apply/4 with rets_reached initialized to term().
+  #
+  # When the arguments are within the domain, this is the standard
+  # application operator. When the arguments escape the domain, the
+  # result is term() (see aux_apply/4).
   defp fun_apply_static(arguments, arrows) do
     type_args = args_to_domain(arguments)
 
@@ -1476,50 +1604,40 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  # Helper function for function application that handles the application of
-  # function arrows to input types.
-
-  # This function recursively processes a list of function arrows (an intersection),
-  # applying each arrow to the input type and accumulating the result.
-
-  # ## Parameters
-
-  # - result: The accumulated result type so far
-  # - input: The input type being applied to the function
-  # - rets_reached: The intersection of return types reached so far
-  # - arrow_intersections: The list of function arrows to process
-
-  # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
+  # Applies one clause (an intersection of arrows) to an input type.
+  # Processes arrows one at a time, splitting into two recursive branches.
+  #
+  # Domain escape: if the input is not covered by the union of all the
+  # arrow domains in the clause, the result is term(). This is because
+  # rets_reached starts at term() and is only refined (intersected) when
+  # an arrow's domain covers the input, which is check by dom_subtract.
+  # Along a path where no arrow covers the input, rets_reached stays
+  # term() and gets unioned into the result at the base case. Since
+  # term() is maximal, the overall result for that clause is term().
   defp aux_apply(result, _input, rets_reached, []) do
     if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
   end
 
   defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do
-    # Calculate the part of the input not covered by this arrow's domain
     dom_subtract = difference(input, args_to_domain(args))
-
-    # Refine the return type by intersecting with this arrow's return type
     ret_refine = intersection(returns_reached, ret)
 
-    # Phase 1: Domain partitioning
-    # If the input is not fully covered by the arrow's domain, then the result type should be
-    # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
-    # parts of the domain.
-    #
-    # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
-    # both atoms and pids in the result.
+    # Phase 1 -- the part of the input not covered by this arrow's domain.
+    # We recurse on that escaped part with rets_reached unchanged (this
+    # arrow does not contribute its return type for inputs outside its domain).
+    # e.g. (integer()->atom()) and (float()->pid()) applied to number():
+    # the float part escapes integer()'s domain, so both return types
+    # contribute to the result.
     result =
       if empty?(dom_subtract),
         do: result,
         else: aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
 
-    # 2. Return type refinement
-    # The result type is also refined (intersected) in the sense that, if several arrows match
-    # the same part of the input, then the result type is an intersection of the return types of
-    # those arrows.
-
-    # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
-    # should result in (atom() ∩ pid()), which is none().
+    # Phase 2 -- the part of the input covered by this arrow's domain.
+    # We recurse on the full input with rets_reached refined (intersected)
+    # by this arrow's return type.
+    # e.g. (integer()->atom()) and (integer()->pid()) applied to integer()
+    # yields atom() and pid() (i.e., none()).
     aux_apply(result, input, ret_refine, arrow_intersections)
   end
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 6e3099f94db..7c97554c25c 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1214,6 +1214,24 @@ defmodule Module.Types.DescrTest do
         )
 
       assert fun_apply(fun3, [atom([:ok])]) == {:ok, dynamic(none())}
+
+      # Testing the special case of uplifiting both the function and argument
+      # when the function is purely dynamic
+      tau =
+        intersection(
+          dynamic_fun([integer()], integer()),
+          dynamic_fun([boolean()], boolean())
+        )
+
+      tau_p = dynamic(integer())
+      # dynamic(int->int and bool->bool) applied to dynamic(int)
+      assert fun_apply(tau, [tau_p]) == {:ok, dynamic(integer())}
+
+      tau_p2 = dynamic(union(integer(), float()))
+      assert fun_apply(tau, [tau_p2]) == {:ok, dynamic()}
+
+      assert fun_apply(dynamic(), [integer()]) == {:ok, dynamic()}
+      assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
     end
 
     test "static and dynamic" do
@@ -1258,6 +1276,132 @@ defmodule Module.Types.DescrTest do
     end
   end
 
+  describe "function domain" do
+    defp dynamic_fun_domain(args, return), do: dynamic(fun(args, return))
+
+    test "non funs" do
+      assert fun_domain(term()) == :badfun
+      assert fun_domain(integer()) == :badfun
+      assert fun_domain(union(integer(), fun([integer()], atom()))) == :badfun
+    end
+
+    test "static" do
+      assert {:ok, domain} = fun_domain(fun([integer()], atom()))
+      assert equal?(domain, tuple([integer()]))
+
+      assert {:ok, domain} = fun_domain(fun([union(integer(), float())], atom()))
+      assert equal?(domain, tuple([union(integer(), float())]))
+
+      assert {:ok, domain} = fun_domain(fun([integer(), atom()], binary()))
+      assert equal?(domain, tuple([integer(), atom()]))
+
+      fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
+      assert {:ok, domain} = fun_domain(fun0)
+      assert subtype?(tuple([integer()]), domain)
+      assert subtype?(tuple([float()]), domain)
+    end
+
+    test "arity errors" do
+      # fun() is {:negation, %{}}, no specific arity
+      assert {:badarity, _} = fun_domain(fun())
+
+      # Multiple arities
+      assert {:badarity, _} =
+               fun_domain(union(fun([integer()], integer()), fun([integer(), atom()], boolean())))
+    end
+
+    # gdom(?) = dom(term ∧ funTop) ∨ ? ∧ dom(none)
+    #         = dom(funTop) ∨ ? = none ∨ ? = ?
+    test "gdom(?) = ? (Example 6.1)" do
+      assert fun_domain(dynamic()) == {:ok, dynamic()}
+    end
+
+    # gdom(? ∧ (int → int)) = dom((int → int) ∧ funTop) ∨ ? ∧ dom(none)
+    #                        = dom(int → int) ∨ ? = int ∨ ?
+    test "gdom(? ∧ (int → int)) = int ∨ ? (Example 6.1)" do
+      assert {:ok, domain} = fun_domain(dynamic_fun_domain([integer()], integer()))
+      assert subtype?(tuple([integer()]), domain)
+      assert match?(%{dynamic: _}, domain)
+    end
+
+    # gdom((bool→bool) ∨ (? ∧ (int → int)))
+    #   = dom((bool→bool) ∨ (int → int)) ∨ ? ∧ dom(bool → bool)
+    #   = none ∨ (? ∧ bool) = ? ∧ bool
+    test "gdom((bool→bool) ∨ (? ∧ (int → int))) = ? ∧ bool (Example 6.1)" do
+      fun_type =
+        union(
+          fun([boolean()], boolean()),
+          dynamic_fun_domain([integer()], integer())
+        )
+
+      assert {:ok, domain} = fun_domain(fun_type)
+      assert subtype?(dynamic(tuple([boolean()])), domain)
+      assert match?(%{dynamic: _}, domain)
+    end
+
+    test "dynamic" do
+      assert fun_domain(dynamic()) == {:ok, dynamic()}
+
+      assert {:ok, domain} = fun_domain(dynamic_fun_domain([integer()], atom()))
+      assert subtype?(tuple([integer()]), domain)
+
+      fun0 =
+        intersection(
+          dynamic_fun_domain([integer()], atom()),
+          dynamic_fun_domain([float()], binary())
+        )
+
+      assert {:ok, domain} = fun_domain(fun0)
+      assert subtype?(tuple([integer()]), domain)
+      assert subtype?(tuple([float()]), domain)
+
+      # Arity mismatches
+      assert {:badarity, _} =
+               fun_domain(
+                 union(
+                   dynamic_fun_domain([integer()], integer()),
+                   dynamic_fun_domain([integer(), atom()], boolean())
+                 )
+               )
+    end
+
+    test "static and dynamic" do
+      # (atom -> int) \/ (dyn /\ (int -> binary))
+      # dom = 0 \/ (dyn /\ atom)
+      fun_mix =
+        union(
+          fun([atom()], integer()),
+          dynamic_fun_domain([integer()], binary())
+        )
+
+      assert {:ok, domain} = fun_domain(fun_mix)
+      assert subtype?(dynamic(tuple([atom()])), domain)
+      assert match?(%{dynamic: _}, domain)
+    end
+
+    # Applying (? ∨ int) → bool to ? ∧ float.
+    # The domain is gdom((? ∨ int) → bool) = dom(int → bool) ∨ ? ∧ dom(term → bool)
+    #                                       = int ∨ ? ∧ term = int ∨ ?
+    # The domain check ? ∧ float ≤ int ∨ ? succeeds.
+    # The static application (term → bool) ◦ float = bool is well-defined.
+    # The dynamic application (int → bool) ◦ float is not well-defined (float ⊄ int),
+    # so it returns term, wrapped in ?: ? ∧ term = ?.
+    # Result: bool ∨ ?.
+    test "applying (? ∨ int) → bool to ? ∧ float yields bool ∨ ?" do
+      fun_type = fun([union(dynamic(), integer())], boolean())
+      arg = dynamic(float())
+
+      # Domain check passes
+      assert {:ok, domain} = fun_domain(fun_type)
+      assert subtype?(tuple([arg]), domain)
+
+      # Application yields bool ∨ ?
+      assert {:ok, result} = fun_apply(fun_type, [arg])
+      assert equal?(union(boolean(), dynamic()), result)
+      assert match?(%{dynamic: _}, result)
+    end
+  end
+
   describe "singleton?" do
     test "non-singleton?" do
       refute singleton?(term())

From ad03a8be3670ba95b5c6f5304de8b3f33e195aa3 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Mon, 9 Mar 2026 16:13:30 +0100
Subject: [PATCH 2/6] Refactor function application and domain handling

---
 lib/elixir/lib/module/types/descr.ex          |  74 +++++++---
 .../test/elixir/module/types/descr_test.exs   | 129 +++++++-----------
 2 files changed, 108 insertions(+), 95 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 401a653994a..805c177b796 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1294,7 +1294,7 @@ defmodule Module.Types.Descr do
 
   ## Function application formula for dynamic types
 
-      τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) ∨ (dynamic(upper_bound(τ) ◦ upper_bound(τ′)))
+      τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) or (dynamic(upper_bound(τ) ◦ upper_bound(τ′)))
 
   Where:
 
@@ -1376,8 +1376,10 @@ defmodule Module.Types.Descr do
     end
   end
 
+  # A function can only have one arity.
+  # Some arities in the BDD map may be semantically empty, so we filter them out.
   defp fun_single_arity(%{fun: {:union, bdds}}) do
-    case :maps.keys(bdds) do
+    case fun_non_empty_arities(bdds) do
       [arity] -> {:ok, arity}
       arities -> {:badarity, arities}
     end
@@ -1386,7 +1388,8 @@ defmodule Module.Types.Descr do
   defp fun_single_arity(_), do: {:badarity, []}
 
   defp fun_single_arity_pair(fun_static, fun_dynamic) do
-    arities = Enum.uniq(fun_arities_of(fun_static) ++ fun_arities_of(fun_dynamic))
+    arities =
+      Enum.uniq(fun_non_empty_arities_of(fun_static) ++ fun_non_empty_arities_of(fun_dynamic))
 
     case arities do
       [arity] -> {:ok, arity}
@@ -1395,12 +1398,25 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp fun_arities_of(%{fun: {:union, bdds}}), do: :maps.keys(bdds)
-  defp fun_arities_of(_), do: []
+  defp fun_non_empty_arities_of(%{fun: {:union, bdds}}), do: fun_non_empty_arities(bdds)
+  defp fun_non_empty_arities_of(_), do: []
+
+  defp fun_non_empty_arities(bdds) do
+    for {arity, bdd} <- bdds,
+        not Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg) end),
+        do: arity
+  end
 
   defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
+
   defp dynamic_fun_top?(:term), do: true
-  defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
+
+  defp dynamic_fun_top?(%{fun: {:negation, map}}) do
+    Enum.all?(map, fn {_arity, bdd} ->
+      Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg) end)
+    end)
+  end
+
   defp dynamic_fun_top?(_), do: false
 
   # Gradual function application algorithm.
@@ -1604,8 +1620,18 @@ defmodule Module.Types.Descr do
     end)
   end
 
-  # Applies one clause (an intersection of arrows) to an input type.
-  # Processes arrows one at a time, splitting into two recursive branches.
+  # Helper function for function application that handles the application of
+  # function arrows to input types.
+
+  # This function recursively processes a list of function arrows (an intersection),
+  # applying each arrow to the input type and accumulating the result.
+
+  # ## Parameters
+
+  # - result: The accumulated result type so far
+  # - input: The input type being applied to the function
+  # - rets_reached: The intersection of return types reached so far
+  # - arrow_intersections: The list of function arrows to process
   #
   # Domain escape: if the input is not covered by the union of all the
   # arrow domains in the clause, the result is term(). This is because
@@ -1614,30 +1640,40 @@ defmodule Module.Types.Descr do
   # Along a path where no arrow covers the input, rets_reached stays
   # term() and gets unioned into the result at the base case. Since
   # term() is maximal, the overall result for that clause is term().
+
+  # For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
+  # For the escape case, see Section 13.2 of
+  # https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf
   defp aux_apply(result, _input, rets_reached, []) do
     if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
   end
 
   defp aux_apply(result, input, returns_reached, [{args, ret} | arrow_intersections]) do
+    # Calculate the part of the input not covered by this arrow's domain
     dom_subtract = difference(input, args_to_domain(args))
+
+    # Refine the return type by intersecting with this arrow's return type
     ret_refine = intersection(returns_reached, ret)
 
-    # Phase 1 -- the part of the input not covered by this arrow's domain.
-    # We recurse on that escaped part with rets_reached unchanged (this
-    # arrow does not contribute its return type for inputs outside its domain).
-    # e.g. (integer()->atom()) and (float()->pid()) applied to number():
-    # the float part escapes integer()'s domain, so both return types
-    # contribute to the result.
+    # Phase 1: Domain partitioning
+    # If the input is not fully covered by the arrow's domain, then the result type should be
+    # _augmented_ with the outputs obtained by applying the remaining arrows to the non-covered
+    # parts of the domain.
+    #
+    # e.g. (integer()->atom()) and (float()->pid()) when applied to number() should unite
+    # both atoms and pids in the result.
     result =
       if empty?(dom_subtract),
         do: result,
         else: aux_apply(result, dom_subtract, returns_reached, arrow_intersections)
 
-    # Phase 2 -- the part of the input covered by this arrow's domain.
-    # We recurse on the full input with rets_reached refined (intersected)
-    # by this arrow's return type.
-    # e.g. (integer()->atom()) and (integer()->pid()) applied to integer()
-    # yields atom() and pid() (i.e., none()).
+    # 2. Return type refinement
+    # The result type is also refined (intersected) in the sense that, if several arrows match
+    # the same part of the input, then the result type is an intersection of the return types of
+    # those arrows.
+
+    # e.g. (integer()->atom()) and (integer()->pid()) when applied to integer()
+    # should result in (atom() ∩ pid()), which is none().
     aux_apply(result, input, ret_refine, arrow_intersections)
   end
 
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 7c97554c25c..ff8703aca1a 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1058,6 +1058,7 @@ defmodule Module.Types.DescrTest do
     test "non funs" do
       assert fun_apply(term(), [integer()]) == :badfun
       assert fun_apply(union(integer(), none_fun(1)), [integer()]) == :badfun
+      assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
     end
 
     test "static" do
@@ -1217,21 +1218,20 @@ defmodule Module.Types.DescrTest do
 
       # Testing the special case of uplifiting both the function and argument
       # when the function is purely dynamic
-      tau =
+      fun4 =
         intersection(
           dynamic_fun([integer()], integer()),
           dynamic_fun([boolean()], boolean())
         )
 
-      tau_p = dynamic(integer())
       # dynamic(int->int and bool->bool) applied to dynamic(int)
-      assert fun_apply(tau, [tau_p]) == {:ok, dynamic(integer())}
+      assert fun_apply(fun4, [dynamic(integer())]) == {:ok, dynamic(integer())}
 
-      tau_p2 = dynamic(union(integer(), float()))
-      assert fun_apply(tau, [tau_p2]) == {:ok, dynamic()}
+      # float escapes the domain so the result is dynamic()
+      arg = dynamic(union(integer(), float()))
+      assert fun_apply(fun4, [arg]) == {:ok, dynamic()}
 
       assert fun_apply(dynamic(), [integer()]) == {:ok, dynamic()}
-      assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
     end
 
     test "static and dynamic" do
@@ -1273,19 +1273,36 @@ defmodule Module.Types.DescrTest do
                dynamic_fun([integer()], binary())
              )
              |> fun_apply([integer()]) == {:ok, dynamic(binary())}
+
+      # Applying (dynamic or int) -> bool to (dynamic and float).
+      # The domain is
+      #   gdom((dynamic or int) -> bool) = dom(int -> bool) or dynamic and dom(term -> bool)
+      #                                  = int or dynamic and term = int or dynamic
+
+      # The domain check dynamic and float <= int or dynamic succeeds.
+      # The static application (term -> bool) o float = bool is well-defined.
+      # The dynamic application (int -> bool) o float is not well-defined (float not <: int),
+      # but since it is dynamic it returns term wrapped in dynamic, which is dynamic.
+      # Result: bool or dynamic.
+      fun_type = fun([union(dynamic(), integer())], boolean())
+      arg = dynamic(float())
+
+      # Domain check passes
+      assert {:ok, domain} = fun_domain(fun_type)
+      assert subtype?(tuple([arg]), domain)
+
+      # Application yields bool or dynamic
+      assert {:ok, result} = fun_apply(fun_type, [arg])
+      assert equal?(union(boolean(), dynamic()), result)
     end
   end
 
   describe "function domain" do
-    defp dynamic_fun_domain(args, return), do: dynamic(fun(args, return))
-
-    test "non funs" do
+    test "static" do
       assert fun_domain(term()) == :badfun
       assert fun_domain(integer()) == :badfun
       assert fun_domain(union(integer(), fun([integer()], atom()))) == :badfun
-    end
 
-    test "static" do
       assert {:ok, domain} = fun_domain(fun([integer()], atom()))
       assert equal?(domain, tuple([integer()]))
 
@@ -1297,8 +1314,7 @@ defmodule Module.Types.DescrTest do
 
       fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
       assert {:ok, domain} = fun_domain(fun0)
-      assert subtype?(tuple([integer()]), domain)
-      assert subtype?(tuple([float()]), domain)
+      assert subtype?(tuple([integer() |> union(float())]), domain)
     end
 
     test "arity errors" do
@@ -1310,95 +1326,56 @@ defmodule Module.Types.DescrTest do
                fun_domain(union(fun([integer()], integer()), fun([integer(), atom()], boolean())))
     end
 
-    # gdom(?) = dom(term ∧ funTop) ∨ ? ∧ dom(none)
-    #         = dom(funTop) ∨ ? = none ∨ ? = ?
-    test "gdom(?) = ? (Example 6.1)" do
+    test "dynamic" do
+      # gdom(dynamic) = dom(term and funTop) or dynamic(dom(none))
+      #               = dom(fun) or dynamic = none or dynamic = dynamic
       assert fun_domain(dynamic()) == {:ok, dynamic()}
-    end
 
-    # gdom(? ∧ (int → int)) = dom((int → int) ∧ funTop) ∨ ? ∧ dom(none)
-    #                        = dom(int → int) ∨ ? = int ∨ ?
-    test "gdom(? ∧ (int → int)) = int ∨ ? (Example 6.1)" do
-      assert {:ok, domain} = fun_domain(dynamic_fun_domain([integer()], integer()))
-      assert subtype?(tuple([integer()]), domain)
-      assert match?(%{dynamic: _}, domain)
-    end
-
-    # gdom((bool→bool) ∨ (? ∧ (int → int)))
-    #   = dom((bool→bool) ∨ (int → int)) ∨ ? ∧ dom(bool → bool)
-    #   = none ∨ (? ∧ bool) = ? ∧ bool
-    test "gdom((bool→bool) ∨ (? ∧ (int → int))) = ? ∧ bool (Example 6.1)" do
-      fun_type =
-        union(
-          fun([boolean()], boolean()),
-          dynamic_fun_domain([integer()], integer())
-        )
+      # gdom(dynamic and (int -> int)) = dom((int -> int) and funTop) or dynamic and dom(none)
+      #                                = dom(int -> int) or dynamic = int or dynamic
+      assert {:ok, domain} = fun_domain(dynamic_fun([integer()], integer()))
+      assert equal?(domain, union(dynamic(), tuple([integer()])))
 
+      # gdom((bool->bool) or (dynamic and (int -> int)))
+      #       = dom((bool->bool) or (int -> int)) or dynamic and dom(bool -> bool)
+      #       = none or (dynamic and bool) = dynamic and bool
+      fun_type = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
       assert {:ok, domain} = fun_domain(fun_type)
-      assert subtype?(dynamic(tuple([boolean()])), domain)
-      assert match?(%{dynamic: _}, domain)
-    end
+      assert equal?(dynamic(tuple([boolean()])), domain)
 
-    test "dynamic" do
-      assert fun_domain(dynamic()) == {:ok, dynamic()}
-
-      assert {:ok, domain} = fun_domain(dynamic_fun_domain([integer()], atom()))
-      assert subtype?(tuple([integer()]), domain)
+      assert {:ok, domain} = fun_domain(dynamic_fun([integer()], atom()))
+      assert equal?(domain, union(dynamic(), tuple([integer()])))
 
       fun0 =
         intersection(
-          dynamic_fun_domain([integer()], atom()),
-          dynamic_fun_domain([float()], binary())
+          dynamic_fun([integer()], atom()),
+          dynamic_fun([float()], binary())
         )
 
       assert {:ok, domain} = fun_domain(fun0)
-      assert subtype?(tuple([integer()]), domain)
-      assert subtype?(tuple([float()]), domain)
+      assert equal?(domain, tuple([integer() |> union(float())]) |> union(dynamic()))
 
-      # Arity mismatches
+      # Arity mismatches: no function accepts two or three arguments
       assert {:badarity, _} =
                fun_domain(
                  union(
-                   dynamic_fun_domain([integer()], integer()),
-                   dynamic_fun_domain([integer(), atom()], boolean())
+                   dynamic_fun([integer()], integer()),
+                   dynamic_fun([integer(), atom()], boolean())
                  )
                )
     end
 
     test "static and dynamic" do
-      # (atom -> int) \/ (dyn /\ (int -> binary))
-      # dom = 0 \/ (dyn /\ atom)
+      # (atom -> int) or (dyn and (int -> binary))
+      # dom = none or (dyn and atom)
       fun_mix =
         union(
           fun([atom()], integer()),
-          dynamic_fun_domain([integer()], binary())
+          dynamic_fun([integer()], binary())
         )
 
       assert {:ok, domain} = fun_domain(fun_mix)
-      assert subtype?(dynamic(tuple([atom()])), domain)
-      assert match?(%{dynamic: _}, domain)
-    end
-
-    # Applying (? ∨ int) → bool to ? ∧ float.
-    # The domain is gdom((? ∨ int) → bool) = dom(int → bool) ∨ ? ∧ dom(term → bool)
-    #                                       = int ∨ ? ∧ term = int ∨ ?
-    # The domain check ? ∧ float ≤ int ∨ ? succeeds.
-    # The static application (term → bool) ◦ float = bool is well-defined.
-    # The dynamic application (int → bool) ◦ float is not well-defined (float ⊄ int),
-    # so it returns term, wrapped in ?: ? ∧ term = ?.
-    # Result: bool ∨ ?.
-    test "applying (? ∨ int) → bool to ? ∧ float yields bool ∨ ?" do
-      fun_type = fun([union(dynamic(), integer())], boolean())
-      arg = dynamic(float())
-
-      # Domain check passes
-      assert {:ok, domain} = fun_domain(fun_type)
-      assert subtype?(tuple([arg]), domain)
-
-      # Application yields bool ∨ ?
-      assert {:ok, result} = fun_apply(fun_type, [arg])
-      assert equal?(union(boolean(), dynamic()), result)
-      assert match?(%{dynamic: _}, result)
+      assert equal?(dynamic(tuple([atom()])), domain)
     end
   end
 

From f23334dcfb5eff40e90cf63f94e8a7126804f1a3 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 10 Mar 2026 11:07:21 +0100
Subject: [PATCH 3/6] Remove fun_domain, recover coverage via fun_apply tests
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

fun_domain was only used in tests; its behavior is fully observable
through fun_apply (wrong-domain arg → :badarg, right-domain → :ok).
Removed it and converted the domain tests to fun_apply assertions,
adding a few previously uncovered cases along the way: pure non-fun
badfun, union-arg-type enforcement, 2-arity, mixed-arity badarity
for both static and dynamic unions, and the mixed static+dynamic
gradual domain case.
---
 lib/elixir/lib/module/types/descr.ex          |  35 ------
 .../test/elixir/module/types/descr_test.exs   | 118 +++++-------------
 2 files changed, 32 insertions(+), 121 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 805c177b796..856cab4fd8c 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1341,41 +1341,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  def fun_domain(:term), do: :badfun
-
-  def fun_domain(fun) do
-    case :maps.take(:dynamic, fun) do
-      :error ->
-        if fun_only?(fun) do
-          with {:ok, arity} <- fun_single_arity(fun) do
-            case fun_normalize(fun, arity) do
-              {:ok, domain, _arrows} -> {:ok, domain}
-              error -> error
-            end
-          end
-        else
-          :badfun
-        end
-
-      {fun_dynamic, fun_static} ->
-        cond do
-          fun_static == %{} and dynamic_fun_top?(fun_dynamic) ->
-            {:ok, dynamic()}
-
-          fun_only?(fun_static) ->
-            with {:ok, arity} <- fun_single_arity_pair(fun_static, fun_dynamic) do
-              case fun_normalize_both(fun_static, fun_dynamic, arity) do
-                {:ok, domain, _static_arrows, _dynamic_arrows} -> {:ok, domain}
-                error -> error
-              end
-            end
-
-          true ->
-            :badfun
-        end
-    end
-  end
-
   # A function can only have one arity.
   # Some arities in the BDD map may be semantically empty, so we filter them out.
   defp fun_single_arity(%{fun: {:union, bdds}}) do
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index ff8703aca1a..a0f3c6263be 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1057,7 +1057,9 @@ defmodule Module.Types.DescrTest do
 
     test "non funs" do
       assert fun_apply(term(), [integer()]) == :badfun
+      assert fun_apply(integer(), [integer()]) == :badfun
       assert fun_apply(union(integer(), none_fun(1)), [integer()]) == :badfun
+      assert fun_apply(union(integer(), fun([integer()], atom())), [integer()]) == :badfun
       assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
     end
 
@@ -1071,6 +1073,17 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(fun([integer()], atom()), [float()]) == {:badarg, [integer()]}
       assert fun_apply(fun([integer()], atom()), [term()]) == {:badarg, [integer()]}
 
+      # Union argument type: domain is int | float
+      assert fun_apply(fun([union(integer(), float())], atom()), [integer()]) == {:ok, atom()}
+      assert fun_apply(fun([union(integer(), float())], atom()), [float()]) == {:ok, atom()}
+      assert fun_apply(fun([union(integer(), float())], atom()), [atom()]) ==
+               {:badarg, [union(integer(), float())]}
+
+      # 2-arity function
+      assert fun_apply(fun([integer(), atom()], binary()), [integer(), atom()]) == {:ok, binary()}
+      assert fun_apply(fun([integer(), atom()], binary()), [boolean(), atom()]) ==
+               {:badarg, [integer(), atom()]}
+
       # Return types
       assert fun_apply(fun([integer()], none()), [integer()]) == {:ok, none()}
       assert fun_apply(fun([integer()], term()), [integer()]) == {:ok, term()}
@@ -1089,6 +1102,12 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
       assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, [2]}
 
+      # Union of two different arities
+      assert fun_apply(
+               union(fun([integer()], integer()), fun([integer(), atom()], boolean())),
+               [integer()]
+             ) == {:badarity, [1, 2]}
+
       # Function intersection tests (no overlap)
       fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
       assert fun_apply(fun0, [integer()]) == {:ok, atom()}
@@ -1172,6 +1191,12 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
                {:badarity, [2]}
 
+      # Union of two dynamic functions with different arities
+      assert fun_apply(
+               union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean())),
+               [integer()]
+             ) == {:badarity, [1, 2]}
+
       # Function intersection tests
       fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))
       assert fun_apply(fun0, [integer()]) == {:ok, dynamic(atom())}
@@ -1259,6 +1284,13 @@ defmodule Module.Types.DescrTest do
       assert fun_args |> fun_apply([atom()]) == {:ok, dynamic()}
       assert fun_args |> fun_apply([integer()]) == {:badarg, [dynamic(atom())]}
 
+      # gdom((bool->bool) | dyn(int->int)) = dynamic(bool): boolean is in domain,
+      # static integer is not (int ≤ bool is false, and int ≤ dynamic is false for static args)
+      fun_mixed_gdom = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
+      assert fun_apply(fun_mixed_gdom, [boolean()]) == {:ok, boolean()}
+      assert fun_apply(fun_mixed_gdom, [dynamic(boolean())]) |> elem(1) |> equal?(boolean())
+      assert fun_apply(fun_mixed_gdom, [integer()]) == {:badarg, [dynamic(boolean())]}
+
       # Badfun
       assert union(
                fun([atom()], integer()),
@@ -1287,98 +1319,12 @@ defmodule Module.Types.DescrTest do
       fun_type = fun([union(dynamic(), integer())], boolean())
       arg = dynamic(float())
 
-      # Domain check passes
-      assert {:ok, domain} = fun_domain(fun_type)
-      assert subtype?(tuple([arg]), domain)
-
       # Application yields bool or dynamic
       assert {:ok, result} = fun_apply(fun_type, [arg])
       assert equal?(union(boolean(), dynamic()), result)
     end
   end
 
-  describe "function domain" do
-    test "static" do
-      assert fun_domain(term()) == :badfun
-      assert fun_domain(integer()) == :badfun
-      assert fun_domain(union(integer(), fun([integer()], atom()))) == :badfun
-
-      assert {:ok, domain} = fun_domain(fun([integer()], atom()))
-      assert equal?(domain, tuple([integer()]))
-
-      assert {:ok, domain} = fun_domain(fun([union(integer(), float())], atom()))
-      assert equal?(domain, tuple([union(integer(), float())]))
-
-      assert {:ok, domain} = fun_domain(fun([integer(), atom()], binary()))
-      assert equal?(domain, tuple([integer(), atom()]))
-
-      fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
-      assert {:ok, domain} = fun_domain(fun0)
-      assert subtype?(tuple([integer() |> union(float())]), domain)
-    end
-
-    test "arity errors" do
-      # fun() is {:negation, %{}}, no specific arity
-      assert {:badarity, _} = fun_domain(fun())
-
-      # Multiple arities
-      assert {:badarity, _} =
-               fun_domain(union(fun([integer()], integer()), fun([integer(), atom()], boolean())))
-    end
-
-    test "dynamic" do
-      # gdom(dynamic) = dom(term and funTop) or dynamic(dom(none))
-      #               = dom(fun) or dynamic = none or dynamic = dynamic
-      assert fun_domain(dynamic()) == {:ok, dynamic()}
-
-      # gdom(dynamic and (int -> int)) = dom((int -> int) and funTop) or dynamic and dom(none)
-      #                                = dom(int -> int) or dynamic = int or dynamic
-      assert {:ok, domain} = fun_domain(dynamic_fun([integer()], integer()))
-      assert equal?(domain, union(dynamic(), tuple([integer()])))
-
-      # gdom((bool->bool) or (dynamic and (int -> int)))
-      #       = dom((bool->bool) or (int -> int)) or dynamic and dom(bool -> bool)
-      #       = none or (dynamic and bool) = dynamic and bool
-      fun_type = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
-      assert {:ok, domain} = fun_domain(fun_type)
-      assert equal?(dynamic(tuple([boolean()])), domain)
-
-      assert {:ok, domain} = fun_domain(dynamic_fun([integer()], atom()))
-      assert equal?(domain, union(dynamic(), tuple([integer()])))
-
-      fun0 =
-        intersection(
-          dynamic_fun([integer()], atom()),
-          dynamic_fun([float()], binary())
-        )
-
-      assert {:ok, domain} = fun_domain(fun0)
-      assert equal?(domain, tuple([integer() |> union(float())]) |> union(dynamic()))
-
-      # Arity mismatches: no function accepts two or three arguments
-      assert {:badarity, _} =
-               fun_domain(
-                 union(
-                   dynamic_fun([integer()], integer()),
-                   dynamic_fun([integer(), atom()], boolean())
-                 )
-               )
-    end
-
-    test "static and dynamic" do
-      # (atom -> int) or (dyn and (int -> binary))
-      # dom = none or (dyn and atom)
-      fun_mix =
-        union(
-          fun([atom()], integer()),
-          dynamic_fun([integer()], binary())
-        )
-
-      assert {:ok, domain} = fun_domain(fun_mix)
-      assert equal?(dynamic(tuple([atom()])), domain)
-    end
-  end
-
   describe "singleton?" do
     test "non-singleton?" do
       refute singleton?(term())

From f2c8bdaaead8e15cf7bd9e50af835c9337d2adcb Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 10 Mar 2026 11:23:53 +0100
Subject: [PATCH 4/6] Remove dead helpers introduced alongside fun_domain
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

fun_single_arity, fun_single_arity_pair, fun_non_empty_arities_of,
and fun_non_empty_arities are now unreachable. Also revert
dynamic_fun_top? to the simpler map == %{} check — the semantic
emptiness scan added in the refactor was only needed to handle
the same edge cases fun_domain was handling.
---
 lib/elixir/lib/module/types/descr.ex | 40 +---------------------------
 1 file changed, 1 insertion(+), 39 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 856cab4fd8c..3f497545b85 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1341,47 +1341,9 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # A function can only have one arity.
-  # Some arities in the BDD map may be semantically empty, so we filter them out.
-  defp fun_single_arity(%{fun: {:union, bdds}}) do
-    case fun_non_empty_arities(bdds) do
-      [arity] -> {:ok, arity}
-      arities -> {:badarity, arities}
-    end
-  end
-
-  defp fun_single_arity(_), do: {:badarity, []}
-
-  defp fun_single_arity_pair(fun_static, fun_dynamic) do
-    arities =
-      Enum.uniq(fun_non_empty_arities_of(fun_static) ++ fun_non_empty_arities_of(fun_dynamic))
-
-    case arities do
-      [arity] -> {:ok, arity}
-      [] -> {:badarity, []}
-      arities -> {:badarity, arities}
-    end
-  end
-
-  defp fun_non_empty_arities_of(%{fun: {:union, bdds}}), do: fun_non_empty_arities(bdds)
-  defp fun_non_empty_arities_of(_), do: []
-
-  defp fun_non_empty_arities(bdds) do
-    for {arity, bdd} <- bdds,
-        not Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg) end),
-        do: arity
-  end
-
   defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
-
   defp dynamic_fun_top?(:term), do: true
-
-  defp dynamic_fun_top?(%{fun: {:negation, map}}) do
-    Enum.all?(map, fn {_arity, bdd} ->
-      Enum.all?(bdd_to_dnf(bdd), fn {pos, neg} -> fun_line_empty?(pos, neg) end)
-    end)
-  end
-
+  defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
   defp dynamic_fun_top?(_), do: false
 
   # Gradual function application algorithm.

From f64a5874a11b799a36580974377f3bdc96e42fa5 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 10 Mar 2026 11:43:21 +0100
Subject: [PATCH 5/6] Move mixed-arity badarity check to static side of
 fun_normalize_both
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

fun_normalize itself stays simple (no arity cross-check). The check
for other non-empty arities now lives in fun_normalize_both via
fun_other_non_empty_arities/2, and only fires for the static
component. This means:

- union(fun/1, fun/2) applied with 1 arg → {:badarity, [1, 2]}
  (static: we know one branch will always fail at runtime)

- union(dynamic_fun/1, dynamic_fun/2) applied with 1 arg →
  {:ok, dynamic(integer())} (dynamic: picks matching-arity arrows,
  wraps in dynamic() to reflect that the other branch may fail)
---
 lib/elixir/lib/module/types/descr.ex          | 46 +++++++++++++++----
 .../test/elixir/module/types/descr_test.exs   | 17 ++++---
 2 files changed, 47 insertions(+), 16 deletions(-)

diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 3f497545b85..24fea7b048d 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -1447,21 +1447,33 @@ defmodule Module.Types.Descr do
   #   The application proceeds as purely dynamic (static_arrows = []).
   defp fun_normalize_both(fun_static, fun_dynamic, arity) do
     case fun_normalize(fun_static, arity) do
-      {:ok, static_domain, static_arrows} when fun_dynamic == nil ->
-        {:ok, static_domain, static_arrows, static_arrows}
+      {:ok, static_domain, static_arrows} ->
+        # A static function with arrows at other arities is a mixed-arity union:
+        # we cannot safely apply it because at runtime the value may have a
+        # different arity than the one being called with.
+        case fun_other_non_empty_arities(fun_static, arity) do
+          [] when fun_dynamic == nil ->
+            {:ok, static_domain, static_arrows, static_arrows}
 
-      {:ok, static_domain, static_arrows} when fun_dynamic != nil ->
-        case fun_normalize(fun_dynamic, arity) do
-          {:ok, dynamic_domain, dynamic_arrows} ->
-            domain = union(dynamic_domain, dynamic(static_domain))
-            {:ok, domain, static_arrows, dynamic_arrows}
+          [] ->
+            case fun_normalize(fun_dynamic, arity) do
+              {:ok, dynamic_domain, dynamic_arrows} ->
+                domain = union(dynamic_domain, dynamic(static_domain))
+                {:ok, domain, static_arrows, dynamic_arrows}
 
-          _ ->
-            # Dynamic normalization failed: fall back to static-only.
-            {:ok, static_domain, static_arrows, static_arrows}
+              _ ->
+                # Dynamic normalization failed: fall back to static-only.
+                {:ok, static_domain, static_arrows, static_arrows}
+            end
+
+          other ->
+            {:badarity, [arity | other]}
         end
 
       :badfun ->
+        # No static arrows: dynamic-only path. Mixed-arity in the dynamic
+        # component is fine — we pick the matching-arity arrows and the
+        # result is wrapped in dynamic(), reflecting the uncertainty.
         case fun_normalize(fun_dynamic, arity) do
           {:ok, dynamic_domain, dynamic_arrows} ->
             {:ok, union(dynamic_domain, dynamic()), [], dynamic_arrows}
@@ -1475,6 +1487,20 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp fun_other_non_empty_arities(%{fun: {:union, bdds}}, arity) do
+    case :maps.take(arity, bdds) do
+      {_bdd, rest} ->
+        for {a, b} <- rest,
+            not Enum.all?(bdd_to_dnf(b), fn {pos, neg} -> fun_line_empty?(pos, neg) end),
+            do: a
+
+      :error ->
+        []
+    end
+  end
+
+  defp fun_other_non_empty_arities(_, _), do: []
+
   # Transforms a binary decision diagram (BDD) into the canonical `domain-arrows` pair:
   #
   # 1. **domain**: The union of all domains from positive functions in the BDD
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index a0f3c6263be..5c50cde7115 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1076,11 +1076,13 @@ defmodule Module.Types.DescrTest do
       # Union argument type: domain is int | float
       assert fun_apply(fun([union(integer(), float())], atom()), [integer()]) == {:ok, atom()}
       assert fun_apply(fun([union(integer(), float())], atom()), [float()]) == {:ok, atom()}
+
       assert fun_apply(fun([union(integer(), float())], atom()), [atom()]) ==
                {:badarg, [union(integer(), float())]}
 
       # 2-arity function
       assert fun_apply(fun([integer(), atom()], binary()), [integer(), atom()]) == {:ok, binary()}
+
       assert fun_apply(fun([integer(), atom()], binary()), [boolean(), atom()]) ==
                {:badarg, [integer(), atom()]}
 
@@ -1191,11 +1193,13 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
                {:badarity, [2]}
 
-      # Union of two dynamic functions with different arities
+      # Union of two dynamic functions with different arities: the call may succeed
+      # (if the value is the 1-arity branch), so we pick the matching-arity arrows
+      # and wrap in dynamic() to reflect the uncertainty.
       assert fun_apply(
                union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean())),
                [integer()]
-             ) == {:badarity, [1, 2]}
+             ) == {:ok, dynamic(integer())}
 
       # Function intersection tests
       fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))
@@ -1284,12 +1288,13 @@ defmodule Module.Types.DescrTest do
       assert fun_args |> fun_apply([atom()]) == {:ok, dynamic()}
       assert fun_args |> fun_apply([integer()]) == {:badarg, [dynamic(atom())]}
 
-      # gdom((bool->bool) | dyn(int->int)) = dynamic(bool): boolean is in domain,
-      # static integer is not (int ≤ bool is false, and int ≤ dynamic is false for static args)
+      # ((bool->bool) or dyn(int->int))
+      # booleans work, but not integers
       fun_mixed_gdom = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
-      assert fun_apply(fun_mixed_gdom, [boolean()]) == {:ok, boolean()}
-      assert fun_apply(fun_mixed_gdom, [dynamic(boolean())]) |> elem(1) |> equal?(boolean())
+      assert fun_apply(fun_mixed_gdom, [boolean()]) == {:ok, dynamic()}
+      assert fun_apply(fun_mixed_gdom, [dynamic(boolean())]) == {:ok, union(dynamic(), boolean())}
       assert fun_apply(fun_mixed_gdom, [integer()]) == {:badarg, [dynamic(boolean())]}
+      assert fun_apply(fun_mixed_gdom, [dynamic(integer())]) == {:badarg, [dynamic(boolean())]}
 
       # Badfun
       assert union(

From bf461bf4401a12dca2a07fd861b59212777ad4b9 Mon Sep 17 00:00:00 2001
From: Guillaume Duboc <guilduboc@gmail.com>
Date: Tue, 10 Mar 2026 12:02:39 +0100
Subject: [PATCH 6/6] Add tests for mixed-arity union behavior

Static union: badarity regardless of which arity is called with,
with the called arity listed first followed by the others.

Dynamic union: picks the matching-arity arrows and wraps in dynamic(),
gives badarity only when no arity matches at all, and falls back to
dynamic() when the arg is outside the domain but dynamically compatible.
---
 .../test/elixir/module/types/descr_test.exs   | 29 +++++++++++--------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 5c50cde7115..1e335aabfcb 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1104,11 +1104,10 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
       assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, [2]}
 
-      # Union of two different arities
-      assert fun_apply(
-               union(fun([integer()], integer()), fun([integer(), atom()], boolean())),
-               [integer()]
-             ) == {:badarity, [1, 2]}
+      # Union of two different arities: always badarity regardless of which arity is called
+      fun_mixed = union(fun([integer()], integer()), fun([integer(), atom()], boolean()))
+      assert fun_apply(fun_mixed, [integer()]) == {:badarity, [1, 2]}
+      assert fun_apply(fun_mixed, [integer(), atom()]) == {:badarity, [2, 1]}
 
       # Function intersection tests (no overlap)
       fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
@@ -1193,13 +1192,19 @@ defmodule Module.Types.DescrTest do
       assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
                {:badarity, [2]}
 
-      # Union of two dynamic functions with different arities: the call may succeed
-      # (if the value is the 1-arity branch), so we pick the matching-arity arrows
-      # and wrap in dynamic() to reflect the uncertainty.
-      assert fun_apply(
-               union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean())),
-               [integer()]
-             ) == {:ok, dynamic(integer())}
+      # Union of two dynamic functions with different arities: the call may succeed,
+      # so we pick the matching-arity arrows and wrap in dynamic().
+      fun_dyn_mixed =
+        union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean()))
+
+      # picks arity-1 arrows → dynamic(integer())
+      assert fun_apply(fun_dyn_mixed, [integer()]) == {:ok, dynamic(integer())}
+      # picks arity-2 arrows → dynamic(boolean())
+      assert fun_apply(fun_dyn_mixed, [integer(), atom()]) == {:ok, dynamic(boolean())}
+      # no matching arity → badarity (no dynamic escape here)
+      assert fun_apply(fun_dyn_mixed, [integer(), atom(), float()]) == {:badarity, [1, 2]}
+      # arg outside arity-1 domain but dynamic-compatible → dynamic()
+      assert fun_apply(fun_dyn_mixed, [atom()]) == {:ok, dynamic()}
 
       # Function intersection tests
       fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))