diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e1958e95ac8..24fea7b048d 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(τ′)) or (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
 
@@ -1345,6 +1346,19 @@ defmodule Module.Types.Descr do
   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 +1370,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 +1391,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,22 +1423,57 @@ 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 ->
-        {: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}
 
-          _ ->
-            {: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}
@@ -1411,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
@@ -1456,6 +1546,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)
 
@@ -1488,8 +1585,18 @@ defmodule Module.Types.Descr do
   # - 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
+  # 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().
 
   # 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
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 6e3099f94db..1e335aabfcb 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -1057,7 +1057,10 @@ 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
 
     test "static" do
@@ -1070,6 +1073,19 @@ 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()}
@@ -1088,6 +1104,11 @@ 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: 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()))
       assert fun_apply(fun0, [integer()]) == {:ok, atom()}
@@ -1171,6 +1192,20 @@ 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,
+      # 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()))
       assert fun_apply(fun0, [integer()]) == {:ok, dynamic(atom())}
@@ -1214,6 +1249,23 @@ 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
+      fun4 =
+        intersection(
+          dynamic_fun([integer()], integer()),
+          dynamic_fun([boolean()], boolean())
+        )
+
+      # dynamic(int->int and bool->bool) applied to dynamic(int)
+      assert fun_apply(fun4, [dynamic(integer())]) == {:ok, dynamic(integer())}
+
+      # 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()}
     end
 
     test "static and dynamic" do
@@ -1241,6 +1293,14 @@ defmodule Module.Types.DescrTest do
       assert fun_args |> fun_apply([atom()]) == {:ok, dynamic()}
       assert fun_args |> fun_apply([integer()]) == {:badarg, [dynamic(atom())]}
 
+      # ((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, 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(
                fun([atom()], integer()),
@@ -1255,6 +1315,23 @@ 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())
+
+      # Application yields bool or dynamic
+      assert {:ok, result} = fun_apply(fun_type, [arg])
+      assert equal?(union(boolean(), dynamic()), result)
     end
   end