diff --git a/lib/elixir/lib/module/parallel_checker.ex b/lib/elixir/lib/module/parallel_checker.ex
index 87d81c8220..dcf5fe9b6e 100644
--- a/lib/elixir/lib/module/parallel_checker.ex
+++ b/lib/elixir/lib/module/parallel_checker.ex
@@ -208,7 +208,7 @@ defmodule Module.ParallelChecker do
   or if the function does not exist return `{:error, :function}`.
   """
   @spec fetch_export(cache(), module(), atom(), arity()) ::
-          {:ok, mode(), binary() | nil, {:infer, [term()]} | :none}
+          {:ok, mode(), binary() | nil, {:infer, [term()] | nil, [term()]} | :none}
           | :badmodule
           | {:badfunction, mode()}
   def fetch_export({checker, table}, module, fun, arity) do
@@ -451,10 +451,15 @@ defmodule Module.ParallelChecker do
 
   defp cache_chunk(table, module, exports) do
     Enum.each(exports, fn {{fun, arity}, info} ->
-      # TODO: Match on signature directly in Elixir v1.22+
+      sig =
+        case info do
+          %{sig: {key, _, _} = sig} when key in [:infer, :strong] -> sig
+          _ -> :none
+        end
+
       :ets.insert(
         table,
-        {{module, {fun, arity}}, Map.get(info, :deprecated), Map.get(info, :sig, :none)}
+        {{module, {fun, arity}}, Map.get(info, :deprecated), sig}
       )
     end)
 
diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index 4374e4c0e2..1d1532d10f 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -281,11 +281,18 @@ defmodule Module.Types do
           context = fresh_context(context)
 
           try do
-            {args_types, context} =
+            {trees, context} =
               Pattern.of_head(args, guards, expected, {:infer, expected}, meta, stack, context)
 
             {return_type, context} =
-              Expr.of_expr(body, stack, context)
+              Expr.of_expr(body, Descr.term(), body, stack, context)
+
+            args_types =
+              if stack.mode == :traversal do
+                expected
+              else
+                Pattern.of_domain(trees, expected, context)
+              end
 
             {type_index, inferred} =
               add_inferred(inferred, args_types, return_type, total - 1, [])
@@ -301,8 +308,19 @@ defmodule Module.Types do
           end
       end)
 
-    inferred = {:infer, Enum.reverse(clauses_types)}
-    {inferred, mapping, restore_context(context, clauses_context)}
+    domain =
+      case clauses_types do
+        [_] ->
+          nil
+
+        _ ->
+          clauses_types
+          |> Enum.map(fn {args, _} -> args end)
+          |> Enum.zip_with(fn types -> Enum.reduce(types, &Descr.union/2) end)
+      end
+
+    inferred = {:infer, domain, Enum.reverse(clauses_types)}
+    {inferred, mapping, restore_context(clauses_context, context)}
   end
 
   # We check for term equality of types as an optimization
@@ -399,7 +417,7 @@ defmodule Module.Types do
     %{context | vars: %{}, failed: false}
   end
 
-  defp restore_context(%{vars: vars, failed: failed}, later_context) do
+  defp restore_context(later_context, %{vars: vars, failed: failed}) do
     %{later_context | vars: vars, failed: failed}
   end
 
diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index 9ca5e96caf..d403658981 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -72,16 +72,16 @@ defmodule Module.Types.Apply do
     domain = atom(Keyword.keys(clauses))
     clauses = Enum.map(clauses, fn {key, return} -> {[atom([key])], return} end)
 
-    defp signature(unquote(name), 1) do
+    def signature(unquote(name), 1) do
       {:strong, [unquote(Macro.escape(domain))], unquote(Macro.escape(clauses))}
     end
   end
 
-  defp signature(:module_info, 0) do
+  def signature(:module_info, 0) do
     {:strong, nil, [{[], unquote(Macro.escape(kw.(module_info)))}]}
   end
 
-  defp signature(_, _), do: :none
+  def signature(_, _), do: :none
 
   # Remote for compiler functions
 
@@ -254,200 +254,224 @@ defmodule Module.Types.Apply do
           {:strong, domain, clauses}
       end
 
-    defp signature(unquote(mod), unquote(fun), unquote(arity)),
+    def signature(unquote(mod), unquote(fun), unquote(arity)),
       do: unquote(Macro.escape(domain_clauses))
   end
 
-  defp signature(_mod, _fun, _arity), do: :none
+  def signature(_mod, _fun, _arity), do: :none
 
   @doc """
-  Applies a function in unknown modules.
+  Returns the domain of an unknown module.
 
   Used only by info functions.
   """
-  def remote(_name, _args_types, _expr, %{mode: :traversal}, context) do
-    {dynamic(), context}
+  def remote_domain(_fun, args, _expected, %{mode: :traversal}) do
+    {:none, Enum.map(args, fn _ -> term() end)}
   end
 
-  def remote(name, args_types, expr, stack, context) do
-    arity = length(args_types)
+  def remote_domain(fun, args, _expected, _stack) do
+    arity = length(args)
 
-    case signature(name, arity) do
-      :none -> {dynamic(), context}
-      info -> apply_remote(nil, name, info, args_types, expr, stack, context)
+    case signature(fun, arity) do
+      :none -> {:none, Enum.map(args, fn _ -> term() end)}
+      {:strong, domain, clauses} = info -> {info, domain(domain, clauses)}
     end
   end
 
   @doc """
-  Applies a function in a given module.
+  Returns the domain of a remote function with info to apply it.
   """
-  def remote(_module, _fun, _args, _args_types, _expr, %{mode: :traversal}, context) do
-    {dynamic(), context}
+  def remote_domain(_module, _fun, args, _expected, _meta, %{mode: :traversal}, context) do
+    {:none, Enum.map(args, fn _ -> term() end), context}
   end
 
-  def remote(:erlang, :element, [index, _], [_, tuple], expr, stack, context)
+  def remote_domain(:erlang, :element, [index, _], expected, _meta, _stack, context)
       when is_integer(index) do
-    case tuple_fetch(tuple, index - 1) do
-      {_optional?, value_type} ->
-        {value_type, context}
-
-      :badtuple ->
-        {error_type(),
-         badremote_error(:erlang, :element, expr, [integer(), tuple], stack, context)}
-
-      :badindex ->
-        mfac = mfac(expr, :erlang, :element, 2)
+    tuple = open_tuple(List.duplicate(term(), max(index - 1, 0)) ++ [expected])
+    {{:element, index}, [integer(), tuple], context}
+  end
 
-        {error_type(),
-         error({:badindex, mfac, expr, tuple, index - 1, context}, elem(expr, 1), stack, context)}
-    end
+  def remote_domain(:erlang, :insert_element, [index, _, _], _expected, _meta, _stack, context)
+      when is_integer(index) do
+    tuple = open_tuple(List.duplicate(term(), max(index - 1, 0)))
+    {{:insert_element, index}, [integer(), tuple, term()], context}
   end
 
-  def remote(:erlang, :insert_element, [index, _, _], [_, tuple, value], expr, stack, context)
+  def remote_domain(:erlang, :delete_element, [index, _], _expected, _meta, _stack, context)
       when is_integer(index) do
-    case tuple_insert_at(tuple, index - 1, value) do
-      value_type when is_descr(value_type) ->
-        {value_type, context}
+    tuple = open_tuple(List.duplicate(term(), max(index, 1)))
+    {{:delete_element, index}, [integer(), tuple], context}
+  end
+
+  def remote_domain(:erlang, :make_tuple, [size, _elem], _expected, _meta, _stack, context)
+      when is_integer(size) and size >= 0 do
+    {{:make_tuple, size}, [integer(), term()], context}
+  end
 
-      :badtuple ->
-        args_types = [integer(), tuple, value]
+  def remote_domain(:erlang, :hd, [_list], expected, _meta, _stack, context) do
+    {:hd, [non_empty_list(expected, term())], context}
+  end
 
-        {error_type(),
-         badremote_error(:erlang, :insert_element, expr, args_types, stack, context)}
+  def remote_domain(:erlang, :tl, [_list], _expected, _meta, _stack, context) do
+    {:tl, [non_empty_list(term(), term())], context}
+  end
 
-      :badindex ->
-        mfac = mfac(expr, :erlang, :insert_element, 3)
+  def remote_domain(:erlang, name, [_left, _right], _expected, _meta, stack, context)
+      when name in [:>=, :"=<", :>, :<, :min, :max] do
+    skip? = stack.mode == :infer
+    {{:ordered_compare, name, skip?}, [term(), term()], context}
+  end
 
-        {error_type(),
-         error({:badindex, mfac, expr, tuple, index - 2, context}, elem(expr, 1), stack, context)}
-    end
+  def remote_domain(:erlang, name, [_left, _right] = args, _expected, _meta, stack, context)
+      when name in [:==, :"/=", :"=:=", :"=/="] do
+    skip? = stack.mode == :infer or Macro.quoted_literal?(args)
+    {{:compare, name, skip?}, [term(), term()], context}
   end
 
-  def remote(:erlang, :delete_element, [index, _], [_, tuple], expr, stack, context)
-      when is_integer(index) do
-    case tuple_delete_at(tuple, index - 1) do
-      value_type when is_descr(value_type) ->
-        {value_type, context}
+  def remote_domain(mod, fun, args, expected, meta, stack, context) do
+    arity = length(args)
 
-      :badtuple ->
-        args_types = [integer(), tuple]
+    case :elixir_rewrite.inline(mod, fun, arity) do
+      {new_mod, new_fun} ->
+        remote_domain(new_mod, new_fun, args, expected, meta, stack, context)
 
-        {error_type(),
-         badremote_error(:erlang, :delete_element, expr, args_types, stack, context)}
+      false ->
+        {info, context} = signature(mod, fun, arity, meta, stack, context)
 
-      :badindex ->
-        mfac = mfac(expr, :erlang, :delete_element, 2)
+        case info do
+          {type, domain, clauses} ->
+            domain = domain(domain, clauses)
+            {{type, domain, clauses}, domain, context}
 
-        {error_type(),
-         error({:badindex, mfac, expr, tuple, index - 1, context}, elem(expr, 1), stack, context)}
+          :none ->
+            {:none, List.duplicate(term(), arity), context}
+        end
     end
   end
 
-  def remote(:erlang, :make_tuple, [size, _], [_, elem], _expr, _stack, context)
-      when is_integer(size) and size >= 0 do
-    {tuple(List.duplicate(elem, size)), context}
+  @doc """
+  Applies a previously collected domain from `remote_domain/7`.
+  """
+  def remote_apply(info, mod, fun, args_types, expr, stack, context) do
+    case remote_apply(info, args_types, stack) do
+      {:ok, type} ->
+        {type, context}
+
+      {:error, error} ->
+        mfac = mfac(expr, mod, fun, length(args_types))
+        error = {error, args_types, mfac, expr, context}
+        {error_type(), error(error, elem(expr, 1), stack, context)}
+    end
   end
 
-  def remote(:erlang, :hd, _args, [list], expr, stack, context) do
-    case list_hd(list) do
-      {_, value_type} ->
-        {value_type, context}
+  defp remote_apply(:none, _args_types, _stack) do
+    {:ok, dynamic()}
+  end
 
-      :badnonemptylist ->
-        {error_type(), badremote_error(:erlang, :hd, expr, [list], stack, context)}
+  defp remote_apply({:infer, domain, clauses}, args_types, _stack) do
+    case apply_infer(domain, clauses, args_types) do
+      {_used, type} -> {:ok, type}
+      {:error, domain, clauses} -> {:error, {:badremote, domain, clauses}}
     end
   end
 
-  def remote(:erlang, :tl, _args, [list], expr, stack, context) do
-    case list_tl(list) do
-      {_, value_type} ->
-        {value_type, context}
-
-      :badnonemptylist ->
-        {error_type(), badremote_error(:erlang, :tl, expr, [list], stack, context)}
+  defp remote_apply({:strong, domain, clauses}, args_types, stack) do
+    case apply_strong(domain, clauses, args_types, stack) do
+      {_used, type} -> {:ok, type}
+      {:error, domain, clauses} -> {:error, {:badremote, domain, clauses}}
     end
   end
 
-  def remote(:erlang, name, _args, [left, right], expr, stack, context)
-      when name in [:>=, :"=<", :>, :<, :min, :max] do
-    context =
-      cond do
-        stack.mode == :infer ->
-          context
+  defp remote_apply({:element, index}, [_index, tuple], _stack) do
+    case tuple_fetch(tuple, index - 1) do
+      {_optional?, value_type} -> {:ok, value_type}
+      :badtuple -> {:error, badremote(:erlang, :element, 2)}
+      :badindex -> {:error, {:badindex, index, tuple}}
+    end
+  end
 
-        match?({false, _}, map_fetch(left, :__struct__)) or
-            match?({false, _}, map_fetch(right, :__struct__)) ->
-          warning = {:struct_comparison, expr, name, left, right, context}
-          warn(__MODULE__, warning, elem(expr, 1), stack, context)
+  defp remote_apply({:insert_element, index}, [_index, tuple, value], _stack) do
+    case tuple_insert_at(tuple, index - 1, value) do
+      value_type when is_descr(value_type) -> {:ok, value_type}
+      :badtuple -> {:error, badremote(:erlang, :insert_element, 3)}
+      :badindex -> {:error, {:badindex, index - 1, tuple}}
+    end
+  end
 
-        number_type?(left) and number_type?(right) ->
-          context
+  defp remote_apply({:delete_element, index}, [_index, tuple], _stack) do
+    case tuple_delete_at(tuple, index - 1) do
+      value_type when is_descr(value_type) -> {:ok, value_type}
+      :badtuple -> {:error, badremote(:erlang, :delete_element, 2)}
+      :badindex -> {:error, {:badindex, index, tuple}}
+    end
+  end
 
-        disjoint?(left, right) ->
-          warning = {:mismatched_comparison, expr, name, left, right, context}
-          warn(__MODULE__, warning, elem(expr, 1), stack, context)
+  defp remote_apply({:make_tuple, size}, [_size, elem], _stack) do
+    {:ok, tuple(List.duplicate(elem, size))}
+  end
 
-        true ->
-          context
-      end
+  defp remote_apply(:hd, [list], _stack) do
+    case list_hd(list) do
+      {_, value_type} -> {:ok, value_type}
+      :badnonemptylist -> {:error, badremote(:erlang, :hd, 1)}
+    end
+  end
 
-    if name in [:min, :max] do
-      {union(left, right), context}
-    else
-      {return(boolean(), [left, right], stack), context}
+  defp remote_apply(:tl, [list], _stack) do
+    case list_tl(list) do
+      {_, value_type} -> {:ok, value_type}
+      :badnonemptylist -> {:error, badremote(:erlang, :tl, 1)}
     end
   end
 
-  def remote(:erlang, name, args, [left, right] = args_types, expr, stack, context)
-      when name in [:==, :"/=", :"=:=", :"=/="] do
-    context =
-      cond do
-        # We ignore quoted literals as they most likely come from generated code.
-        stack.mode == :infer or Macro.quoted_literal?(args) ->
-          context
+  defp remote_apply({:ordered_compare, name, skip?}, [left, right], stack) do
+    result =
+      if name in [:min, :max] do
+        union(left, right)
+      else
+        return(boolean(), [left, right], stack)
+      end
 
-        name in [:==, :"/="] and number_type?(left) and number_type?(right) ->
-          context
+    cond do
+      skip? ->
+        {:ok, result}
 
-        disjoint?(left, right) ->
-          warning = {:mismatched_comparison, expr, name, left, right, context}
-          warn(__MODULE__, warning, elem(expr, 1), stack, context)
+      match?({false, _}, map_fetch(left, :__struct__)) or
+          match?({false, _}, map_fetch(right, :__struct__)) ->
+        {:error, :struct_comparison}
 
-        true ->
-          context
-      end
+      number_type?(left) and number_type?(right) ->
+        {:ok, result}
+
+      disjoint?(left, right) ->
+        {:error, :mismatched_comparison}
 
-    {return(boolean(), args_types, stack), context}
+      true ->
+        {:ok, result}
+    end
   end
 
-  def remote(mod, fun, args, args_types, expr, stack, context) do
-    arity = length(args_types)
+  defp remote_apply({:compare, name, skip?}, [left, right], stack) do
+    result = return(boolean(), [left, right], stack)
 
-    case :elixir_rewrite.inline(mod, fun, arity) do
-      {new_mod, new_fun} ->
-        expr = inline_meta(expr, mod, fun)
-        remote(new_mod, new_fun, args, args_types, expr, stack, context)
+    cond do
+      skip? ->
+        {:ok, result}
 
-      false ->
-        {info, context} = signature(mod, fun, arity, elem(expr, 1), stack, context)
-        apply_remote(mod, fun, info, args_types, expr, stack, context)
-    end
-  end
+      name in [:==, :"/="] and number_type?(left) and number_type?(right) ->
+        {:ok, result}
 
-  defp apply_remote(mod, fun, info, args_types, expr, stack, context) do
-    case apply_signature(info, args_types, stack) do
-      {:ok, _indexes, type} ->
-        {type, context}
+      disjoint?(left, right) ->
+        {:error, :mismatched_comparison}
 
-      {:error, domain, clauses} ->
-        mfac = mfac(expr, mod, fun, length(args_types))
-        error = {:badremote, mfac, expr, args_types, domain, clauses, context}
-        {error_type(), error(error, elem(expr, 1), stack, context)}
+      true ->
+        {:ok, result}
     end
   end
 
-  defp inline_meta({node, meta, args}, mod, fun) do
-    {node, [inline: {mod, fun}] ++ meta, args}
+  defp badremote(mod, fun, arity) do
+    {_, domain, clauses} = signature(mod, fun, arity)
+    {:badremote, domain, clauses}
   end
 
   @doc """
@@ -478,7 +502,7 @@ defmodule Module.Types.Apply do
 
     * `:none` - no typing information found.
 
-    * `{:infer, clauses}` - clauses from inferences. You must check all
+    * `{: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.
@@ -604,48 +628,63 @@ defmodule Module.Types.Apply do
 
   ## Local
 
-  @doc """
-  Deal with local functions.
-  """
-  def local(fun, args_types, {_, meta, _} = expr, stack, context) do
-    fun_arity = {fun, length(args_types)}
+  def local_domain(fun, args, meta, stack, context) do
+    arity = length(args)
 
-    case stack.local_handler.(meta, fun_arity, stack, context) do
+    case stack.local_handler.(meta, {fun, arity}, stack, context) do
       false ->
-        {dynamic(), context}
-
-      {_kind, _info, context} when stack.mode == :traversal ->
-        {dynamic(), context}
+        {{false, :none}, List.duplicate(term(), arity), context}
 
       {kind, info, context} ->
-        case apply_signature(info, args_types, stack) do
-          {:ok, indexes, type} ->
-            context =
-              if stack.mode != :infer and kind == :defp do
-                update_in(context.local_used[fun_arity], fn current ->
-                  if info == :none do
-                    []
-                  else
-                    (current || used_from_clauses(info)) -- indexes
-                  end
-                end)
+        update_used? = stack.mode not in [:traversal, :infer] and kind == :defp
+
+        case info do
+          _ when stack.mode == :traversal or info == :none ->
+            {{update_used?, :none}, List.duplicate(term(), arity), context}
+
+          {_strong_or_infer, domain, clauses} ->
+            {{update_used?, info}, domain(domain, clauses), context}
+        end
+    end
+  end
+
+  def local_apply({update_used?, info}, fun, args_types, expr, stack, context) do
+    case local_apply(info, args_types, stack) do
+      {indexes, type} ->
+        context =
+          if update_used? do
+            update_in(context.local_used[{fun, length(args_types)}], fn current ->
+              if info == :none do
+                []
               else
-                context
+                (current || used_from_clauses(info)) -- indexes
               end
+            end)
+          else
+            context
+          end
 
-            {type, context}
+        {type, context}
 
-          {:error, domain, clauses} ->
-            error = {:badlocal, expr, args_types, domain, clauses, context}
-            {error_type(), error(error, with_span(meta, fun), stack, context)}
-        end
+      {:error, domain, clauses} ->
+        error = {:badlocal, domain, clauses, args_types, expr, context}
+        {error_type(), error(error, with_span(elem(expr, 1), fun), stack, context)}
     end
   end
 
-  defp used_from_clauses({:infer, clauses}),
-    do: Enum.with_index(clauses, fn _, i -> i end)
+  defp local_apply(:none, _args_types, _stack) do
+    {[], dynamic()}
+  end
 
-  defp used_from_clauses({:strong, _, clauses}),
+  defp local_apply({:infer, domain, clauses}, args_types, _stack) do
+    apply_infer(domain, clauses, args_types)
+  end
+
+  defp local_apply({:strong, domain, clauses}, args_types, stack) do
+    apply_strong(domain, clauses, args_types, stack)
+  end
+
+  defp used_from_clauses({_strong_or_infer, _domain, clauses}),
     do: Enum.with_index(clauses, fn _, i -> i end)
 
   @doc """
@@ -681,47 +720,41 @@ defmodule Module.Types.Apply do
     end
   end
 
-  defp apply_signature(:none, _args_types, _stack) do
-    {:ok, [], dynamic()}
+  defp domain(nil, [{domain, _}]), do: domain
+  defp domain(domain, _clauses), do: domain
+
+  defp apply_infer(domain, clauses, args_types) do
+    case apply_clauses(clauses, args_types, 0, 0, [], []) do
+      {0, [], []} ->
+        {:error, domain, clauses}
+
+      {count, used, _returns} when count > @max_clauses ->
+        {used, dynamic()}
+
+      {_count, used, returns} ->
+        {used, returns |> Enum.reduce(&union/2) |> dynamic()}
+    end
   end
 
-  defp apply_signature({:strong, nil, [{expected, return}] = clauses}, args_types, stack) do
+  defp apply_strong(domain, [{expected, return}] = clauses, args_types, stack) do
     # Optimize single clauses as the domain is the single clause args.
     case zip_compatible?(args_types, expected) do
-      true -> {:ok, [0], return(return, args_types, stack)}
-      false -> {:error, expected, clauses}
+      true -> {[0], return(return, args_types, stack)}
+      false -> {:error, domain, clauses}
     end
   end
 
-  defp apply_signature({:strong, domain, clauses}, args_types, stack) do
+  defp apply_strong(domain, clauses, args_types, stack) do
     # If the type is only gradual, the compatibility check is the same
     # as a non disjoint check. So we skip checking compatibility twice.
     with true <- zip_compatible_or_only_gradual?(args_types, domain),
          {count, used, returns} when count > 0 <- apply_clauses(clauses, args_types, 0, 0, [], []) do
-      {:ok, used, returns |> Enum.reduce(&union/2) |> return(args_types, stack)}
+      {used, returns |> Enum.reduce(&union/2) |> return(args_types, stack)}
     else
       _ -> {:error, domain, clauses}
     end
   end
 
-  defp apply_signature({:infer, clauses}, args_types, _stack) do
-    case apply_clauses(clauses, args_types, 0, 0, [], []) do
-      {0, [], []} ->
-        domain =
-          clauses
-          |> Enum.map(fn {args, _} -> args end)
-          |> Enum.zip_with(fn types -> Enum.reduce(types, &union/2) end)
-
-        {:error, domain, clauses}
-
-      {count, used, _returns} when count > @max_clauses ->
-        {:ok, used, dynamic()}
-
-      {_count, used, returns} ->
-        {:ok, used, returns |> Enum.reduce(&union/2) |> dynamic()}
-    end
-  end
-
   defp apply_clauses([{expected, return} | clauses], args_types, index, count, used, returns) do
     if zip_not_disjoint?(args_types, expected) do
       apply_clauses(clauses, args_types, index + 1, count + 1, [index | used], [return | returns])
@@ -759,73 +792,66 @@ defmodule Module.Types.Apply do
     error(__MODULE__, warning, meta, stack, context)
   end
 
-  defp badremote_error(mod, fun, {_, meta, _} = expr, args_types, stack, context) do
-    arity = length(args_types)
-    mfac = mfac(expr, mod, fun, arity)
-    {_type, domain, [{args, _} | _] = clauses} = signature(mod, fun, arity)
-    domain = domain || args
-    tuple = {:badremote, mfac, expr, args_types, domain, clauses, context}
-    error(tuple, meta, stack, context)
-  end
-
   ## Diagnostics
 
-  def format_diagnostic({:badindex, mfac, expr, type, index, context}) do
+  def format_diagnostic({:badlocal, domain, clauses, args_types, expr, context}) do
+    domain = domain(domain, clauses)
     traces = collect_traces(expr, context)
-    {mod, fun, arity, _converter} = mfac
-    mfa = Exception.format_mfa(mod, fun, arity)
+    converter = &Function.identity/1
+    {fun, _, _} = expr
+
+    explanation =
+      empty_arg_reason(args_types) ||
+        """
+        but expected one of:
+        #{clauses_args_to_quoted_string(clauses, converter, [])}
+        """
 
     %{
       details: %{typing_traces: traces},
       message:
         IO.iodata_to_binary([
           """
-          expected a tuple with at least #{pluralize(index + 1, "element", "elements")} in #{mfa}:
+          incompatible types given to #{fun}/#{length(args_types)}:
 
               #{expr_to_string(expr) |> indent(4)}
 
-          the given type does not have the given index:
+          given types:
+
+              #{args_to_quoted_string(args_types, domain, converter) |> indent(4)}
 
-              #{to_quoted_string(type) |> indent(4)}
           """,
+          explanation,
           format_traces(traces)
         ])
     }
   end
 
-  def format_diagnostic({:badlocal, expr, args_types, domain, clauses, context}) do
+  def format_diagnostic({{:badindex, index, type}, _args_types, mfac, expr, context}) do
     traces = collect_traces(expr, context)
-    converter = &Function.identity/1
-    {fun, _, _} = expr
-
-    explanation =
-      empty_arg_reason(args_types) ||
-        """
-        but expected one of:
-        #{clauses_args_to_quoted_string(clauses, converter, [])}
-        """
+    {mod, fun, arity, _converter} = mfac
+    mfa = Exception.format_mfa(mod, fun, arity)
 
     %{
       details: %{typing_traces: traces},
       message:
         IO.iodata_to_binary([
           """
-          incompatible types given to #{fun}/#{length(args_types)}:
+          expected a tuple with at least #{pluralize(index, "element", "elements")} in #{mfa}:
 
               #{expr_to_string(expr) |> indent(4)}
 
-          given types:
-
-              #{args_to_quoted_string(args_types, domain, converter) |> indent(4)}
+          the given type does not have the given index:
 
+              #{to_quoted_string(type) |> indent(4)}
           """,
-          explanation,
           format_traces(traces)
         ])
     }
   end
 
-  def format_diagnostic({:badremote, mfac, expr, args_types, domain, clauses, context}) do
+  def format_diagnostic({{:badremote, domain, clauses}, args_types, mfac, expr, context}) do
+    domain = domain(domain, clauses)
     {mod, fun, arity, converter} = mfac
     meta = elem(expr, 1)
 
@@ -911,7 +937,8 @@ defmodule Module.Types.Apply do
     }
   end
 
-  def format_diagnostic({:mismatched_comparison, expr, name, left, right, context}) do
+  def format_diagnostic({:mismatched_comparison, [left, right], mfac, expr, context}) do
+    {_, name, _, _} = mfac
     traces = collect_traces(expr, context)
 
     %{
@@ -938,7 +965,8 @@ defmodule Module.Types.Apply do
     }
   end
 
-  def format_diagnostic({:struct_comparison, expr, name, left, right, context}) do
+  def format_diagnostic({:struct_comparison, [left, right], mfac, expr, context}) do
+    {_, name, _, _} = mfac
     traces = collect_traces(expr, context)
 
     %{
@@ -1033,10 +1061,6 @@ defmodule Module.Types.Apply do
   defp pluralize(1, singular, _), do: "1 #{singular}"
   defp pluralize(i, _, plural), do: "#{i} #{plural}"
 
-  defp mfac({_, [inline: {mod, fun}] ++ _, _}, _mod, _fun, arity) do
-    {mod, fun, arity, & &1}
-  end
-
   defp mfac({{:., _, [mod, fun]}, _, args}, _mod, _fun, _arity)
        when is_atom(mod) and is_atom(fun) do
     {mod, fun, args, converter} = :elixir_rewrite.erl_to_ex(mod, fun, args)
@@ -1053,7 +1077,7 @@ defmodule Module.Types.Apply do
   alias Inspect.Algebra, as: IA
 
   defp type_comparison_to_string(fun, left, right) do
-    {Kernel, fun, [left, right], _} = :elixir_rewrite.erl_to_ex(:erlang, fun, [left, right])
+    {_, fun, _, _} = :elixir_rewrite.erl_to_ex(:erlang, fun, [left, right])
 
     {fun, [], [to_quoted(left, collapse_structs: true), to_quoted(right, collapse_structs: true)]}
     |> Code.Formatter.to_algebra()
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index e808be394a..04b3f1dee4 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -382,7 +382,8 @@ defmodule Module.Types.Descr do
       {dynamic, descr} =
         case :maps.take(:dynamic, descr) do
           :error -> {[], descr}
-          {dynamic, descr} -> {to_quoted(:dynamic, dynamic, opts), descr}
+          {:term, descr} -> {to_quoted(:dynamic, :term, opts), descr}
+          {dynamic, descr} -> {to_quoted(:dynamic, difference(dynamic, descr), opts), descr}
         end
 
       # Merge empty list and list together if they both exist
@@ -547,6 +548,41 @@ defmodule Module.Types.Descr do
     end
   end
 
+  @doc """
+  Returns the intersection between two types
+  only if they are compatible. Otherwise returns `:error`.
+
+  This finds the intersection between the arguments and the
+  domain of a function. It is used to refine dynamic types
+  as we traverse the program.
+  """
+  def compatible_intersection(left, right) do
+    {left_dynamic, left_static} =
+      case left do
+        :term -> {:term, :term}
+        _ -> Map.pop(left, :dynamic, left)
+      end
+
+    right_dynamic =
+      case right do
+        %{dynamic: dynamic} -> dynamic
+        _ -> right
+      end
+
+    cond do
+      empty?(left_static) ->
+        dynamic = intersection_static(unfold(left_dynamic), unfold(right_dynamic))
+        if empty?(dynamic), do: {:error, left}, else: {:ok, dynamic(dynamic)}
+
+      subtype_static?(left_static, right_dynamic) ->
+        dynamic = intersection_static(unfold(left_dynamic), unfold(right_dynamic))
+        {:ok, union(dynamic(dynamic), left_static)}
+
+      true ->
+        {:error, left}
+    end
+  end
+
   @doc """
   Optimized version of `not empty?(term(), type)`.
   """
@@ -601,15 +637,6 @@ defmodule Module.Types.Descr do
   def number_type?(%{bitmap: bitmap}) when (bitmap &&& @bit_number) != 0, do: true
   def number_type?(_), do: false
 
-  @doc """
-  Optimized version of `not empty?(intersection(atom(), type))`.
-  """
-  def atom_type?(:term), do: true
-  def atom_type?(%{dynamic: :term}), do: true
-  def atom_type?(%{dynamic: %{atom: _}}), do: true
-  def atom_type?(%{atom: _}), do: true
-  def atom_type?(_), do: false
-
   ## Bitmaps
 
   defp bitmap_to_quoted(val) do
@@ -713,20 +740,6 @@ defmodule Module.Types.Descr do
     end
   end
 
-  @doc """
-  Optimized version of `not empty?(intersection(atom([atom]), type))`.
-  """
-  def atom_type?(:term, _atom), do: true
-
-  def atom_type?(%{} = descr, atom) do
-    case Map.get(descr, :dynamic, descr) do
-      :term -> true
-      %{atom: {:union, set}} -> :sets.is_element(atom, set)
-      %{atom: {:negation, set}} -> not :sets.is_element(atom, set)
-      %{} -> false
-    end
-  end
-
   @doc """
   Returns a set of all known atoms.
 
@@ -1872,6 +1885,7 @@ defmodule Module.Types.Descr do
         end
 
       :open ->
+        fields = Map.to_list(fields)
         {:%{}, [], [{:..., [], nil} | map_fields_to_quoted(tag, Enum.sort(fields), opts)]}
     end
   end
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index 3d23650d74..4fb7eaed2f 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -30,6 +30,8 @@ defmodule Module.Types.Expr do
             versioned_vars: open_map()
           )
 
+  # An annotation for terms where the reverse arrow is not yet fully defined
+  @pending term()
   @atom_true atom([true])
   @exception open_map(__struct__: atom(), __exception__: @atom_true)
 
@@ -50,125 +52,145 @@ defmodule Module.Types.Expr do
               )
 
   # :atom
-  def of_expr(atom, _stack, context) when is_atom(atom),
+  def of_expr(atom, _expected, _expr, _stack, context) when is_atom(atom),
     do: {atom([atom]), context}
 
   # 12
-  def of_expr(literal, _stack, context) when is_integer(literal),
+  def of_expr(literal, _expected, _expr, _stack, context) when is_integer(literal),
     do: {integer(), context}
 
   # 1.2
-  def of_expr(literal, _stack, context) when is_float(literal),
+  def of_expr(literal, _expected, _expr, _stack, context) when is_float(literal),
     do: {float(), context}
 
   # "..."
-  def of_expr(literal, _stack, context) when is_binary(literal),
+  def of_expr(literal, _expected, _expr, _stack, context) when is_binary(literal),
     do: {binary(), context}
 
   # #PID<...>
-  def of_expr(literal, _stack, context) when is_pid(literal),
+  def of_expr(literal, _expected, _expr, _stack, context) when is_pid(literal),
     do: {pid(), context}
 
   # []
-  def of_expr([], _stack, context),
+  def of_expr([], _expected, _expr, _stack, context),
     do: {empty_list(), context}
 
   # [expr, ...]
-  def of_expr(list, stack, context) when is_list(list) do
+  def of_expr(list, expected, expr, stack, context) when is_list(list) do
     {prefix, suffix} = unpack_list(list, [])
-    {prefix, context} = Enum.map_reduce(prefix, context, &of_expr(&1, stack, &2))
-    {suffix, context} = of_expr(suffix, stack, context)
 
     if stack.mode == :traversal do
+      {_, context} = Enum.map_reduce(prefix, context, &of_expr(&1, term(), expr, stack, &2))
+      {_, context} = of_expr(suffix, term(), expr, stack, context)
       {dynamic(), context}
     else
+      hd_type =
+        case list_hd(expected) do
+          {_, type} -> type
+          _ -> term()
+        end
+
+      {prefix, context} = Enum.map_reduce(prefix, context, &of_expr(&1, hd_type, expr, stack, &2))
+
+      {suffix, context} =
+        if suffix == [] do
+          {empty_list(), context}
+        else
+          tl_type =
+            case list_tl(expected) do
+              {_, type} -> type
+              _ -> term()
+            end
+
+          of_expr(suffix, tl_type, expr, stack, context)
+        end
+
       {non_empty_list(Enum.reduce(prefix, &union/2), suffix), context}
     end
   end
 
   # {left, right}
-  def of_expr({left, right}, stack, context) do
-    {left, context} = of_expr(left, stack, context)
-    {right, context} = of_expr(right, stack, context)
-
-    if stack.mode == :traversal do
-      {dynamic(), context}
-    else
-      {tuple([left, right]), context}
-    end
+  def of_expr({left, right}, expected, expr, stack, context) do
+    of_tuple([left, right], expected, expr, stack, context)
   end
 
   # {...}
-  def of_expr({:{}, _meta, exprs}, stack, context) do
-    {types, context} = Enum.map_reduce(exprs, context, &of_expr(&1, stack, &2))
-
-    if stack.mode == :traversal do
-      {dynamic(), context}
-    else
-      {tuple(types), context}
-    end
+  def of_expr({:{}, _meta, exprs}, expected, expr, stack, context) do
+    of_tuple(exprs, expected, expr, stack, context)
   end
 
   # <<...>>>
-  def of_expr({:<<>>, _meta, args}, stack, context) do
+  def of_expr({:<<>>, _meta, args}, _expected, _expr, stack, context) do
     context = Of.binary(args, :expr, stack, context)
     {binary(), context}
   end
 
-  def of_expr({:__CALLER__, _meta, var_context}, _stack, context) when is_atom(var_context) do
+  def of_expr({:__CALLER__, _meta, var_context}, _expected, _expr, _stack, context)
+      when is_atom(var_context) do
     {@caller, context}
   end
 
-  def of_expr({:__STACKTRACE__, _meta, var_context}, _stack, context)
+  def of_expr({:__STACKTRACE__, _meta, var_context}, _expected, _expr, _stack, context)
       when is_atom(var_context) do
     {@stacktrace, context}
   end
 
   # left = right
-  def of_expr({:=, _, [left_expr, right_expr]} = expr, stack, context) do
+  def of_expr({:=, _, [left_expr, right_expr]} = match, expected, expr, stack, context) do
     {left_expr, right_expr} = repack_match(left_expr, right_expr)
-    {right_type, context} = of_expr(right_expr, stack, context)
 
-    # We do not raise on underscore in case someone writes _ = raise "omg"
     case left_expr do
-      {:_, _, ctx} when is_atom(ctx) -> {right_type, context}
-      _ -> Pattern.of_match(left_expr, right_type, expr, {:match, right_type}, stack, context)
+      # We do not raise on underscore in case someone writes _ = raise "omg"
+      {:_, _, ctx} when is_atom(ctx) ->
+        of_expr(right_expr, expected, expr, stack, context)
+
+      _ ->
+        type_fun = fn pattern_type, context ->
+          # See if we can use the expected type to further refine the pattern type,
+          # if we cannot, use the pattern type as that will fail later on.
+          {_ok_or_error, type} = compatible_intersection(pattern_type, expected)
+          of_expr(right_expr, type, expr, stack, context)
+        end
+
+        Pattern.of_match(left_expr, type_fun, match, stack, context)
     end
   end
 
   # %{map | ...}
   # TODO: Once we support typed structs, we need to type check them here.
-  def of_expr({:%{}, meta, [{:|, _, [map, args]}]} = expr, stack, context) do
-    {map_type, context} = of_expr(map, stack, context)
-
-    Of.permutate_map(args, stack, context, &of_expr/3, fn fallback, keys, pairs ->
-      # If there is no fallback (i.e. it is closed), we can update the existing map,
-      # otherwise we only assert the existing keys.
-      keys = if fallback == none(), do: keys, else: Enum.map(pairs, &elem(&1, 0)) ++ keys
-
-      # Assert the keys exist
-      Enum.each(keys, fn key ->
-        case map_fetch(map_type, key) do
-          {_, _} -> :ok
-          :badkey -> throw({:badkey, map_type, key, expr, context})
-          :badmap -> throw({:badmap, map_type, expr, context})
-        end
-      end)
-
-      if fallback == none() do
-        Enum.reduce(pairs, map_type, fn {key, type}, acc ->
-          case map_fetch_and_put(acc, key, type) do
-            {_value, descr} -> descr
+  # PENDING: here
+  def of_expr({:%{}, meta, [{:|, _, [map, args]}]} = expr, _expected, _expr, stack, context) do
+    {map_type, context} = of_expr(map, @pending, expr, stack, context)
+
+    Of.permutate_map(args, stack, context, &of_expr(&1, @pending, expr, &2, &3), fn
+      fallback, keys, pairs ->
+        # If there is no fallback (i.e. it is closed), we can update the existing map,
+        # otherwise we only assert the existing keys.
+        keys = if fallback == none(), do: keys, else: Enum.map(pairs, &elem(&1, 0)) ++ keys
+
+        # Assert the keys exist
+        Enum.each(keys, fn key ->
+          case map_fetch(map_type, key) do
+            {_, _} -> :ok
             :badkey -> throw({:badkey, map_type, key, expr, context})
             :badmap -> throw({:badmap, map_type, expr, context})
           end
         end)
-      else
-        # TODO: Use the fallback type to actually indicate if open or closed.
-        # The fallback must be unioned with the result of map_values with all
-        # `keys` deleted.
-        open_map(pairs)
-      end
+
+        if fallback == none() do
+          Enum.reduce(pairs, map_type, fn {key, type}, acc ->
+            case map_fetch_and_put(acc, key, type) do
+              {_value, descr} -> descr
+              :badkey -> throw({:badkey, map_type, key, expr, context})
+              :badmap -> throw({:badmap, map_type, expr, context})
+            end
+          end)
+        else
+          # TODO: Use the fallback type to actually indicate if open or closed.
+          # The fallback must be unioned with the result of map_values with all
+          # `keys` deleted.
+          open_map(pairs)
+        end
     end)
   catch
     error -> {error_type(), error(__MODULE__, error, meta, stack, context)}
@@ -178,14 +200,17 @@ defmodule Module.Types.Expr do
   # Note this code, by definition, adds missing struct fields to `map`
   # because at runtime we do not check for them (only for __struct__ itself).
   # TODO: Once we support typed structs, we need to type check them here.
+  # PENDING: here
   def of_expr(
         {:%, struct_meta, [module, {:%{}, _, [{:|, update_meta, [map, args]}]}]} = expr,
+        _expected,
+        _expr,
         stack,
         context
       ) do
     {info, context} = Of.struct_info(module, struct_meta, stack, context)
     struct_type = Of.struct_type(module, info)
-    {map_type, context} = of_expr(map, stack, context)
+    {map_type, context} = of_expr(map, @pending, expr, stack, context)
 
     if disjoint?(struct_type, map_type) do
       warning = {:badstruct, expr, struct_type, map_type, context}
@@ -195,45 +220,47 @@ defmodule Module.Types.Expr do
 
       Enum.reduce(args, {map_type, context}, fn
         {key, value}, {map_type, context} when is_atom(key) ->
-          {value_type, context} = of_expr(value, stack, context)
+          {value_type, context} = of_expr(value, @pending, expr, stack, context)
           {map_put!(map_type, key, value_type), context}
       end)
     end
   end
 
   # %{...}
-  def of_expr({:%{}, _meta, args}, stack, context) do
-    Of.closed_map(args, stack, context, &of_expr/3)
+  # PENDING: here
+  def of_expr({:%{}, _meta, args}, _expected, expr, stack, context) do
+    Of.closed_map(args, stack, context, &of_expr(&1, @pending, expr, &2, &3))
   end
 
   # %Struct{}
-  def of_expr({:%, meta, [module, {:%{}, _, args}]}, stack, context) do
-    Of.struct_instance(module, args, meta, stack, context, &of_expr/3)
+  # PENDING: here
+  def of_expr({:%, meta, [module, {:%{}, _, args}]}, _expected, expr, stack, context) do
+    Of.struct_instance(module, args, meta, stack, context, &of_expr(&1, @pending, expr, &2, &3))
   end
 
   # ()
-  def of_expr({:__block__, _meta, []}, _stack, context) do
+  def of_expr({:__block__, _meta, []}, _expected, _expr, _stack, context) do
     {atom([nil]), context}
   end
 
   # (expr; expr)
-  def of_expr({:__block__, _meta, exprs}, stack, context) do
+  def of_expr({:__block__, _meta, exprs}, expected, _expr, stack, context) do
     {pre, [post]} = Enum.split(exprs, -1)
 
     context =
       Enum.reduce(pre, context, fn expr, context ->
-        {_, context} = of_expr(expr, stack, context)
+        {_, context} = of_expr(expr, term(), expr, stack, context)
         context
       end)
 
-    of_expr(post, stack, context)
+    of_expr(post, expected, post, stack, context)
   end
 
-  def of_expr({:cond, _meta, [[{:do, clauses}]]}, stack, context) do
+  def of_expr({:cond, _meta, [[{:do, clauses}]]}, expected, expr, stack, original) do
     clauses
-    |> reduce_non_empty({none(), context}, fn
+    |> reduce_non_empty({none(), original}, fn
       {:->, meta, [[head], body]}, {acc, context}, last? ->
-        {head_type, context} = of_expr(head, stack, context)
+        {head_type, context} = of_expr(head, @pending, head, stack, context)
 
         context =
           if stack.mode in [:infer, :traversal] do
@@ -253,14 +280,15 @@ defmodule Module.Types.Expr do
             end
           end
 
-        {body_type, context} = of_expr(body, stack, context)
-        {union(body_type, acc), context}
+        {body_type, context} = of_expr(body, expected, expr, stack, context)
+        {union(body_type, acc), reset_vars(context, original)}
     end)
     |> dynamic_unless_static(stack)
   end
 
-  def of_expr({:case, meta, [case_expr, [{:do, clauses}]]}, stack, context) do
-    {case_type, context} = of_expr(case_expr, stack, context)
+  def of_expr({:case, meta, [case_expr, [{:do, clauses}]]}, expected, expr, stack, context) do
+    {case_type, context} = of_expr(case_expr, @pending, case_expr, stack, context)
+    info = {:case, meta, case_type, case_expr}
 
     # If we are only type checking the expression and the expression is a literal,
     # let's mark it as generated, as it is most likely a macro code. However, if
@@ -270,65 +298,88 @@ defmodule Module.Types.Expr do
     else
       clauses
     end
-    |> of_clauses([case_type], {:case, meta, case_type, case_expr}, stack, {none(), context})
+    |> of_clauses([case_type], expected, expr, info, stack, {none(), context})
     |> dynamic_unless_static(stack)
   end
 
   # TODO: fn pat -> expr end
-  def of_expr({:fn, _meta, clauses}, stack, context) do
+  def of_expr({:fn, _meta, clauses}, _expected, _expr, stack, context) do
     [{:->, _, [head, _]} | _] = clauses
     {patterns, _guards} = extract_head(head)
-    expected = Enum.map(patterns, fn _ -> dynamic() end)
-    {_acc, context} = of_clauses(clauses, expected, :fn, stack, {none(), context})
+    domain = Enum.map(patterns, fn _ -> dynamic() end)
+    {_acc, context} = of_clauses(clauses, domain, @pending, nil, :fn, stack, {none(), context})
     {fun(), context}
   end
 
-  def of_expr({:try, _meta, [[do: body] ++ blocks]}, stack, context) do
-    {body_type, context} = of_expr(body, stack, context)
-    initial = if Keyword.has_key?(blocks, :else), do: none(), else: body_type
+  def of_expr({:try, _meta, [[do: body] ++ blocks]}, expected, expr, stack, original) do
+    {after_block, blocks} = Keyword.pop(blocks, :after)
+    {else_block, blocks} = Keyword.pop(blocks, :else)
 
-    blocks
-    |> Enum.reduce({initial, context}, fn
-      {:rescue, clauses}, acc_context ->
-        Enum.reduce(clauses, acc_context, fn
-          {:->, _, [[{:in, meta, [var, exceptions]} = expr], body]}, {acc, context} ->
-            {type, context} = of_rescue(var, exceptions, body, expr, [], meta, stack, context)
-            {union(type, acc), context}
-
-          {:->, meta, [[var], body]}, {acc, context} ->
-            hint = [:anonymous_rescue]
-            {type, context} = of_rescue(var, [], body, var, hint, meta, stack, context)
-            {union(type, acc), context}
-        end)
+    {type, context} =
+      if else_block do
+        {type, context} = of_expr(body, @pending, body, stack, original)
+        info = {:try_else, type}
+        of_clauses(else_block, [type], expected, expr, info, stack, {none(), context})
+      else
+        of_expr(body, expected, expr, stack, original)
+      end
 
-      {:after, body}, {acc, context} ->
-        {_type, context} = of_expr(body, stack, context)
-        {acc, context}
+    {type, context} =
+      blocks
+      |> Enum.reduce({type, reset_vars(context, original)}, fn
+        {:rescue, clauses}, acc_context ->
+          Enum.reduce(clauses, acc_context, fn
+            {:->, _, [[{:in, meta, [var, exceptions]} = expr], body]}, {acc, context} ->
+              {type, context} =
+                of_rescue(var, exceptions, body, expr, :rescue, meta, stack, context)
 
-      {:catch, clauses}, acc_context ->
-        of_clauses(clauses, [@try_catch, dynamic()], :try_catch, stack, acc_context)
+              {union(type, acc), context}
 
-      {:else, clauses}, acc_context ->
-        of_clauses(clauses, [body_type], {:try_else, body_type}, stack, acc_context)
-    end)
-    |> dynamic_unless_static(stack)
+            {:->, meta, [[var], body]}, {acc, context} ->
+              {type, context} =
+                of_rescue(var, [], body, var, :anonymous_rescue, meta, stack, context)
+
+              {union(type, acc), context}
+          end)
+
+        {:catch, clauses}, {acc, context} ->
+          of_clauses(
+            clauses,
+            [@try_catch, dynamic()],
+            expected,
+            expr,
+            :try_catch,
+            stack,
+            {acc, context}
+          )
+      end)
+      |> dynamic_unless_static(stack)
+
+    if after_block do
+      {_type, context} = of_expr(after_block, term(), after_block, stack, context)
+      {type, context}
+    else
+      {type, context}
+    end
   end
 
-  def of_expr({:receive, _meta, [blocks]}, stack, context) do
+  @timeout_type union(integer(), atom([:infinity]))
+
+  def of_expr({:receive, _meta, [blocks]}, expected, expr, stack, original) do
     blocks
-    |> Enum.reduce({none(), context}, fn
+    |> Enum.reduce({none(), original}, fn
       {:do, {:__block__, _, []}}, acc_context ->
         acc_context
 
       {:do, clauses}, acc_context ->
-        of_clauses(clauses, [dynamic()], :receive, stack, acc_context)
+        of_clauses(clauses, [dynamic()], expected, expr, :receive, stack, acc_context)
 
-      {:after, [{:->, meta, [[timeout], body]}]}, {acc, context} ->
-        {timeout_type, context} = of_expr(timeout, stack, context)
-        {body_type, context} = of_expr(body, stack, context)
+      {:after, [{:->, meta, [[timeout], body]}] = after_expr}, {acc, context} ->
+        {timeout_type, context} = of_expr(timeout, @timeout_type, after_expr, stack, context)
+        {body_type, context} = of_expr(body, expected, expr, stack, context)
 
-        if integer_type?(timeout_type) do
-          {union(body_type, acc), context}
+        if compatible?(timeout_type, @timeout_type) do
+          {union(body_type, acc), reset_vars(context, original)}
         else
           error = {:badtimeout, timeout_type, timeout, context}
           {union(body_type, acc), error(__MODULE__, error, meta, stack, context)}
@@ -337,8 +388,7 @@ defmodule Module.Types.Expr do
     |> dynamic_unless_static(stack)
   end
 
-  # TODO: for pat <- expr do expr end
-  def of_expr({:for, meta, [_ | _] = args}, stack, context) do
+  def of_expr({:for, meta, [_ | _] = args}, expected, expr, stack, context) do
     {clauses, [[{:do, block} | opts]]} = Enum.split(args, -1)
     context = Enum.reduce(clauses, context, &for_clause(&1, stack, &2))
 
@@ -346,14 +396,15 @@ defmodule Module.Types.Expr do
     # We handle reduce and into accordingly instead.
     if Keyword.has_key?(opts, :reduce) do
       reduce = Keyword.fetch!(opts, :reduce)
-      {reduce_type, context} = of_expr(reduce, stack, context)
+      {reduce_type, context} = of_expr(reduce, expected, expr, stack, context)
       # TODO: We need to type check against dynamic() instead of using reduce_type
       # because this is recursive. We need to infer the block type first.
-      of_clauses(block, [dynamic()], :for_reduce, stack, {reduce_type, context})
+      of_clauses(block, [dynamic()], expected, expr, :for_reduce, stack, {reduce_type, context})
     else
+      # TODO: Use the collectable protocol for the output
       into = Keyword.get(opts, :into, [])
       {into_wrapper, gradual?, context} = for_into(into, meta, stack, context)
-      {block_type, context} = of_expr(block, stack, context)
+      {block_type, context} = of_expr(block, @pending, block, stack, context)
 
       for_type =
         for type <- into_wrapper do
@@ -370,17 +421,19 @@ defmodule Module.Types.Expr do
   end
 
   # TODO: with pat <- expr do expr end
-  def of_expr({:with, _meta, [_ | _] = clauses}, stack, context) do
+  def of_expr({:with, _meta, [_ | _] = clauses}, _expected, _expr, stack, original) do
     {clauses, [options]} = Enum.split(clauses, -1)
-    context = Enum.reduce(clauses, context, &with_clause(&1, stack, &2))
-    context = Enum.reduce(options, context, &with_option(&1, stack, &2))
+    context = Enum.reduce(clauses, original, &with_clause(&1, stack, &2))
+    context = Enum.reduce(options, context, &with_option(&1, stack, &2, original))
     {dynamic(), context}
   end
 
   # TODO: fun.(args)
-  def of_expr({{:., meta, [fun]}, _meta, args} = call, stack, context) do
-    {fun_type, context} = of_expr(fun, stack, context)
-    {_args_types, context} = Enum.map_reduce(args, context, &of_expr(&1, stack, &2))
+  def of_expr({{:., meta, [fun]}, _meta, args} = call, _expected, _expr, stack, context) do
+    {fun_type, context} = of_expr(fun, fun(), call, stack, context)
+
+    {_args_types, context} =
+      Enum.map_reduce(args, context, &of_expr(&1, @pending, &1, stack, &2))
 
     case fun_fetch(fun_type, length(args)) do
       :ok ->
@@ -392,22 +445,28 @@ defmodule Module.Types.Expr do
     end
   end
 
-  def of_expr({{:., _, [callee, key_or_fun]}, meta, []} = expr, stack, context)
+  def of_expr({{:., _, [callee, key_or_fun]}, meta, []} = call, expected, expr, stack, context)
       when not is_atom(callee) and is_atom(key_or_fun) do
-    {type, context} = of_expr(callee, stack, context)
-
     if Keyword.get(meta, :no_parens, false) do
-      Of.map_fetch(expr, type, key_or_fun, stack, context)
+      {type, context} = of_expr(callee, open_map([{key_or_fun, expected}]), expr, stack, context)
+      Of.map_fetch(call, type, key_or_fun, stack, context)
     else
-      {mods, context} = Of.modules(type, key_or_fun, 0, [:dot], expr, meta, stack, context)
-      apply_many(mods, key_or_fun, [], [], expr, stack, context)
+      {type, context} = of_expr(callee, atom(), call, stack, context)
+      {mods, context} = Of.modules(type, key_or_fun, 0, [:dot], call, meta, stack, context)
+      apply_many(mods, key_or_fun, [], expected, call, stack, context)
     end
   end
 
-  def of_expr({{:., _, [remote, :apply]}, _meta, [mod, fun, args]} = expr, stack, context)
+  def of_expr(
+        {{:., _, [remote, :apply]}, _meta, [mod, fun, args]} = call,
+        expected,
+        _expr,
+        stack,
+        context
+      )
       when remote in [Kernel, :erlang] and is_list(args) do
-    {mod_type, context} = of_expr(mod, stack, context)
-    {fun_type, context} = of_expr(fun, stack, context)
+    {mod_type, context} = of_expr(mod, atom(), call, stack, context)
+    {fun_type, context} = of_expr(fun, atom(), call, stack, context)
     improper_list? = Enum.any?(args, &match?({:|, _, [_, _]}, &1))
 
     case atom_fetch(fun_type) do
@@ -418,76 +477,100 @@ defmodule Module.Types.Expr do
             _ -> []
           end
 
-        {args_types, context} = Enum.map_reduce(args, context, &of_expr(&1, stack, &2))
-
         {types, context} =
           Enum.map_reduce(funs, context, fn fun, context ->
-            apply_many(mods, fun, args, args_types, expr, stack, context)
+            apply_many(mods, fun, args, expected, call, stack, context)
           end)
 
         {Enum.reduce(types, &union/2), context}
 
       _ ->
-        {args_type, context} = of_expr(args, stack, context)
-        args_types = [mod_type, fun_type, args_type]
-        Apply.remote(:erlang, :apply, [mod, fun, args], args_types, expr, stack, context)
+        info = Apply.signature(:erlang, :apply, 3)
+        {args_type, context} = of_expr(args, list(term()), call, stack, context)
+        apply_types = [mod_type, fun_type, args_type]
+        Apply.remote_apply(info, :erlang, :apply, apply_types, call, stack, context)
     end
   end
 
-  def of_expr({{:., _, [remote, name]}, meta, args} = expr, stack, context) do
-    {remote_type, context} = of_expr(remote, stack, context)
-    {args_types, context} = Enum.map_reduce(args, context, &of_expr(&1, stack, &2))
-    {mods, context} = Of.modules(remote_type, name, length(args), expr, meta, stack, context)
-    apply_many(mods, name, args, args_types, expr, stack, context)
+  def of_expr({{:., _, [remote, name]}, meta, args} = call, expected, _expr, stack, context) do
+    {remote_type, context} = of_expr(remote, atom(), call, stack, context)
+    {mods, context} = Of.modules(remote_type, name, length(args), call, meta, stack, context)
+    apply_many(mods, name, args, expected, call, stack, context)
   end
 
   # TODO: &Foo.bar/1
   def of_expr(
-        {:&, _, [{:/, _, [{{:., _, [remote, name]}, meta, []}, arity]}]} = expr,
+        {:&, _, [{:/, _, [{{:., _, [remote, name]}, meta, []}, arity]}]} = call,
+        _expected,
+        _expr,
         stack,
         context
       )
       when is_atom(name) and is_integer(arity) do
-    {remote_type, context} = of_expr(remote, stack, context)
-    {mods, context} = Of.modules(remote_type, name, arity, expr, meta, stack, context)
+    {remote_type, context} = of_expr(remote, atom(), call, stack, context)
+    {mods, context} = Of.modules(remote_type, name, arity, call, meta, stack, context)
     Apply.remote_capture(mods, name, arity, meta, stack, context)
   end
 
   # TODO: &foo/1
-  def of_expr({:&, _meta, [{:/, _, [{fun, meta, _}, arity]}]}, stack, context) do
+  def of_expr({:&, _meta, [{:/, _, [{fun, meta, _}, arity]}]}, _expected, _expr, stack, context) do
     Apply.local_capture(fun, arity, meta, stack, context)
   end
 
   # Super
-  def of_expr({:super, meta, args} = expr, stack, context) when is_list(args) do
+  def of_expr({:super, meta, args} = call, expected, _expr, stack, context) when is_list(args) do
     {_kind, fun} = Keyword.fetch!(meta, :super)
-    {args_types, context} = Enum.map_reduce(args, context, &of_expr(&1, stack, &2))
-    Apply.local(fun, args_types, expr, stack, context)
+    apply_local(fun, args, expected, call, stack, context)
   end
 
   # Local calls
-  def of_expr({fun, _meta, args} = expr, stack, context)
+  def of_expr({fun, _meta, args} = call, expected, _expr, stack, context)
       when is_atom(fun) and is_list(args) do
-    {args_types, context} = Enum.map_reduce(args, context, &of_expr(&1, stack, &2))
-    Apply.local(fun, args_types, expr, stack, context)
+    apply_local(fun, args, expected, call, stack, context)
   end
 
   # var
-  def of_expr(var, stack, context) when is_var(var) do
+  def of_expr(var, expected, expr, stack, context) when is_var(var) do
     if stack.mode == :traversal do
       {dynamic(), context}
     else
-      {Of.var(var, context), context}
+      Of.refine_body_var(var, expected, expr, stack, context)
     end
   end
 
+  ## Tuples
+
+  defp of_tuple(elems, _expected, expr, %{mode: :traversal} = stack, context) do
+    {_types, context} = Enum.map_reduce(elems, context, &of_expr(&1, term(), expr, stack, &2))
+    {dynamic(), context}
+  end
+
+  defp of_tuple(elems, expected, expr, stack, context) do
+    of_tuple(elems, 0, [], expected, expr, stack, context)
+  end
+
+  defp of_tuple([elem | elems], index, acc, expected, expr, stack, context) do
+    expr_expected =
+      case tuple_fetch(expected, index) do
+        {_, type} -> type
+        _ -> term()
+      end
+
+    {type, context} = of_expr(elem, expr_expected, expr, stack, context)
+    of_tuple(elems, index + 1, [type | acc], expected, expr, stack, context)
+  end
+
+  defp of_tuple([], _index, acc, _expected, _expr, _stack, context) do
+    {tuple(Enum.reverse(acc)), context}
+  end
+
   ## Try
 
-  defp of_rescue(var, exceptions, body, expr, hints, meta, stack, context) do
+  defp of_rescue(var, exceptions, body, expr, info, meta, stack, original) do
     args = [__exception__: @atom_true]
 
     {structs, context} =
-      Enum.map_reduce(exceptions, context, fn exception, context ->
+      Enum.map_reduce(exceptions, original, fn exception, context ->
         # Exceptions are not validated in the compiler,
         # to avoid export dependencies. So we do it here.
         if Code.ensure_loaded?(exception) and function_exported?(exception, :__struct__, 0) do
@@ -508,12 +591,13 @@ defmodule Module.Types.Expr do
 
         _ ->
           expected = if structs == [], do: @exception, else: Enum.reduce(structs, &union/2)
-          formatter = fn expr -> {"rescue #{expr_to_string(expr)} ->", hints} end
-          {_ok?, _type, context} = Of.refine_var(var, expected, expr, formatter, stack, context)
+          expr = {:__block__, [type_check: info], [expr]}
+          {_ok?, _type, context} = Of.refine_head_var(var, expected, expr, stack, context)
           context
       end
 
-    of_expr(body, stack, context)
+    {type, context} = of_expr(body, @pending, body, stack, context)
+    {type, reset_vars(context, original)}
   end
 
   ## Comprehensions
@@ -521,24 +605,18 @@ defmodule Module.Types.Expr do
   defp for_clause({:<-, meta, [left, right]}, stack, context) do
     expr = {:<-, [type_check: :generator] ++ meta, [left, right]}
     {pattern, guards} = extract_head([left])
-    {type, context} = of_expr(right, stack, context)
-
-    {_type, context} =
-      Pattern.of_match(pattern, guards, dynamic(), expr, :for, stack, context)
 
     {_type, context} =
-      Apply.remote(Enumerable, :count, [right], [type], expr, stack, context)
+      apply_one(Enumerable, :count, [right], dynamic(), expr, stack, context)
 
-    context
+    Pattern.of_generator(pattern, guards, dynamic(), :for, expr, stack, context)
   end
 
   defp for_clause({:<<>>, _, [{:<-, meta, [left, right]}]} = expr, stack, context) do
-    {right_type, context} = of_expr(right, stack, context)
-
-    {_pattern_type, context} =
-      Pattern.of_match(left, binary(), expr, :for, stack, context)
+    {right_type, context} = of_expr(right, binary(), expr, stack, context)
+    context = Pattern.of_generator(left, [], binary(), :for, expr, stack, context)
 
-    if binary_type?(right_type) do
+    if compatible?(right_type, binary()) do
       context
     else
       error = {:badbinary, right_type, right, context}
@@ -547,7 +625,7 @@ defmodule Module.Types.Expr do
   end
 
   defp for_clause(expr, stack, context) do
-    {_type, context} = of_expr(expr, stack, context)
+    {_type, context} = of_expr(expr, term(), expr, stack, context)
     context
   end
 
@@ -559,10 +637,22 @@ defmodule Module.Types.Expr do
   defp for_into(binary, _meta, _stack, context) when is_binary(binary),
     do: {[:binary], false, context}
 
-  # TODO: Use the collectable protocol for the output
   defp for_into(into, meta, stack, context) do
-    {type, context} = of_expr(into, stack, context)
+    meta =
+      case into do
+        {_, meta, _} -> meta
+        _ -> meta
+      end
+
+    expr = {:__block__, [type_check: :into] ++ meta, [into]}
+
+    {info, [domain], context} =
+      Apply.remote_domain(Collectable, :into, [into], term(), meta, stack, context)
+
+    {type, context} = of_expr(into, domain, expr, stack, context)
 
+    # We use subtype? instead of compatible because we want to handle
+    # only binary/list, even if a dynamic with something else is given.
     if subtype?(type, @into_compile) do
       case {binary_type?(type), empty_list_type?(type)} do
         {false, true} -> {[:list], gradual?(type), context}
@@ -570,14 +660,9 @@ defmodule Module.Types.Expr do
         {_, _} -> {[:binary, :list], gradual?(type), context}
       end
     else
-      meta =
-        case into do
-          {_, meta, _} -> meta
-          _ -> meta
-        end
+      {_type, context} =
+        Apply.remote_apply(info, Collectable, :into, [type], expr, stack, context)
 
-      expr = {:__block__, [type_check: :into] ++ meta, [into]}
-      {_type, context} = Apply.remote(Collectable, :into, [into], [type], expr, stack, context)
       {[:term], true, context}
     end
   end
@@ -586,40 +671,66 @@ defmodule Module.Types.Expr do
 
   defp with_clause({:<-, _meta, [left, right]} = expr, stack, context) do
     {pattern, guards} = extract_head([left])
-    {_type, context} = Pattern.of_match(pattern, guards, dynamic(), expr, :with, stack, context)
-    {_, context} = of_expr(right, stack, context)
-    context
+    {_type, context} = of_expr(right, @pending, right, stack, context)
+    Pattern.of_generator(pattern, guards, dynamic(), :with, expr, stack, context)
   end
 
   defp with_clause(expr, stack, context) do
-    {_type, context} = of_expr(expr, stack, context)
+    {_type, context} = of_expr(expr, @pending, expr, stack, context)
     context
   end
 
-  defp with_option({:do, body}, stack, context) do
-    {_type, context} = of_expr(body, stack, context)
-    context
+  defp with_option({:do, body}, stack, context, original) do
+    {_type, context} = of_expr(body, @pending, body, stack, context)
+    reset_vars(context, original)
   end
 
-  defp with_option({:else, clauses}, stack, context) do
-    {_, context} = of_clauses(clauses, [dynamic()], :with_else, stack, {none(), context})
+  defp with_option({:else, clauses}, stack, context, _original) do
+    {_, context} =
+      of_clauses(clauses, [dynamic()], @pending, nil, :with_else, stack, {none(), context})
+
     context
   end
 
   ## General helpers
 
-  defp apply_many([], function, _args, args_types, expr, stack, context) do
-    Apply.remote(function, args_types, expr, stack, context)
+  defp apply_local(fun, args, _expected, {_, meta, _} = expr, stack, context) do
+    {local_info, domain, context} = Apply.local_domain(fun, args, meta, stack, context)
+
+    {args_types, context} =
+      zip_map_reduce(args, domain, context, &of_expr(&1, &2, expr, stack, &3))
+
+    Apply.local_apply(local_info, fun, args_types, expr, stack, context)
   end
 
-  defp apply_many([mod], function, args, args_types, expr, stack, context) do
-    Apply.remote(mod, function, args, args_types, expr, stack, context)
+  defp apply_one(mod, fun, args, expected, expr, stack, context) do
+    {info, domain, context} =
+      Apply.remote_domain(mod, fun, args, expected, elem(expr, 1), stack, context)
+
+    {args_types, context} =
+      zip_map_reduce(args, domain, context, &of_expr(&1, &2, expr, stack, &3))
+
+    Apply.remote_apply(info, mod, fun, args_types, expr, stack, context)
   end
 
-  defp apply_many(mods, function, args, args_types, expr, stack, context) do
+  defp apply_many([], fun, args, expected, expr, stack, context) do
+    {info, domain} = Apply.remote_domain(fun, args, expected, stack)
+
+    {args_types, context} =
+      zip_map_reduce(args, domain, context, &of_expr(&1, &2, expr, stack, &3))
+
+    Apply.remote_apply(info, nil, fun, args_types, expr, stack, context)
+  end
+
+  defp apply_many([mod], fun, args, expected, expr, stack, context) do
+    apply_one(mod, fun, args, expected, expr, stack, context)
+  end
+
+  defp apply_many(mods, fun, args, expected, {remote, meta, args}, stack, context) do
     {returns, context} =
       Enum.map_reduce(mods, context, fn mod, context ->
-        Apply.remote(mod, function, args, args_types, expr, stack, context)
+        expr = {remote, [type_check: {:invoked_as, mod, fun, length(args)}] ++ meta, args}
+        apply_one(mod, fun, args, expected, expr, stack, context)
       end)
 
     {Enum.reduce(returns, &union/2), context}
@@ -634,15 +745,16 @@ defmodule Module.Types.Expr do
   defp dynamic_unless_static({_, _} = output, %{mode: :static}), do: output
   defp dynamic_unless_static({type, context}, %{mode: _}), do: {dynamic(type), context}
 
-  defp of_clauses(clauses, expected, info, %{mode: mode} = stack, {acc, context}) do
-    %{failed: failed?} = context
+  defp of_clauses(clauses, domain, expected, expr, info, %{mode: mode} = stack, {acc, original}) do
+    %{failed: failed?} = original
 
-    Enum.reduce(clauses, {acc, context}, fn {:->, meta, [head, body]}, {acc, context} ->
+    Enum.reduce(clauses, {acc, original}, fn {:->, meta, [head, body]}, {acc, context} ->
       {failed?, context} = reset_failed(context, failed?)
       {patterns, guards} = extract_head(head)
-      {_types, context} = Pattern.of_head(patterns, guards, expected, info, meta, stack, context)
-      {body, context} = of_expr(body, stack, context)
-      context = set_failed(context, failed?)
+      {_trees, context} = Pattern.of_head(patterns, guards, domain, info, meta, stack, context)
+
+      {body, context} = of_expr(body, expected, expr || body, stack, context)
+      context = context |> set_failed(failed?) |> reset_vars(original)
 
       if mode == :traversal do
         {dynamic(), context}
@@ -658,6 +770,8 @@ defmodule Module.Types.Expr do
   defp set_failed(%{failed: false} = context, true), do: %{context | failed: true}
   defp set_failed(context, _bool), do: context
 
+  defp reset_vars(context, %{vars: vars}), do: %{context | vars: vars}
+
   defp extract_head([{:when, _meta, args}]) do
     case Enum.split(args, -1) do
       {patterns, [guards]} -> {patterns, flatten_when(guards)}
diff --git a/lib/elixir/lib/module/types/helpers.ex b/lib/elixir/lib/module/types/helpers.ex
index 7ae354bef5..61230400d3 100644
--- a/lib/elixir/lib/module/types/helpers.ex
+++ b/lib/elixir/lib/module/types/helpers.ex
@@ -137,7 +137,7 @@ defmodule Module.Types.Helpers do
                  type: :variable,
                  name: name,
                  context: context,
-                 traces: collect_var_traces(off_traces)
+                 traces: collect_var_traces(expr, off_traces)
                })}
 
             _ ->
@@ -153,33 +153,27 @@ defmodule Module.Types.Helpers do
     |> Enum.sort_by(& &1.name)
   end
 
-  defp collect_var_traces(traces) do
+  defp collect_var_traces(parent_expr, traces) do
     traces
-    |> Enum.reject(fn {_expr, _file, type, _formatter} ->
+    |> Enum.reject(fn {expr, _file, type} ->
       # As an otimization do not care about dynamic terms
-      type == %{dynamic: :term}
+      type == %{dynamic: :term} or expr == parent_expr
     end)
     |> case do
       [] -> traces
       filtered -> filtered
     end
     |> Enum.reverse()
-    |> Enum.map(fn {expr, file, type, formatter} ->
+    |> Enum.map(fn {expr, file, type} ->
       meta = get_meta(expr)
 
-      {formatted_expr, formatter_hints} =
-        case formatter do
-          :default -> {expr_to_string(expr), []}
-          formatter -> formatter.(expr)
-        end
-
       # This information is exposed to language servers and
       # therefore must remain backwards compatible.
       %{
         file: file,
         meta: meta,
-        formatted_expr: formatted_expr,
-        formatted_hints: format_hints(formatter_hints ++ expr_hints(expr)),
+        formatted_expr: expr_to_string(expr),
+        formatted_hints: format_hints(expr_hints(expr)),
         formatted_type: Module.Types.Descr.to_quoted_string(type, collapse_structs: true)
       }
     end)
@@ -187,6 +181,22 @@ defmodule Module.Types.Helpers do
     |> Enum.dedup()
   end
 
+  defp expr_hints(expr) do
+    case expr do
+      {:<<>>, [inferred_bitstring_spec: true] ++ _meta, _} ->
+        [:inferred_bitstring_spec]
+
+      {_, meta, _} ->
+        case meta[:type_check] do
+          :anonymous_rescue -> [:anonymous_rescue]
+          _ -> []
+        end
+
+      _ ->
+        []
+    end
+  end
+
   @doc """
   Format previously collected traces.
   """
@@ -230,11 +240,6 @@ defmodule Module.Types.Helpers do
   defp pluralize([_], singular, _plural), do: singular
   defp pluralize(_, _singular, plural), do: plural
 
-  defp expr_hints({:<<>>, [inferred_bitstring_spec: true] ++ _meta, _}),
-    do: [:inferred_bitstring_spec]
-
-  defp expr_hints(_), do: []
-
   @doc """
   Converts the given expression to a string,
   translating inlined Erlang calls back to Elixir.
@@ -242,6 +247,30 @@ defmodule Module.Types.Helpers do
   We also undo some macro expressions done by the Kernel module.
   """
   def expr_to_string(expr) do
+    string = prewalk_expr_to_string(expr)
+
+    case expr do
+      {_, meta, _} ->
+        case meta[:type_check] do
+          :anonymous_rescue ->
+            "rescue " <> string
+
+          :rescue ->
+            "rescue " <> string
+
+          {:invoked_as, mod, fun, arity} ->
+            string <> "\n#=> invoked as " <> Exception.format_mfa(mod, fun, arity)
+
+          _ ->
+            string
+        end
+
+      _ ->
+        string
+    end
+  end
+
+  defp prewalk_expr_to_string(expr) do
     expr
     |> Macro.prewalk(fn
       {:%, _, [Range, {:%{}, _, fields}]} = node ->
@@ -264,6 +293,42 @@ defmodule Module.Types.Helpers do
       {{:., _, [mod, fun]}, meta, args} ->
         erl_to_ex(mod, fun, args, meta)
 
+      {:case, meta, [expr, [do: clauses]]} = case ->
+        if meta[:type_check] == :expr do
+          case clauses do
+            [
+              {:->, _,
+               [
+                 [
+                   {:when, _,
+                    [
+                      {var, _, Kernel},
+                      {{:., _, [:erlang, :orelse]}, _,
+                       [
+                         {{:., _, [:erlang, :"=:="]}, _, [{var, _, Kernel}, false]},
+                         {{:., _, [:erlang, :"=:="]}, _, [{var, _, Kernel}, nil]}
+                       ]}
+                    ]}
+                 ],
+                 else_block
+               ]},
+              {:->, _, [[{:_, _, Kernel}], do_block]}
+            ] ->
+              {:if, meta, [expr, [do: do_block, else: else_block]]}
+
+            [
+              {:->, _, [[false], else_block]},
+              {:->, _, [[true], do_block]}
+            ] ->
+              {:if, meta, [expr, [do: do_block, else: else_block]]}
+
+            _ ->
+              case
+          end
+        else
+          case
+        end
+
       other ->
         other
     end)
@@ -333,4 +398,19 @@ defmodule Module.Types.Helpers do
   The type to return when there is an error.
   """
   def error_type, do: Module.Types.Descr.dynamic()
+
+  ## Enum helpers
+
+  def zip_map_reduce(args1, args2, acc, fun) do
+    zip_map_reduce(args1, args2, [], acc, fun)
+  end
+
+  defp zip_map_reduce([arg1 | args1], [arg2 | args2], list, acc, fun) do
+    {item, acc} = fun.(arg1, arg2, acc)
+    zip_map_reduce(args1, args2, [item | list], acc, fun)
+  end
+
+  defp zip_map_reduce([], [], list, acc, _fun) do
+    {Enum.reverse(list), acc}
+  end
 end
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index c356ecbfcd..9f241e6173 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -41,51 +41,88 @@ defmodule Module.Types.Of do
     put_in(context.vars[version], data)
   end
 
+  @doc """
+  Refines a variable that already exists (in a body).
+
+  This only happens if the var contains a gradual type,
+  or if we are doing a guard analysis or occurrence typing.
+  Returns `true` if there was a refinement, `false` otherwise.
+  """
+  def refine_body_var({_, meta, _}, type, expr, stack, context) do
+    version = Keyword.fetch!(meta, :version)
+    %{vars: %{^version => %{type: old_type, off_traces: off_traces} = data} = vars} = context
+
+    context =
+      if gradual?(old_type) and type not in [term(), dynamic()] do
+        case compatible_intersection(old_type, type) do
+          {:ok, new_type} when new_type != old_type ->
+            data = %{
+              data
+              | type: new_type,
+                off_traces: new_trace(expr, new_type, stack, off_traces)
+            }
+
+            %{context | vars: %{vars | version => data}}
+
+          _ ->
+            context
+        end
+      else
+        context
+      end
+
+    {old_type, context}
+  end
+
   @doc """
   Refines the type of a variable.
+
+  Since this happens in a head, we use intersection
+  because we want to refine types. Otherwise we should
+  use compatibility.
   """
-  def refine_var(var, type, expr, formatter \\ :default, stack, context) do
+  def refine_head_var(var, type, expr, stack, context) do
     {var_name, meta, var_context} = var
     version = Keyword.fetch!(meta, :version)
 
     case context.vars do
-      %{^version => %{type: old_type, off_traces: off_traces} = data} ->
+      %{^version => %{type: old_type, off_traces: off_traces} = data} = vars ->
         new_type = intersection(type, old_type)
 
         data = %{
           data
           | type: new_type,
-            off_traces: new_trace(expr, type, formatter, stack, off_traces)
+            off_traces: new_trace(expr, type, stack, off_traces)
         }
 
-        context = put_in(context.vars[version], data)
+        context = %{context | vars: %{vars | version => data}}
 
         # We need to return error otherwise it leads to cascading errors
         if empty?(new_type) do
           {:error, error_type(),
-           error({:refine_var, old_type, type, var, context}, meta, stack, context)}
+           error({:refine_head_var, old_type, type, var, context}, meta, stack, context)}
         else
           {:ok, new_type, context}
         end
 
-      %{} ->
+      %{} = vars ->
         data = %{
           type: type,
           name: var_name,
           context: var_context,
-          off_traces: new_trace(expr, type, formatter, stack, [])
+          off_traces: new_trace(expr, type, stack, [])
         }
 
-        context = put_in(context.vars[version], data)
+        context = %{context | vars: Map.put(vars, version, data)}
         {:ok, type, context}
     end
   end
 
-  defp new_trace(nil, _type, _formatter, _stack, traces),
+  defp new_trace(nil, _type, _stack, traces),
     do: traces
 
-  defp new_trace(expr, type, formatter, stack, traces),
-    do: [{expr, stack.file, type, formatter} | traces]
+  defp new_trace(expr, type, stack, traces),
+    do: [{expr, stack.file, type} | traces]
 
   ## Implementations
 
@@ -324,12 +361,13 @@ defmodule Module.Types.Of do
           Module.Types.Pattern.of_match_var(left, type, expr, stack, context)
 
         :guard ->
-          Module.Types.Pattern.of_guard(left, type, expr, stack, context)
+          {actual, context} = Module.Types.Pattern.of_guard(left, type, expr, stack, context)
+          compatible(actual, type, expr, stack, context)
 
         :expr ->
           left = annotate_interpolation(left, right)
-          {actual, context} = Module.Types.Expr.of_expr(left, stack, context)
-          intersect(actual, type, expr, stack, context)
+          {actual, context} = Module.Types.Expr.of_expr(left, type, expr, stack, context)
+          compatible(actual, type, expr, stack, context)
       end
 
     specifier_size(kind, right, stack, context)
@@ -368,14 +406,15 @@ defmodule Module.Types.Of do
 
   defp specifier_size(:expr, {:size, _, [arg]} = expr, stack, context)
        when not is_integer(arg) do
-    {actual, context} = Module.Types.Expr.of_expr(arg, stack, context)
-    {_, context} = intersect(actual, integer(), expr, stack, context)
+    {actual, context} = Module.Types.Expr.of_expr(arg, integer(), expr, stack, context)
+    {_, context} = compatible(actual, integer(), expr, stack, context)
     context
   end
 
   defp specifier_size(_pattern_or_guard, {:size, _, [arg]} = expr, stack, context)
        when not is_integer(arg) do
-    {_type, context} = Module.Types.Pattern.of_guard(arg, integer(), expr, stack, context)
+    {actual, context} = Module.Types.Pattern.of_guard(arg, integer(), expr, stack, context)
+    {_, context} = compatible(actual, integer(), expr, stack, context)
     context
   end
 
@@ -404,15 +443,14 @@ defmodule Module.Types.Of do
   ## Warning helpers
 
   @doc """
-  Intersects two types and emit an incompatible error if empty.
+  Checks if two types are compatible and emit an incompatible error if not.
   """
-  def intersect(actual, expected, expr, stack, context) do
-    type = intersection(actual, expected)
-
-    if empty?(type) do
-      {error_type(), incompatible_error(expr, expected, actual, stack, context)}
+  # TODO: Consider getting rid of this and emitting precise errors instead.
+  def compatible(actual, expected, expr, stack, context) do
+    if compatible?(actual, expected) do
+      {actual, context}
     else
-      {type, context}
+      {error_type(), incompatible_error(expr, expected, actual, stack, context)}
     end
   end
 
@@ -435,7 +473,7 @@ defmodule Module.Types.Of do
 
   ## Warning formatting
 
-  def format_diagnostic({:refine_var, old_type, new_type, var, context}) do
+  def format_diagnostic({:refine_head_var, old_type, new_type, var, context}) do
     traces = collect_traces(var, context)
 
     %{
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 400599f358..7976673e51 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -1,7 +1,7 @@
 defmodule Module.Types.Pattern do
   @moduledoc false
 
-  alias Module.Types.Of
+  alias Module.Types.{Apply, Of}
   import Module.Types.{Helpers, Descr}
 
   @guard atom([true, false, :fail])
@@ -25,32 +25,45 @@ defmodule Module.Types.Pattern do
      is refined, we restart at step 2.
 
   """
-  def of_head(_patterns, _guards, expected, _tag, _meta, %{mode: :traversal}, context) do
-    {expected, context}
+  def of_head(patterns, _guards, _expected, _tag, _meta, %{mode: :traversal}, context) do
+    term = term()
+    {Enum.map(patterns, &{&1, term}), context}
   end
 
   def of_head(patterns, guards, expected, tag, meta, stack, context) do
     stack = %{stack | meta: meta}
 
-    {_trees, types, context} = of_pattern_args(patterns, expected, tag, stack, context)
+    {trees, context} = of_pattern_args(patterns, expected, tag, stack, context)
     {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
-    {types, context}
+    {trees, context}
+  end
+
+  @doc """
+  Computes the domain from the pattern tree and expected types.
+  """
+  def of_domain([{_pattern, tree} | trees], [type | expected], context) do
+    [intersection(of_pattern_tree(tree, context), type) | of_domain(trees, expected, context)]
+  end
+
+  def of_domain([], [], _context) do
+    []
   end
 
   defp of_pattern_args([], [], _tag, _stack, context) do
-    {[], [], context}
+    {[], context}
   end
 
   defp of_pattern_args(patterns, expected, tag, stack, context) do
     context = init_pattern_info(context)
     {trees, context} = of_pattern_args_index(patterns, 0, [], stack, context)
+    {pattern_info, context} = pop_pattern_info(context)
 
-    {types, context} =
-      of_pattern_recur(expected, tag, stack, context, fn types, changed, context ->
+    {_, context} =
+      of_pattern_recur(expected, tag, pattern_info, stack, context, fn types, changed, context ->
         of_pattern_args_tree(trees, types, changed, 0, [], tag, stack, context)
       end)
 
-    {trees, types, context}
+    {trees, context}
   end
 
   defp of_pattern_args_index([pattern | tail], index, acc, stack, context) do
@@ -98,48 +111,70 @@ defmodule Module.Types.Pattern do
   end
 
   @doc """
-  A simplified version of `of_head` used by `=` and `<-`.
-
-  This version tracks the whole expression in tracing,
-  instead of only the pattern.
+  Handles the match operator.
   """
-  def of_match(pattern, guards \\ [], expected, expr, tag, stack, context)
+  def of_match(pattern, expected_fun, expr, stack, context)
 
-  def of_match(_pattern, _guards, expected, _expr, _tag, %{mode: :traversal}, context) do
-    {expected, context}
+  def of_match(_pattern, expected_fun, _expr, %{mode: :traversal}, context) do
+    expected_fun.(dynamic(), context)
   end
 
-  def of_match(pattern, guards, expected, expr, tag, stack, context) do
+  def of_match(pattern, expected_fun, expr, stack, context) do
     context = init_pattern_info(context)
     {tree, context} = of_pattern(pattern, [{:arg, 0, expr}], stack, context)
+    {pattern_info, context} = pop_pattern_info(context)
+    {expected, context} = expected_fun.(of_pattern_tree(tree, context), context)
+    tag = {:match, expected}
 
     {[type], context} =
-      of_pattern_recur([expected], tag, stack, context, fn [type], [0], context ->
-        with {:ok, type, context} <-
-               of_pattern_intersect(tree, type, expr, 0, tag, stack, context) do
-          {:ok, [type], context}
-        end
-      end)
+      of_single_pattern_recur(expected, tag, tree, pattern_info, expr, stack, context)
 
-    {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
     {type, context}
   end
 
+  @doc """
+  Handles matches in generators.
+  """
+  def of_generator(pattern, guards, expected, tag, expr, stack, context)
+
+  def of_generator(_pattern, _guards, _expected, _tag, _expr, %{mode: :traversal}, context) do
+    context
+  end
+
+  def of_generator(pattern, guards, expected, tag, expr, stack, context) do
+    context = init_pattern_info(context)
+    {tree, context} = of_pattern(pattern, [{:arg, 0, expr}], stack, context)
+    {pattern_info, context} = pop_pattern_info(context)
+
+    {_, context} =
+      of_single_pattern_recur(expected, tag, tree, pattern_info, expr, stack, context)
+
+    {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
+    context
+  end
+
+  defp of_single_pattern_recur(expected, tag, tree, pattern_info, expr, stack, context) do
+    of_pattern_recur([expected], tag, pattern_info, stack, context, fn [type], [0], context ->
+      with {:ok, type, context} <-
+             of_pattern_intersect(tree, type, expr, 0, tag, stack, context) do
+        {:ok, [type], context}
+      end
+    end)
+  end
+
   defp all_single_path?(vars, info, index) do
     info
     |> Map.get(index, [])
     |> Enum.all?(fn version -> match?([_], Map.fetch!(vars, version)) end)
   end
 
-  defp of_pattern_recur(types, tag, stack, context, callback) do
-    %{pattern_info: {vars, info, _counter}} = context
-    context = nilify_pattern_info(context)
+  defp of_pattern_recur(types, tag, pattern_info, stack, context, callback) do
+    {vars, info, _counter} = pattern_info
     changed = :lists.seq(0, length(types) - 1)
 
     # If all variables in a given index have a single path,
     # then there are no changes to propagate
     unchangeable = for index <- changed, all_single_path?(vars, info, index), do: index
-
     vars = Map.to_list(vars)
 
     try do
@@ -165,13 +200,13 @@ defmodule Module.Types.Pattern do
 
               case of_pattern_var(path, actual, true, info, context) do
                 {type, reachable_var?} ->
-                  # If current type is already a subtype, there is nothing to refine.
+                  # Optimization: if current type is already a subtype, there is nothing to refine.
                   with %{^version => %{type: current_type}} <- context.vars,
                        true <- subtype?(current_type, type) do
                     {var_changed?, context}
                   else
                     _ ->
-                      case Of.refine_var(var, type, expr, stack, context) do
+                      case Of.refine_head_var(var, type, expr, stack, context) do
                         {:ok, _type, context} -> {var_changed? or reachable_var?, context}
                         {:error, _type, context} -> throw({types, context})
                       end
@@ -283,36 +318,39 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  defp of_pattern_tree(descr, _context) when is_descr(descr),
+  @doc """
+  Receives the pattern tree and the context and returns a concrete type.
+  """
+  def of_pattern_tree(descr, _context) when is_descr(descr),
     do: descr
 
-  defp of_pattern_tree({:tuple, entries}, context) do
+  def of_pattern_tree({:tuple, entries}, context) do
     tuple(Enum.map(entries, &of_pattern_tree(&1, context)))
   end
 
-  defp of_pattern_tree({:open_map, static, dynamic}, context) do
+  def of_pattern_tree({:open_map, static, dynamic}, context) do
     dynamic = Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, context)} end)
     open_map(static ++ dynamic)
   end
 
-  defp of_pattern_tree({:closed_map, static, dynamic}, context) do
+  def of_pattern_tree({:closed_map, static, dynamic}, context) do
     dynamic = Enum.map(dynamic, fn {key, value} -> {key, of_pattern_tree(value, context)} end)
     closed_map(static ++ dynamic)
   end
 
-  defp of_pattern_tree({:non_empty_list, [head | tail], suffix}, context) do
+  def of_pattern_tree({:non_empty_list, [head | tail], suffix}, context) do
     tail
     |> Enum.reduce(of_pattern_tree(head, context), &union(of_pattern_tree(&1, context), &2))
     |> non_empty_list(of_pattern_tree(suffix, context))
   end
 
-  defp of_pattern_tree({:intersection, entries}, context) do
+  def of_pattern_tree({:intersection, entries}, context) do
     entries
     |> Enum.map(&of_pattern_tree(&1, context))
     |> Enum.reduce(&intersection/2)
   end
 
-  defp of_pattern_tree({:var, version}, context) do
+  def of_pattern_tree({:var, version}, context) do
     case context do
       %{vars: %{^version => %{type: type}}} -> type
       _ -> term()
@@ -322,9 +360,14 @@ defmodule Module.Types.Pattern do
   @doc """
   Function used to assign a type to a variable. Used by %struct{}
   and binary patterns.
+
+  Given those values are actually checked at compile-time,
+  except for the variables, that's the only scenario we need to handle.
   """
+  # TODO: Perhaps merge this with guards
   def of_match_var({:^, _, [var]}, expected, expr, stack, context) do
-    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+    {type, context} = Of.refine_body_var(var, expected, expr, stack, context)
+    Of.compatible(type, expected, expr, stack, context)
   end
 
   def of_match_var({:_, _, _}, expected, _expr, _stack, context) do
@@ -332,12 +375,12 @@ defmodule Module.Types.Pattern do
   end
 
   def of_match_var(var, expected, expr, stack, context) when is_var(var) do
-    {_ok?, type, context} = Of.refine_var(var, expected, expr, stack, context)
+    {_ok?, type, context} = Of.refine_head_var(var, expected, expr, stack, context)
     {type, context}
   end
 
-  def of_match_var(ast, expected, expr, stack, context) do
-    of_match(ast, expected, expr, :default, stack, context)
+  def of_match_var(_ast, expected, _expr, _stack, context) do
+    {expected, context}
   end
 
   ## Patterns
@@ -602,48 +645,28 @@ defmodule Module.Types.Pattern do
   # This function is public as it is invoked from Of.binary/4.
 
   # :atom
-  def of_guard(atom, expected, expr, stack, context) when is_atom(atom) do
-    if atom_type?(expected, atom) do
-      {atom([atom]), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, atom([atom]), stack, context)}
-    end
+  def of_guard(atom, _expected, _expr, _stack, context) when is_atom(atom) do
+    {atom([atom]), context}
   end
 
   # 12
-  def of_guard(literal, expected, expr, stack, context) when is_integer(literal) do
-    if integer_type?(expected) do
-      {integer(), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, integer(), stack, context)}
-    end
+  def of_guard(literal, _expected, _expr, _stack, context) when is_integer(literal) do
+    {integer(), context}
   end
 
   # 1.2
-  def of_guard(literal, expected, expr, stack, context) when is_float(literal) do
-    if float_type?(expected) do
-      {float(), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, float(), stack, context)}
-    end
+  def of_guard(literal, _expected, _expr, _stack, context) when is_float(literal) do
+    {float(), context}
   end
 
   # "..."
-  def of_guard(literal, expected, expr, stack, context) when is_binary(literal) do
-    if binary_type?(expected) do
-      {binary(), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, binary(), stack, context)}
-    end
+  def of_guard(literal, _expected, _expr, _stack, context) when is_binary(literal) do
+    {binary(), context}
   end
 
   # []
-  def of_guard([], expected, expr, stack, context) do
-    if empty_list_type?(expected) do
-      {empty_list(), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, empty_list(), stack, context)}
-    end
+  def of_guard([], _expected, _expr, _stack, context) do
+    {empty_list(), context}
   end
 
   # [expr, ...]
@@ -675,19 +698,16 @@ defmodule Module.Types.Pattern do
   end
 
   # <<>>
-  def of_guard({:<<>>, _meta, args}, expected, expr, stack, context) do
-    if binary_type?(expected) do
-      context = Of.binary(args, :guard, stack, context)
-      {binary(), context}
-    else
-      {error_type(), Of.incompatible_error(expr, expected, binary(), stack, context)}
-    end
+  def of_guard({:<<>>, _meta, args}, _expected, _expr, stack, context) do
+    context = Of.binary(args, :guard, stack, context)
+    {binary(), context}
   end
 
   # ^var
   def of_guard({:^, _meta, [var]}, expected, expr, stack, context) do
-    # This is by definition a variable defined outside of this pattern, so we don't track it.
-    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+    # This is used by binary size, which behaves as a mixture of match and guard
+    {type, context} = Of.refine_body_var(var, expected, expr, stack, context)
+    Of.compatible(type, expected, expr, stack, context)
   end
 
   # {...}
@@ -713,17 +733,20 @@ defmodule Module.Types.Pattern do
   end
 
   # Remote
-  def of_guard({{:., _, [:erlang, function]}, _, args} = call, _expected, expr, stack, context)
-      when is_atom(function) do
-    {args_type, context} =
-      Enum.map_reduce(args, context, &of_guard(&1, dynamic(), expr, stack, &2))
+  def of_guard({{:., _, [:erlang, fun]}, meta, args} = call, expected, _expr, stack, context)
+      when is_atom(fun) do
+    {info, domain, context} =
+      Apply.remote_domain(:erlang, fun, args, expected, meta, stack, context)
+
+    {args_types, context} =
+      zip_map_reduce(args, domain, context, &of_guard(&1, &2, call, stack, &3))
 
-    Module.Types.Apply.remote(:erlang, function, args, args_type, call, stack, context)
+    Apply.remote_apply(info, :erlang, fun, args_types, call, stack, context)
   end
 
   # var
   def of_guard(var, expected, expr, stack, context) when is_var(var) do
-    Of.intersect(Of.var(var, context), expected, expr, stack, context)
+    Of.compatible(Of.var(var, context), expected, expr, stack, context)
   end
 
   ## Helpers
@@ -736,8 +759,8 @@ defmodule Module.Types.Pattern do
     %{context | pattern_info: {%{}, %{}, 1}}
   end
 
-  defp nilify_pattern_info(context) do
-    %{context | pattern_info: nil}
+  defp pop_pattern_info(%{pattern_info: pattern_info} = context) do
+    {pattern_info, %{context | pattern_info: nil}}
   end
 
   # $ type tag = head_pattern() or match_pattern()
diff --git a/lib/elixir/pages/references/gradual-set-theoretic-types.md b/lib/elixir/pages/references/gradual-set-theoretic-types.md
index ab8a0abcb9..21ca2fd868 100644
--- a/lib/elixir/pages/references/gradual-set-theoretic-types.md
+++ b/lib/elixir/pages/references/gradual-set-theoretic-types.md
@@ -90,17 +90,9 @@ Inferring type signatures comes with a series of trade-offs:
 
   * Cascading errors - when a user accidentally makes type errors or the code has conflicting assumptions, type inference may lead to less clear error messages as the type system tries to reconcile diverging type assumptions across code paths.
 
-On the other hand, type inference offers the benefit of enabling type checking for functions and codebases without requiring the user to add type annotations. To balance these trade-offs, Elixir’s type system provides the following type reconstruction capabilities:
+On the other hand, type inference offers the benefit of enabling type checking for functions and codebases without requiring the user to add type annotations. To balance these trade-offs, Elixir performs module-local inference: the arguments, returns types, and all variables in a function are computed considering all of the function calls to the same module and to Elixir's standard library. Any call to a function in another module is conservatively assumed to return `dynamic()` during inference. Our goal is to provide an efficient type reconstruction algorithm that can detect definite bugs in dynamic codebases, even in the absence of explicit type annotations.
 
-  * Local type inference - the type system automatically infer the types of variables, at the place those variables are defined.
-
-  * Type inference of patterns (and guards in future releases) - the argument types of a function are automatically inferred based on patterns and guards, which capture and narrow types based on common Elixir constructs.
-
-  * Module-local inference of return types - the gradual return types of functions are computed considering all of the functions within the module itself. Any call to a function in another module is conservatively assumed to return `dynamic()`.
-
-The last two items offer gradual reconstruction of type signatures. Our goal is to provide an efficient type reconstruction algorithm that can detect definite bugs in dynamic codebases, even in the absence of explicit type annotations. The gradual system focuses on proving cases where all combinations of a type *will* fail, rather than issuing warnings for cases where some combinations *might* error.
-
-Once Elixir introduces typed function signatures (see "Roadmap"), any function with an explicit type signature will be checked against the user-provided type, as in other statically typed languages, without performing type inference of the function signature.
+The gradual system focuses on proving cases where all combinations of a type *will* fail, rather than issuing warnings for cases where some combinations *might* error. Once Elixir introduces typed function signatures (see "Roadmap"), any function with an explicit type signature will be checked against the user-provided type, as in other statically typed languages, without performing type inference.
 
 ## Roadmap
 
diff --git a/lib/elixir/src/elixir_bitstring.erl b/lib/elixir/src/elixir_bitstring.erl
index 4a92a9827a..7210f24f1b 100644
--- a/lib/elixir/src/elixir_bitstring.erl
+++ b/lib/elixir/src/elixir_bitstring.erl
@@ -1,6 +1,6 @@
 -module(elixir_bitstring).
 -export([expand/5, format_error/1, validate_spec/2]).
--import(elixir_errors, [function_error/4, file_error/4]).
+-import(elixir_errors, [function_error/4]).
 -include("elixir.hrl").
 
 expand_match(Expr, {S, OriginalS}, E) ->
@@ -13,11 +13,6 @@ expand(Meta, Args, S, E, RequireSize) ->
       {EArgs, Alignment, {SA, _}, EA} =
         expand(Meta, fun expand_match/3, Args, [], {S, S}, E, 0, RequireSize),
 
-      case find_match(EArgs) of
-        false -> ok;
-        Match -> file_error(Meta, EA, ?MODULE, {nested_match, Match})
-      end,
-
       {{'<<>>', [{alignment, Alignment} | Meta], EArgs}, SA, EA};
     _ ->
       PairS = {elixir_env:prepare_write(S), S},
@@ -32,6 +27,7 @@ expand(_BitstrMeta, _Fun, [], Acc, S, E, Alignment, _RequireSize) ->
   {lists:reverse(Acc), Alignment, S, E};
 expand(BitstrMeta, Fun, [{'::', Meta, [Left, Right]} | T], Acc, S, E, Alignment, RequireSize) ->
   {ELeft, {SL, OriginalS}, EL} = expand_expr(Left, Fun, S, E),
+  validate_expr(ELeft, Meta, E),
 
   MatchOrRequireSize = RequireSize or is_match_size(T, EL),
   EType = expr_type(ELeft),
@@ -47,6 +43,7 @@ expand(BitstrMeta, Fun, [{'::', Meta, [Left, Right]} | T], Acc, S, E, Alignment,
 expand(BitstrMeta, Fun, [H | T], Acc, S, E, Alignment, RequireSize) ->
   Meta = extract_meta(H, BitstrMeta),
   {ELeft, {SS, OriginalS}, ES} = expand_expr(H, Fun, S, E),
+  validate_expr(ELeft, Meta, E),
 
   MatchOrRequireSize = RequireSize or is_match_size(T, ES),
   EType = expr_type(ELeft),
@@ -145,6 +142,17 @@ expand_expr({{'.', _, [Mod, to_string]}, _, [Arg]} = AST, Fun, S, #{context := C
 expand_expr(Component, Fun, S, E) ->
   Fun(Component, S, E).
 
+validate_expr(Expr, Meta, #{context := match} = E) ->
+  case Expr of
+    {Var, _Meta, Ctx} when is_atom(Var), is_atom(Ctx) -> ok;
+    {'<<>>', _, _} -> ok;
+    {'^', _, _} -> ok;
+    _ when is_number(Expr); is_binary(Expr) -> ok;
+    _ -> function_error(extract_meta(Expr, Meta), E, ?MODULE, {unknown_match, Expr})
+  end;
+validate_expr(_Expr, _Meta, _E) ->
+  ok.
+
 %% Expands and normalizes types of a bitstring.
 
 expand_specs(ExprType, Meta, Info, S, OriginalS, E, ExpectSize) ->
@@ -353,18 +361,6 @@ valid_float_size(_) -> false.
 add_spec(default, Spec) -> Spec;
 add_spec(Key, Spec) -> [{Key, [], nil} | Spec].
 
-find_match([{'=', _, [_Left, _Right]} = Expr | _Rest]) ->
-  Expr;
-find_match([{_, _, Args} | Rest]) when is_list(Args) ->
-  case find_match(Args) of
-    false -> find_match(Rest);
-    Match -> Match
-  end;
-find_match([_Arg | Rest]) ->
-  find_match(Rest);
-find_match([]) ->
-  false.
-
 format_error({unaligned_binary, Expr}) ->
   Message = "expected ~ts to be a binary but its number of bits is not divisible by 8",
   io_lib:format(Message, ['Elixir.Macro':to_string(Expr)]);
@@ -409,10 +405,9 @@ format_error({bittype_mismatch, Val1, Val2, Where}) ->
 format_error({bad_unit_argument, Unit}) ->
   io_lib:format("unit in bitstring expects an integer as argument, got: ~ts",
                 ['Elixir.Macro':to_string(Unit)]);
-format_error({nested_match, Expr}) ->
+format_error({unknown_match, Expr}) ->
   Message =
-    "cannot pattern match inside a bitstring "
-      "that is already in match, got: ~ts",
+    "a bitstring only accepts binaries, numbers, and variables inside a match, got: ~ts",
   io_lib:format(Message, ['Elixir.Macro':to_string(Expr)]);
 format_error({undefined_var_in_spec, Var}) ->
   Message =
diff --git a/lib/elixir/test/elixir/kernel/errors_test.exs b/lib/elixir/test/elixir/kernel/errors_test.exs
index a328f3767e..8b99ae2178 100644
--- a/lib/elixir/test/elixir/kernel/errors_test.exs
+++ b/lib/elixir/test/elixir/kernel/errors_test.exs
@@ -941,7 +941,7 @@ defmodule Kernel.ErrorsTest do
 
   test "failed remote call stacktrace includes file/line info" do
     try do
-      bad_remote_call(1)
+      bad_remote_call(Process.get(:unused, 1))
     rescue
       ArgumentError ->
         assert [
diff --git a/lib/elixir/test/elixir/kernel/expansion_test.exs b/lib/elixir/test/elixir/kernel/expansion_test.exs
index 4e08384a5b..aeaea9bc40 100644
--- a/lib/elixir/test/elixir/kernel/expansion_test.exs
+++ b/lib/elixir/test/elixir/kernel/expansion_test.exs
@@ -2387,6 +2387,15 @@ defmodule Kernel.ExpansionTest do
                |> clean_bit_modifiers()
     end
 
+    test "invalid match" do
+      assert_compile_error(
+        "a bitstring only accepts binaries, numbers, and variables inside a match",
+        fn ->
+          expand(quote(do: <<%{}>> = foo()))
+        end
+      )
+    end
+
     test "nested match" do
       assert expand(quote(do: <<foo = bar>>)) |> clean_meta([:alignment]) ==
                quote(do: <<foo = bar()::integer>>) |> clean_bit_modifiers()
@@ -2395,16 +2404,6 @@ defmodule Kernel.ExpansionTest do
              |> clean_meta([:alignment]) ==
                quote(do: <<45::integer, <<_::integer, _::binary>> = rest()::binary>>)
                |> clean_bit_modifiers()
-
-      message = ~r"cannot pattern match inside a bitstring that is already in match"
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: <<bar = baz>> = foo()))
-      end)
-
-      assert_compile_error(message, fn ->
-        expand(quote(do: <<?-, <<_, _::binary>> = rest::binary>> = foo()))
-      end)
     end
 
     test "inlines binaries inside interpolation" do
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 2d814672a1..2ffcb97786 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -579,20 +579,6 @@ defmodule Module.Types.DescrTest do
     end
   end
 
-  describe "queries" do
-    test "atom_type?" do
-      assert atom_type?(term(), :foo)
-      assert atom_type?(dynamic(), :foo)
-
-      assert atom_type?(atom([:foo, :bar]), :foo)
-      refute atom_type?(atom([:foo, :bar]), :baz)
-      assert atom_type?(negation(atom([:foo, :bar])), :baz)
-
-      refute atom_type?(union(atom([:foo, :bar]), integer()), :baz)
-      refute atom_type?(dynamic(union(atom([:foo, :bar]), integer())), :baz)
-    end
-  end
-
   describe "projections" do
     test "fun_fetch" do
       assert fun_fetch(term(), 1) == :error
@@ -1198,6 +1184,10 @@ defmodule Module.Types.DescrTest do
 
     test "dynamic" do
       assert dynamic() |> to_quoted_string() == "dynamic()"
+
+      assert dynamic(union(atom(), integer())) |> union(integer()) |> to_quoted_string() ==
+               "dynamic(atom()) or integer()"
+
       assert intersection(binary(), dynamic()) |> to_quoted_string() == "binary()"
 
       assert intersection(union(binary(), pid()), dynamic()) |> to_quoted_string() ==
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 6b5ec1a804..28318a10f5 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -41,6 +41,16 @@ defmodule Module.Types.ExprTest do
       assert typecheck!([x], [:ok | x]) == dynamic(non_empty_list(term(), term()))
     end
 
+    test "inference" do
+      assert typecheck!(
+               [x, y, z],
+               (
+                 List.to_integer([x, y | z])
+                 {x, y, z}
+               )
+             ) == dynamic(tuple([integer(), integer(), list(integer())]))
+    end
+
     test "hd" do
       assert typecheck!([x = [123, :foo]], hd(x)) == dynamic(union(atom([:foo]), integer()))
       assert typecheck!([x = [123 | :foo]], hd(x)) == dynamic(integer())
@@ -115,6 +125,16 @@ defmodule Module.Types.ExprTest do
   end
 
   describe "funs" do
+    test "infers funs" do
+      assert typecheck!(
+               [x],
+               (
+                 x.(1, 2)
+                 x
+               )
+             ) == dynamic(fun())
+    end
+
     test "incompatible" do
       assert typeerror!([%x{}, a1, a2], x.(a1, a2)) == ~l"""
              expected a 2-arity function on call:
@@ -139,6 +159,43 @@ defmodule Module.Types.ExprTest do
       assert typecheck!([%x{}], x.foo_bar()) == dynamic()
     end
 
+    test "infers atoms" do
+      assert typecheck!(
+               [x],
+               (
+                 x.foo_bar()
+                 x
+               )
+             ) == dynamic(atom())
+
+      assert typecheck!(
+               [x],
+               (
+                 x.foo_bar(123)
+                 x
+               )
+             ) == dynamic(atom())
+
+      assert typecheck!(
+               [x],
+               (
+                 &x.foo_bar/1
+                 x
+               )
+             ) == dynamic(atom())
+    end
+
+    test "infers maps" do
+      assert typecheck!(
+               [x],
+               (
+                 :foo = x.foo_bar
+                 123 = x.baz_bat
+                 x
+               )
+             ) == dynamic(open_map(foo_bar: atom([:foo]), baz_bat: integer()))
+    end
+
     test "undefined function warnings" do
       assert typewarn!(URI.unknown("foo")) ==
                {dynamic(), "URI.unknown/1 is undefined or private"}
@@ -215,7 +272,7 @@ defmodule Module.Types.ExprTest do
                """
 
       assert typeerror!(
-               [<<x::integer>>, y = Atom, z],
+               [<<x::integer>>, y = SomeMod, z],
                (
                  mod =
                    cond do
@@ -233,7 +290,7 @@ defmodule Module.Types.ExprTest do
 
                where "mod" was given the type:
 
-                   # type: dynamic(Atom or integer()) or integer()
+                   # type: dynamic(SomeMod) or integer()
                    # from: types_test.ex:LINE-9
                    mod =
                      cond do
@@ -290,9 +347,61 @@ defmodule Module.Types.ExprTest do
                    <<x::integer>>
                """
     end
+
+    test "requires all combinations to be compatible" do
+      assert typeerror!(
+               [condition, string],
+               (
+                 mod = if condition, do: String, else: List
+                 mod.to_integer(string)
+               )
+             )
+             |> strip_ansi() == ~l"""
+             incompatible types given to String.to_integer/1:
+
+                 mod.to_integer(string)
+                 #=> invoked as String.to_integer/1
+
+             given types:
+
+                 dynamic(non_empty_list(integer()))
+
+             but expected one of:
+
+                 binary()
+
+             where "mod" was given the type:
+
+                 # type: List or String
+                 # from: types_test.ex:LINE-4
+                 mod =
+                   if condition do
+                     String
+                   else
+                     List
+                   end
+
+             where "string" was given the type:
+
+                 # type: dynamic(non_empty_list(integer()))
+                 # from: types_test.ex:LINE-3
+                 mod.to_integer(string)
+                 #=> invoked as List.to_integer/1
+             """
+    end
   end
 
   describe "binaries" do
+    test "inference" do
+      assert typecheck!(
+               [x, y],
+               (
+                 <<x::float-size(y)>>
+                 {x, y}
+               )
+             ) == dynamic(tuple([union(float(), integer()), integer()]))
+    end
+
     test "warnings" do
       assert typeerror!([<<x::binary-size(2)>>], <<x::float>>) ==
                ~l"""
@@ -396,6 +505,16 @@ defmodule Module.Types.ExprTest do
       assert typecheck!([x], {:ok, x}) == dynamic(tuple([atom([:ok]), term()]))
     end
 
+    test "inference" do
+      assert typecheck!(
+               [x, y],
+               (
+                 {:ok, :error} = {x, y}
+                 {x, y}
+               )
+             ) == dynamic(tuple([atom([:ok]), atom([:error])]))
+    end
+
     test "elem/2" do
       assert typecheck!(elem({:ok, 123}, 0)) == atom([:ok])
       assert typecheck!(elem({:ok, 123}, 1)) == integer()
@@ -519,7 +638,7 @@ defmodule Module.Types.ExprTest do
                """
     end
 
-    test "duplicate/2" do
+    test "Tuple.duplicate/2" do
       assert typecheck!(Tuple.duplicate(123, 0)) == tuple([])
       assert typecheck!(Tuple.duplicate(123, 1)) == tuple([integer()])
       assert typecheck!(Tuple.duplicate(123, 2)) == tuple([integer(), integer()])
@@ -875,93 +994,90 @@ defmodule Module.Types.ExprTest do
     end
 
     test "warns when comparison is constant" do
-      assert typewarn!([x = :foo, y = 321], min(x, y)) ==
-               {dynamic(union(integer(), atom([:foo]))),
-                ~l"""
-                comparison between distinct types found:
+      assert typeerror!([x = :foo, y = 321], min(x, y)) ==
+               ~l"""
+               comparison between distinct types found:
 
-                    min(x, y)
+                   min(x, y)
 
-                given types:
+               given types:
 
-                    min(dynamic(:foo), integer())
+                   min(dynamic(:foo), integer())
 
-                where "x" was given the type:
+               where "x" was given the type:
 
-                    # type: dynamic(:foo)
-                    # from: types_test.ex:LINE-2
-                    x = :foo
+                   # type: dynamic(:foo)
+                   # from: types_test.ex:LINE-1
+                   x = :foo
 
-                where "y" was given the type:
+               where "y" was given the type:
 
-                    # type: integer()
-                    # from: types_test.ex:LINE-2
-                    y = 321
+                   # type: integer()
+                   # from: types_test.ex:LINE-1
+                   y = 321
 
-                While Elixir can compare across all types, you are comparing across types \
-                which are always disjoint, and the result is either always true or always false
-                """}
+               While Elixir can compare across all types, you are comparing across types \
+               which are always disjoint, and the result is either always true or always false
+               """
 
-      assert typewarn!([x = 123, y = 456.0], x === y) ==
-               {boolean(),
-                ~l"""
-                comparison between distinct types found:
+      assert typeerror!([x = 123, y = 456.0], x === y) ==
+               ~l"""
+               comparison between distinct types found:
 
-                    x === y
+                   x === y
 
-                given types:
+               given types:
 
-                    integer() === float()
+                   integer() === float()
 
-                where "x" was given the type:
+               where "x" was given the type:
 
-                    # type: integer()
-                    # from: types_test.ex:LINE-2
-                    x = 123
+                   # type: integer()
+                   # from: types_test.ex:LINE-1
+                   x = 123
 
-                where "y" was given the type:
+               where "y" was given the type:
 
-                    # type: float()
-                    # from: types_test.ex:LINE-2
-                    y = 456.0
+                   # type: float()
+                   # from: types_test.ex:LINE-1
+                   y = 456.0
 
-                While Elixir can compare across all types, you are comparing across types \
-                which are always disjoint, and the result is either always true or always false
-                """}
+               While Elixir can compare across all types, you are comparing across types \
+               which are always disjoint, and the result is either always true or always false
+               """
     end
 
     test "warns on comparison with struct across dynamic call" do
-      assert typewarn!([x = :foo, y = %Point{}, mod = Kernel], mod.<=(x, y)) ==
-               {boolean(),
-                ~l"""
-                comparison with structs found:
+      assert typeerror!([x = :foo, y = %Point{}, mod = Kernel], mod.<=(x, y)) ==
+               ~l"""
+               comparison with structs found:
 
-                    mod.<=(x, y)
+                   mod.<=(x, y)
 
-                given types:
+               given types:
 
-                    dynamic(:foo) <= dynamic(%Point{})
+                   dynamic(:foo) <= dynamic(%Point{})
 
-                where "mod" was given the type:
+               where "mod" was given the type:
 
-                    # type: dynamic(Kernel)
-                    # from: types_test.ex:LINE-2
-                    mod = Kernel
+                   # type: dynamic(Kernel)
+                   # from: types_test.ex:LINE-1
+                   mod = Kernel
 
-                where "x" was given the type:
+               where "x" was given the type:
 
-                    # type: dynamic(:foo)
-                    # from: types_test.ex:LINE-2
-                    x = :foo
+                   # type: dynamic(:foo)
+                   # from: types_test.ex:LINE-1
+                   x = :foo
 
-                where "y" was given the type:
+               where "y" was given the type:
 
-                    # type: dynamic(%Point{})
-                    # from: types_test.ex:LINE-2
-                    y = %Point{}
+                   # type: dynamic(%Point{})
+                   # from: types_test.ex:LINE-1
+                   y = %Point{}
 
-                Comparison operators (>, <, >=, <=, min, and max) perform structural and not semantic comparison. Comparing with a struct won't give meaningful results. Structs that can be compared typically define a compare/2 function within their modules that can be used for semantic comparison.
-                """}
+               Comparison operators (>, <, >=, <=, min, and max) perform structural and not semantic comparison. Comparing with a struct won't give meaningful results. Structs that can be compared typically define a compare/2 function within their modules that can be used for semantic comparison.
+               """
     end
   end
 
@@ -1073,6 +1189,20 @@ defmodule Module.Types.ExprTest do
              ) == atom([:ok, :error])
     end
 
+    test "resets branches" do
+      assert typecheck!(
+               [x],
+               (
+                 case :rand.uniform() do
+                   y when y < 0.5 -> x.foo
+                   y when y > 0.5 -> x.bar()
+                 end
+
+                 x
+               )
+             ) == dynamic()
+    end
+
     test "returns unions of all clauses" do
       assert typecheck!(
                [x],
@@ -1170,6 +1300,32 @@ defmodule Module.Types.ExprTest do
              ) == dynamic(atom([:ok, :error, :timeout]))
     end
 
+    test "infers type for timeout" do
+      assert typecheck!(
+               [x],
+               receive do
+               after
+                 x -> x
+               end
+             ) == dynamic(union(integer(), atom([:infinity])))
+    end
+
+    test "resets branches" do
+      assert typecheck!(
+               [x, timeout = :infinity],
+               (
+                 receive do
+                   y when y > 0.5 -> x.foo
+                   _ -> x.bar()
+                 after
+                   timeout -> <<^x::integer>> = :crypto.strong_rand_bytes(1)
+                 end
+
+                 x
+               )
+             ) == dynamic()
+    end
+
     test "errors on bad timeout" do
       assert typeerror!(
                [x = :timeout],
@@ -1192,6 +1348,17 @@ defmodule Module.Types.ExprTest do
                  # from: types_test.ex:LINE-5
                  x = :timeout
              """
+
+      # Check for compatibility, not subtyping
+      assert typeerror!(
+               [<<x::integer, y::float>>],
+               receive do
+               after
+                 if(:rand.uniform(), do: x, else: y) -> :ok
+               end
+             ) =~ "expected "
+    after
+      " timeout given to receive to be an integer"
     end
   end
 
@@ -1228,6 +1395,25 @@ defmodule Module.Types.ExprTest do
              ) == atom([:caught1, :caught2, :rescue, :else1, :else2])
     end
 
+    test "resets branches (except after)" do
+      assert typecheck!(
+               [x],
+               (
+                 try do
+                   <<^x::float>> = :crypto.strong_rand_bytes(8)
+                 rescue
+                   ArgumentError -> x.foo
+                 catch
+                   _, _ -> x.bar()
+                 after
+                   <<^x::integer>> = :crypto.strong_rand_bytes(8)
+                 end
+
+                 x
+               )
+             ) == dynamic(integer())
+    end
+
     test "reports error from clause that will never match" do
       assert typeerror!(
                [x],
@@ -1298,6 +1484,38 @@ defmodule Module.Types.ExprTest do
                )
     end
 
+    test "generates custom traces" do
+      assert typeerror!(
+               try do
+                 raise "oops"
+               rescue
+                 e ->
+                   Integer.to_string(e)
+               end
+             )
+             |> strip_ansi() == ~l"""
+             incompatible types given to Integer.to_string/1:
+
+                 Integer.to_string(e)
+
+             given types:
+
+                 %{..., __exception__: true, __struct__: atom()}
+
+             but expected one of:
+
+                 integer()
+
+             where "e" was given the type:
+
+                 # type: %{..., __exception__: true, __struct__: atom()}
+                 # from: types_test.ex
+                 rescue e
+
+             hint: when you rescue without specifying exception names, the variable is assigned a type of a struct but all of its fields are unknown. If you are trying to access an exception's :message key, either specify the exception names or use `Exception.message/1`.
+             """
+    end
+
     test "defines an open map of two fields in anonymous rescue" do
       assert typecheck!(
                try do
@@ -1409,6 +1627,20 @@ defmodule Module.Types.ExprTest do
                     y = false
                 """}
     end
+
+    test "resets branches" do
+      assert typecheck!(
+               [x],
+               (
+                 cond do
+                   :rand.uniform() > 0.5 -> x.foo
+                   true -> x.bar()
+                 end
+
+                 x
+               )
+             ) == dynamic()
+    end
   end
 
   describe "comprehensions" do
@@ -1431,6 +1663,47 @@ defmodule Module.Types.ExprTest do
 
                #{hints(:inferred_bitstring_spec)}
                """
+
+      # Check for compatibility, not subtyping
+      assert typeerror!(
+               [<<x::integer, y::binary>>],
+               for(<<i <- if(:rand.uniform() > 0.5, do: x, else: y)>>, do: i)
+             ) =~
+               ~l"""
+               expected the right side of <- in a binary generator to be a binary:
+
+                   if :rand.uniform() > 0.5 do
+                     x
+                   else
+                     y
+                   end
+
+               but got type:
+
+                   binary() or integer()
+
+               where "x" was given the type:
+
+                   # type: integer()
+                   # from: types_test.ex:LINE-3
+                   <<x::integer, ...>>
+
+               where "y" was given the type:
+
+                   # type: binary()
+                   # from: types_test.ex:LINE-3
+                   <<..., y::binary>>
+               """
+    end
+
+    test "infers binary generators" do
+      assert typecheck!(
+               [x],
+               (
+                 for <<_ <- x>>, do: :ok
+                 x
+               )
+             ) == dynamic(binary())
     end
 
     test ":into" do
@@ -1461,7 +1734,7 @@ defmodule Module.Types.ExprTest do
              ) == dynamic(union(binary(), list(float())))
     end
 
-    test ":reduce" do
+    test ":reduce checks" do
       assert typecheck!(
                [list],
                for _ <- list, reduce: :ok do
@@ -1470,43 +1743,19 @@ defmodule Module.Types.ExprTest do
                end
              ) == union(atom([:ok]), union(integer(), float()))
     end
-  end
-
-  describe "apply" do
-    test "handles conditional modules and functions" do
-      assert typecheck!([fun], apply(String, fun, ["foo", "bar", "baz"])) == dynamic()
 
+    test ":reduce inference" do
       assert typecheck!(
-               [condition, string],
-               (
-                 fun = if condition, do: :to_integer, else: :to_float
-                 apply(String, fun, [string])
-               )
-             ) == union(integer(), float())
-
-      assert typecheck!(
-               [condition, string],
+               [list, x],
                (
-                 mod = if condition, do: String, else: List
-                 fun = if condition, do: :to_integer, else: :to_float
-                 apply(mod, fun, [string])
-               )
-             ) == union(integer(), float())
+                 123 =
+                   for _ <- list, reduce: x do
+                     x -> x
+                   end
 
-      assert typeerror!(
-               [condition, string],
-               (
-                 mod = if condition, do: String, else: List
-                 fun = if condition, do: :to_integer, else: :to_float
-                 :erlang.apply(mod, fun, [string | "tail"])
+                 x
                )
-             ) =~
-               """
-               incompatible types given to Kernel.apply/3:
-
-                   apply(mod, fun, [string | "tail"])
-
-               """
+             ) == dynamic(integer())
     end
   end
 
diff --git a/lib/elixir/test/elixir/module/types/infer_test.exs b/lib/elixir/test/elixir/module/types/infer_test.exs
index 656ee74748..6fcb821d83 100644
--- a/lib/elixir/test/elixir/module/types/infer_test.exs
+++ b/lib/elixir/test/elixir/module/types/infer_test.exs
@@ -42,10 +42,24 @@ defmodule Module.Types.InferTest do
       dynamic(atom([Point]))
     ]
 
-    assert types[{:fun1, 4}] == {:infer, [{args, atom([:ok])}]}
-    assert types[{:fun2, 4}] == {:infer, [{args, atom([:ok])}]}
-    assert types[{:fun3, 4}] == {:infer, [{args, atom([:ok])}]}
-    assert types[{:fun4, 4}] == {:infer, [{args, atom([:ok])}]}
+    assert types[{:fun1, 4}] == {:infer, nil, [{args, atom([:ok])}]}
+    assert types[{:fun2, 4}] == {:infer, nil, [{args, atom([:ok])}]}
+    assert types[{:fun3, 4}] == {:infer, nil, [{args, atom([:ok])}]}
+    assert types[{:fun4, 4}] == {:infer, nil, [{args, atom([:ok])}]}
+  end
+
+  test "infer types from expressions", config do
+    types =
+      infer config do
+        def fun(x) do
+          x.foo + x.bar
+        end
+      end
+
+    number = union(integer(), float())
+
+    assert types[{:fun, 1}] ==
+             {:infer, nil, [{[dynamic(open_map(foo: number, bar: number))], dynamic(number)}]}
   end
 
   test "infer with Elixir built-in", config do
@@ -55,7 +69,8 @@ defmodule Module.Types.InferTest do
       end
 
     assert types[{:parse, 1}] ==
-             {:infer, [{[dynamic()], dynamic(union(atom([:error]), tuple([integer(), term()])))}]}
+             {:infer, nil,
+              [{[dynamic()], dynamic(union(atom([:error]), tuple([integer(), term()])))}]}
   end
 
   test "merges patterns", config do
@@ -69,7 +84,7 @@ defmodule Module.Types.InferTest do
       end
 
     assert types[{:fun, 1}] ==
-             {:infer,
+             {:infer, [dynamic(union(atom([:ok, :error]), binary()))],
               [
                 {[dynamic(atom([:ok]))], atom([:one])},
                 {[dynamic(binary())], atom([:two, :three, :four])},
@@ -85,7 +100,9 @@ defmodule Module.Types.InferTest do
         defp priv(:error), do: :error
       end
 
-    assert types[{:pub, 1}] == {:infer, [{[dynamic()], dynamic(atom([:ok, :error]))}]}
+    assert types[{:pub, 1}] ==
+             {:infer, nil, [{[dynamic(atom([:ok, :error]))], dynamic(atom([:ok, :error]))}]}
+
     assert types[{:priv, 1}] == nil
   end
 
@@ -98,7 +115,8 @@ defmodule Module.Types.InferTest do
         def pub(x), do: super(x)
       end
 
-    assert types[{:pub, 1}] == {:infer, [{[dynamic()], dynamic(atom([:ok, :error]))}]}
+    assert types[{:pub, 1}] ==
+             {:infer, nil, [{[dynamic(atom([:ok, :error]))], dynamic(atom([:ok, :error]))}]}
   end
 
   test "infers return types even with loops", config do
@@ -107,6 +125,6 @@ defmodule Module.Types.InferTest do
         def pub(x), do: pub(x)
       end
 
-    assert types[{:pub, 1}] == {:infer, [{[dynamic()], dynamic()}]}
+    assert types[{:pub, 1}] == {:infer, nil, [{[dynamic()], dynamic()}]}
   end
 end
diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs
index 0e89c5630e..25dd062d21 100644
--- a/lib/elixir/test/elixir/module/types/integration_test.exs
+++ b/lib/elixir/test/elixir/module/types/integration_test.exs
@@ -68,7 +68,7 @@ defmodule Module.Types.IntegrationTest do
 
       assert [
                {{:c, 0}, %{}},
-               {{:e, 0}, %{deprecated: "oops", sig: {:infer, _}}}
+               {{:e, 0}, %{deprecated: "oops", sig: {:infer, _, _}}}
              ] = read_chunk(modules[A]).exports
 
       assert read_chunk(modules[B]).exports == [
@@ -119,7 +119,7 @@ defmodule Module.Types.IntegrationTest do
       refute stderr =~ "this_wont_warn"
 
       itself_arg = fn mod ->
-        {_, %{sig: {:infer, [{[value], value}]}}} =
+        {_, %{sig: {:infer, nil, [{[value], value}]}}} =
           List.keyfind(read_chunk(modules[mod]).exports, {:itself, 1}, 0)
 
         value
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 28558fc4ae..66d6f2e2ff 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -42,9 +42,9 @@ defmodule Module.Types.PatternTest do
 
                where "name" was given the type:
 
-                   # type: dynamic()
-                   # from: types_test.ex
-                   {name, arity}
+                   # type: dynamic(atom())
+                   # from: types_test.ex:LINE-1
+                   Atom.to_charlist(name)
                """
     end
 
@@ -103,6 +103,16 @@ defmodule Module.Types.PatternTest do
              ) == uri_type
     end
 
+    test "refines types" do
+      assert typecheck!(
+               [x, foo = :foo, bar = 123],
+               (
+                 {^foo, ^bar} = x
+                 x
+               )
+             ) == dynamic(tuple([atom([:foo]), integer()]))
+    end
+
     test "reports incompatible types" do
       assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""
              the following pattern will never match:
@@ -287,6 +297,16 @@ defmodule Module.Types.PatternTest do
              """
     end
 
+    test "pin inference" do
+      assert typecheck!(
+               [x, y],
+               (
+                 <<^x>> = y
+                 x
+               )
+             ) == dynamic(integer())
+    end
+
     test "size ok" do
       assert typecheck!([<<x, y, _::size(x - y)>>], :ok) == atom([:ok])
     end
@@ -313,5 +333,15 @@ defmodule Module.Types.PatternTest do
                    <<x::float, ...>>
                """
     end
+
+    test "size pin inference" do
+      assert typecheck!(
+               [x, y],
+               (
+                 <<_::size(^x)>> = y
+                 x
+               )
+             ) == dynamic(integer())
+    end
   end
 end
diff --git a/lib/elixir/test/elixir/module/types/type_helper.exs b/lib/elixir/test/elixir/module/types/type_helper.exs
index 4ecd03ef87..33a8a4c0bc 100644
--- a/lib/elixir/test/elixir/module/types/type_helper.exs
+++ b/lib/elixir/test/elixir/module/types/type_helper.exs
@@ -116,12 +116,12 @@ defmodule TypeHelper do
 
   def __typecheck__(mode, patterns, guards, body) do
     stack = new_stack(mode)
-    expected = Enum.map(patterns, fn _ -> Module.Types.Descr.dynamic() end)
+    expected = Enum.map(patterns, fn _ -> Descr.dynamic() end)
 
-    {_types, context} =
+    {_trees, context} =
       Pattern.of_head(patterns, guards, expected, :default, [], stack, new_context())
 
-    Expr.of_expr(body, stack, context)
+    Expr.of_expr(body, Descr.term(), :ok, stack, context)
   end
 
   defp expand_and_unpack(patterns, guards, body, env) do
diff --git a/lib/mix/lib/mix/compilers/elixir.ex b/lib/mix/lib/mix/compilers/elixir.ex
index e663432068..362c50833b 100644
--- a/lib/mix/lib/mix/compilers/elixir.ex
+++ b/lib/mix/lib/mix/compilers/elixir.ex
@@ -1,7 +1,7 @@
 defmodule Mix.Compilers.Elixir do
   @moduledoc false
 
-  @manifest_vsn 27
+  @manifest_vsn 28
   @checkpoint_vsn 2
 
   import Record
diff --git a/lib/mix/lib/mix/tasks/local.hex.ex b/lib/mix/lib/mix/tasks/local.hex.ex
index 2d43db6755..82f4bd4ad3 100644
--- a/lib/mix/lib/mix/tasks/local.hex.ex
+++ b/lib/mix/lib/mix/tasks/local.hex.ex
@@ -37,6 +37,7 @@ defmodule Mix.Tasks.Local.Hex do
   used for fetching Hex, set the `HEX_BUILDS_URL` environment variable.
   """
   @switches [if_missing: :boolean, force: :boolean]
+  @compile {:no_warn_undefined, {Hex, :version, 0}}
 
   @impl true
   def run(argv) do
@@ -46,8 +47,7 @@ defmodule Mix.Tasks.Local.Hex do
     should_install? =
       if Keyword.get(opts, :if_missing, false) do
         if version do
-          not Code.ensure_loaded?(Hex) or
-            Version.compare(apply(Hex, :version, []), version) == :gt
+          not Code.ensure_loaded?(Hex) or Version.compare(Hex.version(), version) == :gt
         else
           not Code.ensure_loaded?(Hex)
         end