diff --git a/lib/elixir/lib/inspect.ex b/lib/elixir/lib/inspect.ex
index e6404b2cbe7..290e8b25270 100644
--- a/lib/elixir/lib/inspect.ex
+++ b/lib/elixir/lib/inspect.ex
@@ -571,20 +571,26 @@ defimpl Inspect, for: Any do
       |> Enum.reject(&(&1 in except))
       |> Enum.filter(&(&1 in only))
 
-    optional? =
+    filtered_guard =
+      quote do
+        var!(field) in unquote(filtered_fields)
+      end
+
+    field_guard =
       if optional == [] do
-        false
+        filtered_guard
       else
         optional_map = for field <- optional, into: %{}, do: {field, Map.fetch!(struct, field)}
 
         quote do
-          case unquote(Macro.escape(optional_map)) do
-            %{^var!(field) => var!(default)} ->
-              var!(default) == Map.get(var!(struct), var!(field))
-
-            %{} ->
-              false
-          end
+          unquote(filtered_guard) and
+            not case unquote(Macro.escape(optional_map)) do
+              %{^var!(field) => var!(default)} ->
+                var!(default) == Map.get(var!(struct), var!(field))
+
+              %{} ->
+                false
+            end
         end
       end
 
@@ -593,7 +599,7 @@ defimpl Inspect, for: Any do
         def inspect(var!(struct), var!(opts)) do
           var!(infos) =
             for %{field: var!(field)} = var!(info) <- unquote(module).__info__(:struct),
-                var!(field) in unquote(filtered_fields) and not unquote(optional?),
+                unquote(field_guard),
                 do: var!(info)
 
           var!(name) = Macro.inspect_atom(:literal, unquote(module))
diff --git a/lib/elixir/lib/kernel.ex b/lib/elixir/lib/kernel.ex
index 986ff74d519..cbef8391339 100644
--- a/lib/elixir/lib/kernel.ex
+++ b/lib/elixir/lib/kernel.ex
@@ -1905,8 +1905,8 @@ defmodule Kernel do
 
   ## Implemented in Elixir
 
-  defp optimize_boolean({:case, meta, args}) do
-    {:case, [{:optimize_boolean, true} | meta], args}
+  defp annotate_case(extra, {:case, meta, args}) do
+    {:case, extra ++ meta, args}
   end
 
   @doc """
@@ -1973,7 +1973,8 @@ defmodule Kernel do
   end
 
   defp build_boolean_check(operator, check, true_clause, false_clause) do
-    optimize_boolean(
+    annotate_case(
+      [optimize_boolean: true, type_check: :expr],
       quote do
         case unquote(check) do
           false -> unquote(false_clause)
@@ -2006,7 +2007,8 @@ defmodule Kernel do
   defmacro !{:!, _, [value]} do
     assert_no_match_or_guard_scope(__CALLER__.context, "!")
 
-    optimize_boolean(
+    annotate_case(
+      [optimize_boolean: true, type_check: :expr],
       quote do
         case unquote(value) do
           x when :"Elixir.Kernel".in(x, [false, nil]) -> false
@@ -2019,7 +2021,8 @@ defmodule Kernel do
   defmacro !value do
     assert_no_match_or_guard_scope(__CALLER__.context, "!")
 
-    optimize_boolean(
+    annotate_case(
+      [optimize_boolean: true, type_check: :expr],
       quote do
         case unquote(value) do
           x when :"Elixir.Kernel".in(x, [false, nil]) -> true
@@ -3910,7 +3913,8 @@ defmodule Kernel do
   end
 
   defp build_if(condition, do: do_clause, else: else_clause) do
-    optimize_boolean(
+    annotate_case(
+      [optimize_boolean: true, type_check: :expr],
       quote do
         case unquote(condition) do
           x when :"Elixir.Kernel".in(x, [false, nil]) -> unquote(else_clause)
@@ -4228,15 +4232,18 @@ defmodule Kernel do
   defmacro left && right do
     assert_no_match_or_guard_scope(__CALLER__.context, "&&")
 
-    quote do
-      case unquote(left) do
-        x when :"Elixir.Kernel".in(x, [false, nil]) ->
-          x
+    annotate_case(
+      [type_check: :expr],
+      quote do
+        case unquote(left) do
+          x when :"Elixir.Kernel".in(x, [false, nil]) ->
+            x
 
-        _ ->
-          unquote(right)
+          _ ->
+            unquote(right)
+        end
       end
-    end
+    )
   end
 
   @doc """
@@ -4268,15 +4275,18 @@ defmodule Kernel do
   defmacro left || right do
     assert_no_match_or_guard_scope(__CALLER__.context, "||")
 
-    quote do
-      case unquote(left) do
-        x when :"Elixir.Kernel".in(x, [false, nil]) ->
-          unquote(right)
+    annotate_case(
+      [type_check: :expr],
+      quote do
+        case unquote(left) do
+          x when :"Elixir.Kernel".in(x, [false, nil]) ->
+            unquote(right)
 
-        x ->
-          x
+          x ->
+            x
+        end
       end
-    end
+    )
   end
 
   @doc """
diff --git a/lib/elixir/lib/module/types.ex b/lib/elixir/lib/module/types.ex
index b5fd1b00db6..e6e4ff646f6 100644
--- a/lib/elixir/lib/module/types.ex
+++ b/lib/elixir/lib/module/types.ex
@@ -53,7 +53,9 @@ defmodule Module.Types do
   end
 
   defp warnings_from_clause(meta, args, guards, body, stack, context) do
-    {_types, context} = Pattern.of_head(args, guards, meta, stack, context)
+    dynamic = Module.Types.Descr.dynamic()
+    expected = Enum.map(args, fn _ -> dynamic end)
+    {_types, context} = Pattern.of_head(args, guards, expected, :default, meta, stack, context)
     {_type, context} = Expr.of_expr(body, stack, context)
     context.warnings
   end
diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 7d75388ad82..6efc243ace7 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -582,6 +582,15 @@ 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
diff --git a/lib/elixir/lib/module/types/expr.ex b/lib/elixir/lib/module/types/expr.ex
index c0e2203f963..42ebed324ad 100644
--- a/lib/elixir/lib/module/types/expr.ex
+++ b/lib/elixir/lib/module/types/expr.ex
@@ -10,13 +10,15 @@ defmodule Module.Types.Expr do
   functions_and_macros = list(tuple([atom(), list(tuple([atom(), integer()]))]))
   list_of_modules = list(atom())
 
+  @try_catch atom([:error, :exit, :throw])
+
   @caller closed_map(
             __struct__: atom([Macro.Env]),
             aliases: aliases,
             context: atom([:match, :guard, nil]),
             context_modules: list_of_modules,
             file: binary(),
-            function: union(tuple(), atom([nil])),
+            function: union(tuple([atom(), integer()]), atom([nil])),
             functions: functions_and_macros,
             lexical_tracker: union(pid(), atom([nil])),
             line: integer(),
@@ -108,13 +110,13 @@ defmodule Module.Types.Expr do
   end
 
   # left = right
-  def of_expr({:=, _meta, [left_expr, right_expr]} = expr, stack, context) do
+  def of_expr({:=, _, [left_expr, right_expr]} = expr, stack, context) do
     {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, stack, context)
+      _ -> Pattern.of_match(left_expr, right_type, expr, {:match, right_type}, stack, context)
     end
   end
 
@@ -241,19 +243,26 @@ defmodule Module.Types.Expr do
     |> dynamic_unless_static(stack)
   end
 
-  def of_expr({:case, _meta, [case_expr, [{:do, clauses}]]}, stack, context) do
-    {expr_type, context} = of_expr(case_expr, stack, context)
+  def of_expr({:case, meta, [case_expr, [{:do, clauses}]]}, stack, context) do
+    {case_type, context} = of_expr(case_expr, stack, context)
 
-    clauses
-    |> of_clauses(stack, [expr_type], {none(), context})
+    # 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.
+    if is_atom(case_expr) and {:type_check, :expr} in meta do
+      for {:->, meta, args} <- clauses, do: {:->, [generated: true] ++ meta, args}
+    else
+      clauses
+    end
+    |> of_clauses([case_type], {:case, meta, case_type, case_expr}, stack, {none(), context})
     |> dynamic_unless_static(stack)
   end
 
   # TODO: fn pat -> expr end
   def of_expr({:fn, _meta, clauses}, stack, context) do
-    [{:->, _, [args, _]} | _] = clauses
-    expected = Enum.map(args, fn _ -> dynamic() end)
-    {_acc, context} = of_clauses(clauses, stack, expected, {none(), context})
+    [{:->, _, [head, _]} | _] = clauses
+    {patterns, _guards} = extract_head(head)
+    expected = Enum.map(patterns, fn _ -> dynamic() end)
+    {_acc, context} = of_clauses(clauses, expected, :fn, stack, {none(), context})
     {fun(), context}
   end
 
@@ -280,10 +289,10 @@ defmodule Module.Types.Expr do
         {acc, context}
 
       {:catch, clauses}, acc_context ->
-        of_clauses(clauses, stack, [atom([:error, :exit, :throw]), dynamic()], acc_context)
+        of_clauses(clauses, [@try_catch, dynamic()], :try_catch, stack, acc_context)
 
       {:else, clauses}, acc_context ->
-        of_clauses(clauses, stack, [body_type], acc_context)
+        of_clauses(clauses, [body_type], {:try_else, body_type}, stack, acc_context)
     end)
     |> dynamic_unless_static(stack)
   end
@@ -291,11 +300,11 @@ defmodule Module.Types.Expr do
   def of_expr({:receive, _meta, [blocks]}, stack, context) do
     blocks
     |> Enum.reduce({none(), context}, fn
-      {:do, {:__block__, _, []}}, {acc, context} ->
-        {acc, context}
+      {:do, {:__block__, _, []}}, acc_context ->
+        acc_context
 
-      {:do, clauses}, {acc, context} ->
-        of_clauses(clauses, stack, [dynamic()], {acc, context})
+      {:do, clauses}, acc_context ->
+        of_clauses(clauses, [dynamic()], :receive, stack, acc_context)
 
       {:after, [{:->, meta, [[timeout], body]}]}, {acc, context} ->
         {timeout_type, context} = of_expr(timeout, stack, context)
@@ -318,7 +327,7 @@ defmodule Module.Types.Expr do
     context = Enum.reduce(opts, context, &for_option(&1, stack, &2))
 
     if Keyword.has_key?(opts, :reduce) do
-      {_, context} = of_clauses(block, stack, [dynamic()], {none(), context})
+      {_, context} = of_clauses(block, [dynamic()], :for_reduce, stack, {none(), context})
       {dynamic(), context}
     else
       {_type, context} = of_expr(block, stack, context)
@@ -441,16 +450,21 @@ defmodule Module.Types.Expr do
 
   ## Comprehensions
 
-  defp for_clause({:<-, meta, [left, expr]}, stack, context) do
+  defp for_clause({:<-, _, [left, right]} = expr, stack, context) do
     {pattern, guards} = extract_head([left])
-    {_expr_type, context} = of_expr(expr, stack, context)
-    {[_type], context} = Pattern.of_head([pattern], guards, meta, stack, context)
+    {_, context} = of_expr(right, stack, context)
+
+    {_type, context} =
+      Pattern.of_match(pattern, guards, dynamic(), expr, :for, stack, context)
+
     context
   end
 
-  defp for_clause({:<<>>, _, [{:<-, meta, [left, right]}]}, stack, context) do
+  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(), left, stack, context)
+
+    {_pattern_type, context} =
+      Pattern.of_match(left, binary(), expr, :for, stack, context)
 
     if binary_type?(right_type) do
       context
@@ -481,11 +495,10 @@ defmodule Module.Types.Expr do
 
   ## With
 
-  defp with_clause({:<-, meta, [left, expr]}, stack, context) do
+  defp with_clause({:<-, _meta, [left, right]} = expr, stack, context) do
     {pattern, guards} = extract_head([left])
-
-    {[_type], context} = Pattern.of_head([pattern], guards, meta, stack, context)
-    {_expr_type, context} = of_expr(expr, stack, context)
+    {_type, context} = Pattern.of_match(pattern, guards, dynamic(), :with, expr, stack, context)
+    {_, context} = of_expr(right, stack, context)
     context
   end
 
@@ -500,7 +513,7 @@ defmodule Module.Types.Expr do
   end
 
   defp with_option({:else, clauses}, stack, context) do
-    {_, context} = of_clauses(clauses, stack, [dynamic()], {none(), context})
+    {_, context} = of_clauses(clauses, [dynamic()], :with_else, stack, {none(), context})
     context
   end
 
@@ -532,15 +545,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, stack, _expected, acc_context) do
-    Enum.reduce(clauses, acc_context, fn {:->, meta, [head, body]}, {acc, context} ->
+  defp of_clauses(clauses, expected, info, stack, {acc, context}) do
+    %{failed: failed?} = context
+
+    Enum.reduce(clauses, {acc, context}, fn {:->, meta, [head, body]}, {acc, context} ->
+      {failed?, context} = reset_failed(context, failed?)
       {patterns, guards} = extract_head(head)
-      {_types, context} = Pattern.of_head(patterns, guards, meta, stack, context)
+      {_types, context} = Pattern.of_head(patterns, guards, expected, info, meta, stack, context)
       {body, context} = of_expr(body, stack, context)
-      {union(acc, body), context}
+      {union(acc, body), set_failed(context, failed?)}
     end)
   end
 
+  defp reset_failed(%{failed: true} = context, false), do: {true, %{context | failed: false}}
+  defp reset_failed(context, _), do: {false, context}
+
+  defp set_failed(%{failed: false} = context, true), do: %{context | failed: true}
+  defp set_failed(context, _bool), do: context
+
   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 aae945b620c..f3c78adbcec 100644
--- a/lib/elixir/lib/module/types/helpers.ex
+++ b/lib/elixir/lib/module/types/helpers.ex
@@ -223,12 +223,16 @@ defmodule Module.Types.Helpers do
     if Keyword.get(meta, :generated, false) do
       context
     else
-      {fun, arity} = stack.function
-      location = {stack.file, meta, {stack.module, fun, arity}}
-      %{context | warnings: [{module, warning, location} | context.warnings]}
+      effectively_warn(module, warning, meta, stack, context)
     end
   end
 
+  defp effectively_warn(module, warning, meta, stack, context) do
+    {fun, arity} = stack.function
+    location = {stack.file, meta, {stack.module, fun, arity}}
+    %{context | warnings: [{module, warning, location} | context.warnings]}
+  end
+
   @doc """
   Emits an error.
 
@@ -236,8 +240,15 @@ defmodule Module.Types.Helpers do
   """
   def error(module, warning, meta, stack, context) do
     case context do
-      %{failed: true} -> context
-      %{failed: false} -> warn(module, warning, meta, stack, %{context | failed: true})
+      %{failed: true} ->
+        context
+
+      %{failed: false} ->
+        if Keyword.get(meta, :generated, false) do
+          context
+        else
+          effectively_warn(module, warning, meta, stack, %{context | failed: true})
+        end
     end
   end
 
diff --git a/lib/elixir/lib/module/types/of.ex b/lib/elixir/lib/module/types/of.ex
index e597472f8a6..ef4e9331d18 100644
--- a/lib/elixir/lib/module/types/of.ex
+++ b/lib/elixir/lib/module/types/of.ex
@@ -121,7 +121,7 @@ defmodule Module.Types.Of do
     {dynamic?, fallback, single, multiple, assert, context} =
       Enum.reduce(pairs, {false, none(), [], [], [], context}, fn
         {key, value}, {dynamic?, fallback, single, multiple, assert, context} ->
-          {dynamic_key?, keys, context} = of_finite_key_type(key, stack, context, of_fun)
+          {dynamic_key?, keys, context} = finite_key_type(key, stack, context, of_fun)
           {value_type, context} = of_fun.(value, stack, context)
           dynamic? = dynamic? or dynamic_key? or gradual?(value_type)
 
@@ -164,11 +164,11 @@ defmodule Module.Types.Of do
     if dynamic?, do: {dynamic(map), context}, else: {map, context}
   end
 
-  defp of_finite_key_type(key, _stack, context, _of_fun) when is_atom(key) do
+  defp finite_key_type(key, _stack, context, _of_fun) when is_atom(key) do
     {false, [key], context}
   end
 
-  defp of_finite_key_type(key, stack, context, of_fun) do
+  defp finite_key_type(key, stack, context, of_fun) do
     {key_type, context} = of_fun.(key, stack, context)
 
     case atom_fetch(key_type) do
diff --git a/lib/elixir/lib/module/types/pattern.ex b/lib/elixir/lib/module/types/pattern.ex
index a0b6f60c9ec..68b9bd95e18 100644
--- a/lib/elixir/lib/module/types/pattern.ex
+++ b/lib/elixir/lib/module/types/pattern.ex
@@ -25,48 +25,37 @@ defmodule Module.Types.Pattern do
      is refined, we restart at step 2.
 
   """
-  # TODO: The expected types for patterns/guards must always given as arguments.
-  # TODO: Perform full guard inference
-  def of_head(patterns, guards, meta, stack, context) do
+  def of_head(patterns, guards, expected, tag, meta, stack, context) do
     stack = %{stack | meta: meta}
-    dynamic = dynamic()
-    expected_types = Enum.map(patterns, fn _ -> dynamic end)
 
-    {_trees, types, context} = of_pattern_args(patterns, expected_types, stack, context)
+    {_trees, types, context} = of_pattern_args(patterns, expected, tag, stack, context)
     {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
     {types, context}
   end
 
-  defp of_pattern_args([], [], _stack, context) do
+  defp of_pattern_args([], [], _tag, _stack, context) do
     {[], [], context}
   end
 
-  defp of_pattern_args(patterns, expected_types, stack, context) do
+  defp of_pattern_args(patterns, expected, tag, stack, context) do
     context = init_pattern_info(context)
-    {trees, context} = of_pattern_args_index(patterns, expected_types, 0, [], stack, context)
+    {trees, context} = of_pattern_args_index(patterns, 0, [], stack, context)
 
     {types, context} =
-      of_pattern_recur(expected_types, stack, context, fn types, changed, context ->
-        of_pattern_args_tree(trees, types, changed, 0, [], stack, context)
+      of_pattern_recur(expected, tag, stack, context, fn types, changed, context ->
+        of_pattern_args_tree(trees, types, changed, 0, [], tag, stack, context)
       end)
 
     {trees, types, context}
   end
 
-  defp of_pattern_args_index(
-         [pattern | tail],
-         [type | expected_types],
-         index,
-         acc,
-         stack,
-         context
-       ) do
-    {tree, context} = of_pattern(pattern, [{:arg, index, type, pattern}], stack, context)
+  defp of_pattern_args_index([pattern | tail], index, acc, stack, context) do
+    {tree, context} = of_pattern(pattern, [{:arg, index, pattern}], stack, context)
     acc = [{pattern, tree} | acc]
-    of_pattern_args_index(tail, expected_types, index + 1, acc, stack, context)
+    of_pattern_args_index(tail, index + 1, acc, stack, context)
   end
 
-  defp of_pattern_args_index([], [], _index, acc, _stack, context),
+  defp of_pattern_args_index([], _index, acc, _stack, context),
     do: {Enum.reverse(acc), context}
 
   defp of_pattern_args_tree(
@@ -75,11 +64,13 @@ defmodule Module.Types.Pattern do
          [index | changed],
          index,
          acc,
+         tag,
          stack,
          context
        ) do
-    with {:ok, type, context} <- of_pattern_intersect(tree, type, pattern, stack, context) do
-      of_pattern_args_tree(tail, expected_types, changed, index + 1, [type | acc], stack, context)
+    with {:ok, type, context} <- of_pattern_intersect(tree, type, pattern, tag, stack, context) do
+      acc = [type | acc]
+      of_pattern_args_tree(tail, expected_types, changed, index + 1, acc, tag, stack, context)
     end
   end
 
@@ -89,35 +80,41 @@ defmodule Module.Types.Pattern do
          changed,
          index,
          acc,
+         tag,
          stack,
          context
        ) do
-    of_pattern_args_tree(tail, expected_types, changed, index + 1, [type | acc], stack, context)
+    acc = [type | acc]
+    of_pattern_args_tree(tail, expected_types, changed, index + 1, acc, tag, stack, context)
   end
 
-  defp of_pattern_args_tree([], [], [], _index, acc, _stack, context) do
+  defp of_pattern_args_tree([], [], [], _index, acc, _tag, _stack, context) do
     {:ok, Enum.reverse(acc), context}
   end
 
   @doc """
-  Return the type and typing context of a pattern expression with
-  the given expected and expr or an error in case of a typing conflict.
+  A simplified version of `of_head` used by `=` and `<-`.
+
+  This version tracks the whole expression in tracing,
+  instead of only the pattern.
   """
-  def of_match(pattern, expected, expr, stack, context) do
+  def of_match(pattern, guards \\ [], expected, expr, tag, stack, context) do
     context = init_pattern_info(context)
-    {tree, context} = of_pattern(pattern, [{:arg, 0, expected, expr}], stack, context)
+    {tree, context} = of_pattern(pattern, [{:arg, 0, expr}], stack, context)
 
     {[type], context} =
-      of_pattern_recur([expected], stack, context, fn [type], [0], context ->
-        with {:ok, type, context} <- of_pattern_intersect(tree, type, expr, stack, context) do
+      of_pattern_recur([expected], tag, stack, context, fn [type], [0], context ->
+        with {:ok, type, context} <-
+               of_pattern_intersect(tree, type, expr, tag, stack, context) do
           {:ok, [type], context}
         end
       end)
 
+    {_, context} = Enum.map_reduce(guards, context, &of_guard(&1, @guard, &1, stack, &2))
     {type, context}
   end
 
-  defp of_pattern_recur(types, stack, context, callback) do
+  defp of_pattern_recur(types, tag, stack, context, callback) do
     %{pattern_info: {pattern_vars, pattern_info, _counter}} = context
     context = nilify_pattern_info(context)
     pattern_vars = Map.to_list(pattern_vars)
@@ -126,7 +123,7 @@ defmodule Module.Types.Pattern do
     try do
       case callback.(types, changed, context) do
         {:ok, types, context} ->
-          of_pattern_recur(types, pattern_vars, pattern_info, stack, context, callback)
+          of_pattern_recur(types, pattern_vars, pattern_info, tag, stack, context, callback)
 
         {:error, context} ->
           {types, error_vars(pattern_vars, context)}
@@ -136,7 +133,7 @@ defmodule Module.Types.Pattern do
     end
   end
 
-  defp of_pattern_recur(types, vars, info, stack, context, callback) do
+  defp of_pattern_recur(types, vars, info, tag, stack, context, callback) do
     %{vars: context_vars} = context
 
     {changed, context} =
@@ -145,7 +142,7 @@ defmodule Module.Types.Pattern do
 
         {var_changed?, context} =
           Enum.reduce(paths, {false, context}, fn
-            [var, {:arg, index, expected, expr} | path], {var_changed?, context} ->
+            [var, {:arg, index, expr} | path], {var_changed?, context} ->
               actual = Enum.fetch!(types, index)
 
               case of_pattern_var(path, actual, true, info, context) do
@@ -161,9 +158,7 @@ defmodule Module.Types.Pattern do
                   end
 
                 :error ->
-                  # TODO: This should be precised about the operation (case/=/try/etc)
-                  context = Of.incompatible_error(expr, expected, actual, stack, context)
-                  throw({types, context})
+                  throw({types, to_badpattern_error(expr, tag, stack, context)})
               end
           end)
 
@@ -174,7 +169,7 @@ defmodule Module.Types.Pattern do
           true ->
             case paths do
               # A single change, check if there are other variables in this index.
-              [[_var, {:arg, index, _, _} | _]] ->
+              [[_var, {:arg, index, _} | _]] ->
                 case info do
                   %{^index => true} -> {[index | changed], context}
                   %{^index => false} -> {changed, context}
@@ -182,7 +177,7 @@ defmodule Module.Types.Pattern do
 
               # Several changes, we have to recompute all indexes.
               _ ->
-                var_changed = Enum.map(paths, fn [_var, {:arg, index, _, _} | _] -> index end)
+                var_changed = Enum.map(paths, fn [_var, {:arg, index, _} | _] -> index end)
                 {var_changed ++ changed, context}
             end
         end
@@ -195,9 +190,14 @@ defmodule Module.Types.Pattern do
       changed ->
         case callback.(types, changed, context) do
           # A simple structural comparison for optimization
-          {:ok, ^types, context} -> {types, context}
-          {:ok, types, context} -> of_pattern_recur(types, vars, info, stack, context, callback)
-          {:error, context} -> {types, error_vars(vars, context)}
+          {:ok, ^types, context} ->
+            {types, context}
+
+          {:ok, types, context} ->
+            of_pattern_recur(types, vars, info, tag, stack, context, callback)
+
+          {:error, context} ->
+            {types, error_vars(vars, context)}
         end
     end
   end
@@ -208,22 +208,25 @@ defmodule Module.Types.Pattern do
     end)
   end
 
-  defp of_pattern_intersect(tree, expected, expr, stack, context) do
-    actual = of_pattern_tree(tree, context)
-    type = intersection(actual, expected)
+  defp to_badpattern_error(expr, tag, stack, context) do
+    meta =
+      if meta = get_meta(expr) do
+        meta ++ Keyword.take(stack.meta, [:generated, :line])
+      else
+        stack.meta
+      end
 
-    cond do
-      not empty?(type) ->
-        {:ok, type, context}
+    error(__MODULE__, {:badpattern, expr, tag, context}, meta, stack, context)
+  end
 
-      empty?(actual) ->
-        # The pattern itself is invalid
-        meta = get_meta(expr) || stack.meta
-        {:error, error(__MODULE__, {:invalid_pattern, expr, context}, meta, stack, context)}
+  defp of_pattern_intersect(tree, expected, expr, tag, stack, context) do
+    actual = of_pattern_tree(tree, context)
+    type = intersection(actual, expected)
 
-      true ->
-        # TODO: This should be precised about the operation (case/=/try/etc)
-        {:error, Of.incompatible_error(expr, expected, actual, stack, context)}
+    if empty?(type) do
+      {:error, to_badpattern_error(expr, tag, stack, context)}
+    else
+      {:ok, type, context}
     end
   end
 
@@ -325,7 +328,7 @@ defmodule Module.Types.Pattern do
   end
 
   def of_match_var(ast, expected, expr, stack, context) do
-    of_match(ast, expected, expr, stack, context)
+    of_match(ast, expected, expr, {:match_var, expected}, stack, context)
   end
 
   ## Patterns
@@ -480,7 +483,7 @@ defmodule Module.Types.Pattern do
   defp of_pattern({name, meta, ctx} = var, reverse_path, _stack, context)
        when is_atom(name) and is_atom(ctx) do
     version = Keyword.fetch!(meta, :version)
-    [{:arg, arg, _type, _pattern} | _] = path = Enum.reverse(reverse_path)
+    [{:arg, arg, _pattern} | _] = path = Enum.reverse(reverse_path)
     {vars, info, counter} = context.pattern_info
 
     paths = [[var | path] | Map.get(vars, version, [])]
@@ -697,13 +700,22 @@ defmodule Module.Types.Pattern do
     Of.map_fetch(map_fetch, type, key, stack, context)
   end
 
-  # Remote
+  # Comparison operators
   def of_guard({{:., _, [:erlang, function]}, _, args}, _expected, expr, stack, context)
+      when function in [:==, :"/=", :"=:=", :"=/="] do
+    {_args_type, context} =
+      Enum.map_reduce(args, context, &of_guard(&1, dynamic(), expr, stack, &2))
+
+    {boolean(), context}
+  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))
 
-    Of.apply(:erlang, function, args_type, expr, stack, context)
+    Of.apply(:erlang, function, args_type, call, stack, context)
   end
 
   # var
@@ -725,20 +737,85 @@ defmodule Module.Types.Pattern do
     %{context | pattern_info: nil}
   end
 
-  def format_diagnostic({:invalid_pattern, expr, context}) do
-    traces = collect_traces(expr, context)
+  # $ type tag = head_pattern() or match_pattern()
+  #
+  # $ typep head_pattern =
+  #     :for_reduce or :with_else or :receive or :try_catch or :fn or :default or
+  #       {:try_else, type} or {:case, meta, type, expr}
+  #
+  # $ typep match_pattern =
+  #     :with or :for or {:match, type}
+  #
+  # The match pattern ones have the whole expression instead
+  # of a single pattern.
+  def format_diagnostic({:badpattern, pattern_or_expr, tag, context}) do
+    {to_trace, message} = badpattern(tag, pattern_or_expr)
+    traces = collect_traces(to_trace, context)
 
     %{
       details: %{typing_traces: traces},
-      message:
-        IO.iodata_to_binary([
-          """
-          the following pattern will never match:
-
-              #{expr_to_string(expr) |> indent(4)}
-          """,
-          format_traces(traces)
-        ])
+      message: IO.iodata_to_binary([message, format_traces(traces)])
     }
   end
+
+  defp badpattern({:try_else, type}, pattern) do
+    {pattern,
+     """
+     the following clause will never match:
+
+         #{expr_to_string(pattern) |> indent(4)}
+
+     it attempts to match on the result of the try do-block which has incompatible type:
+
+         #{to_quoted_string(type) |> indent(4)}
+     """}
+  end
+
+  defp badpattern({:case, meta, type, expr}, pattern) do
+    if meta[:type_check] == :expr do
+      {expr,
+       """
+       the following conditional expression will always evaluate to #{to_quoted_string(type)}:
+
+           #{expr_to_string(expr) |> indent(4)}
+       """}
+    else
+      {pattern,
+       """
+       the following clause will never match:
+
+           #{expr_to_string(pattern) |> indent(4)}
+
+       because it attempts to match on the result of:
+
+           #{expr_to_string(expr) |> indent(4)}
+
+       which has type:
+
+           #{to_quoted_string(type) |> indent(4)}
+       """}
+    end
+  end
+
+  defp badpattern({:match, type}, expr) do
+    {expr,
+     """
+     the following pattern will never match:
+
+         #{expr_to_string(expr) |> indent(4)}
+
+     because the right-hand side has type:
+
+         #{to_quoted_string(type) |> indent(4)}
+     """}
+  end
+
+  defp badpattern(_tag, pattern_or_expr) do
+    {pattern_or_expr,
+     """
+     the following pattern will never match:
+
+         #{expr_to_string(pattern_or_expr) |> indent(4)}
+     """}
+  end
 end
diff --git a/lib/elixir/src/elixir_erl_compiler.erl b/lib/elixir/src/elixir_erl_compiler.erl
index 0eb075d4df3..ea2eb7c8245 100644
--- a/lib/elixir/src/elixir_erl_compiler.erl
+++ b/lib/elixir/src/elixir_erl_compiler.erl
@@ -119,6 +119,12 @@ format_warnings(Opts, Warnings) ->
 handle_file_warning(_, _File, {_Line, v3_core, {map_key_repeated, _}}) -> ok;
 handle_file_warning(_, _File, {_Line, sys_core_fold, {ignored, useless_building}}) -> ok;
 
+%% We skip all of no_match related to no_clause, clause_type, guard, shadow.
+%% Those have too little information and they overlap with the type system.
+%% We keep the remaining ones because the Erlang compiler performs analyses
+%% on literals (including numbers), which the type system does not do.
+handle_file_warning(_, _File, {_Line, sys_core_fold, {nomatch, Reason}}) when is_atom(Reason) -> ok;
+
 %% Ignore all linting errors (only come up on parse transforms)
 handle_file_warning(_, _File, {_Line, erl_lint, _}) -> ok;
 
@@ -150,10 +156,6 @@ custom_format(sys_core_fold, {ignored, {no_effect, {erlang, F, A}}}) ->
   end,
   io_lib:format(Fmt, Args);
 
-%% Rewrite nomatch to be more generic, it can happen inside if, unless, and the like
-custom_format(sys_core_fold, {nomatch, X}) when X == guard; X == no_clause ->
-  "this check/guard will always yield the same result";
-
 custom_format(sys_core_fold, {nomatch, {shadow, Line, {ErlName, ErlArity}}}) ->
   {Name, Arity} = elixir_utils:erl_fa_to_elixir_fa(ErlName, ErlArity),
 
diff --git a/lib/elixir/src/elixir_erl_pass.erl b/lib/elixir/src/elixir_erl_pass.erl
index f4a1669f653..f1c13ca243b 100644
--- a/lib/elixir/src/elixir_erl_pass.erl
+++ b/lib/elixir/src/elixir_erl_pass.erl
@@ -302,9 +302,16 @@ translate(Other, Ann, S) ->
 
 translate_case(Meta, Expr, Opts, S) ->
   Ann = ?ann(Meta),
-  Clauses = elixir_erl_clauses:get_clauses(do, Opts, match),
   {TExpr, SE} = translate(Expr, Ann, S),
-  {TClauses, SC} = elixir_erl_clauses:clauses(Clauses, SE),
+  Clauses = elixir_erl_clauses:get_clauses(do, Opts, match),
+  RClauses =
+    %% For constructs that optimize booleans, we mark them as generated
+    %% to avoid reports from the Erlang compiler but specially Dialyzer.
+    case lists:member({optimize_boolean, true}, Meta) of
+      true -> [{N, ?generated(M), H, B} || {N, M, H, B} <- Clauses];
+      false -> Clauses
+    end,
+  {TClauses, SC} = elixir_erl_clauses:clauses(RClauses, SE),
   {{'case', Ann, TExpr, TClauses}, SC}.
 
 translate_list([{'|', _, [Left, Right]}], Ann, List, Acc) ->
diff --git a/lib/elixir/src/elixir_expand.erl b/lib/elixir/src/elixir_expand.erl
index f0b8a91ab7b..a6c6e913c99 100644
--- a/lib/elixir/src/elixir_expand.erl
+++ b/lib/elixir/src/elixir_expand.erl
@@ -720,15 +720,9 @@ expand_case(Meta, Expr, Opts, S, E) ->
   {EExpr, SE, EE} = expand(Expr, S, E),
 
   ROpts =
-    case proplists:get_value(optimize_boolean, Meta, false) of
-      true ->
-        case elixir_utils:returns_boolean(EExpr) of
-          true -> rewrite_case_clauses(Opts);
-          false -> generated_case_clauses(Opts)
-        end;
-
-      false ->
-        Opts
+    case lists:member({optimize_boolean, true}, Meta) andalso elixir_utils:returns_boolean(EExpr) of
+      true -> rewrite_case_clauses(Opts);
+      false -> Opts
     end,
 
   {EOpts, SO, EO} = elixir_clauses:'case'(Meta, ROpts, SE, EE),
@@ -752,19 +746,15 @@ rewrite_case_clauses([{do, [
 ]}]) ->
   rewrite_case_clauses(FalseMeta, FalseExpr, TrueMeta, TrueExpr);
 
-rewrite_case_clauses(Other) ->
-  generated_case_clauses(Other).
+rewrite_case_clauses(Opts) ->
+  Opts.
 
 rewrite_case_clauses(FalseMeta, FalseExpr, TrueMeta, TrueExpr) ->
   [{do, [
-    {'->', ?generated(FalseMeta), [[false], FalseExpr]},
-    {'->', ?generated(TrueMeta), [[true], TrueExpr]}
+    {'->', FalseMeta, [[false], FalseExpr]},
+    {'->', TrueMeta, [[true], TrueExpr]}
   ]}].
 
-generated_case_clauses([{do, Clauses}]) ->
-  RClauses = [{'->', ?generated(Meta), Args} || {'->', Meta, Args} <- Clauses],
-  [{do, RClauses}].
-
 %% Comprehensions
 
 expand_for({for, Meta, [_ | _] = Args}, S, E, Return) ->
diff --git a/lib/elixir/test/elixir/kernel/import_test.exs b/lib/elixir/test/elixir/kernel/import_test.exs
index d081de08adc..a17608e873e 100644
--- a/lib/elixir/test/elixir/kernel/import_test.exs
+++ b/lib/elixir/test/elixir/kernel/import_test.exs
@@ -219,7 +219,7 @@ defmodule Kernel.ImportTest do
   end
 
   test "import lexical on case" do
-    case true do
+    case Process.get(:unused, true) do
       false ->
         import List
         flatten([1, [2], 3])
diff --git a/lib/elixir/test/elixir/kernel/quote_test.exs b/lib/elixir/test/elixir/kernel/quote_test.exs
index d67784bb881..36f99d57c85 100644
--- a/lib/elixir/test/elixir/kernel/quote_test.exs
+++ b/lib/elixir/test/elixir/kernel/quote_test.exs
@@ -392,13 +392,12 @@ defmodule Kernel.QuoteTest.ErrorsTest do
   test "outside function error" do
     try do
       will_raise()
+      flunk("expected failure")
     rescue
       RuntimeError ->
         mod = Kernel.QuoteTest.ErrorsTest
         file = __ENV__.file |> Path.relative_to_cwd() |> String.to_charlist()
         assert [{^mod, _, _, [file: ^file, line: @line] ++ _} | _] = __STACKTRACE__
-    else
-      _ -> flunk("expected failure")
     end
   end
 end
diff --git a/lib/elixir/test/elixir/kernel/raise_test.exs b/lib/elixir/test/elixir/kernel/raise_test.exs
index 843bf74e210..35b23e84056 100644
--- a/lib/elixir/test/elixir/kernel/raise_test.exs
+++ b/lib/elixir/test/elixir/kernel/raise_test.exs
@@ -349,12 +349,12 @@ defmodule Kernel.RaiseTest do
     test "function clause error" do
       result =
         try do
-          zero(1)
+          Access.get(:ok, :error)
         rescue
           x in [FunctionClauseError] -> Exception.message(x)
         end
 
-      assert result == "no function clause matching in Kernel.RaiseTest.zero/1"
+      assert result == "no function clause matching in Access.get/3"
     end
 
     test "badarg error" do
@@ -450,7 +450,7 @@ defmodule Kernel.RaiseTest do
 
       result =
         try do
-          ^x = zero(0)
+          ^x = Process.get(:unused, 0)
         rescue
           x in [MatchError] -> Exception.message(x)
         end
@@ -483,7 +483,7 @@ defmodule Kernel.RaiseTest do
     test "bad map error" do
       result =
         try do
-          %{zero(0) | foo: :bar}
+          %{Process.get(:unused, 0) | foo: :bar}
         rescue
           x in [BadMapError] -> Exception.message(x)
         end
@@ -494,7 +494,7 @@ defmodule Kernel.RaiseTest do
     test "bad boolean error" do
       result =
         try do
-          1 and true
+          Process.get(:unused, 1) and true
         rescue
           x in [BadBooleanError] -> Exception.message(x)
         end
@@ -507,7 +507,7 @@ defmodule Kernel.RaiseTest do
 
       result =
         try do
-          case zero(0) do
+          case Process.get(:unused, 0) do
             ^x -> nil
           end
         rescue
@@ -521,7 +521,7 @@ defmodule Kernel.RaiseTest do
       result =
         try do
           cond do
-            !zero(0) -> :ok
+            !Process.get(:unused, 0) -> :ok
           end
         rescue
           x in [CondClauseError] -> Exception.message(x)
@@ -581,6 +581,4 @@ defmodule Kernel.RaiseTest do
              "function DoNotExist.for_sure/0 is undefined (module DoNotExist is not available). " <>
                "Make sure the module name is correct and has been specified in full (or that an alias has been defined)"
   end
-
-  defp zero(0), do: 0
 end
diff --git a/lib/elixir/test/elixir/kernel/warning_test.exs b/lib/elixir/test/elixir/kernel/warning_test.exs
index c29b2d5412e..832efd0dcd1 100644
--- a/lib/elixir/test/elixir/kernel/warning_test.exs
+++ b/lib/elixir/test/elixir/kernel/warning_test.exs
@@ -881,25 +881,6 @@ defmodule Kernel.WarningTest do
     assert map_size(%{System.unique_integer() => 1, System.unique_integer() => 2}) == 2
   end
 
-  test "unused guard" do
-    assert_warn_eval(
-      ["nofile:5:25\n", "this check/guard will always yield the same result"],
-      """
-      defmodule Sample do
-        def atom_case do
-          v = "bc"
-          case v do
-            _ when is_atom(v) -> :ok
-            _ -> :fail
-          end
-        end
-      end
-      """
-    )
-  after
-    purge(Sample)
-  end
-
   test "length(list) == 0 in guard" do
     assert_warn_eval(
       [
@@ -1212,19 +1193,6 @@ defmodule Kernel.WarningTest do
     purge(Sample)
   end
 
-  test "in guard empty list" do
-    assert_warn_eval(
-      ["nofile:2:7\n", "this check/guard will always yield the same result"],
-      """
-      defmodule Sample do
-        def a(x) when x in [], do: x
-      end
-      """
-    )
-  after
-    purge(Sample)
-  end
-
   test "no effect operator" do
     assert_warn_eval(
       ["nofile:3:7\n", "use of operator != has no effect"],
diff --git a/lib/elixir/test/elixir/kernel_test.exs b/lib/elixir/test/elixir/kernel_test.exs
index 613e6af8e98..dbf9ab84d0a 100644
--- a/lib/elixir/test/elixir/kernel_test.exs
+++ b/lib/elixir/test/elixir/kernel_test.exs
@@ -4,7 +4,10 @@ defmodule KernelTest do
   use ExUnit.Case, async: true
 
   # Skip these doctests are they emit warnings
-  doctest Kernel, except: [===: 2, !==: 2, is_nil: 1]
+  doctest Kernel,
+    except:
+      [===: 2, !==: 2, and: 2, or: 2] ++
+        [is_exception: 1, is_exception: 2, is_nil: 1, is_struct: 1, is_non_struct_map: 1]
 
   def id(arg), do: arg
   def id(arg1, arg2), do: {arg1, arg2}
@@ -298,8 +301,8 @@ defmodule KernelTest do
     assert (false and true) == false
     assert (false and 0) == false
     assert (false and raise("oops")) == false
-    assert ((x = true) and not x) == false
-    assert_raise BadBooleanError, fn -> 0 and 1 end
+    assert ((x = Process.get(:unused, true)) and not x) == false
+    assert_raise BadBooleanError, fn -> Process.get(:unused, 0) and 1 end
   end
 
   test "or/2" do
@@ -310,25 +313,27 @@ defmodule KernelTest do
     assert (false or false) == false
     assert (false or true) == true
     assert (false or 0) == 0
-    assert ((x = false) or not x) == true
-    assert_raise BadBooleanError, fn -> 0 or 1 end
+    assert ((x = Process.get(:unused, false)) or not x) == true
+    assert_raise BadBooleanError, fn -> Process.get(:unused, 0) or 1 end
   end
 
-  defp struct?(arg) when is_struct(arg), do: true
-  defp struct?(_arg), do: false
+  defp delegate_is_struct(arg), do: is_struct(arg)
+
+  defp guarded_is_struct(arg) when is_struct(arg), do: true
+  defp guarded_is_struct(_arg), do: false
 
   defp struct_or_map?(arg) when is_struct(arg) or is_map(arg), do: true
   defp struct_or_map?(_arg), do: false
 
   test "is_struct/1" do
-    assert is_struct(%{}) == false
-    assert is_struct([]) == false
-    assert is_struct(%Macro.Env{}) == true
-    assert is_struct(%{__struct__: "foo"}) == false
-    assert struct?(%Macro.Env{}) == true
-    assert struct?(%{__struct__: "foo"}) == false
-    assert struct?([]) == false
-    assert struct?(%{}) == false
+    assert delegate_is_struct(%{}) == false
+    assert delegate_is_struct([]) == false
+    assert delegate_is_struct(%Macro.Env{}) == true
+    assert delegate_is_struct(%{__struct__: "foo"}) == false
+    assert guarded_is_struct(%Macro.Env{}) == true
+    assert guarded_is_struct(%{__struct__: "foo"}) == false
+    assert guarded_is_struct([]) == false
+    assert guarded_is_struct(%{}) == false
   end
 
   test "is_struct/1 and other match works" do
@@ -337,8 +342,10 @@ defmodule KernelTest do
     assert struct_or_map?(10) == false
   end
 
-  defp struct?(arg, name) when is_struct(arg, name), do: true
-  defp struct?(_arg, _name), do: false
+  defp delegate_is_struct(arg, name), do: is_struct(arg, name)
+
+  defp guarded_is_struct(arg, name) when is_struct(arg, name), do: true
+  defp guarded_is_struct(_arg, _name), do: false
 
   defp struct_or_map?(arg, name) when is_struct(arg, name) or is_map(arg), do: true
   defp struct_or_map?(_arg, _name), do: false
@@ -346,16 +353,16 @@ defmodule KernelTest do
   defp not_atom(), do: "not atom"
 
   test "is_struct/2" do
-    assert is_struct(%{}, Macro.Env) == false
-    assert is_struct([], Macro.Env) == false
-    assert is_struct(%Macro.Env{}, Macro.Env) == true
-    assert is_struct(%Macro.Env{}, URI) == false
-    assert struct?(%Macro.Env{}, Macro.Env) == true
-    assert struct?(%Macro.Env{}, URI) == false
-    assert struct?(%{__struct__: "foo"}, "foo") == false
-    assert struct?(%{__struct__: "foo"}, Macro.Env) == false
-    assert struct?([], Macro.Env) == false
-    assert struct?(%{}, Macro.Env) == false
+    assert delegate_is_struct(%{}, Macro.Env) == false
+    assert delegate_is_struct([], Macro.Env) == false
+    assert delegate_is_struct(%Macro.Env{}, Macro.Env) == true
+    assert delegate_is_struct(%Macro.Env{}, URI) == false
+    assert guarded_is_struct(%Macro.Env{}, Macro.Env) == true
+    assert guarded_is_struct(%Macro.Env{}, URI) == false
+    assert guarded_is_struct(%{__struct__: "foo"}, "foo") == false
+    assert guarded_is_struct(%{__struct__: "foo"}, Macro.Env) == false
+    assert guarded_is_struct([], Macro.Env) == false
+    assert guarded_is_struct(%{}, Macro.Env) == false
 
     assert_raise ArgumentError, "argument error", fn ->
       is_struct(%{}, not_atom())
@@ -368,21 +375,23 @@ defmodule KernelTest do
     assert struct_or_map?(%Macro.Env{}, Macro.Env) == true
   end
 
-  defp non_struct_map?(arg) when is_non_struct_map(arg), do: true
-  defp non_struct_map?(_arg), do: false
+  defp delegate_is_non_struct_map(arg), do: is_non_struct_map(arg)
+
+  defp guarded_is_non_struct_map(arg) when is_non_struct_map(arg), do: true
+  defp guarded_is_non_struct_map(_arg), do: false
 
   defp non_struct_map_or_struct?(arg) when is_non_struct_map(arg) or is_struct(arg), do: true
   defp non_struct_map_or_struct?(_arg), do: false
 
   test "is_non_struct_map/1" do
-    assert is_non_struct_map(%{}) == true
-    assert is_non_struct_map([]) == false
-    assert is_non_struct_map(%Macro.Env{}) == false
-    assert is_non_struct_map(%{__struct__: "foo"}) == true
-    assert non_struct_map?(%Macro.Env{}) == false
-    assert non_struct_map?(%{__struct__: "foo"}) == true
-    assert non_struct_map?([]) == false
-    assert non_struct_map?(%{}) == true
+    assert delegate_is_non_struct_map(%{}) == true
+    assert delegate_is_non_struct_map([]) == false
+    assert delegate_is_non_struct_map(%Macro.Env{}) == false
+    assert delegate_is_non_struct_map(%{__struct__: "foo"}) == true
+    assert guarded_is_non_struct_map(%Macro.Env{}) == false
+    assert guarded_is_non_struct_map(%{__struct__: "foo"}) == true
+    assert guarded_is_non_struct_map([]) == false
+    assert guarded_is_non_struct_map(%{}) == true
   end
 
   test "is_non_struct_map/1 and other match works" do
@@ -391,21 +400,23 @@ defmodule KernelTest do
     assert non_struct_map_or_struct?(10) == false
   end
 
-  defp exception?(arg) when is_exception(arg), do: true
-  defp exception?(_arg), do: false
+  defp delegate_is_exception(arg), do: is_exception(arg)
+
+  defp guarded_is_exception(arg) when is_exception(arg), do: true
+  defp guarded_is_exception(_arg), do: false
 
   defp exception_or_map?(arg) when is_exception(arg) or is_map(arg), do: true
   defp exception_or_map?(_arg), do: false
 
   test "is_exception/1" do
-    assert is_exception(%{}) == false
-    assert is_exception([]) == false
-    assert is_exception(%RuntimeError{}) == true
-    assert is_exception(%{__exception__: "foo"}) == false
-    assert exception?(%RuntimeError{}) == true
-    assert exception?(%{__exception__: "foo"}) == false
-    assert exception?([]) == false
-    assert exception?(%{}) == false
+    assert delegate_is_exception(%{}) == false
+    assert delegate_is_exception([]) == false
+    assert delegate_is_exception(%RuntimeError{}) == true
+    assert delegate_is_exception(%{__exception__: "foo"}) == false
+    assert guarded_is_exception(%RuntimeError{}) == true
+    assert guarded_is_exception(%{__exception__: "foo"}) == false
+    assert guarded_is_exception([]) == false
+    assert guarded_is_exception(%{}) == false
   end
 
   test "is_exception/1 and other match works" do
@@ -414,26 +425,28 @@ defmodule KernelTest do
     assert exception_or_map?(10) == false
   end
 
-  defp exception?(arg, name) when is_exception(arg, name), do: true
-  defp exception?(_arg, _name), do: false
+  defp delegate_is_exception(arg, name), do: is_exception(arg, name)
+
+  defp guarded_is_exception(arg, name) when is_exception(arg, name), do: true
+  defp guarded_is_exception(_arg, _name), do: false
 
   defp exception_or_map?(arg, name) when is_exception(arg, name) or is_map(arg), do: true
   defp exception_or_map?(_arg, _name), do: false
 
   test "is_exception/2" do
-    assert is_exception(%{}, RuntimeError) == false
-    assert is_exception([], RuntimeError) == false
-    assert is_exception(%RuntimeError{}, RuntimeError) == true
-    assert is_exception(%RuntimeError{}, Macro.Env) == false
-    assert exception?(%RuntimeError{}, RuntimeError) == true
-    assert exception?(%RuntimeError{}, Macro.Env) == false
-    assert exception?(%{__exception__: "foo"}, "foo") == false
-    assert exception?(%{__exception__: "foo"}, RuntimeError) == false
-    assert exception?([], RuntimeError) == false
-    assert exception?(%{}, RuntimeError) == false
+    assert delegate_is_exception(%{}, RuntimeError) == false
+    assert delegate_is_exception([], RuntimeError) == false
+    assert delegate_is_exception(%RuntimeError{}, RuntimeError) == true
+    assert delegate_is_exception(%RuntimeError{}, Macro.Env) == false
+    assert guarded_is_exception(%RuntimeError{}, RuntimeError) == true
+    assert guarded_is_exception(%RuntimeError{}, Macro.Env) == false
+    assert guarded_is_exception(%{__exception__: "foo"}, "foo") == false
+    assert guarded_is_exception(%{__exception__: "foo"}, RuntimeError) == false
+    assert guarded_is_exception([], RuntimeError) == false
+    assert guarded_is_exception(%{}, RuntimeError) == false
 
     assert_raise ArgumentError, "argument error", fn ->
-      is_exception(%{}, not_atom())
+      delegate_is_exception(%{}, not_atom())
     end
   end
 
diff --git a/lib/elixir/test/elixir/macro_test.exs b/lib/elixir/test/elixir/macro_test.exs
index 227127855f8..eba21a11fe5 100644
--- a/lib/elixir/test/elixir/macro_test.exs
+++ b/lib/elixir/test/elixir/macro_test.exs
@@ -214,7 +214,7 @@ defmodule MacroTest do
     end
 
     defp expand_once_and_clean(quoted, env) do
-      cleaner = &Keyword.drop(&1, [:counter])
+      cleaner = &Keyword.drop(&1, [:counter, :type_check])
 
       quoted
       |> Macro.expand_once(env)
@@ -276,7 +276,7 @@ defmodule MacroTest do
   end
 
   defp expand_and_clean(quoted, env) do
-    cleaner = &Keyword.drop(&1, [:counter])
+    cleaner = &Keyword.drop(&1, [:counter, :type_check])
 
     quoted
     |> Macro.expand(env)
@@ -490,7 +490,7 @@ defmodule MacroTest do
     end
 
     test "with case" do
-      list = [1, 2, 3]
+      list = List.flatten([1, 2, 3])
 
       {result, formatted} =
         dbg_format(
diff --git a/lib/elixir/test/elixir/module/types/expr_test.exs b/lib/elixir/test/elixir/module/types/expr_test.exs
index cec8c4634cc..c39a469615b 100644
--- a/lib/elixir/test/elixir/module/types/expr_test.exs
+++ b/lib/elixir/test/elixir/module/types/expr_test.exs
@@ -143,7 +143,7 @@ defmodule Module.Types.ExprTest do
       assert typewarn!(URI.unknown("foo")) ==
                {dynamic(), "URI.unknown/1 is undefined or private"}
 
-      assert typewarn!(if(true, do: URI.unknown("foo"))) ==
+      assert typewarn!(if(:rand.uniform() > 0.5, do: URI.unknown("foo"))) ==
                {dynamic() |> union(atom([nil])), "URI.unknown/1 is undefined or private"}
 
       assert typewarn!(try(do: :ok, after: URI.unknown("foo"))) ==
@@ -755,9 +755,9 @@ defmodule Module.Types.ExprTest do
     end
 
     test "accessing an unknown field on struct with diagnostic" do
-      {type, diagnostic} = typediag!(%Point{}.foo_bar)
+      {type, [diagnostic]} = typediag!(%Point{}.foo_bar)
       assert type == dynamic()
-      assert diagnostic.span == {__ENV__.line - 2, 54}
+      assert diagnostic.span == {__ENV__.line - 2, 56}
 
       assert diagnostic.message == ~l"""
              unknown key .foo_bar in expression:
@@ -771,9 +771,9 @@ defmodule Module.Types.ExprTest do
     end
 
     test "accessing an unknown field on struct in a var with diagnostic" do
-      {type, diagnostic} = typediag!([x = %URI{}], x.foo_bar)
+      {type, [diagnostic]} = typediag!([x = %URI{}], x.foo_bar)
       assert type == dynamic()
-      assert diagnostic.span == {__ENV__.line - 2, 61}
+      assert diagnostic.span == {__ENV__.line - 2, 63}
 
       assert diagnostic.message == ~l"""
              unknown key .foo_bar in expression:
@@ -792,7 +792,7 @@ defmodule Module.Types.ExprTest do
                    scheme: term(),
                    userinfo: term()
                  })
-                 # from: types_test.ex:LINE-4:41
+                 # from: types_test.ex:LINE-4:43
                  x = %URI{}
              """
 
@@ -1014,6 +1014,63 @@ defmodule Module.Types.ExprTest do
                end
              ) == dynamic(atom([:ok, :error]))
     end
+
+    test "reports error from clause that will never match" do
+      assert typeerror!(
+               [x],
+               case Atom.to_string(x) do
+                 :error -> :error
+                 x -> x
+               end
+             ) == ~l"""
+             the following clause will never match:
+
+                 :error
+
+             because it attempts to match on the result of:
+
+                 Atom.to_string(x)
+
+             which has type:
+
+                 binary()
+             """
+    end
+
+    test "reports errors from multiple clauses" do
+      {type, [_, _]} =
+        typediag!(
+          [x],
+          case Atom.to_string(x) do
+            :ok -> :ok
+            :error -> :error
+          end
+        )
+
+      assert type == atom([:ok, :error])
+    end
+  end
+
+  describe "conditionals" do
+    test "if does not report on literal atoms" do
+      assert typecheck!(
+               if true do
+                 :ok
+               end
+             ) == atom([:ok, nil])
+    end
+
+    test "and does not report on literal atoms" do
+      assert typecheck!(false and true) == boolean()
+    end
+
+    test "and reports on non-atom literals" do
+      assert typeerror!(1 and true) == ~l"""
+             the following conditional expression will always evaluate to integer():
+
+                 1
+             """
+    end
   end
 
   describe "receive" do
@@ -1095,6 +1152,28 @@ defmodule Module.Types.ExprTest do
              ) == atom([:caught1, :caught2, :rescue, :else1, :else2])
     end
 
+    test "reports error from clause that will never match" do
+      assert typeerror!(
+               [x],
+               try do
+                 Atom.to_string(x)
+               rescue
+                 _ -> :ok
+               else
+                 :error -> :error
+                 x -> x
+               end
+             ) == ~l"""
+             the following clause will never match:
+
+                 :error
+
+             it attempts to match on the result of the try do-block which has incompatible type:
+
+                 binary()
+             """
+    end
+
     test "warns on undefined exceptions" do
       assert typewarn!(
                try do
diff --git a/lib/elixir/test/elixir/module/types/pattern_test.exs b/lib/elixir/test/elixir/module/types/pattern_test.exs
index 8f1f6ac79c4..d6131ae41df 100644
--- a/lib/elixir/test/elixir/module/types/pattern_test.exs
+++ b/lib/elixir/test/elixir/module/types/pattern_test.exs
@@ -76,7 +76,7 @@ defmodule Module.Types.PatternTest do
                  [info | _] = __ENV__.function
                  info
                )
-             ) =~ "incompatible types in expression"
+             ) =~ "the following pattern will never match"
     end
 
     test "does not check underscore" do
@@ -84,6 +84,26 @@ defmodule Module.Types.PatternTest do
     end
   end
 
+  describe "=" do
+    test "reports incompatible types" do
+      assert typeerror!([x = {:ok, _}], [_ | _] = x) == ~l"""
+             the following pattern will never match:
+
+                 [_ | _] = x
+
+             because the right-hand side has type:
+
+                 dynamic({:ok, term()})
+
+             where "x" was given the type:
+
+                 # type: dynamic({:ok, term()})
+                 # from: types_test.ex:LINE
+                 x = {:ok, _}
+             """
+    end
+  end
+
   describe "structs" do
     test "variable name" do
       assert typecheck!([%x{}], x) == dynamic(atom())
diff --git a/lib/elixir/test/elixir/module/types/type_helper.exs b/lib/elixir/test/elixir/module/types/type_helper.exs
index 018addf7442..0f7cd95e8ad 100644
--- a/lib/elixir/test/elixir/module/types/type_helper.exs
+++ b/lib/elixir/test/elixir/module/types/type_helper.exs
@@ -92,14 +92,11 @@ defmodule TypeHelper do
     do: raise("type checking ok but expected error: #{Descr.to_quoted_string(type)}")
 
   @doc false
-  def __typediag__!({type, %{warnings: [{module, warning, _locs}]}}),
-    do: {type, module.format_diagnostic(warning)}
+  def __typediag__!({type, %{warnings: [_ | _] = warnings}}),
+    do: {type, for({module, arg, _} <- warnings, do: module.format_diagnostic(arg))}
 
   def __typediag__!({type, %{warnings: []}}),
-    do: raise("type checking without warnings/errors: #{Descr.to_quoted_string(type)}")
-
-  def __typediag__!({_type, %{warnings: warnings}}),
-    do: raise("type checking with too many warnings/errors: #{inspect(warnings)}")
+    do: raise("type checking without diagnostics: #{Descr.to_quoted_string(type)}")
 
   @doc false
   def __typewarn__!({type, %{warnings: [{module, warning, _locs}], failed: false}}),
@@ -126,7 +123,8 @@ defmodule TypeHelper do
   end
 
   def __typeinfer__(patterns, guards) do
-    Pattern.of_head(patterns, guards, [], new_stack(:infer), new_context())
+    expected = Enum.map(patterns, fn _ -> Module.Types.Descr.dynamic() end)
+    Pattern.of_head(patterns, guards, expected, :default, [], new_stack(:infer), new_context())
   end
 
   defp typecheck(mode, patterns, guards, body, env) do
@@ -144,7 +142,11 @@ defmodule TypeHelper do
 
   def __typecheck__(mode, patterns, guards, body) do
     stack = new_stack(mode)
-    {_types, context} = Pattern.of_head(patterns, guards, [], stack, new_context())
+    expected = Enum.map(patterns, fn _ -> Module.Types.Descr.dynamic() end)
+
+    {_types, context} =
+      Pattern.of_head(patterns, guards, expected, :default, [], stack, new_context())
+
     Expr.of_expr(body, stack, context)
   end