diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index 84886688aa..be5f050462 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -472,19 +472,27 @@ defmodule Module.Types.Apply do
   Returns the type of a remote capture.
   """
   def remote_capture(modules, fun, arity, meta, stack, context) do
-    # TODO: We cannot return the unions of functions. Do we forbid this?
-    # Do we check it is always the same return type? Do we simply say it is a function?
-    if stack.mode == :traversal do
+    # TODO: Do we check when the union of functions is invalid?
+    # TODO: Deal with :infer types
+    if stack.mode == :traversal or modules == [] do
       {dynamic(fun(arity)), context}
     else
-      context =
-        Enum.reduce(
-          modules,
-          context,
-          &(signature(&1, fun, arity, meta, stack, &2) |> elem(1))
-        )
+      {type, fallback?, context} =
+        Enum.reduce(modules, {none(), false, context}, fn module, {type, fallback?, context} ->
+          case signature(module, fun, arity, meta, stack, context) do
+            {{:strong, _, clauses}, context} ->
+              {union(type, fun_from_non_overlapping_clauses(clauses)), fallback?, context}
+
+            {_, context} ->
+              {type, true, context}
+          end
+        end)
 
-      {dynamic(fun(arity)), context}
+      if fallback? do
+        {dynamic(fun(arity)), context}
+      else
+        {type, context}
+      end
     end
   end
 
@@ -496,10 +504,10 @@ defmodule Module.Types.Apply do
 
     * `:none` - no typing information found.
 
-    * `{:infer, domain or nil, clauses}` - clauses from inferences. You must check all
-      all clauses and return the union between them. They are dynamic
-      and they can only be converted into arrows by computing the union
-      of all arguments.
+    * `{:infer, domain or nil, clauses}` - clauses from inferences.
+      You must check all clauses and return the union between them.
+      They are dynamic and they can only be converted into arrows by
+      computing the union of all arguments.
 
     * `{:strong, domain or nil, clauses}` - clauses from signatures. So far
       these are strong arrows with non-overlapping domains
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index c9506403e6..4c8ff2b461 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -87,6 +87,11 @@ defmodule Module.Types.Descr do
   @boolset :sets.from_list([true, false], version: 2)
   def boolean(), do: %{atom: {:union, @boolset}}
 
+  ## Function constructors
+
+  @doc """
+  The top function type.
+  """
   def fun(), do: %{fun: @fun_top}
 
   @doc """
@@ -118,6 +123,15 @@ defmodule Module.Types.Descr do
     fun(List.duplicate(none(), arity), term())
   end
 
+  @doc """
+  Creates a function from non-overlapping function clauses.
+  """
+  def fun_from_non_overlapping_clauses([{args, return} | clauses]) do
+    Enum.reduce(clauses, fun(args, return), fn {args, return}, acc ->
+      intersection(acc, fun(args, return))
+    end)
+  end
+
   @doc """
   Tuples represent function domains, using unions to combine parameters.
 
@@ -715,6 +729,7 @@ defmodule Module.Types.Descr do
      - Either the static part is a non-empty function type of the given arity, or
      - The static part is empty and the dynamic part contains functions of the given arity
   """
+  # TODO: REMOVE ME
   def fun_fetch(:term, _arity), do: :error
 
   def fun_fetch(%{} = descr, arity) when is_integer(arity) do
@@ -733,7 +748,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
   defp fun_only?(descr, arity), do: empty?(difference(descr, fun(arity)))
 
   ## Atoms
@@ -916,7 +930,7 @@ defmodule Module.Types.Descr do
   # * Representation:
   #   - fun(): Top function type (leaf 1)
   #   - Function literals: {[t1, ..., tn], t} where [t1, ..., tn] are argument types and t is return type
-  #   - Normalized form for function applications: {domain, arrows, arity} is produced by `fun_normalize/1`
+  #   - Normalized form for function applications: {domain, arrows} is produced by `fun_normalize/3`
 
   # * Examples:
   #   - fun([integer()], atom()): A function from integer to atom
@@ -939,12 +953,12 @@ defmodule Module.Types.Descr do
   #   For `dynamic(integer())`, it is `integer()`.
   # - `lower_bound(t)` extracts the lower bound (most specific type) of a gradual type.
   defp fun_descr(args, output) when is_list(args) do
-    dynamic_arguments? = are_arguments_dynamic?(args)
+    dynamic_arguments? = any_dynamic?(args)
     dynamic_output? = match?(%{dynamic: _}, output)
 
     if dynamic_arguments? or dynamic_output? do
-      input_static = if dynamic_arguments?, do: materialize_arguments(args, :up), else: args
-      input_dynamic = if dynamic_arguments?, do: materialize_arguments(args, :down), else: args
+      input_static = if dynamic_arguments?, do: Enum.map(args, &upper_bound/1), else: args
+      input_dynamic = if dynamic_arguments?, do: Enum.map(args, &lower_bound/1), else: args
 
       output_static = if dynamic_output?, do: lower_bound(output), else: output
       output_dynamic = if dynamic_output?, do: upper_bound(output), else: output
@@ -967,74 +981,6 @@ defmodule Module.Types.Descr do
   defp lower_bound(:term), do: :term
   defp lower_bound(type), do: Map.delete(type, :dynamic)
 
-  @doc """
-  Calculates the domain of a function type.
-
-  For a function type, the domain is the set of valid input types.
-
-  Returns:
-  - `:badfun` if the type is not a function type
-  - A tuple type representing the domain for valid function types
-
-  Handles both static and dynamic function types:
-  1. For static functions, returns their exact domain
-  2. For dynamic functions, computes domain based on both static and dynamic parts
-
-  Formula is dom(t) = dom(upper_bound(t)) ∪ dynamic(dom(lower_bound(t))).
-  See Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf.
-
-  ## Examples
-      iex> fun_domain(fun([integer()], atom()))
-      domain_repr([integer()])
-
-      iex> fun_domain(fun([integer(), float()], boolean()))
-      domain_repr([integer(), float()])
-  """
-  def fun_domain(:term), do: :badfun
-
-  def fun_domain(type) do
-    result =
-      case :maps.take(:dynamic, type) do
-        :error ->
-          # Static function type
-          with true <- fun_only?(type), {:ok, domain} <- fun_domain_static(type) do
-            domain
-          else
-            _ -> :badfun
-          end
-
-        {dynamic, static} when static == @none ->
-          with {:ok, domain} <- fun_domain_static(dynamic), do: domain
-
-        {dynamic, static} ->
-          with true <- fun_only?(static),
-               {:ok, static_domain} <- fun_domain_static(static),
-               {:ok, dynamic_domain} <- fun_domain_static(dynamic) do
-            union(dynamic_domain, dynamic(static_domain))
-          else
-            _ -> :badfun
-          end
-      end
-
-    case result do
-      :badfun -> :badfun
-      result -> if empty?(result), do: :badfun, else: result
-    end
-  end
-
-  # Returns {:ok, domain} if the domain of the static type is well-defined.
-  # For that, it has to contain a non-empty function type.
-  # Otherwise, returns :badfun.
-  defp fun_domain_static(%{fun: bdd}) do
-    case fun_normalize(bdd) do
-      {domain, _, _} -> {:ok, domain}
-      _ -> {:ok, none()}
-    end
-  end
-
-  defp fun_domain_static(:term), do: :badfun
-  defp fun_domain_static(%{}), do: {:ok, none()}
-
   @doc """
   Applies a function type to a list of argument types.
 
@@ -1056,95 +1002,191 @@ defmodule Module.Types.Descr do
   # For more details, see Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf
 
   ## Examples
+
       iex> fun_apply(fun([integer()], atom()), [integer()])
-      atom()
+      {:ok, atom()}
 
       iex> fun_apply(fun([integer()], atom()), [float()])
       :badarg
 
       iex> fun_apply(fun([dynamic()], atom()), [dynamic()])
-      atom()
+      {:ok, atom()}
   """
+  def fun_apply(:term, _arguments) do
+    :badfun
+  end
+
   def fun_apply(fun, arguments) do
     if empty?(domain_descr(arguments)) do
       :badarg
     else
       case :maps.take(:dynamic, fun) do
-        :error -> fun_apply_with_strategy(fun, nil, arguments)
-        {fun_dynamic, fun_static} -> fun_apply_with_strategy(fun_static, fun_dynamic, arguments)
+        :error ->
+          if fun_only?(fun) do
+            fun_apply_with_strategy(fun, nil, arguments)
+          else
+            :badfun
+          end
+
+        {fun_dynamic, fun_static} ->
+          if fun_only?(fun_static) do
+            fun_apply_with_strategy(fun_static, fun_dynamic, arguments)
+          else
+            :badfun
+          end
       end
     end
   end
 
+  defp fun_only?(descr), do: empty?(Map.delete(descr, :fun))
+
   defp fun_apply_with_strategy(fun_static, fun_dynamic, arguments) do
-    args_dynamic? = are_arguments_dynamic?(arguments)
+    args_dynamic? = any_dynamic?(arguments)
+    arity = length(arguments)
 
     # For non-dynamic function and arguments, just return the static result
     if fun_dynamic == nil and not args_dynamic? do
-      with {:ok, type} <- fun_apply_static(fun_static, arguments), do: type
+      with {:ok, static_domain, static_arrows} <- fun_normalize(fun_static, arity, :static) do
+        if subtype?(domain_descr(arguments), static_domain) do
+          {:ok, fun_apply_static(arguments, static_arrows, false)}
+        else
+          :badarg
+        end
+      end
     else
-      # For dynamic cases, combine static and dynamic results
-      {static_args, dynamic_args} =
-        if args_dynamic?,
-          do: {materialize_arguments(arguments, :up), materialize_arguments(arguments, :down)},
-          else: {arguments, arguments}
+      with {:ok, domain, static_arrows, dynamic_arrows} <-
+             fun_normalize_both(fun_static, fun_dynamic, arity) do
+        cond do
+          not subtype?(domain_descr(arguments), domain) ->
+            :badarg
 
-      dynamic_fun = fun_dynamic || fun_static
+          static_arrows == [] ->
+            {:ok, dynamic(fun_apply_static(arguments, dynamic_arrows, false))}
 
-      with {:ok, res1} <- fun_apply_static(fun_static, static_args),
-           {:ok, res2} <- fun_apply_static(dynamic_fun, dynamic_args) do
-        union(res1, dynamic(res2))
-      else
-        _ -> :badarg
+          true ->
+            # For dynamic cases, combine static and dynamic results
+            {static_args, dynamic_args, maybe_empty?} =
+              if args_dynamic? do
+                {Enum.map(arguments, &upper_bound/1), Enum.map(arguments, &lower_bound/1), true}
+              else
+                {arguments, arguments, false}
+              end
+
+            {:ok,
+             union(
+               fun_apply_static(static_args, static_arrows, false),
+               dynamic(fun_apply_static(dynamic_args, dynamic_arrows, maybe_empty?))
+             )}
+        end
       end
     end
   end
 
-  # Materializes arguments using the specified direction (up or down)
-  defp materialize_arguments(arguments, :up), do: Enum.map(arguments, &upper_bound/1)
-  defp materialize_arguments(arguments, :down), do: Enum.map(arguments, &lower_bound/1)
+  defp any_dynamic?(arguments), do: Enum.any?(arguments, &match?(%{dynamic: _}, &1))
 
-  defp are_arguments_dynamic?(arguments), do: Enum.any?(arguments, &match?(%{dynamic: _}, &1))
+  defp fun_normalize_both(fun_static, fun_dynamic, arity) do
+    case fun_normalize(fun_static, arity, :static) do
+      {:ok, static_domain, static_arrows} when fun_dynamic == nil ->
+        {:ok, static_domain, static_arrows, static_arrows}
 
-  defp fun_apply_static(%{fun: fun_bdd}, arguments) do
-    type_args = domain_descr(arguments)
+      {:ok, static_domain, static_arrows} when fun_dynamic != nil ->
+        case fun_normalize(fun_dynamic, arity, :dynamic) do
+          {:ok, dynamic_domain, dynamic_arrows} ->
+            domain = union(dynamic_domain, dynamic(static_domain))
+            {:ok, domain, static_arrows, dynamic_arrows}
 
-    case fun_normalize(fun_bdd) do
-      {domain, arrows, arity} when arity == length(arguments) ->
-        cond do
-          empty?(type_args) ->
-            # Opti: short-circuits when inner loop is none() or outer loop is term()
-            result =
-              Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
-                Enum.reduce_while(intersection_of_arrows, term(), fn
-                  {_dom, _ret}, acc when acc == @none -> {:halt, acc}
-                  {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
-                end)
-                |> case do
-                  :term -> {:halt, :term}
-                  inner -> {:cont, union(inner, acc)}
-                end
-              end)
+          _ ->
+            {:ok, static_domain, static_arrows, static_arrows}
+        end
 
-            {:ok, result}
+      :badfun ->
+        case fun_normalize(fun_dynamic, arity, :dynamic) do
+          {:ok, dynamic_domain, dynamic_arrows} ->
+            {:ok, dynamic_domain, [], dynamic_arrows}
 
-          subtype?(type_args, domain) ->
-            result =
-              Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
-                aux_apply(acc, type_args, term(), intersection_of_arrows)
-              end)
+          error ->
+            error
+        end
 
-            {:ok, result}
+      error ->
+        error
+    end
+  end
 
-          true ->
-            :badarg
-        end
+  # 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
+  # 2. **arrows**: List of lists, where each inner list contains an intersection of function arrows
+  #
+  # ## Return Values
+  #
+  # - `{:ok, domain, arrows}` for valid function BDDs
+  # - `{:badarity, supported_arities}` if the given arity is not supported
+  # - `:badfun` if the BDD represents an empty function type
+  #
+  # ## Internal Use
+  #
+  # This function is used internally by `fun_apply_*`, and others to
+  # ensure consistent handling of function types in all operations.
+  defp fun_normalize(%{fun: bdd}, arity, mode) do
+    {domain, arrows, bad_arities} =
+      Enum.reduce(fun_get(bdd), {term(), [], []}, fn
+        {[{args, _} | _] = pos_funs, neg_funs}, {domain, arrows, bad_arities} ->
+          arrow_arity = length(args)
+
+          cond do
+            arrow_arity != arity ->
+              {domain, arrows, [arrow_arity | bad_arities]}
 
-      {_, _, arity} ->
-        {:badarity, arity}
+            fun_empty?(pos_funs, neg_funs) ->
+              {domain, arrows, bad_arities}
 
-      :badfun ->
+            true ->
+              # Calculate domain from all positive functions
+              path_domain =
+                Enum.reduce(pos_funs, none(), fn {args, _}, acc ->
+                  union(acc, domain_descr(args))
+                end)
+
+              {intersection(domain, path_domain), [pos_funs | arrows], bad_arities}
+          end
+      end)
+
+    case {arrows, bad_arities} do
+      {[], []} ->
         :badfun
+
+      {arrows, [_ | _] = bad_arities} when mode == :static or arrows == [] ->
+        {:badarity, Enum.uniq(bad_arities)}
+
+      {_, _} ->
+        {:ok, domain, arrows}
+    end
+  end
+
+  defp fun_normalize(%{}, _arity, _mode) do
+    :badfun
+  end
+
+  defp fun_apply_static(arguments, arrows, maybe_empty?) do
+    type_args = domain_descr(arguments)
+
+    # Optimization: short-circuits when inner loop is none() or outer loop is term()
+    if maybe_empty? and empty?(type_args) do
+      Enum.reduce_while(arrows, none(), fn intersection_of_arrows, acc ->
+        Enum.reduce_while(intersection_of_arrows, term(), fn
+          {_dom, _ret}, acc when acc == @none -> {:halt, acc}
+          {_dom, ret}, acc -> {:cont, intersection(acc, ret)}
+        end)
+        |> case do
+          :term -> {:halt, :term}
+          inner -> {:cont, union(inner, acc)}
+        end
+      end)
+    else
+      Enum.reduce(arrows, none(), fn intersection_of_arrows, acc ->
+        aux_apply(acc, type_args, term(), intersection_of_arrows)
+      end)
     end
   end
 
@@ -1200,9 +1242,9 @@ defmodule Module.Types.Descr do
   # Takes all the paths from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Positive nodes are
   # those followed by a left path, negative nodes are those followed by a right path.
-  def fun_get(bdd), do: fun_get([], [], [], bdd)
+  defp fun_get(bdd), do: fun_get([], [], [], bdd)
 
-  def fun_get(acc, pos, neg, bdd) do
+  defp fun_get(acc, pos, neg, bdd) do
     case bdd do
       :fun_bottom -> acc
       :fun_top -> [{pos, neg} | acc]
@@ -1210,45 +1252,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Transforms a binary decision diagram (BDD) into the canonical form {domain, arrows, arity}:
-  #
-  # 1. **domain**: The union of all domains from positive functions in the BDD
-  # 2. **arrows**: List of lists, where each inner list contains an intersection of function arrows
-  # 3. **arity**: Function arity (number of parameters)
-  #
-  ## Return Values
-  #
-  # - `{domain, arrows, arity}` for valid function BDDs
-  # - `:badfun` if the BDD represents an empty function type
-  #
-  # ## Internal Use
-  #
-  # This function is used internally by `fun_apply`, `fun_domain`, and others to
-  # ensure consistent handling of function types in all operations.
-  defp fun_normalize(bdd) do
-    {domain, arrows, arity} =
-      fun_get(bdd)
-      |> Enum.reduce({term(), [], nil}, fn {pos_funs, neg_funs}, {domain, arrows, arity} ->
-        # Skip empty function intersections
-        if fun_empty?(pos_funs, neg_funs) do
-          {domain, arrows, arity}
-        else
-          # Determine arity from first positive function or keep existing
-          new_arity = arity || pos_funs |> List.first() |> elem(0) |> length()
-
-          # Calculate domain from all positive functions
-          path_domain =
-            Enum.reduce(pos_funs, none(), fn {args, _}, acc ->
-              union(acc, domain_descr(args))
-            end)
-
-          {intersection(domain, path_domain), [pos_funs | arrows], new_arity}
-        end
-      end)
-
-    if arrows == [], do: :badfun, else: {domain, arrows, arity}
-  end
-
   # Checks if a function type is empty.
   #
   # A function type is empty if:
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 7747a6bb74..56f60126eb 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -13,12 +13,6 @@ defmodule Module.Types.DescrTest do
   import Module.Types.Descr
 
   describe "union" do
-    test "zoom" do
-      # 1. dynamic() -> dynamic() applied to dynamic() gives dynamic()
-      f = fun([dynamic()], dynamic())
-      assert fun_apply(f, [dynamic()]) == dynamic()
-    end
-
     test "bitmap" do
       assert union(integer(), float()) == union(float(), integer())
     end
@@ -339,6 +333,10 @@ defmodule Module.Types.DescrTest do
       # Intersection with proper list (should result in empty list)
       assert intersection(list(integer(), atom()), list(integer())) == empty_list()
     end
+
+    test "function" do
+      assert not empty?(intersection(negation(fun(2)), negation(fun(3))))
+    end
   end
 
   describe "difference" do
@@ -753,150 +751,184 @@ defmodule Module.Types.DescrTest do
     end
   end
 
-  describe "function operators" do
-    defmacro assert_domain(f, expected) do
-      quote do
-        assert equal?(fun_domain(unquote(f)), domain_descr(unquote(expected)))
-      end
+  describe "function application" do
+    test "non funs" do
+      assert fun_apply(term(), [integer()]) == :badfun
+      assert fun_apply(union(integer(), fun(1)), [integer()]) == :badfun
     end
 
-    test "domain operator" do
-      # For function domain:
-      # 1. The domain of an intersection of functions is the union of the domains of the functions
-      # 2. The domain of a union of functions is the intersection of the domains of the functions
-      # 3. If a type is not a function or its domain is empty, return :badfun
-
-      # For gradual domain of a function type t:
-      # It is dom(t) = dom(up(t)) ∪ dynamic(dom(down(t)))
-      # where dom is the static domain, up is the upcast, and down is the downcast.
-
-      ## Basic domain tests
-      assert fun_domain(term()) == :badfun
-      assert fun_domain(none()) == :badfun
-      assert fun_domain(intersection(fun(1), fun(2))) == :badfun
-      assert union(atom(), intersection(fun(1), fun(2))) |> fun_domain() == :badfun
-      assert fun_domain(fun([none()], term())) == :badfun
-      assert fun_domain(difference(fun([pid()], pid()), fun([pid()], term()))) == :badfun
-
-      assert_domain(fun([], term()), [])
-      assert_domain(fun([term()], atom()), [term()])
-      assert_domain(fun([integer(), atom()], boolean()), [integer(), atom()])
-      # See 1. for intersection of functions
-      assert_domain(intersection(fun([float()], term()), fun([integer()], term())), [number()])
-      # See 2. for union of functions
-      assert_domain(union(fun([number()], term()), fun([float()], term())), [float()])
-
-      ## Gradual domain tests
-      assert fun_domain(dynamic()) == :badfun
-      assert fun_domain(intersection(dynamic(), fun([none()], term()))) == :badfun
-      assert_domain(fun([dynamic()], dynamic()), [dynamic()])
-      assert_domain(fun([dynamic(), dynamic()], dynamic()), [dynamic(), dynamic()])
-      assert_domain(intersection(fun([integer()], atom()), dynamic()), [integer()])
-      assert_domain(intersection(fun([integer()], term()), fun([float()], term())), [number()])
-
-      assert_domain(
-        intersection(fun([dynamic(integer())], float()), fun([float()], term())),
-        [union(dynamic(integer()), float())]
-      )
-
-      assert_domain(
-        intersection(fun([dynamic(integer())], term()), fun([integer()], term())),
-        [integer()]
-      )
-
-      # Domain of an intersection is union of domains
-      f = intersection(fun([atom(), pid()], term()), fun([pid(), atom()], term()))
-      dom = fun_domain(f)
-      refute dom |> equal?(domain_descr([union(atom(), pid()), union(pid(), atom())]))
-      assert dom |> equal?(union(domain_descr([atom(), pid()]), domain_descr([pid(), atom()])))
-
-      assert_domain(
-        intersection(fun([none(), integer()], term()), fun([float(), float()], term())),
-        [float(), float()]
-      )
-
-      # Intersection of domains int and float is empty
-      assert union(fun([integer()], atom()), fun([float()], boolean())) |> fun_domain() ==
-               :badfun
-    end
-
-    test "function application" do
-      # This should not be empty
-      assert not empty?(intersection(negation(fun(2)), negation(fun(3))))
-
+    test "static" do
       # Basic function application scenarios
-      assert fun_apply(fun([integer()], atom()), [integer()]) == atom()
+      assert fun_apply(fun([integer()], atom()), [integer()]) == {:ok, atom()}
       assert fun_apply(fun([integer()], atom()), [float()]) == :badarg
       assert fun_apply(fun([integer()], atom()), [term()]) == :badarg
-      assert fun_apply(fun([integer()], none()), [integer()]) == none()
-      assert fun_apply(fun([integer()], term()), [integer()]) == term()
+      assert fun_apply(fun([integer()], none()), [integer()]) == {:ok, none()}
+      assert fun_apply(fun([integer()], term()), [integer()]) == {:ok, term()}
 
-      # Arity mismatches
-      assert fun_apply(fun([dynamic()], integer()), [dynamic(), dynamic()]) == :badarg
-      assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, 2}
+      # Dynamic args
+      assert fun_apply(fun([term()], term()), [dynamic()]) == {:ok, term()}
 
-      # Dynamic type handling
-      assert fun_apply(fun([dynamic()], term()), [dynamic()]) == term()
-      assert fun_apply(fun([dynamic()], integer()), [dynamic()]) |> equal?(integer())
-      assert fun_apply(fun([dynamic(), atom()], float()), [dynamic(), atom()]) |> equal?(float())
-      assert fun_apply(fun([integer()], dynamic()), [integer()]) == dynamic()
+      # Arity mismatches
+      assert fun_apply(fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
+      assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, [2]}
 
       # Function intersection tests - basic
       fun1 = intersection(fun([integer()], atom()), fun([number()], term()))
-      assert fun_apply(fun1, [integer()]) == atom()
-      assert fun_apply(fun1, [float()]) == term()
+      assert fun_apply(fun1, [integer()]) == {:ok, atom()}
+      assert fun_apply(fun1, [float()]) == {:ok, term()}
+
+      # Function intersection with unions
+      fun2 =
+        intersection(
+          fun([union(integer(), atom())], term()),
+          fun([union(integer(), pid())], atom())
+        )
+
+      assert fun_apply(fun2, [integer()]) == {:ok, atom()}
+      assert fun_apply(fun2, [atom()]) == {:ok, term()}
+      assert fun_apply(fun2, [pid()]) == {:ok, atom()}
 
       # Function intersection with same domain, different codomains
       assert fun([integer()], term())
              |> intersection(fun([integer()], atom()))
-             |> fun_apply([integer()]) == atom()
+             |> fun_apply([integer()]) == {:ok, atom()}
 
       # Function intersection with singleton atoms
       fun3 = intersection(fun([atom([:ok])], atom([:success])), fun([atom([:ok])], atom([:done])))
-      assert fun_apply(fun3, [atom([:ok])]) == none()
+      assert fun_apply(fun3, [atom([:ok])]) == {:ok, none()}
+    end
+
+    test "static with dynamic signature" do
+      assert fun_apply(fun([dynamic()], term()), [dynamic()]) == {:ok, term()}
+      assert fun_apply(fun([integer()], dynamic()), [integer()]) == {:ok, dynamic()}
+
+      assert fun_apply(fun([dynamic()], integer()), [dynamic()])
+             |> elem(1)
+             |> equal?(integer())
+
+      assert fun_apply(fun([dynamic(), atom()], float()), [dynamic(), atom()])
+             |> elem(1)
+             |> equal?(float())
+
+      fun = fun([dynamic(integer())], atom())
+      assert fun_apply(fun, [dynamic(integer())]) |> elem(1) |> equal?(atom())
+      assert fun_apply(fun, [dynamic(number())]) == :badarg
+      assert fun_apply(fun, [integer()]) == :badarg
+      assert fun_apply(fun, [float()]) == :badarg
+    end
+
+    defp dynamic_fun(args, return), do: dynamic(fun(args, return))
+
+    test "dynamic" do
+      # Basic function application scenarios
+      assert fun_apply(dynamic_fun([integer()], atom()), [integer()]) == {:ok, dynamic(atom())}
+      assert fun_apply(dynamic_fun([integer()], atom()), [float()]) == :badarg
+      assert fun_apply(dynamic_fun([integer()], atom()), [term()]) == :badarg
+      assert fun_apply(dynamic_fun([integer()], none()), [integer()]) == {:ok, dynamic(none())}
+      assert fun_apply(dynamic_fun([integer()], term()), [integer()]) == {:ok, dynamic()}
+
+      # Dynamic return and dynamic args
+      assert fun_apply(dynamic_fun([term()], term()), [dynamic()]) == {:ok, dynamic()}
+
+      fun = dynamic_fun([integer()], binary())
+      assert fun_apply(fun, [integer()]) == {:ok, dynamic(binary())}
+      assert fun_apply(fun, [dynamic(integer())]) == {:ok, dynamic(binary())}
+      assert fun_apply(fun, [dynamic(atom())]) == :badarg
 
-      # (dynamic(integer()) -> atom()
-      # cannot apply it to integer() bc integer() is not a subtype of dynamic() /\ integer()
-      # dynamic(atom())
+      # Arity mismatches
+      assert fun_apply(dynamic_fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
+
+      assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
+               {:badarity, [2]}
+
+      # Function intersection tests
+      fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))
+      assert fun_apply(fun0, [integer()]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun0, [float()]) == {:ok, dynamic(binary())}
+      assert fun_apply(fun0, [dynamic(integer())]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun0, [dynamic(float())]) == {:ok, dynamic(binary())}
+      assert fun_apply(fun0, [dynamic(number())]) == {:ok, dynamic(union(binary(), atom()))}
+
+      # Function intersection with subset domain
+      fun1 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([number()], term()))
+      assert fun_apply(fun1, [integer()]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun1, [float()]) == {:ok, dynamic()}
+      assert fun_apply(fun1, [dynamic(integer())]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun1, [dynamic(float())]) == {:ok, dynamic()}
+
+      # Function intersection with same domain, different codomains
+      assert dynamic_fun([integer()], term())
+             |> intersection(dynamic_fun([integer()], atom()))
+             |> fun_apply([integer()]) == {:ok, dynamic(atom())}
+
+      # Function intersection with overlapping domains
+      fun2 =
+        intersection(
+          dynamic_fun([union(integer(), atom())], term()),
+          dynamic_fun([union(integer(), pid())], atom())
+        )
 
-      # $ dynamic(map()) -> map()
-      # def f(x) when is_map(x) do
-      #     x.foo
-      # end
+      assert fun_apply(fun2, [integer()]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun2, [atom()]) == {:ok, dynamic()}
+      assert fun_apply(fun2, [pid()]) |> elem(1) |> equal?(dynamic(atom()))
 
-      fun9 = fun([intersection(dynamic(), integer())], atom())
-      assert fun_apply(fun9, [dynamic(integer())]) |> equal?(atom())
-      assert fun_apply(fun9, [dynamic()]) == :badarg
-      # TODO: discuss this case
-      assert fun_apply(fun9, [integer()]) == :badarg
+      assert fun_apply(fun2, [dynamic(integer())]) == {:ok, dynamic(atom())}
+      assert fun_apply(fun2, [dynamic(atom())]) == {:ok, dynamic()}
+      assert fun_apply(fun2, [dynamic(pid())]) |> elem(1) |> equal?(dynamic(atom()))
 
-      # Dynamic with function type combinations
-      fun12 =
+      # Function intersection with singleton atoms
+      fun3 =
         intersection(
-          fun([union(integer(), atom())], dynamic()),
-          fun([union(integer(), pid())], atom())
+          dynamic_fun([atom([:ok])], atom([:success])),
+          dynamic_fun([atom([:ok])], atom([:done]))
         )
 
-      assert fun_apply(fun12, [integer()]) == dynamic(atom())
-      assert fun_apply(fun12, [atom()]) == dynamic()
-      assert fun_apply(fun12, [pid()]) |> equal?(atom())
+      assert fun_apply(fun3, [atom([:ok])]) == {:ok, dynamic(none())}
     end
-  end
 
-  describe "projections" do
-    test "fun_fetch" do
-      assert fun_fetch(none(), 1) == :error
-      assert fun_fetch(term(), 1) == :error
-      assert fun_fetch(union(term(), dynamic(fun())), 1) == :error
-      assert fun_fetch(union(atom(), dynamic(fun())), 1) == :error
-      assert fun_fetch(intersection(fun([], term()), fun([], atom())), 0) == :ok
-      assert fun_fetch(fun([], term()), 0) == :ok
-      assert fun_fetch(union(fun([], term()), fun([pid()], term())), 0) == :error
-      assert fun_fetch(dynamic(fun()), 1) == :ok
-      assert fun_fetch(dynamic(), 1) == :ok
-      assert fun_fetch(dynamic(fun(2)), 1) == :error
+    test "static and dynamic" do
+      # Bad arity
+      fun_arities =
+        union(
+          fun([atom()], integer()),
+          dynamic_fun([integer(), float()], binary())
+        )
+
+      assert fun_arities
+             |> fun_apply([atom()])
+             |> elem(1)
+             |> equal?(integer())
+
+      assert fun_arities |> fun_apply([integer(), float()]) == {:badarity, [1]}
+
+      # Bad argument
+      fun_args =
+        union(
+          fun([atom()], integer()),
+          dynamic_fun([integer()], binary())
+        )
+
+      assert fun_args |> fun_apply([atom()]) == :badarg
+      assert fun_args |> fun_apply([integer()]) == :badarg
+
+      # Badfun
+      assert union(
+               fun([atom()], integer()),
+               dynamic_fun([integer()], binary()) |> intersection(fun(2))
+             )
+             |> fun_apply([atom()])
+             |> elem(1)
+             |> equal?(integer())
+
+      assert union(
+               fun([atom()], integer()) |> intersection(fun(2)),
+               dynamic_fun([integer()], binary())
+             )
+             |> fun_apply([integer()]) == {:ok, dynamic(binary())}
     end
+  end
 
+  describe "projections" do
     test "truthiness" do
       for type <- [term(), none(), atom(), boolean(), union(atom([false]), integer())] do
         assert truthiness(type) == :undefined
@@ -1676,6 +1708,12 @@ defmodule Module.Types.DescrTest do
       assert fun() |> to_quoted_string() == "fun()"
       assert fun(1) |> to_quoted_string() == "(none() -> term())"
 
+      assert fun([dynamic(integer())], float()) |> to_quoted_string() ==
+               "dynamic((none() -> float())) or (integer() -> float())"
+
+      assert fun([integer(), float()], dynamic()) |> to_quoted_string() ==
+               "dynamic((integer(), float() -> term())) or (integer(), float() -> none())"
+
       assert fun([integer(), float()], boolean()) |> to_quoted_string() ==
                "(integer(), float() -> boolean())"
 
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 7af6b1368a..1d6fc8bdf6 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -422,6 +422,17 @@ defmodule Module.Types.ExprTest do
     end
   end
 
+  describe "remote capture" do
+    test "strong" do
+      assert typecheck!(&String.to_atom/1) == fun([binary()], atom())
+    end
+
+    test "unknown" do
+      assert typecheck!(&Module.Types.ExprTest.__ex_unit__/1) == dynamic(fun(1))
+      assert typecheck!([x], &x.something/1) == dynamic(fun(1))
+    end
+  end
+
   describe "binaries" do
     test "inference" do
       assert typecheck!(