diff --git a/lib/elixir/lib/access.ex b/lib/elixir/lib/access.ex
index bacf3bc4e87..0aca88af757 100644
--- a/lib/elixir/lib/access.ex
+++ b/lib/elixir/lib/access.ex
@@ -873,11 +873,6 @@ defmodule Access do
       ...> end)
       {[], [%{name: "john", salary: 10}, %{name: "francine", salary: 30}]}
 
-  An error is raised if the predicate is not a function or is of the incorrect arity:
-
-      iex> get_in([], [Access.filter(5)])
-      ** (FunctionClauseError) no function clause matching in Access.filter/1
-
   An error is raised if the accessed structure is not a list:
 
       iex> get_in(%{}, [Access.filter(fn a -> a == 10 end)])
@@ -1154,11 +1149,6 @@ defmodule Access do
       ...> end)
       {nil, [%{name: "john", salary: 10}, %{name: "francine", salary: 30}]}
 
-  An error is raised if the predicate is not a function or is of the incorrect arity:
-
-      iex> get_in([], [Access.find(5)])
-      ** (FunctionClauseError) no function clause matching in Access.find/1
-
   An error is raised if the accessed structure is not a list:
 
       iex> get_in(%{}, [Access.find(fn a -> a == 10 end)])
diff --git a/lib/elixir/lib/exception.ex b/lib/elixir/lib/exception.ex
index 209980d5e0c..3d2fdc60b40 100644
--- a/lib/elixir/lib/exception.ex
+++ b/lib/elixir/lib/exception.ex
@@ -1930,8 +1930,8 @@ defmodule FunctionClauseError do
 
   For example:
 
-      iex> URI.parse(:wrong_argument)
-      ** (FunctionClauseError) no function clause matching in URI.parse/1
+      iex> List.duplicate(:ok, -3)
+      ** (FunctionClauseError) no function clause matching in List.duplicate/2
 
   The following fields of this exception are public and can be accessed freely:
 
diff --git a/lib/elixir/lib/list.ex b/lib/elixir/lib/list.ex
index e964099fd63..689bc9c002b 100644
--- a/lib/elixir/lib/list.ex
+++ b/lib/elixir/lib/list.ex
@@ -187,9 +187,10 @@ defmodule List do
   """
   @spec duplicate(any, 0) :: []
   @spec duplicate(elem, pos_integer) :: [elem, ...] when elem: var
-  def duplicate(elem, n) do
-    :lists.duplicate(n, elem)
-  end
+  def duplicate(elem, n) when is_integer(n) and n >= 0, do: duplicate(n, elem, [])
+
+  defp duplicate(0, _elem, acc), do: acc
+  defp duplicate(n, elem, acc), do: duplicate(n - 1, elem, [elem | acc])
 
   @doc """
   Flattens the given `list` of nested lists.
diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index e6ed0c2f86e..a2da1223597 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -442,7 +442,9 @@ defmodule Module.Types do
       warnings: [],
       # All vars and their types
       vars: %{},
-      # Variables and arguments from patterns
+      # Variables that are specific to the current environment/conditional
+      conditional_vars: nil,
+      # Track metadata specific to matches and guards
       pattern_info: nil,
       # If type checking has found an error/failure
       failed: false,
diff --git a/lib/elixir/lib/module/types/apply.ex b/lib/elixir/lib/module/types/apply.ex
index cde9e3f0d07..fcfea38ebfc 100644
--- a/lib/elixir/lib/module/types/apply.ex
+++ b/lib/elixir/lib/module/types/apply.ex
@@ -105,8 +105,6 @@ defmodule Module.Types.Apply do
     {[float(), float()], float()}
   ]
 
-  is_clauses = [{[term()], boolean()}]
-
   args_or_arity = union(list(term()), integer())
   args_or_none = union(list(term()), atom([:none]))
   extra_info = kw.(file: list(integer()), line: integer(), error_info: open_map())
@@ -119,6 +117,11 @@ defmodule Module.Types.Apply do
       |> union(tuple([fun(), args_or_arity]))
     )
 
+  not_signature =
+    for bool <- [true, false] do
+      {[atom([bool])], atom([not bool])}
+    end
+
   and_signature =
     for left <- [true, false], right <- [true, false] do
       {[atom([left]), atom([right])], atom([left and right])}
@@ -180,22 +183,8 @@ defmodule Module.Types.Apply do
         {:erlang, :integer_to_binary, [{[integer(), integer()], binary()}]},
         {:erlang, :integer_to_list, [{[integer()], non_empty_list(integer())}]},
         {:erlang, :integer_to_list, [{[integer(), integer()], non_empty_list(integer())}]},
-        {:erlang, :is_atom, is_clauses},
-        {:erlang, :is_binary, is_clauses},
-        {:erlang, :is_bitstring, is_clauses},
-        {:erlang, :is_boolean, is_clauses},
-        {:erlang, :is_float, is_clauses},
-        {:erlang, :is_function, is_clauses},
         {:erlang, :is_function, [{[term(), integer()], boolean()}]},
-        {:erlang, :is_integer, is_clauses},
-        {:erlang, :is_list, is_clauses},
-        {:erlang, :is_map, is_clauses},
         {:erlang, :is_map_key, [{[term(), open_map()], boolean()}]},
-        {:erlang, :is_number, is_clauses},
-        {:erlang, :is_pid, is_clauses},
-        {:erlang, :is_port, is_clauses},
-        {:erlang, :is_reference, is_clauses},
-        {:erlang, :is_tuple, is_clauses},
         {:erlang, :length, [{[list(term())], integer()}]},
         {:erlang, :list_to_atom, [{[list(integer())], atom()}]},
         {:erlang, :list_to_existing_atom, [{[list(integer())], atom()}]},
@@ -206,7 +195,7 @@ defmodule Module.Types.Apply do
         {:erlang, :map_size, [{[open_map()], integer()}]},
         {:erlang, :node, [{[], atom()}]},
         {:erlang, :node, [{[pid() |> union(reference()) |> union(port())], atom()}]},
-        {:erlang, :not, [{[atom([false])], atom([true])}, {[atom([true])], atom([false])}]},
+        {:erlang, :not, not_signature},
         {:erlang, :or, or_signature},
         {:erlang, :raise, [{[atom([:error, :exit, :throw]), term(), raise_stacktrace], none()}]},
         {:erlang, :rem, [{[integer(), integer()], integer()}]},
@@ -216,8 +205,8 @@ defmodule Module.Types.Apply do
         {:erlang, :spawn, [{mfargs, pid()}]},
         {:erlang, :spawn_link, [{[fun(0)], pid()}]},
         {:erlang, :spawn_link, [{mfargs, pid()}]},
-        {:erlang, :spawn_monitor, [{[fun(0)], tuple([reference(), pid()])}]},
-        {:erlang, :spawn_monitor, [{mfargs, tuple([reference(), pid()])}]},
+        {:erlang, :spawn_monitor, [{[fun(0)], tuple([pid(), reference()])}]},
+        {:erlang, :spawn_monitor, [{mfargs, tuple([pid(), reference()])}]},
         {:erlang, :tuple_size, [{[open_tuple([])], integer()}]},
         {:erlang, :trunc, [{[union(integer(), float())], integer()}]},
 
@@ -263,14 +252,14 @@ defmodule Module.Types.Apply do
          [{[term(), open_map()], tuple([atom([:ok]), term()]) |> union(atom([:error]))}]},
         {:maps, :get, [{[term(), open_map()], term()}]},
         {:maps, :is_key, [{[term(), open_map()], boolean()}]},
-        {:maps, :keys, [{[open_map()], dynamic(list(term()))}]},
+        {:maps, :keys, [{[open_map()], list(term())}]},
         {:maps, :put, [{[term(), term(), open_map()], open_map()}]},
         {:maps, :remove, [{[term(), open_map()], open_map()}]},
         {:maps, :take,
          [{[term(), open_map()], tuple([term(), open_map()]) |> union(atom([:error]))}]},
-        {:maps, :to_list, [{[open_map()], dynamic(list(tuple([term(), term()])))}]},
+        {:maps, :to_list, [{[open_map()], list(tuple([term(), term()]))}]},
         {:maps, :update, [{[term(), term(), open_map()], open_map()}]},
-        {:maps, :values, [{[open_map()], dynamic(list(term()))}]}
+        {:maps, :values, [{[open_map()], list(term())}]}
       ] do
     [arity] = Enum.map(clauses, fn {args, _return} -> length(args) end) |> Enum.uniq()
 
@@ -296,6 +285,38 @@ defmodule Module.Types.Apply do
       do: unquote(Macro.escape(domain_clauses))
   end
 
+  is_guards = [
+    is_atom: atom(),
+    is_binary: binary(),
+    is_bitstring: binary(),
+    is_boolean: boolean(),
+    is_float: float(),
+    is_function: fun(),
+    is_integer: integer(),
+    is_list: union(empty_list(), non_empty_list(term(), term())),
+    is_map: open_map(),
+    is_number: union(float(), integer()),
+    is_pid: pid(),
+    is_port: port(),
+    is_reference: reference(),
+    is_tuple: tuple()
+  ]
+
+  for {guard, type} <- is_guards do
+    # is_binary can actually fail for binaries if they are bitstrings
+    return = if guard == :is_binary, do: boolean(), else: atom([true])
+
+    domain_clauses =
+      {:strong, [term()],
+       [
+         {[type], return},
+         {[negation(type)], atom([false])}
+       ]}
+
+    def signature(:erlang, unquote(guard), 1),
+      do: unquote(Macro.escape(domain_clauses))
+  end
+
   def signature(_mod, _fun, _arity), do: :none
 
   @doc """
@@ -320,6 +341,32 @@ defmodule Module.Types.Apply do
     {:none, Enum.map(args, fn _ -> term() end), context}
   end
 
+  def remote_domain(:erlang, :is_function, [_, arity], expected, _meta, _stack, context)
+      when is_integer(arity) and arity >= 0 do
+    type = fun(arity)
+
+    info =
+      {:strong, [term(), integer()],
+       [
+         {[type, integer()], atom([true])},
+         {[negation(type), integer()], atom([false])}
+       ]}
+
+    {info, filter_domain(info, expected, 2), context}
+  end
+
+  def remote_domain(:erlang, :is_map_key, [key, _map], expected, _meta, _stack, context)
+      when is_atom(key) do
+    info =
+      {:strong, [term(), open_map()],
+       [
+         {[term(), open_map([{key, term()}])], atom([true])},
+         {[term(), open_map([{key, not_set()}])], atom([false])}
+       ]}
+
+    {info, filter_domain(info, expected, 2), context}
+  end
+
   def remote_domain(:erlang, :element, [index, _], expected, _meta, _stack, context)
       when is_integer(index) do
     tuple = open_tuple(List.duplicate(term(), max(index - 1, 0)) ++ [expected])
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 4fa5d838748..8e0f1f4c374 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -902,6 +902,24 @@ defmodule Module.Types.Descr do
     :sets.from_list([false], version: 2)
   ]
 
+  @doc """
+  Returns true if the type can never be true.
+  """
+  def never_true?(:term), do: false
+
+  def never_true?(%{} = descr) do
+    descr = Map.get(descr, :dynamic, descr)
+
+    case descr do
+      :term -> false
+      %{atom: {:union, %{true => _}}} -> false
+      %{atom: {:union, _}} -> true
+      %{atom: {:negation, %{true => _}}} -> true
+      %{atom: {:negation, _}} -> false
+      _ -> true
+    end
+  end
+
   @doc """
   Compute the truthiness of an element.
 
@@ -1687,7 +1705,16 @@ defmodule Module.Types.Descr do
   defp pivot([], _acc, _fun), do: :error
 
   # Converts a function BDD (Binary Decision Diagram) to its quoted representation
-  defp fun_to_quoted({:negation, _bdds}, _opts), do: [{:fun, [], []}]
+  defp fun_to_quoted({:negation, bdds}, opts) do
+    case fun_to_quoted({:union, bdds}, opts) do
+      [] ->
+        [{:fun, [], []}]
+
+      parts ->
+        ors = Enum.reduce(parts, &{:or, [], [&2, &1]})
+        [{:and, [], [{:fun, [], []}, {:not, [], [ors]}]}]
+    end
+  end
 
   defp fun_to_quoted({:union, bdds}, opts) do
     for {arity, bdd} <- bdds,
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index 9591dcc7735..9bc032bcd1c 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -459,7 +459,7 @@ 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)
+          Module.Types.Pattern.of_guard(left, {false, type}, expr, stack, context)
 
         :expr ->
           left = annotate_interpolation(left, right)
@@ -511,9 +511,9 @@ defmodule Module.Types.Of do
     compatible_size(actual, expr, stack, context)
   end
 
-  defp specifier_size(_pattern_or_guard, {:size, _, [arg]} = expr, stack, context)
+  defp specifier_size(match_or_guard, {:size, _, [arg]} = expr, stack, context)
        when not is_integer(arg) do
-    {actual, context} = Module.Types.Pattern.of_guard(arg, integer(), expr, stack, context)
+    {actual, context} = Module.Types.Pattern.of_size(match_or_guard, arg, expr, stack, context)
     compatible_size(actual, expr, stack, context)
   end
 
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 0fb8354fd0d..702ad0cc4f0 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -8,8 +8,6 @@ defmodule Module.Types.Pattern do
   alias Module.Types.{Apply, Of}
   import Module.Types.{Helpers, Descr}
 
-  @guard atom([true, false, :fail])
-
   @doc """
   Handles patterns and guards at once.
 
@@ -36,9 +34,8 @@ defmodule Module.Types.Pattern do
 
   def of_head(patterns, guards, expected, tag, meta, stack, context) do
     stack = %{stack | meta: meta}
-
     {trees, context} = of_pattern_args(patterns, expected, tag, stack, context)
-    {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
+    context = of_guards(guards, stack, context)
     {trees, context}
   end
 
@@ -58,9 +55,9 @@ defmodule Module.Types.Pattern do
   end
 
   defp of_pattern_args(patterns, expected, tag, stack, context) do
-    context = init_pattern_info(context)
+    context = init_match_info(context)
     {trees, context} = of_pattern_args_zip(patterns, expected, 0, [], stack, context)
-    {pattern_info, context} = pop_pattern_info(context)
+    {pattern_info, context} = pop_match_info(context)
 
     context =
       case of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context) do
@@ -90,9 +87,9 @@ defmodule Module.Types.Pattern do
   end
 
   def of_match(pattern, expected_fun, expr, stack, context) do
-    context = init_pattern_info(context)
+    context = init_match_info(context)
     {tree, context} = of_pattern(pattern, [%{root: {:arg, 0}, expr: expr}], stack, context)
-    {pattern_info, context} = pop_pattern_info(context)
+    {pattern_info, context} = pop_match_info(context)
     {expected, context} = expected_fun.(of_pattern_tree(tree, context), context)
 
     args = [{tree, expected, expr}]
@@ -114,9 +111,9 @@ defmodule Module.Types.Pattern do
   end
 
   def of_generator(pattern, guards, expected, tag, expr, stack, context) do
-    context = init_pattern_info(context)
+    context = init_match_info(context)
     {tree, context} = of_pattern(pattern, [%{root: {:arg, 0}, expr: expr}], stack, context)
-    {pattern_info, context} = pop_pattern_info(context)
+    {pattern_info, context} = pop_match_info(context)
     args = [{tree, expected, pattern}]
 
     context =
@@ -125,8 +122,7 @@ defmodule Module.Types.Pattern do
         {:error, context} -> context
       end
 
-    {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
-    context
+    of_guards(guards, stack, context)
   end
 
   defp of_pattern_intersect([head | tail], index, acc, pattern_info, tag, stack, context) do
@@ -290,6 +286,19 @@ defmodule Module.Types.Pattern do
     end
   end
 
+  # pattern_info stores the variables defined in patterns,
+  # additional information about the number of variables in
+  # arguments and list heads, and a counter used to compute
+  # the number of list heads.
+  # TODO: Move vars_deps and vars_paths into context.vars.
+  defp init_match_info(context) do
+    %{context | pattern_info: {[], %{}, %{}}}
+  end
+
+  defp pop_match_info(%{pattern_info: pattern_info} = context) do
+    {pattern_info, %{context | pattern_info: nil}}
+  end
+
   defp of_pattern_var([], type, _context) do
     {:ok, type}
   end
@@ -397,8 +406,39 @@ defmodule Module.Types.Pattern do
     {binary(), Of.binary(args, :match, stack, context)}
   end
 
-  def of_match_var(ast, expected, expr, stack, context) do
-    of_guard(ast, expected, expr, stack, context)
+  def of_match_var({:^, _meta, [var]}, expected, expr, stack, context) do
+    Of.refine_body_var(var, expected, expr, stack, context)
+  end
+
+  def of_match_var(atom, _expected, _expr, _stack, context) when is_atom(atom) do
+    {atom(), context}
+  end
+
+  def of_match_var(binary, _expected, _expr, _stack, context) when is_binary(binary) do
+    {binary(), context}
+  end
+
+  def of_match_var(integer, _expected, _expr, _stack, context) when is_integer(integer) do
+    {integer(), context}
+  end
+
+  def of_match_var(float, _expected, _expr, _stack, context) when is_float(float) do
+    {float(), context}
+  end
+
+  @doc """
+  Handle `size` in binary modifiers.
+
+  They behave like guards, so we need to take into account their scope.
+  """
+  def of_size(:match, arg, expr, stack, %{pattern_info: pattern_info} = context) do
+    context = init_guard_info(context)
+    {type, context} = of_guard(arg, {false, integer()}, expr, stack, context)
+    {type, %{context | pattern_info: pattern_info}}
+  end
+
+  def of_size(:guard, arg, expr, stack, context) do
+    of_guard(arg, {false, integer()}, expr, stack, context)
   end
 
   ## Patterns
@@ -704,116 +744,223 @@ defmodule Module.Types.Pattern do
   end
 
   ## Guards
-  # This function is public as it is invoked from Of.binary/4.
+  #
+  # Whenever we have a or/orelse, we need to build multiple environments
+  # and we only preserve intersections of those environments. However,
+  # when building those environments, domain checks are always passed
+  # upstream, except when they are on the right-side of `orelse`.
+  #
+  # Therefore, in addition to `conditional_vars`, we have to track:
+  #
+  # 1. Should we process type checks? We always do so at the root of guards.
+  #    Inside or/orelse, we also need to check the environments.
+  #
+  # 2. Should we process domain checks? We always process it, except that, if
+  #    on the right-side of orelse, it is only kept if it is shared across
+  #    the environment vars.
+
+  @atom_true atom([true])
+
+  defp of_guards([], _stack, context) do
+    context
+  end
+
+  defp of_guards(guards, stack, context) do
+    # TODO: This match? is temporary until we support multiple guards
+    context = init_guard_info(context, match?([_], guards))
+
+    context =
+      Enum.reduce(guards, context, fn guard, context ->
+        {type, context} = of_guard(guard, {true, term()}, guard, stack, context)
+
+        if never_true?(type) do
+          error = {:badguard, type, guard, context}
+          error(__MODULE__, error, error_meta(guard, stack), stack, context)
+        else
+          context
+        end
+      end)
+
+    {_, context} = pop_guard_info(context)
+    context
+  end
+
+  defp init_guard_info(context, check_domain? \\ true) do
+    %{context | pattern_info: {check_domain?}}
+  end
+
+  defp pop_guard_info(%{pattern_info: pattern_info} = context) do
+    {pattern_info, %{context | pattern_info: nil}}
+  end
 
   # :atom
-  def of_guard(atom, _expected, _expr, _stack, context) when is_atom(atom) do
+  def of_guard(atom, _root_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
+  def of_guard(literal, _root_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
+  def of_guard(literal, _root_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
+  def of_guard(literal, _root_expected, _expr, _stack, context) when is_binary(literal) do
     {binary(), context}
   end
 
   # []
-  def of_guard([], _expected, _expr, _stack, context) do
+  def of_guard([], _root_expected, _expr, _stack, context) do
     {empty_list(), context}
   end
 
   # [expr, ...]
-  def of_guard(list, _expected, expr, stack, context) when is_list(list) do
+  def of_guard(list, _root_expected, expr, stack, context) when is_list(list) do
     {prefix, suffix} = unpack_list(list, [])
 
     {prefix, context} =
-      Enum.map_reduce(prefix, context, &of_guard(&1, term(), expr, stack, &2))
+      Enum.map_reduce(prefix, context, &of_guard(&1, {false, term()}, expr, stack, &2))
 
-    {suffix, context} = of_guard(suffix, term(), expr, stack, context)
+    {suffix, context} = of_guard(suffix, {false, term()}, expr, stack, context)
     {non_empty_list(Enum.reduce(prefix, &union/2), suffix), context}
   end
 
   # {left, right}
-  def of_guard({left, right}, expected, expr, stack, context) do
-    of_guard({:{}, [], [left, right]}, expected, expr, stack, context)
+  def of_guard({left, right}, root_expected, expr, stack, context) do
+    of_guard({:{}, [], [left, right]}, root_expected, expr, stack, context)
   end
 
   # %Struct{...}
-  def of_guard({:%, meta, [module, {:%{}, _, args}]} = struct, expected, _expr, stack, context)
+  def of_guard(
+        {:%, meta, [module, {:%{}, _, args}]} = struct,
+        {_root, expected},
+        _expr,
+        stack,
+        context
+      )
       when is_atom(module) do
-    fun = &of_guard(&1, &2, struct, &3, &4)
+    fun = &of_guard(&1, {false, &2}, struct, &3, &4)
     Of.struct_instance(module, args, expected, meta, stack, context, fun)
   end
 
   # %{...}
-  def of_guard({:%{}, _meta, args}, expected, expr, stack, context) do
-    Of.closed_map(args, expected, stack, context, &of_guard(&1, &2, expr, &3, &4))
+  def of_guard({:%{}, _meta, args}, {_root, expected}, expr, stack, context) do
+    Of.closed_map(args, expected, stack, context, &of_guard(&1, {false, &2}, expr, &3, &4))
   end
 
   # <<>>
-  def of_guard({:<<>>, _meta, args}, _expected, _expr, stack, context) do
+  def of_guard({:<<>>, _meta, args}, _root_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
+  def of_guard({:^, _meta, [var]}, {_root, expected}, expr, stack, context) do
     # This is used by binary size, which behaves as a mixture of match and guard
     Of.refine_body_var(var, expected, expr, stack, context)
   end
 
   # {...}
-  def of_guard({:{}, _meta, args}, _expected, expr, stack, context) do
-    {types, context} = Enum.map_reduce(args, context, &of_guard(&1, term(), expr, stack, &2))
+  def of_guard({:{}, _meta, args}, _root_expected, expr, stack, context) do
+    {types, context} =
+      Enum.map_reduce(args, context, &of_guard(&1, {false, term()}, expr, stack, &2))
+
     {tuple(types), context}
   end
 
   # var.field
-  def of_guard({{:., _, [callee, key]}, _, []} = map_fetch, _expected, expr, stack, context)
+  def of_guard(
+        {{:., _, [callee, key]}, _, []} = map_fetch,
+        {_root, expected},
+        expr,
+        stack,
+        context
+      )
       when not is_atom(callee) do
-    {type, context} = of_guard(callee, term(), expr, stack, context)
+    {type, context} = of_guard(callee, {false, open_map([{key, expected}])}, expr, stack, context)
     Of.map_fetch(map_fetch, type, key, stack, context)
   end
 
   # Remote
-  def of_guard({{:., _, [:erlang, fun]}, meta, args} = call, expected, _expr, stack, context)
+  def of_guard({{:., _, [:erlang, fun]}, meta, args} = call, root_expected, _, stack, context)
       when is_atom(fun) do
+    of_remote(fun, meta, args, call, root_expected, stack, context)
+  end
+
+  # var
+  def of_guard(var, {_root, expected}, expr, stack, context) when is_var(var) do
+    case context.pattern_info do
+      {true} -> Of.refine_body_var(var, expected, expr, stack, context)
+      {false} -> {Of.var(var, context), context}
+    end
+  end
+
+  # TODO: Move orelse and andalso handling here
+  defp of_remote(fun, meta, [left, right], call, {_root, expected}, stack, context)
+       when fun in [:or, :orelse] do
+    {info, [left_domain, right_domain], context} =
+      Apply.remote_domain(:erlang, fun, [left, right], expected, meta, stack, context)
+
+    {left_type, context} = of_guard(left, {false, left_domain}, call, stack, context)
+
+    {right_type, context} =
+      if fun == :or do
+        of_guard(right, {false, right_domain}, call, stack, context)
+      else
+        %{pattern_info: pattern_info} = context
+        context = %{context | pattern_info: {false}}
+        {type, context} = of_guard(right, {false, right_domain}, call, stack, context)
+        {type, %{context | pattern_info: pattern_info}}
+      end
+
+    args_types = [left_type, right_type]
+    Apply.remote_apply(info, :erlang, fun, args_types, call, stack, context)
+  end
+
+  defp of_remote(fun, meta, args, call, {root, expected}, stack, context) do
+    # If we are the root, we are only interested in positive results,
+    # except for the operations that can return :fail.
+    expected =
+      if root and fun not in [:element, :hd, :map_get, :max, :min, :tl] do
+        @atom_true
+      else
+        expected
+      end
+
     {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))
+      zip_map_reduce(args, domain, context, &of_guard(&1, {false, &2}, call, stack, &3))
 
     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.var(var, context), context}
-  end
-
   ## Helpers
 
-  # pattern_info stores the variables defined in patterns,
-  # additional information about the number of variables in
-  # arguments and list heads, and a counter used to compute
-  # the number of list heads.
-  # TODO: Consider moving pattern_info into context.vars.
-  defp init_pattern_info(context) do
-    %{context | pattern_info: {[], %{}, %{}}}
-  end
+  def format_diagnostic({:badguard, type, expr, context}) do
+    traces = collect_traces(expr, context)
 
-  defp pop_pattern_info(%{pattern_info: pattern_info} = context) do
-    {pattern_info, %{context | pattern_info: nil}}
+    %{
+      details: %{typing_traces: traces},
+      message:
+        IO.iodata_to_binary([
+          """
+          this guard will never succeed:
+
+              #{expr_to_string(expr) |> indent(4)}
+
+          because it returns type:
+
+              #{to_quoted_string(type) |> indent(4)}
+          """,
+          format_traces(traces)
+        ])
+    }
   end
 
   def format_diagnostic({:badmatch, expr, context}) do
diff --git a/lib/elixir/pages/cheatsheets/types-cheat.cheatmd b/lib/elixir/pages/cheatsheets/types-cheat.cheatmd
index 0b60cd1808b..93bbd776c42 100644
--- a/lib/elixir/pages/cheatsheets/types-cheat.cheatmd
+++ b/lib/elixir/pages/cheatsheets/types-cheat.cheatmd
@@ -173,12 +173,17 @@ tuple()
 
 ## Additional types for convenience
 
-#### Booleans
+#### Aliases
 
 ```elixir
+bitstring() = binary()
 boolean() = true or false
+number() = integer() or float()
 ```
 
+The type system currently does not distinguish between
+binaries and bitstrings.
+
 #### Lists
 
 ```elixir
diff --git a/lib/elixir/pages/references/gradual-set-theoretic-types.md b/lib/elixir/pages/references/gradual-set-theoretic-types.md
index 812d3b72352..745504764af 100644
--- a/lib/elixir/pages/references/gradual-set-theoretic-types.md
+++ b/lib/elixir/pages/references/gradual-set-theoretic-types.md
@@ -9,7 +9,7 @@ Elixir is in the process of incorporating set-theoretic types into the compiler.
 
   * **sound** - the inferred and assigned by the type system align with the behaviour of the program
 
-  * **gradual** - Elixir's type system includes the `dynamic()` type, which can be used when the type of a variable or expression is checked at runtime. In the absence of `dynamic()`, Elixir's type system behaves as a static one
+  * **gradual** - Elixir's type system includes the `dynamic()` type, which can be used when the type of a variable or expression is checked at runtime. However, instead of simply discarding all typing information, Elixir's `dynamic()` type works as a range. For example, if you write `dynamic(integer() or binary())`, Elixir's type system will still emit violations if none of those types are accepted. Furthermore, in the absence of `dynamic()`, Elixir's type system behaves as a static one
 
   * **developer friendly** - the types are described, implemented, and composed using basic set operations: unions, intersections, and negation (hence it is a set-theoretic type system)
 
@@ -92,13 +92,37 @@ If you pass a list type as the tail, then the list type is merged into the eleme
 
 You can represent all maps as `map()`.
 
-Maps may also be written using their literal syntax, such as `%{name: binary(), age: integer()}`, which outlines a map with exactly two keys, `:name` and `:age`, and values of type `binary()` and `integer()` respectively.
+Maps may also be written using their literal syntax:
 
-A key may be marked as optional using the `if_set/1` operation on its value type. For example, `%{name: binary(), age: if_set(integer())}` is a map that certainly has the `:name` key but it may have the `:age` key (and if it has such key, its value type is `integer()`).
+```elixir
+%{name: binary(), age: integer()}
+```
+
+which outlines a map with exactly two keys, `:name` and `:age`, and values of type `binary()` and `integer()` respectively. We say the map above is "closed": it only supports the keys explicitly defined. We can also mark a map as "open", by including `...` as its first element:
+
+```elixir
+%{..., name: binary(), age: integer()}
+```
+
+The type above says the keys `:name` and `:age` must exist, with their respective types, but other keys may be present. The `map()` type is the same as `%{...}`. For the empty map, you may write `%{}`, although we recommend using `empty_map()` for clarity.
+
+#### Optional keys
 
-We say the maps above are "closed": they only support the keys explicitly defined. We can also mark a map as "open", by including `...` as its first element.
+A key may be marked as optional using the `if_set/1` operation on its value type:
+
+```elixir
+%{name: binary(), age: if_set(integer())}
+```
+
+is a map that certainly has the `:name` key but it may have the `:age` key (and if it has such key, its value type is `integer()`).
+
+You can also use `not_set()` to denote a key cannot be present:
+
+```elixir
+%{..., age: not_set()}
+```
 
-For example, the type `%{..., name: binary(), age: integer()}` means the keys `:name` and `:age` must exist, with their respective types, but any other key may also be present. In other words, `map()` is the same as `%{...}`. For the empty map, you may write `%{}`, although we recommend using `empty_map()` for clarity.
+The type above says the map may have any key, except the `:age` one. This is, for instance, the type returned by `Map.delete(map, :age)`.
 
 #### Domain types
 
@@ -190,7 +214,7 @@ If the user provides their own types, and those types are not `dynamic()`, then
 
 ## Type inference
 
-Type inference (or reconstruction) is the ability of a type system automatically deduce, either partially or fully, the type of an expression at compile time. Type inference may occur at different levels. For example, many programming languages can automatically infer the types of variables, also known "local type inference", but not all can infer type signatures of functions.
+Type inference (or reconstruction) is the ability of a type system to automatically deduce, either partially or fully, the type of an expression at compile time. Type inference may occur at different levels. For example, many programming languages can automatically infer the types of variables, also known "local type inference", but not all can infer type signatures of functions.
 
 Inferring type signatures comes with a series of trade-offs:
 
@@ -202,7 +226,7 @@ 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 aims to provide "module type inference": our goal is to infer the types of functions considering the current module, Elixir's standard library and your dependencies (in the future). Calls to modules within the same project are assumed to be `dynamic()` as to reduce cyclic dependencies and the need for recompilations. Once types are inferred, then the whole project is type checked considering all modules and all types (inferred or otherwise).
+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 aims to provide "module type inference": our goal is to infer the types of functions considering the current module, Elixir's standard library and your dependencies, while calls to modules within the same project are assumed to be `dynamic()`. Once types are inferred, then the whole project is type checked considering all modules and all types (inferred or otherwise).
 
 Type inference in Elixir is best-effort: it doesn't guarantee it will find all possible type incompatibilities, only that it may find bugs where all combinations of a type _will_ fail, even in the absence of explicit type annotations. It is meant to be an efficient routine that brings developers some benefits of static typing without requiring any effort from them.
 
diff --git a/lib/elixir/test/elixir/inspect/algebra_test.exs b/lib/elixir/test/elixir/inspect/algebra_test.exs
index f9ca94b3dc8..9b3a3f7042a 100644
--- a/lib/elixir/test/elixir/inspect/algebra_test.exs
+++ b/lib/elixir/test/elixir/inspect/algebra_test.exs
@@ -50,10 +50,7 @@ defmodule Inspect.AlgebraTest do
     # Consistent with definitions
     assert break("break") == {:doc_break, "break", :strict}
     assert break("") == {:doc_break, "", :strict}
-
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> break(42) end
-
+    Fun
     # Consistent formatting
     assert render(break("_"), 80) == "_"
     assert render(glue("foo", " ", glue("bar", " ", "baz")), 10) == "foo\nbar\nbaz"
@@ -64,9 +61,6 @@ defmodule Inspect.AlgebraTest do
     assert flex_break("break") == {:doc_break, "break", :flex}
     assert flex_break("") == {:doc_break, "", :flex}
 
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> flex_break(42) end
-
     # Consistent formatting
     assert render(flex_break("_"), 80) == "_"
     assert render(flex_glue("foo", " ", flex_glue("bar", " ", "baz")), 10) == "foo bar\nbaz"
@@ -76,9 +70,6 @@ defmodule Inspect.AlgebraTest do
     # Consistent with definitions
     assert glue("a", "->", "b") == ["a", {:doc_break, "->", :strict} | "b"]
     assert glue("a", "b") == glue("a", " ", "b")
-
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> glue("a", 42, "b") end
   end
 
   test "flex glue doc" do
@@ -87,9 +78,6 @@ defmodule Inspect.AlgebraTest do
              ["a", {:doc_break, "->", :flex} | "b"]
 
     assert flex_glue("a", "b") == flex_glue("a", " ", "b")
-
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> flex_glue("a", 42, "b") end
   end
 
   test "binary doc" do
@@ -115,9 +103,6 @@ defmodule Inspect.AlgebraTest do
     assert nest(empty(), 1) == {:doc_nest, empty(), 1, :always}
     assert nest(empty(), 0) == []
 
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> nest("foo", empty()) end
-
     # Consistent formatting
     assert render(nest("a", 1), 80) == "a"
     assert render(nest(glue("a", "b"), 1), 2) == "a\n b"
@@ -129,9 +114,6 @@ defmodule Inspect.AlgebraTest do
     assert nest(empty(), 1, :break) == {:doc_nest, empty(), 1, :break}
     assert nest(empty(), 0, :break) == []
 
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> nest("foo", empty(), :break) end
-
     # Consistent formatting
     assert render(nest("a", 1, :break), 80) == "a"
     assert render(nest(glue("a", "b"), 1, :break), 2) == "a\n b"
@@ -231,10 +213,6 @@ defmodule Inspect.AlgebraTest do
     # Consistent with definitions
     assert collapse_lines(3) == {:doc_collapse, 3}
 
-    # Wrong argument type
-    assert_raise FunctionClauseError, fn -> collapse_lines(0) end
-    assert_raise FunctionClauseError, fn -> collapse_lines(empty()) end
-
     # Consistent formatting
     doc = concat([collapse_lines(2), line(), line(), line()])
     assert render(doc, 10) == "\n\n"
diff --git a/lib/elixir/test/elixir/list_test.exs b/lib/elixir/test/elixir/list_test.exs
index 2d1c283810d..373df343dc9 100644
--- a/lib/elixir/test/elixir/list_test.exs
+++ b/lib/elixir/test/elixir/list_test.exs
@@ -386,10 +386,6 @@ defmodule ListTest do
     refute List.improper?([[1]])
     refute List.improper?([1, 2])
     refute List.improper?([1, 2, 3])
-
-    assert_raise FunctionClauseError, fn ->
-      List.improper?(%{})
-    end
   end
 
   describe "ascii_printable?/2" do
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 330d214e51d..31a0f70899c 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -14,7 +14,7 @@ end
 defmodule Module.Types.DescrTest do
   use ExUnit.Case, async: true
 
-  import Module.Types.Descr, except: [fun: 1]
+  import Module.Types.Descr
   defmacro domain_key(arg) when is_atom(arg), do: [arg]
 
   defp number(), do: union(integer(), float())
@@ -1225,6 +1225,24 @@ defmodule Module.Types.DescrTest do
   end
 
   describe "projections" do
+    test "never_true?" do
+      for type <- [
+            none(),
+            integer(),
+            atom([false]),
+            atom([:other, false]),
+            negation(atom([true]))
+          ] do
+        assert never_true?(type)
+        assert never_true?(dynamic(type))
+      end
+
+      for type <- [atom([true]), boolean(), atom(), term(), negation(atom([false]))] do
+        refute never_true?(type)
+        refute never_true?(dynamic(type))
+      end
+    end
+
     test "truthiness" do
       for type <- [term(), none(), atom(), boolean(), union(atom([false]), integer())] do
         assert truthiness(type) == :undefined
@@ -2710,6 +2728,13 @@ defmodule Module.Types.DescrTest do
              |> union(fun([pid()], pid()))
              |> to_quoted_string() ==
                "(integer() -> integer()) or (float() -> float()) or (pid() -> pid())"
+
+      assert fun(3) |> to_quoted_string() == "(none(), none(), none() -> term())"
+
+      assert intersection(fun(), negation(fun())) |> to_quoted_string() == "none()"
+
+      assert intersection(fun(), negation(fun(3))) |> to_quoted_string() ==
+               "fun() and not (none(), none(), none() -> term())"
     end
 
     test "function with optimized intersections" do
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 34fb45b09ff..5570f10b79c 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -182,25 +182,6 @@ defmodule Module.Types.PatternTest do
                    m = 123
                """
     end
-
-    test "fields in guards" do
-      assert typeerror!([x = %Point{}], x.foo_bar, :ok) ==
-               ~l"""
-               unknown key .foo_bar in expression:
-
-                   x.foo_bar
-
-               the given type does not have the given key:
-
-                   dynamic(%Point{x: term(), y: term(), z: term()})
-
-               where "x" was given the type:
-
-                   # type: dynamic(%Point{})
-                   # from: types_test.ex:LINE-1
-                   x = %Point{}
-               """
-    end
   end
 
   describe "maps" do
@@ -241,10 +222,6 @@ defmodule Module.Types.PatternTest do
                )
     end
 
-    test "atom keys in guards" do
-      assert typecheck!([x = %{foo: :bar}], x.bar, x) == dynamic(open_map(foo: atom([:bar])))
-    end
-
     test "domain keys in patterns" do
       assert typecheck!([x = %{123 => 456}], x) == dynamic(open_map())
       assert typecheck!([x = %{123 => 456, foo: :bar}], x) == dynamic(open_map(foo: atom([:bar])))
@@ -410,4 +387,110 @@ defmodule Module.Types.PatternTest do
              ) == dynamic(integer())
     end
   end
+
+  describe "guards" do
+    test "not" do
+      assert typecheck!([x], not x, x) == dynamic(atom([false]))
+
+      assert typecheck!([x], not x.foo, x) == dynamic(open_map(foo: atom([false])))
+
+      assert typeerror!([x], not length(x), x) |> strip_ansi() == ~l"""
+             incompatible types given to Kernel.not/1:
+
+                 not length(x)
+
+             given types:
+
+                 integer()
+
+             but expected one of:
+
+                 #1
+                 true
+
+                 #2
+                 false
+
+             where "x" was given the type:
+
+                 # type: dynamic()
+                 # from: types_test.ex:LINE
+                 x
+             """
+    end
+
+    test "is_function/2" do
+      assert typecheck!([x], is_function(x, 3), x) == dynamic(fun(3))
+      assert typecheck!([x], not is_function(x, 3), x) == dynamic(negation(fun(3)))
+    end
+
+    test "is_map_key/2" do
+      assert typecheck!([x], is_map_key(x, :foo), x) == dynamic(open_map(foo: term()))
+      assert typecheck!([x], not is_map_key(x, :foo), x) == dynamic(open_map(foo: not_set()))
+    end
+
+    test "elem" do
+      assert typecheck!([x], elem(x, 1), x) ==
+               dynamic(open_tuple([term(), term()]))
+
+      assert typecheck!([x], not elem(x, 1), x) ==
+               dynamic(open_tuple([term(), atom([false])]))
+
+      assert typecheck!([x], is_integer(elem(x, 1)), x) ==
+               dynamic(open_tuple([term(), integer()]))
+    end
+
+    test "map.field" do
+      assert typecheck!([x = %{foo: :bar}], x.bar, x) ==
+               dynamic(open_map(foo: atom([:bar]), bar: term()))
+
+      assert typecheck!([x = %{foo: :bar}], not x.bar, x) ==
+               dynamic(open_map(foo: atom([:bar]), bar: atom([false])))
+
+      assert typeerror!([x = %Point{}], x.foo_bar, :ok) ==
+               ~l"""
+               unknown key .foo_bar in expression:
+
+                   x.foo_bar
+
+               the given type does not have the given key:
+
+                   dynamic(%Point{x: term(), y: term(), z: term()})
+
+               where "x" was given the type:
+
+                   # type: dynamic(%Point{})
+                   # from: types_test.ex:LINE-1
+                   x = %Point{}
+               """
+    end
+
+    test "domain checks propagate across all operations except 'orelse'" do
+      assert typecheck!([x], length(x) == 3, x) == dynamic(list(term()))
+
+      assert typecheck!([x, y], :erlang.or(length(x) == 3, map_size(y) == 1), {x, y}) ==
+               dynamic(tuple([list(term()), open_map()]))
+
+      assert typecheck!([x, y], length(x) == 3 or map_size(y) == 1, {x, y}) ==
+               dynamic(tuple([list(term()), term()]))
+    end
+
+    test "errors in guards" do
+      assert typeerror!([x = {}], is_integer(x), x) == ~l"""
+             this guard will never succeed:
+
+                 is_integer(x)
+
+             because it returns type:
+
+                 false
+
+             where "x" was given the type:
+
+                 # type: dynamic({})
+                 # from: types_test.ex:479
+                 x = {}
+             """
+    end
+  end
 end
diff --git a/lib/elixir/test/elixir/string_test.exs b/lib/elixir/test/elixir/string_test.exs
index 278d753b3e8..cbd1dc18ded 100644
--- a/lib/elixir/test/elixir/string_test.exs
+++ b/lib/elixir/test/elixir/string_test.exs
@@ -418,14 +418,6 @@ defmodule StringTest do
     assert String.pad_leading("---", 5, ["abc"]) == "abcabc---"
     assert String.pad_leading("--", 6, ["a", "bc"]) == "abcabc--"
 
-    assert_raise FunctionClauseError, fn ->
-      String.pad_leading("-", -1)
-    end
-
-    assert_raise FunctionClauseError, fn ->
-      String.pad_leading("-", 1, [])
-    end
-
     message = "expected a string padding element, got: 10"
 
     assert_raise ArgumentError, message, fn ->
@@ -447,14 +439,6 @@ defmodule StringTest do
     assert String.pad_trailing("---", 5, ["abc"]) == "---abcabc"
     assert String.pad_trailing("--", 6, ["a", "bc"]) == "--abcabc"
 
-    assert_raise FunctionClauseError, fn ->
-      String.pad_trailing("-", -1)
-    end
-
-    assert_raise FunctionClauseError, fn ->
-      String.pad_trailing("-", 1, [])
-    end
-
     message = "expected a string padding element, got: 10"
 
     assert_raise ArgumentError, message, fn ->
@@ -720,14 +704,6 @@ defmodule StringTest do
     assert String.at("л", -3) == nil
     assert String.at("Ā̀stute", 1) == "s"
     assert String.at("elixir", 6) == nil
-
-    assert_raise FunctionClauseError, fn ->
-      String.at("elixir", 0.1)
-    end
-
-    assert_raise FunctionClauseError, fn ->
-      String.at("elixir", -0.1)
-    end
   end
 
   test "slice/3" do
@@ -781,10 +757,6 @@ defmodule StringTest do
     assert String.slice("abc", -1..14) == "c"
     assert String.slice("a·̀ͯ‿.⁀:", 0..-2//1) == "a·̀ͯ‿.⁀"
 
-    assert_raise FunctionClauseError, fn ->
-      String.slice(nil, 0..1)
-    end
-
     assert ExUnit.CaptureIO.capture_io(:stderr, fn ->
              assert String.slice("elixir", 0..-2//-1) == "elixi"
            end) =~ "negative steps are not supported in String.slice/2, pass 0..-2//1 instead"
diff --git a/lib/ex_unit/lib/ex_unit/assertions.ex b/lib/ex_unit/lib/ex_unit/assertions.ex
index c55a5db4e62..ed746ec0ce7 100644
--- a/lib/ex_unit/lib/ex_unit/assertions.ex
+++ b/lib/ex_unit/lib/ex_unit/assertions.ex
@@ -1119,6 +1119,6 @@ defmodule ExUnit.Assertions do
   @spec flunk :: no_return
   @spec flunk(String.t()) :: no_return
   def flunk(message \\ "Flunked!") when is_binary(message) do
-    assert false, message: message
+    raise ExUnit.AssertionError, message
   end
 end