diff --git a/lib/elixir/lib/calendar/date_range.ex b/lib/elixir/lib/calendar/date_range.ex
index 5e8c652b781..9914c143870 100644
--- a/lib/elixir/lib/calendar/date_range.ex
+++ b/lib/elixir/lib/calendar/date_range.ex
@@ -59,11 +59,20 @@ defmodule Date.Range do
     end
 
     # TODO: Remove me on v2.0
-    def member?(
-          %{__struct__: Date.Range, first_in_iso_days: first_days, last_in_iso_days: last_days} =
-            date_range,
-          date
-        ) do
+    member? =
+      quote generated: true do
+        member?(
+          %{
+            __struct__: Date.Range,
+            first_in_iso_days: var!(first_days),
+            last_in_iso_days: var!(last_days)
+          } =
+            var!(date_range),
+          var!(date)
+        )
+      end
+
+    def unquote(member?) do
       step = if first_days <= last_days, do: 1, else: -1
       member?(Map.put(date_range, :step, step), date)
     end
@@ -218,11 +227,11 @@ defmodule Date.Range do
   defimpl Inspect do
     import Kernel, except: [inspect: 2]
 
-    def inspect(%Date.Range{first: first, last: last, step: 1}, _) do
+    def inspect(%Date.Range{first: first, last: last, step: 1}, %Inspect.Opts{}) do
       "Date.range(" <> inspect(first) <> ", " <> inspect(last) <> ")"
     end
 
-    def inspect(%Date.Range{first: first, last: last, step: step}, _) do
+    def inspect(%Date.Range{first: first, last: last, step: step}, %Inspect.Opts{}) do
       "Date.range(" <> inspect(first) <> ", " <> inspect(last) <> ", #{step})"
     end
 
diff --git a/lib/elixir/lib/enum.ex b/lib/elixir/lib/enum.ex
index 37d8b5ec707..0261b754bf1 100644
--- a/lib/elixir/lib/enum.ex
+++ b/lib/elixir/lib/enum.ex
@@ -5168,7 +5168,16 @@ defimpl Enumerable, for: Range do
   end
 
   # TODO: Remove me on v2.0
-  def reduce(%{__struct__: Range, first: first, last: last} = range, acc, fun) do
+  reduce =
+    quote generated: true do
+      reduce(
+        %{__struct__: Range, first: var!(first), last: var!(last)} = var!(range),
+        var!(acc),
+        var!(fun)
+      )
+    end
+
+  def unquote(reduce) do
     step = if first <= last, do: 1, else: -1
     reduce(Map.put(range, :step, step), acc, fun)
   end
@@ -5191,12 +5200,12 @@ defimpl Enumerable, for: Range do
     {:done, acc}
   end
 
-  def member?(first..last//step, value) when is_integer(value) do
-    if step > 0 do
-      {:ok, first <= value and value <= last and rem(value - first, step) == 0}
-    else
-      {:ok, last <= value and value <= first and rem(value - first, step) == 0}
-    end
+  def member?(first..last//step, value) when is_integer(value) and step > 0 do
+    {:ok, first <= value and value <= last and rem(value - first, step) == 0}
+  end
+
+  def member?(first..last//step, value) when is_integer(value) and step < 0 do
+    {:ok, last <= value and value <= first and rem(value - first, step) == 0}
   end
 
   # TODO: Remove me on v2.0
@@ -5219,7 +5228,13 @@ defimpl Enumerable, for: Range do
   end
 
   # TODO: Remove me on v2.0
-  def slice(%{__struct__: Range, first: first, last: last} = range) do
+
+  slice =
+    quote generated: true do
+      slice(%{__struct__: Range, first: var!(first), last: var!(last)} = var!(range))
+    end
+
+  def unquote(slice) do
     step = if first <= last, do: 1, else: -1
     slice(Map.put(range, :step, step))
   end
diff --git a/lib/elixir/lib/inspect.ex b/lib/elixir/lib/inspect.ex
index 169ddfac73a..a4d8e8143ab 100644
--- a/lib/elixir/lib/inspect.ex
+++ b/lib/elixir/lib/inspect.ex
@@ -696,7 +696,15 @@ defimpl Inspect, for: Range do
   end
 
   # TODO: Remove me on v2.0
-  def inspect(%{__struct__: Range, first: first, last: last} = range, opts) do
+  inspect =
+    quote generated: true do
+      inspect(
+        %{__struct__: Range, first: var!(first), last: var!(last)} = var!(range),
+        var!(opts)
+      )
+    end
+
+  def unquote(inspect) do
     step = if first <= last, do: 1, else: -1
     inspect(Map.put(range, :step, step), opts)
   end
diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index 6432dffce9d..01868ee2e61 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -319,16 +319,17 @@ defmodule Module.Types do
   defp local_handler(mode, fun_arity, kind, meta, clauses, expected, stack, context) do
     {fun, _arity} = fun_arity
     stack = stack |> fresh_stack(mode, fun_arity) |> with_file_meta(meta)
+    base_info = {:def, kind, fun, expected}
 
-    {_, _, mapping, clauses_types, clauses_context} =
-      Enum.reduce(clauses, {0, 0, [], [], context}, fn
-        {meta, args, guards, body}, {index, total, mapping, inferred, context} ->
-          context = fresh_context(context)
-          info = {:def, kind, fun, args, guards, expected}
+    {_, _, _, mapping, clauses_types, clauses_context} =
+      Enum.reduce(clauses, {0, 0, [], [], [], context}, fn
+        {meta, args, guards, body}, {index, total, previous, mapping, inferred, acc_context} ->
+          fresh_context = fresh_context(acc_context)
+          info = {base_info, args, guards}
 
           try do
-            {trees, _precise?, context} =
-              Pattern.of_head(args, guards, expected, info, meta, stack, context)
+            {trees, previous, context} =
+              Pattern.of_head(args, guards, expected, previous, info, meta, stack, fresh_context)
 
             {return_type, context} =
               Expr.of_expr(body, Descr.term(), body, stack, context)
@@ -339,9 +340,9 @@ defmodule Module.Types do
               add_inferred(inferred, args_types, return_type, total - 1, [])
 
             if type_index == -1 do
-              {index + 1, total + 1, [{index, total} | mapping], inferred, context}
+              {index + 1, total + 1, previous, [{index, total} | mapping], inferred, context}
             else
-              {index + 1, total, [{index, type_index} | mapping], inferred, context}
+              {index + 1, total, previous, [{index, type_index} | mapping], inferred, context}
             end
           rescue
             e ->
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index eed1d499658..5c4aed44bc1 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -719,62 +719,24 @@ 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, domain, expected, clause_info, stack, context, acc) do
+  defp of_clauses(clauses, domain, expected, base_info, stack, context, acc) do
     fun = fn _args_types, result, _context, acc -> union(result, acc) end
-    of_clauses_fun(clauses, domain, expected, clause_info, stack, context, acc, fun)
+    of_clauses_fun(clauses, domain, expected, base_info, stack, context, acc, fun)
   end
 
-  defp of_clauses_fun(clauses, domain, expected, clause_info, stack, original, acc, fun) do
+  defp of_clauses_fun(clauses, domain, expected, base_info, stack, original, acc, fun) do
     %{failed: failed?} = original
 
     {result, _previous, context} =
       Enum.reduce(clauses, {acc, [], original}, fn
-        {:->, meta, [head, body]} = clause, {acc, previous, context} ->
+        {:->, meta, [head, body]}, {acc, previous, context} ->
           {failed?, context} = reset_failed(context, failed?)
           {patterns, guards} = extract_head(head)
-          info = {clause_info, head, previous}
+          info = {base_info, head}
 
-          {trees, precise?, context} =
+          {trees, previous, context} =
             Pattern.of_head(patterns, guards, domain, previous, info, meta, stack, context)
 
-          # It failed, let's try to detect if it was due a previous or current clause.
-          # The current clause will be easier to understand, so we prefer that
-          {trees, precise?, context} =
-            if context.failed and previous != [] do
-              info = {clause_info, head, []}
-
-              case Pattern.of_head(patterns, guards, domain, info, meta, stack, context) do
-                {_, _, %{failed: true}} = result -> result
-                _ -> {trees, precise?, context}
-              end
-            else
-              {trees, precise?, context}
-            end
-
-          {previous, context} =
-            if context.failed do
-              {previous, context}
-            else
-              args_types =
-                Enum.map(trees, fn {tree, _, _} ->
-                  tree
-                  |> Pattern.of_pattern_tree(stack, context)
-                  |> upper_bound()
-                end)
-
-              cond do
-                stack.mode != :infer and previous != [] and
-                    Pattern.args_subtype?(args_types, previous) ->
-                  {previous, Pattern.redundant_warn(clause, previous, stack, context)}
-
-                precise? ->
-                  {[args_types | previous], context}
-
-                true ->
-                  {previous, context}
-              end
-            end
-
           {result, context} = of_expr(body, expected, body, stack, context)
 
           {fun.(trees, result, context, acc), previous,
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index aa9c64f0c28..ba795ee20f1 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -187,6 +187,13 @@ defmodule Module.Types.Of do
       }),
       do: %{context | subpatterns: subpatterns, vars: vars, conditional_vars: conditional_vars}
 
+  @doc """
+  Returns true if all entries have the same conditional vars.
+  """
+  def all_same_conditional_vars?([{_, cond} | tail]) do
+    Enum.all?(tail, fn {_, tail_cond} -> cond == tail_cond end)
+  end
+
   @doc """
   Executes the args with acc using conditional variables.
   """
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index 750b7ad9fb6..826521ec729 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -8,22 +8,6 @@ defmodule Module.Types.Pattern do
   alias Module.Types.{Apply, Of}
   import Module.Types.{Helpers, Descr}
 
-  @doc """
-  Defines if two list of arguments are subtypes of each other.
-  """
-  def args_subtype?([], []),
-    do: true
-
-  def args_subtype?([type], previous),
-    do: subtype?(type, Enum.reduce(previous, none(), &union(&2, hd(&1))))
-
-  def args_subtype?(args, previous) do
-    subtype?(
-      args_to_domain(args),
-      Enum.reduce(previous, none(), &union(&2, args_to_domain(&1)))
-    )
-  end
-
   @doc """
   Refine the dependencies of variables represented by version.
   """
@@ -142,11 +126,62 @@ defmodule Module.Types.Pattern do
 
   4. Then we propagate all dependencies to refine variables
 
+  Every step we deduct previous clauses from the current ones and,
+  in case of failures, we try to break down the root cause.
   """
-  def of_head(patterns, guards, expected, previous \\ [], tag, meta, stack, context) do
-    %{vars: vars} = context
+  def of_head(patterns, guards, expected, previous, tag, meta, stack, original_context) do
     stack = %{stack | meta: meta}
 
+    {trees, precise?, context} =
+      of_precise_head(patterns, guards, expected, previous, tag, stack, original_context)
+
+    if context.failed and previous != [] and Keyword.get(meta, :generated, false) != true do
+      # If it failed, let's try to break it down to a better error message.
+      # First we check if it fails without previous, if it doesn't, check if it is redundant.
+      case of_precise_head(patterns, guards, expected, [], tag, stack, original_context) do
+        {other_trees, _, %{failed: true} = other_context} ->
+          {other_trees, previous, other_context}
+
+        {other_trees, _, other_context} ->
+          args_types =
+            Enum.map(other_trees, fn {tree, _, _} ->
+              tree
+              |> of_pattern_tree(stack, other_context)
+              |> upper_bound()
+            end)
+
+          if args_subtype?(args_types, previous) do
+            warning = {:redundant, tag, expected, args_types, previous, other_context}
+            {other_trees, previous, warn(__MODULE__, warning, meta, stack, other_context)}
+          else
+            {trees, previous, context}
+          end
+      end
+    else
+      args_types =
+        Enum.map(trees, fn {tree, _, _} ->
+          tree
+          |> of_pattern_tree(stack, context)
+          |> upper_bound()
+        end)
+
+      cond do
+        args_subtype?(args_types, previous) ->
+          warning = {:redundant, tag, expected, args_types, previous, context}
+          {trees, previous, warn(__MODULE__, warning, meta, stack, context)}
+
+        precise? ->
+          {trees, [args_types | previous], context}
+
+        true ->
+          {trees, previous, context}
+      end
+    end
+  end
+
+  defp of_precise_head(patterns, guards, expected, previous, tag, stack, context) do
+    %{vars: vars} = context
+
     case of_pattern_args(patterns, expected, previous, tag, stack, context) do
       {trees, pattern_precise?, changed, context} ->
         {guard_precise?, context} = of_guards(guards, changed, vars, stack, context)
@@ -157,6 +192,22 @@ defmodule Module.Types.Pattern do
     end
   end
 
+  defp args_subtype?(_, []),
+    do: false
+
+  defp args_subtype?([], _),
+    do: true
+
+  defp args_subtype?([type], previous),
+    do: subtype?(type, Enum.reduce(previous, none(), &union(&2, hd(&1))))
+
+  defp args_subtype?(args, previous) do
+    subtype?(
+      args_to_domain(args),
+      Enum.reduce(previous, none(), &union(&2, args_to_domain(&1)))
+    )
+  end
+
   @doc """
   Computes the domain from the pattern tree and expected types.
 
@@ -186,9 +237,12 @@ defmodule Module.Types.Pattern do
 
     {pattern_info, context} = pop_pattern_info(context)
 
-    with {:ok, types} <- of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
+    with {:ok, types} <-
+           of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
+         {:ok, types} <-
+           of_pattern_previous(types, previous, trees, pattern_info, tag, stack, context),
          {_types, changed, context} <-
-           of_pattern_refine(types, previous, pattern_info, tag, stack, context) do
+           of_pattern_refine(types, pattern_info, tag, stack, context) do
       {trees, precise?, changed, context}
     else
       {:error, context} -> {trees, context}
@@ -230,9 +284,10 @@ defmodule Module.Types.Pattern do
     args = [{tree, expected, expr}]
     tag = {:match, expr, expected}
 
-    with {:ok, types} <- of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
+    with {:ok, types} <-
+           of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
          {[type], changed, context} <-
-           of_pattern_refine(types, [], pattern_info, tag, stack, context) do
+           of_pattern_refine(types, pattern_info, tag, stack, context) do
       {type, of_changed(changed, stack, context)}
     else
       {:error, context} -> {expected, context}
@@ -253,7 +308,7 @@ defmodule Module.Types.Pattern do
 
     with {:ok, types} <- of_pattern_intersect(args, 0, [], pattern_info, tag, stack, context),
          {_types, changed, context} <-
-           of_pattern_refine(types, [], pattern_info, tag, stack, context) do
+           of_pattern_refine(types, pattern_info, tag, stack, context) do
       {_precise?, context} = of_guards(guards, changed, vars, stack, context)
       context
     else
@@ -271,7 +326,8 @@ defmodule Module.Types.Pattern do
       context = badpattern_error(pattern, index, tag, stack, context)
       {:error, error_vars(pattern_info, context)}
     else
-      of_pattern_intersect(tail, index + 1, [type | acc], pattern_info, tag, stack, context)
+      acc = [type | acc]
+      of_pattern_intersect(tail, index + 1, acc, pattern_info, tag, stack, context)
     end
   end
 
@@ -279,12 +335,13 @@ defmodule Module.Types.Pattern do
     {:ok, Enum.reverse(acc)}
   end
 
-  defp of_pattern_refine(types, previous, pattern_info, tag, stack, context) do
+  defp of_pattern_previous(types, [], _trees, _pattern_info, _tag, _stack, _context) do
+    {:ok, types}
+  end
+
+  defp of_pattern_previous(types, previous, trees, pattern_info, tag, stack, context) do
     types =
       case types do
-        _ when previous == [] ->
-          types
-
         [type] ->
           [Enum.reduce(previous, type, &difference(&2, hd(&1)))]
 
@@ -294,45 +351,53 @@ defmodule Module.Types.Pattern do
           |> domain_to_flat_args(types)
       end
 
-    try do
-      pattern_info
-      |> Enum.reverse()
-      |> Enum.reduce({[], context}, fn {version, _pinned, node}, {changed, context} ->
-        %{var: var, expr: expr, root: root, path: path} = node
+    if index = Enum.find_index(types, &empty?/1) do
+      {_, _, pattern} = Enum.fetch!(trees, index)
+      context = badpattern_error(pattern, index, tag, stack, context)
+      {:error, error_vars(pattern_info, context)}
+    else
+      {:ok, types}
+    end
+  end
 
-        {actual, index} =
-          case root do
-            {:arg, index} -> {Enum.fetch!(types, index), index}
-            _ -> {of_pattern_tree(root, stack, context), nil}
-          end
+  defp of_pattern_refine(types, pattern_info, tag, stack, context) do
+    pattern_info
+    |> Enum.reverse()
+    |> Enum.reduce({[], context}, fn {version, _pinned, node}, {changed, context} ->
+      %{var: var, expr: expr, root: root, path: path} = node
 
-        context =
-          case of_pattern_var(path, actual, context) do
-            {:ok, new_type} ->
-              case Of.refine_head_var(var, new_type, expr, stack, context) do
-                {:ok, _type, context} ->
-                  context
-
-                {:error, old_type, error_context} ->
-                  if match_error?(var, new_type) do
-                    throw(badpattern_error(expr, index, tag, stack, context))
-                  else
-                    throw(badvar_error(var, old_type, new_type, stack, error_context))
-                  end
-              end
+      {actual, index} =
+        case root do
+          {:arg, index} -> {Enum.fetch!(types, index), index}
+          _ -> {of_pattern_tree(root, stack, context), nil}
+        end
 
-            :error ->
-              throw(badpattern_error(expr, index, tag, stack, context))
-          end
+      context =
+        case of_pattern_var(path, actual, context) do
+          {:ok, new_type} ->
+            case Of.refine_head_var(var, new_type, expr, stack, context) do
+              {:ok, _type, context} ->
+                context
+
+              {:error, old_type, error_context} ->
+                if match_error?(var, new_type) do
+                  throw(badpattern_error(expr, index, tag, stack, context))
+                else
+                  throw(badvar_error(var, old_type, new_type, stack, error_context))
+                end
+            end
 
-        {[version | changed], context}
-      end)
-    catch
-      context -> {:error, error_vars(pattern_info, context)}
-    else
-      {changed, context} ->
-        {types, changed, context}
-    end
+          :error ->
+            throw(badpattern_error(expr, index, tag, stack, context))
+        end
+
+      {[version | changed], context}
+    end)
+  catch
+    context -> {:error, error_vars(pattern_info, context)}
+  else
+    {changed, context} ->
+      {types, changed, context}
   end
 
   defp error_vars(pattern_info, context) do
@@ -363,14 +428,6 @@ defmodule Module.Types.Pattern do
     error(__MODULE__, error, meta, stack, context)
   end
 
-  @doc """
-  Warns on redundant clause.
-  """
-  def redundant_warn({:->, meta, [head, _]}, previous, stack, context) do
-    warning = {:redundant_clause, head, previous, context}
-    warn(__MODULE__, warning, meta, stack, context)
-  end
-
   defp error_meta(expr, stack) do
     if meta = get_meta(expr) do
       meta ++ Keyword.take(stack.meta, [:generated, :line, :type_check])
@@ -963,13 +1020,21 @@ defmodule Module.Types.Pattern do
   end
 
   defp of_guards(guards, stack, context) do
+    %{vars: vars, conditional_vars: conditional_vars} = context
+
+    {vars_conds, {precise?, context}} =
+      Enum.map_reduce(guards, {true, context}, fn guard, {precise?, context} ->
+        {type, context} = of_guard(guard, stack, %{context | vars: vars, conditional_vars: %{}})
+        {guard_precise?, context} = maybe_badguard(type, guard, stack, context)
+        %{vars: vars, conditional_vars: cond_vars} = context
+        {{vars, cond_vars}, {guard_precise? and precise?, context}}
+      end)
+
     expr = Enum.reduce(guards, {:_, [], []}, &{:when, [], [&2, &1]})
+    context = %{context | vars: vars, conditional_vars: conditional_vars}
 
-    Of.with_conditional_vars(guards, true, expr, stack, context, fn guard, precise?, context ->
-      {type, context} = of_guard(guard, stack, context)
-      {guard_precise?, context} = maybe_badguard(type, guard, stack, context)
-      {guard_precise? and precise?, context}
-    end)
+    {precise? and Of.all_same_conditional_vars?(vars_conds),
+     Of.reduce_conditional_vars(vars_conds, expr, stack, context)}
   end
 
   defp update_parent_version(parent_version, %{pattern_info: pattern_info} = context) do
@@ -1209,17 +1274,13 @@ defmodule Module.Types.Pattern do
         end
 
       {type, vars_conds} =
-        of_logical_cond([left | right], true, expected, abort_domain, stack, cond_context, [])
+        of_logical_cond([left | right], none(), [], expected, stack, cond_context)
 
       # We will be precise if all branches changed the same variable
       context =
         update_in(context.pattern_info.vars, fn
-          false ->
-            false
-
-          vars ->
-            [{_, cond} | tail] = vars_conds
-            Enum.all?(tail, fn {_, tail_cond} -> cond == tail_cond end) and vars
+          false -> false
+          vars -> Of.all_same_conditional_vars?(vars_conds) and vars
         end)
 
       {type, Of.reduce_conditional_vars(vars_conds, call, stack, context)}
@@ -1286,25 +1347,16 @@ defmodule Module.Types.Pattern do
     of_logical_all(tail, disjoint?, expected, to_abort, stack, context)
   end
 
-  defp of_logical_cond([head], disjoint?, expected, to_abort, stack, context, acc) do
+  defp of_logical_cond([head | tail], acc_type, acc_vars, expected, stack, context) do
     {type, %{vars: vars, conditional_vars: cond_vars}} =
       of_guard(head, expected, head, stack, context)
 
-    acc = [{vars, cond_vars} | acc]
-
-    case disjoint? do
-      true -> {type, acc}
-      false -> {union(to_abort, type), acc}
-    end
+    acc_vars = [{vars, cond_vars} | acc_vars]
+    of_logical_cond(tail, union(acc_type, type), acc_vars, expected, stack, context)
   end
 
-  defp of_logical_cond([head | tail], disjoint?, expected, to_abort, stack, context, acc) do
-    {type, %{vars: vars, conditional_vars: cond_vars}} =
-      of_guard(head, expected, head, stack, context)
-
-    disjoint? = disjoint? and disjoint?(type, to_abort)
-    acc = [{vars, cond_vars} | acc]
-    of_logical_cond(tail, disjoint?, expected, to_abort, stack, context, acc)
+  defp of_logical_cond([], acc_type, acc_vars, _expected, _stack, _context) do
+    {acc_type, acc_vars}
   end
 
   ## Helpers
@@ -1368,27 +1420,103 @@ defmodule Module.Types.Pattern do
     }
   end
 
-  def format_diagnostic({:redundant_clause, args, previous, context}) do
-    traces = collect_traces(args, context)
+  def format_diagnostic(
+        {:redundant, {{:def, kind, fun, _}, args, guards}, _expected, types, previous, _context}
+      ) do
+    call = Enum.reduce(guards, {fun, [], args}, &{:when, [], [&2, &1]})
 
     %{
-      details: %{typing_traces: traces},
       message:
         IO.iodata_to_binary([
           """
           the following clause is redundant:
 
-              #{args_to_string(args) |> indent(4)} ->
+              #{expr_to_string({kind, [], [call]}) |> indent(4)}
+
+          it has type:
+
+              #{args_to_quoted_string(types) |> indent(4)}
 
           previous clauses have already matched on the following types:
 
               #{previous_to_string(previous)}
-          """,
-          format_traces(traces)
+          """
         ])
     }
   end
 
+  def format_diagnostic({:redundant, {info, args}, expected, _types, previous, context}) do
+    traces = collect_traces(args, context)
+
+    message =
+      with {:case, meta, expr, type} <- info,
+           {:case, :||} <- meta[:type_check] do
+        if subtype?(type, atom([false, nil])) do
+          """
+          the following conditional expression will never succeed:
+
+              #{expr_to_string(expr) |> indent(4)}
+
+          because it evaluates to:
+
+              #{to_quoted_string(type) |> indent(4)}
+          """
+        else
+          additional =
+            with {:case, meta, [_, _]} <- expr,
+                 {:case, :||} <- meta[:type_check] do
+              "(shown as ... below) "
+            else
+              _ -> ""
+            end
+
+          """
+          the right-hand side of || #{additional}will never be executed:
+
+              #{expr_to_string({:||, [], [expr, {:..., [], []}]}) |> indent(4)}
+
+          because the left-hand side always evaluates to:
+
+              #{to_quoted_string(type) |> indent(4)}
+          """
+        end
+      else
+        _ ->
+          with {_op, _meta, expr, type} <- info,
+               true <- args_subtype?(expected, previous) do
+            """
+            the following clause cannot match because the previous clauses already matched all possible values:
+
+                #{args_to_string(args) |> indent(4)} ->
+
+            it attempts to match on the result of:
+
+                #{expr_to_string(expr) |> indent(4)}
+
+            which has the already matched type:
+
+                #{to_quoted_string(type) |> indent(4)}
+            """
+          else
+            _ ->
+              """
+              the following clause is redundant:
+
+                  #{args_to_string(args) |> indent(4)} ->
+
+              previous clauses have already matched on the following types:
+
+                  #{previous_to_string(previous)}
+              """
+          end
+      end
+
+    %{
+      details: %{typing_traces: traces},
+      message: IO.iodata_to_binary([message, format_traces(traces)])
+    }
+  end
+
   def format_diagnostic({:badmatch, _meta, pattern, context}) do
     traces = collect_traces(pattern, context)
 
@@ -1406,11 +1534,12 @@ defmodule Module.Types.Pattern do
     }
   end
 
-  # $ type tag = {:def, kind, fun, args, guards, types} or clause_pattern() or match_pattern()
+  # $ type tag = head_pattern() or match_pattern()
   #
-  # $ typep clause_pattern =
-  #     {{:case | :try_else, meta, expr, type}, [arg], [previous]} or
-  #     {:for_reduce | :receive | :try_catch | :with_else | :fn, [arg], [previous]}
+  # $ typep head_pattern =
+  #     {{:def, kind, fun, types}, args, guards} or
+  #     {{:case | :try_else, meta, expr, type}, [arg]} or
+  #     {:for_reduce | :receive | :try_catch | :with_else | :fn, [arg]}
   #
   # $ typep match_pattern =
   #     {:with or :for or :match, pattern, type}
@@ -1430,8 +1559,7 @@ defmodule Module.Types.Pattern do
     }
   end
 
-  defp badpattern({:def, _kind, _fun, args, _guards, types}, index)
-       when is_integer(index) do
+  defp badpattern({{:def, _kind, _fun, types}, args, _guards}, index) when is_integer(index) do
     arg = Enum.fetch!(args, index)
     type = Enum.fetch!(types, index)
 
@@ -1457,113 +1585,59 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  defp badpattern({{op, meta, expr, type}, args, previous}, _index)
-       when op in [:case, :try_else] do
-    type_check = meta[:type_check]
-
-    cond do
-      match?({:case, _}, type_check) ->
-        message =
-          case type_check do
-            {:case, op} when op in [:and, :or] ->
-              {first_message, second_message} =
-                case booleaness(type) do
-                  {true, _} -> {" will always succeed", "because it evaluates to"}
-                  {false, _} -> {" will never succeed", "because it evaluates to"}
-                  :none -> {" will always fail", "because it evaluates to"}
-                  _ -> {"", "will always evaluate to"}
-                end
-
-              """
-              the following conditional expression#{first_message}:
-
-                  #{expr_to_string(expr) |> indent(4)}
-
-              #{second_message}:
-
-                  #{to_quoted_string(type) |> indent(4)}
-              """
-
-            {:case, :||} ->
-              if subtype?(type, atom([false, nil])) do
-                """
-                the following conditional expression will never succeed:
-
-                    #{expr_to_string(expr) |> indent(4)}
-
-                because it evaluates to:
-
-                    #{to_quoted_string(type) |> indent(4)}
-                """
-              else
-                additional =
-                  with {:case, meta, [_, _]} <- expr,
-                       {:case, :||} <- meta[:type_check] do
-                    "(shown as ... below) "
-                  else
-                    _ -> ""
-                  end
-
-                """
-                the right-hand side of || #{additional}will never be executed:
-
-                    #{expr_to_string({:||, [], [expr, {:..., [], []}]}) |> indent(4)}
-
-                because the left-hand side always evaluates to:
-
-                    #{to_quoted_string(type) |> indent(4)}
-                """
-              end
-
-            _ ->
-              """
-              the following conditional expression:
-
-                  #{expr_to_string(expr) |> indent(4)}
-
-              will always evaluate to:
-
-                  #{to_quoted_string(type) |> indent(4)}
-              """
+  defp badpattern({{op, meta, expr, type}, args}, _index) when op in [:case, :try_else] do
+    with {:case, op} <- meta[:type_check] do
+      if op in [:and, :or] do
+        {first_message, second_message} =
+          case booleaness(type) do
+            {true, _} -> {" will always succeed", "because it evaluates to"}
+            {false, _} -> {" will never succeed", "because it evaluates to"}
+            :none -> {" will always fail", "because it evaluates to"}
+            _ -> {"", "will always evaluate to"}
           end
 
-        {expr, message}
-
-      previous == [] ->
-        {args,
+        {expr,
          """
-         the following clause will never match:
+         the following conditional expression#{first_message}:
 
-             #{args_to_string(args) |> indent(4)} ->
+             #{expr_to_string(expr) |> indent(4)}
 
-         because it attempts to match on the result of:
+         #{second_message}:
+
+             #{to_quoted_string(type) |> indent(4)}
+         """}
+      else
+        {expr,
+         """
+         the following conditional expression:
 
              #{expr_to_string(expr) |> indent(4)}
 
-         which has type:
+         will always evaluate to:
 
              #{to_quoted_string(type) |> indent(4)}
          """}
-
-      true ->
+      end
+    else
+      _ ->
         {args,
          """
-         the following clause cannot match because the previous clauses already matched all possible values:
+         the following clause will never match:
 
              #{args_to_string(args) |> indent(4)} ->
 
-         it attempts to match on the result of:
+         because it attempts to match on the result of:
 
              #{expr_to_string(expr) |> indent(4)}
 
-         which has the already matched type:
+         which has type:
 
              #{to_quoted_string(type) |> indent(4)}
          """}
     end
   end
 
-  defp badpattern({op, args, _previous}, index)
+  defp badpattern({op, args}, index)
        when op in [:for_reduce, :receive, :try_catch, :with_else, :fn] do
     arg = Enum.fetch!(args, index)
 
@@ -1604,6 +1678,12 @@ defmodule Module.Types.Pattern do
     |> indent(4)
   end
 
+  defp args_to_quoted_string(args) do
+    args
+    |> Enum.map_join(", ", &to_quoted_string/1)
+    |> indent(4)
+  end
+
   defp previous_to_string(previous) do
     Enum.map_join(previous, "\n    ", fn types ->
       types
diff --git a/lib/elixir/lib/protocol.ex b/lib/elixir/lib/protocol.ex
index 4cd2ef30e71..f8a20258e7e 100644
--- a/lib/elixir/lib/protocol.ex
+++ b/lib/elixir/lib/protocol.ex
@@ -968,16 +968,6 @@ defmodule Protocol do
           built_in
         )
 
-        # Define a catch-all impl_for/1 clause to pacify Dialyzer (since
-        # destructuring opaque types is illegal, Dialyzer will think none of the
-        # previous clauses matches opaque types, and without this clause, will
-        # conclude that impl_for can't handle an opaque argument). This is a hack
-        # since it relies on Dialyzer not being smart enough to conclude that all
-        # opaque types will get the any_impl_for/0 implementation.
-        Kernel.def impl_for(_) do
-          unquote(any_impl_for)
-        end
-
         # Internal handler for Structs
         Kernel.defp struct_impl_for(struct) do
           case Code.ensure_compiled(Protocol.__concat__(__MODULE__, struct)) do
@@ -1021,8 +1011,22 @@ defmodule Protocol do
         )
       end
 
+    # Define a catch-all impl_for/1 clause to pacify Dialyzer (since
+    # destructuring opaque types is illegal, Dialyzer will think none of the
+    # previous clauses matches opaque types, and without this clause, will
+    # conclude that impl_for can't handle an opaque argument). This is a hack
+    # since it relies on Dialyzer not being smart enough to conclude that all
+    # opaque types will get the any_impl_for/0 implementation.
+    impl_for_fallback =
+      quote generated: true, bind_quoted: [] do
+        Kernel.def impl_for(_) do
+          unquote(any_impl_for)
+        end
+      end
+
     quote generated: true do
       unquote(prefix)
+      unquote(impl_for_fallback)
 
       @doc false
       @spec impl_for!(term) :: atom
diff --git a/lib/elixir/test/elixir/kernel/alias_test.exs b/lib/elixir/test/elixir/kernel/alias_test.exs
index d897fedb5ed..ab558840278 100644
--- a/lib/elixir/test/elixir/kernel/alias_test.exs
+++ b/lib/elixir/test/elixir/kernel/alias_test.exs
@@ -39,7 +39,7 @@ defmodule Kernel.AliasTest do
   end
 
   test "lexical" do
-    if true_fun() do
+    if Process.get(:unused, true) do
       alias OMG, as: List, warn: false
     else
       alias ABC, as: List, warn: false
@@ -48,8 +48,6 @@ defmodule Kernel.AliasTest do
     assert List.flatten([1, [2], 3]) == [1, 2, 3]
   end
 
-  defp true_fun(), do: true
-
   defmodule Elixir do
     def sample, do: 1
   end
diff --git a/lib/elixir/test/elixir/kernel/comprehension_test.exs b/lib/elixir/test/elixir/kernel/comprehension_test.exs
index 97a0a6b733e..b68b70dade0 100644
--- a/lib/elixir/test/elixir/kernel/comprehension_test.exs
+++ b/lib/elixir/test/elixir/kernel/comprehension_test.exs
@@ -325,13 +325,11 @@ defmodule Kernel.ComprehensionTest do
   end
 
   test "list for comprehension matched to '_' on last line of block" do
-    assert (if true_fun() do
+    assert (if Process.get(:unused, true) do
               _ = for x <- [1, 2, 3], do: x * 2
             end) == [2, 4, 6]
   end
 
-  defp true_fun(), do: true
-
   test "list for comprehensions with filters" do
     assert for(x <- [1, 2, 3], x > 1, x < 3, do: x * 2) == [4]
   end
diff --git a/lib/elixir/test/elixir/kernel/fn_test.exs b/lib/elixir/test/elixir/kernel/fn_test.exs
index eac16496319..21a8c58efe6 100644
--- a/lib/elixir/test/elixir/kernel/fn_test.exs
+++ b/lib/elixir/test/elixir/kernel/fn_test.exs
@@ -32,7 +32,7 @@ defmodule Kernel.FnTest do
 
   test "case function hoisting does not affect anonymous fns" do
     result =
-      if atom?(0) do
+      if Process.get(:unused, false) do
         user = :defined
         user
       else
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index 7c5a88e76ea..a5d7a829f6b 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -1802,14 +1802,15 @@ defmodule Module.Types.ExprTest do
     end
 
     test "warns on redundant clauses" do
-      assert typeerror!(
+      assert typewarn!(
                [x],
                case System.get_env(x) do
                  nil -> 1
                  b when is_binary(b) -> 2
                  other -> other
                end
-             ) == ~l"""
+             )
+             |> elem(1) =~ ~l"""
              the following clause cannot match because the previous clauses already matched all possible values:
 
                  other ->
@@ -1973,7 +1974,7 @@ defmodule Module.Types.ExprTest do
     end
 
     test "|| reports violations" do
-      assert typeerror!([x = 123], x || true) =~ """
+      assert typewarn!([x = 123], x || true) |> elem(1) =~ """
              the right-hand side of || will never be executed:
 
                  x || ...
@@ -1984,7 +1985,7 @@ defmodule Module.Types.ExprTest do
 
              """
 
-      assert typeerror!([x = 123], System.get_env("foo") || x || true) =~ """
+      assert typewarn!([x = 123], System.get_env("foo") || x || true) |> elem(1) =~ """
              the right-hand side of || (shown as ... below) will never be executed:
 
                  System.get_env("foo") || x || ...
@@ -1995,7 +1996,7 @@ defmodule Module.Types.ExprTest do
 
              """
 
-      assert typeerror!([x = false], x || true) =~ """
+      assert typewarn!([x = false], x || true) |> elem(1) =~ """
              the following conditional expression will never succeed:
 
                  x
diff --git a/lib/elixir/test/elixir/module/types/integration_test.exs b/lib/elixir/test/elixir/module/types/integration_test.exs
index ba37cf3cb04..130e9f9dbc9 100644
--- a/lib/elixir/test/elixir/module/types/integration_test.exs
+++ b/lib/elixir/test/elixir/module/types/integration_test.exs
@@ -315,6 +315,43 @@ defmodule Module.Types.IntegrationTest do
       assert_warnings(files, warnings)
     end
 
+    test "redundant clauses" do
+      files = %{
+        "a.ex" => """
+        defmodule A do
+          def foo(x, _) when is_integer(x), do: :one
+          def foo(_, y) when is_integer(y), do: :two
+          def foo(x, y) when is_integer(x) and is_integer(y), do: :three
+        end
+        """
+      }
+
+      warnings = [
+        """
+            warning: the following clause is redundant:
+
+                def foo(x, y) when is_integer(x) and is_integer(y)
+
+            it has type:
+
+                integer(), integer()
+
+            previous clauses have already matched on the following types:
+
+                term(), integer()
+                integer(), term()
+
+            │
+          4 │   def foo(x, y) when is_integer(x) and is_integer(y), do: :three
+            │       ~
+            │
+            └─ a.ex:4:7: A.foo/2
+        """
+      ]
+
+      assert_warnings(files, warnings)
+    end
+
     test "mismatched locals" do
       files = %{
         "a.ex" => """
@@ -472,7 +509,8 @@ defmodule Module.Types.IntegrationTest do
 
         defimpl Itself, for: Range do
           def itself(nil), do: nil
-          def itself(range), do: range
+          def itself(%Range{} = range), do: range
+          def itself(%Range{}), do: raise "oops"
         end
         """
       }
@@ -495,6 +533,25 @@ defmodule Module.Types.IntegrationTest do
             │   ~~~~~~~~~~~~~~~~~~~~~~~~
             │
             └─ a.ex:6: Itself.Range.itself/1
+        """,
+        """
+            warning: the following clause is redundant:
+
+                def itself(%Range{})
+
+            it has type:
+
+                %Range{}
+
+            previous clauses have already matched on the following types:
+
+                %Range{}
+
+            │
+          8 │   def itself(%Range{}), do: raise "oops"
+            │       ~
+            │
+            └─ a.ex:8:7: Itself.Range.itself/1
         """
       ]
 
@@ -661,7 +718,7 @@ defmodule Module.Types.IntegrationTest do
 
             it has type:
 
-                -dynamic(%Date{})-
+                -dynamic(%Date{year: integer(), month: integer(), day: integer(), calendar: Calendar.ISO})-
 
             but expected a type that implements the Collectable protocol.
             You either passed the wrong value or you forgot to implement the protocol.
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 148f780f62a..2a73eebf860 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -1290,6 +1290,12 @@ defmodule Module.Types.PatternTest do
       refute precise?([x], hd(x) == :ok)
       refute precise?([x, y], x == :ok and y == 123)
       refute precise?([x, y], x == :ok or y == :error)
+      refute precise?([x], x <= 0 or x == :infinity)
+    end
+
+    test "when guards" do
+      assert precise?([x, y], is_integer(x) when is_binary(x))
+      refute precise?([x, y], is_integer(x) when is_binary(y))
     end
 
     test "sized guards" do
diff --git a/lib/elixir/test/elixir/module/types/type_helper.exs b/lib/elixir/test/elixir/module/types/type_helper.exs
index 63f29baec5f..23a9e6370a2 100644
--- a/lib/elixir/test/elixir/module/types/type_helper.exs
+++ b/lib/elixir/test/elixir/module/types/type_helper.exs
@@ -154,10 +154,10 @@ defmodule TypeHelper do
     stack = new_stack(:static)
     expected = Enum.map(patterns, fn _ -> Descr.dynamic() end)
 
-    {_trees, precise?, _context} =
-      Pattern.of_head(patterns, guards, expected, {:fn, patterns, []}, [], stack, new_context())
+    {_trees, previous, _context} =
+      Pattern.of_head(patterns, guards, expected, [], {:fn, patterns}, [], stack, new_context())
 
-    precise?
+    previous != []
   end
 
   def __typecheck__(mode, patterns, guards, body) do
@@ -165,7 +165,7 @@ defmodule TypeHelper do
     expected = Enum.map(patterns, fn _ -> Descr.dynamic() end)
 
     {_trees, _precise?, context} =
-      Pattern.of_head(patterns, guards, expected, {:fn, patterns, []}, [], stack, new_context())
+      Pattern.of_head(patterns, guards, expected, [], {:fn, patterns}, [], stack, new_context())
 
     Expr.of_expr(body, Descr.term(), :ok, stack, context)
   end
diff --git a/lib/elixir/test/elixir/task_test.exs b/lib/elixir/test/elixir/task_test.exs
index 1b5427543dc..69b55aea570 100644
--- a/lib/elixir/test/elixir/task_test.exs
+++ b/lib/elixir/test/elixir/task_test.exs
@@ -224,7 +224,12 @@ defmodule TaskTest do
     end
 
     test "discards late replies" do
-      task = Task.async(fn -> assert_receive(:go) && :ok end)
+      task =
+        Task.async(fn ->
+          assert_receive(:go)
+          :ok
+        end)
+
       assert Task.ignore(task) == nil
       send(task.pid, :go)
       wait_until_down(task)
@@ -240,7 +245,12 @@ defmodule TaskTest do
     end
 
     test "discards late failures" do
-      task = Task.async(fn -> assert_receive(:go) && exit(:oops) end)
+      task =
+        Task.async(fn ->
+          assert_receive(:go)
+          exit(:oops)
+        end)
+
       assert Task.ignore(task) == nil
       send(task.pid, :go)
       wait_until_down(task)
diff --git a/lib/ex_unit/test/ex_unit/assertions_test.exs b/lib/ex_unit/test/ex_unit/assertions_test.exs
index 522441930db..52192206df1 100644
--- a/lib/ex_unit/test/ex_unit/assertions_test.exs
+++ b/lib/ex_unit/test/ex_unit/assertions_test.exs
@@ -125,7 +125,7 @@ defmodule ExUnit.AssertionsTest do
 
   test "assert arguments are not kept for operators" do
     try do
-      assert !Value.truthy()
+      assert !Process.get(:unused, Value.truthy())
       flunk("This should never be tested")
     rescue
       error in [ExUnit.AssertionError] ->