diff --git a/mypy/binder.py b/mypy/binder.py
index 384bdca728b2..9a6da8b84cba 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -22,6 +22,7 @@
     TypeOfAny,
     TypeType,
     TypeVarType,
+    UninhabitedType,
     UnionType,
     UnpackType,
     find_unpack_in_list,
@@ -65,6 +66,7 @@ def __init__(self, id: int, conditional_frame: bool = False) -> None:
         self.unreachable = False
         self.conditional_frame = conditional_frame
         self.suppress_unreachable_warnings = False
+        self.unreachable_warning_emitted = False
 
     def __repr__(self) -> str:
         return f"Frame({self.id}, {self.types}, {self.unreachable}, {self.conditional_frame})"
@@ -166,6 +168,10 @@ def put(self, expr: Expression, typ: Type, *, from_assignment: bool = True) -> N
 
         This is used for isinstance() etc. Assignments should go through assign_type().
         """
+        proper_typ = get_proper_type(typ)
+        if isinstance(proper_typ, UninhabitedType) and not proper_typ.ambiguous:
+            self.frames[-1].unreachable = True
+
         if not isinstance(expr, (IndexExpr, MemberExpr, NameExpr)):
             return
         if not literal(expr):
@@ -183,6 +189,9 @@ def unreachable(self) -> None:
     def suppress_unreachable_warnings(self) -> None:
         self.frames[-1].suppress_unreachable_warnings = True
 
+    def emitted_unreachable_warning(self) -> None:
+        self.frames[-1].unreachable_warning_emitted = True
+
     def get(self, expr: Expression) -> Type | None:
         key = literal_hash(expr)
         assert key is not None, "Internal error: binder tried to get non-literal"
@@ -199,6 +208,9 @@ def is_unreachable(self) -> bool:
     def is_unreachable_warning_suppressed(self) -> bool:
         return any(f.suppress_unreachable_warnings for f in self.frames)
 
+    def is_unreachable_warning_emitted(self) -> bool:
+        return any(f.unreachable_warning_emitted for f in self.frames)
+
     def cleanse(self, expr: Expression) -> None:
         """Remove all references to a Node from the binder."""
         key = literal_hash(expr)
diff --git a/mypy/checker.py b/mypy/checker.py
index 04a286beef5e..c50006f23e5d 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -173,6 +173,7 @@
     ANY_STRATEGY,
     MYPYC_NATIVE_INT_NAMES,
     OVERLOAD_NAMES,
+    REVEAL_TYPE_NAMES,
     AnyType,
     BoolTypeQuery,
     CallableType,
@@ -459,15 +460,16 @@ def check_first_pass(self) -> None:
             )
             with self.tscope.module_scope(self.tree.fullname):
                 with self.enter_partial_types(), self.binder.top_frame_context():
+                    reported_unreachable = False
                     for d in self.tree.defs:
-                        if self.binder.is_unreachable():
+                        if not reported_unreachable and self.binder.is_unreachable():
                             if not self.should_report_unreachable_issues():
-                                break
-                            if not self.is_noop_for_reachability(d):
+                                reported_unreachable = True
+                            elif not self.is_noop_for_reachability(d):
                                 self.msg.unreachable_statement(d)
-                                break
-                        else:
-                            self.accept(d)
+                                self.binder.emitted_unreachable_warning()
+                                reported_unreachable = True
+                        self.accept(d)
 
                 assert not self.current_node_deferred
 
@@ -597,13 +599,12 @@ def accept_loop(
             partials_old = sum(len(pts.map) for pts in self.partial_types)
 
             # Disable error types that we cannot safely identify in intermediate iteration steps:
-            warn_unreachable = self.options.warn_unreachable
             warn_redundant = codes.REDUNDANT_EXPR in self.options.enabled_error_codes
-            self.options.warn_unreachable = False
             self.options.enabled_error_codes.discard(codes.REDUNDANT_EXPR)
 
             while True:
                 with self.binder.frame_context(can_skip=True, break_frame=2, continue_frame=1):
+                    self.binder.suppress_unreachable_warnings()
                     if on_enter_body is not None:
                         on_enter_body()
 
@@ -614,10 +615,9 @@ def accept_loop(
                 partials_old = partials_new
 
             # If necessary, reset the modified options and make up for the postponed error checks:
-            self.options.warn_unreachable = warn_unreachable
             if warn_redundant:
                 self.options.enabled_error_codes.add(codes.REDUNDANT_EXPR)
-            if warn_unreachable or warn_redundant:
+            if self.options.warn_unreachable or warn_redundant or self.options.strict_equality:
                 with self.binder.frame_context(can_skip=True, break_frame=2, continue_frame=1):
                     if on_enter_body is not None:
                         on_enter_body()
@@ -711,7 +711,7 @@ def extract_callable_type(self, inner_type: Type | None, ctx: Context) -> Callab
         """Get type as seen by an overload item caller."""
         inner_type = get_proper_type(inner_type)
         outer_type: FunctionLike | None = None
-        if inner_type is None or isinstance(inner_type, AnyType):
+        if inner_type is None or isinstance(inner_type, (AnyType, UninhabitedType)):
             return None
         if isinstance(inner_type, TypeVarLikeType):
             inner_type = get_proper_type(inner_type.upper_bound)
@@ -1193,6 +1193,9 @@ def check_func_def(
         for item, typ in expanded:
             old_binder = self.binder
             self.binder = ConditionalTypeBinder()
+            if old_binder.is_unreachable_warning_suppressed():
+                self.binder.suppress_unreachable_warnings()
+
             with self.binder.top_frame_context():
                 defn.expanded.append(item)
 
@@ -1380,6 +1383,7 @@ def check_func_def(
                                 new_frame = self.binder.push_frame()
                             new_frame.types[key] = narrowed_type
                             self.binder.declarations[key] = old_binder.declarations[key]
+
                 with self.scope.push_function(defn):
                     # We suppress reachability warnings for empty generator functions
                     # (return; yield) which have a "yield" that's unreachable by definition
@@ -3044,18 +3048,24 @@ def visit_block(self, b: Block) -> None:
         if b.is_unreachable:
             # This block was marked as being unreachable during semantic analysis.
             # It turns out any blocks marked in this way are *intentionally* marked
-            # as unreachable -- so we don't display an error.
+            # as unreachable -- so we don't display an error nor run type checking.
             self.binder.unreachable()
             return
+        reported_unreachable = False
         for s in b.body:
-            if self.binder.is_unreachable():
-                if not self.should_report_unreachable_issues():
+            if not reported_unreachable and self.binder.is_unreachable():
+                # TODO: should this guard against self.current_node_deferred too?
+                if self.binder.is_unreachable_warning_suppressed():
+                    # turns out in these cases we actually don't want to check code.
+                    # for instance, type var values
                     break
-                if not self.is_noop_for_reachability(s):
+                elif not self.should_report_unreachable_issues():
+                    reported_unreachable = True
+                elif not self.is_noop_for_reachability(s):
                     self.msg.unreachable_statement(s)
-                    break
-            else:
-                self.accept(s)
+                    self.binder.emitted_unreachable_warning()
+                    reported_unreachable = True
+            self.accept(s)
 
     def should_report_unreachable_issues(self) -> bool:
         return (
@@ -3063,6 +3073,7 @@ def should_report_unreachable_issues(self) -> bool:
             and self.options.warn_unreachable
             and not self.current_node_deferred
             and not self.binder.is_unreachable_warning_suppressed()
+            and not self.binder.is_unreachable_warning_emitted()
         )
 
     def is_noop_for_reachability(self, s: Statement) -> bool:
@@ -3081,7 +3092,9 @@ def is_noop_for_reachability(self, s: Statement) -> bool:
         elif isinstance(s, ExpressionStmt):
             if isinstance(s.expr, EllipsisExpr):
                 return True
-            elif isinstance(s.expr, CallExpr):
+            elif isinstance(s.expr, CallExpr) and not refers_to_fullname(
+                s.expr.callee, REVEAL_TYPE_NAMES
+            ):
                 with self.expr_checker.msg.filter_errors():
                     typ = get_proper_type(
                         self.expr_checker.accept(
@@ -4242,7 +4255,7 @@ def check_multi_assignment_from_iterable(
     ) -> None:
         rvalue_type = get_proper_type(rvalue_type)
         if self.type_is_iterable(rvalue_type) and isinstance(
-            rvalue_type, (Instance, CallableType, TypeType, Overloaded)
+            rvalue_type, (Instance, CallableType, TypeType, Overloaded, UninhabitedType)
         ):
             item_type = self.iterable_item_type(rvalue_type, context)
             for lv in lvalues:
@@ -5474,24 +5487,24 @@ def visit_match_stmt(self, s: MatchStmt) -> None:
                 )
                 pattern_type = self.pattern_checker.accept(p, current_subject_type)
                 with self.binder.frame_context(can_skip=True, fall_through=2):
-                    if b.is_unreachable or isinstance(
-                        get_proper_type(pattern_type.type), UninhabitedType
-                    ):
-                        self.push_type_map(None, from_assignment=False)
-                        else_map: TypeMap = {}
-                    else:
-                        pattern_map, else_map = conditional_types_to_typemaps(
-                            named_subject, pattern_type.type, pattern_type.rest_type
-                        )
-                        self.remove_capture_conflicts(pattern_type.captures, inferred_types)
-                        self.push_type_map(pattern_map, from_assignment=False)
-                        if pattern_map:
-                            for expr, typ in pattern_map.items():
-                                self.push_type_map(
-                                    self._get_recursive_sub_patterns_map(expr, typ),
-                                    from_assignment=False,
-                                )
-                        self.push_type_map(pattern_type.captures, from_assignment=False)
+                    # TODO: if this following code is necessary, find a failing test case.
+                    # if b.is_unreachable:
+                    #     self.push_type_map(None, from_assignment=False)
+                    #     else_map: TypeMap = {}
+                    # else:
+                    pattern_map, else_map = conditional_types_to_typemaps(
+                        named_subject, pattern_type.type, pattern_type.rest_type
+                    )
+                    self.remove_capture_conflicts(pattern_type.captures, inferred_types)
+                    self.push_type_map(pattern_map, from_assignment=False)
+                    if pattern_map:
+                        for expr, typ in pattern_map.items():
+                            self.push_type_map(
+                                self._get_recursive_sub_patterns_map(expr, typ),
+                                from_assignment=False,
+                            )
+                    self.push_type_map(pattern_type.captures, from_assignment=False)
+
                     if g is not None:
                         with self.binder.frame_context(can_skip=False, fall_through=3):
                             gt = get_proper_type(self.expr_checker.accept(g))
@@ -5506,6 +5519,9 @@ def visit_match_stmt(self, s: MatchStmt) -> None:
                             if isinstance(p, AsPattern):
                                 case_target = p.pattern or p.name
                                 if isinstance(case_target, NameExpr):
+                                    if guard_map is None:
+                                        guard_map = {case_target: UninhabitedType()}
+
                                     for type_map in (guard_map, else_map):
                                         if not type_map:
                                             continue
@@ -5870,15 +5886,11 @@ def conditional_callable_type_map(
 
         callables, uncallables = self.partition_by_callable(current_type, unsound_partition=False)
 
-        if callables and uncallables:
-            callable_map = {expr: UnionType.make_union(callables)} if callables else None
-            uncallable_map = {expr: UnionType.make_union(uncallables)} if uncallables else None
-            return callable_map, uncallable_map
-
-        elif callables:
-            return {}, None
-
-        return None, {}
+        callable_map = {expr: UnionType.make_union(callables) if callables else UninhabitedType()}
+        uncallable_map = {
+            expr: UnionType.make_union(uncallables) if uncallables else UninhabitedType()
+        }
+        return callable_map, uncallable_map
 
     def conditional_types_for_iterable(
         self, item_type: Type, iterable_type: Type
@@ -6088,7 +6100,7 @@ def find_isinstance_check(
         for example, some errors are suppressed.
 
         May return {}, {}.
-        Can return None, None in situations involving NoReturn.
+        Can return None, None in situations involving Never.
         """
         if_map, else_map = self.find_isinstance_check_helper(
             node, in_boolean_context=in_boolean_context
@@ -6223,12 +6235,17 @@ def find_isinstance_check_helper(
 
             if if_condition_map is not None:
                 if_map.update(if_condition_map)
+            else:
+                if_map[node.target] = UninhabitedType()
+
             if else_condition_map is not None:
                 else_map.update(else_condition_map)
+            else:
+                else_map[node.target] = UninhabitedType()
 
             return (
-                (None if if_assignment_map is None or if_condition_map is None else if_map),
-                (None if else_assignment_map is None or else_condition_map is None else else_map),
+                (None if if_assignment_map is None else if_map),
+                (None if else_assignment_map is None else else_map),
             )
         elif isinstance(node, OpExpr) and node.op == "and":
             left_if_vars, left_else_vars = self.find_isinstance_check(node.left)
@@ -6266,14 +6283,8 @@ def find_isinstance_check_helper(
         ):
             # Combine a `len(x) > 0` check with the default logic below.
             yes_type, no_type = self.narrow_with_len(self.lookup_type(node), ">", 0)
-            if yes_type is not None:
-                yes_type = true_only(yes_type)
-            else:
-                yes_type = UninhabitedType()
-            if no_type is not None:
-                no_type = false_only(no_type)
-            else:
-                no_type = UninhabitedType()
+            yes_type = true_only(yes_type)
+            no_type = false_only(no_type)
             if_map = {node: yes_type} if not isinstance(yes_type, UninhabitedType) else None
             else_map = {node: no_type} if not isinstance(no_type, UninhabitedType) else None
             return if_map, else_map
@@ -6289,8 +6300,8 @@ def find_isinstance_check_helper(
 
         if_type = true_only(vartype)
         else_type = false_only(vartype)
-        if_map = {node: if_type} if not isinstance(if_type, UninhabitedType) else None
-        else_map = {node: else_type} if not isinstance(else_type, UninhabitedType) else None
+        if_map = {node: if_type}  # if not isinstance(if_type, UninhabitedType) else None
+        else_map = {node: else_type}  # if not isinstance(else_type, UninhabitedType) else None
         return if_map, else_map
 
     def comparison_type_narrowing_helper(self, node: ComparisonExpr) -> tuple[TypeMap, TypeMap]:
@@ -6623,6 +6634,7 @@ def replay_lookup(new_parent_type: ProperType) -> Type | None:
             # Take each element in the parent union and replay the original lookup procedure
             # to figure out which parents are compatible.
             new_parent_types = []
+            expr_type_p = get_proper_type(expr_type)
             for item in flatten_nested_unions(parent_type.items):
                 member_type = replay_lookup(get_proper_type(item))
                 if member_type is None:
@@ -6630,14 +6642,14 @@ def replay_lookup(new_parent_type: ProperType) -> Type | None:
                     # parent type entirely and abort.
                     return output
 
-                if is_overlapping_types(member_type, expr_type):
-                    new_parent_types.append(item)
+                # note: this is not unconditionally setting `UninhabitedType`
+                #       as there might be X.a which is a Never
+                if isinstance(expr_type_p, UninhabitedType):
+                    if isinstance(get_proper_type(member_type), UninhabitedType):
+                        new_parent_types.append(item)
 
-            # If none of the parent types overlap (if we derived an empty union), something
-            # went wrong. We should never hit this case, but deriving the uninhabited type or
-            # reporting an error both seem unhelpful. So we abort.
-            if not new_parent_types:
-                return output
+                elif is_overlapping_types(member_type, expr_type):
+                    new_parent_types.append(item)
 
             expr = parent_expr
             expr_type = output[parent_expr] = make_simplified_union(new_parent_types)
@@ -6699,7 +6711,7 @@ def should_coerce_inner(typ: Type) -> bool:
             if target and not is_same_type(target, expr_type):
                 # We have multiple disjoint target types. So the 'if' branch
                 # must be unreachable.
-                return None, {}
+                return {operands[j]: UninhabitedType() for j in chain_indices}, {}
             target = expr_type
             possible_target_indices.append(i)
 
@@ -6946,8 +6958,8 @@ def find_tuple_len_narrowing(self, node: ComparisonExpr) -> list[tuple[TypeMap,
                     continue
                 for tpl in tuples:
                     yes_type, no_type = self.narrow_with_len(self.lookup_type(tpl), op, size)
-                    yes_map = None if yes_type is None else {tpl: yes_type}
-                    no_map = None if no_type is None else {tpl: no_type}
+                    yes_map: TypeMap = {tpl: yes_type}
+                    no_map: TypeMap = {tpl: no_type}
                     type_maps.append((yes_map, no_map))
             else:
                 left, right = items
@@ -6964,12 +6976,12 @@ def find_tuple_len_narrowing(self, node: ComparisonExpr) -> list[tuple[TypeMap,
                 yes_type, no_type = self.narrow_with_len(
                     self.lookup_type(left.args[0]), op, r_size
                 )
-                yes_map = None if yes_type is None else {left.args[0]: yes_type}
-                no_map = None if no_type is None else {left.args[0]: no_type}
+                yes_map = {left.args[0]: yes_type}
+                no_map = {left.args[0]: no_type}
                 type_maps.append((yes_map, no_map))
         return type_maps
 
-    def narrow_with_len(self, typ: Type, op: str, size: int) -> tuple[Type | None, Type | None]:
+    def narrow_with_len(self, typ: Type, op: str, size: int) -> tuple[Type, Type]:
         """Dispatch tuple type narrowing logic depending on the kind of type we got."""
         typ = get_proper_type(typ)
         if isinstance(typ, TupleType):
@@ -6985,27 +6997,19 @@ def narrow_with_len(self, typ: Type, op: str, size: int) -> tuple[Type | None, T
                     other_types.append(t)
                     continue
                 yt, nt = self.narrow_with_len(t, op, size)
-                if yt is not None:
-                    yes_types.append(yt)
-                if nt is not None:
-                    no_types.append(nt)
+                yes_types.append(yt)
+                no_types.append(nt)
+
             yes_types += other_types
             no_types += other_types
-            if yes_types:
-                yes_type = make_simplified_union(yes_types)
-            else:
-                yes_type = None
-            if no_types:
-                no_type = make_simplified_union(no_types)
-            else:
-                no_type = None
+
+            yes_type = make_simplified_union(yes_types)
+            no_type = make_simplified_union(no_types)
             return yes_type, no_type
         else:
             assert False, "Unsupported type for len narrowing"
 
-    def refine_tuple_type_with_len(
-        self, typ: TupleType, op: str, size: int
-    ) -> tuple[Type | None, Type | None]:
+    def refine_tuple_type_with_len(self, typ: TupleType, op: str, size: int) -> tuple[Type, Type]:
         """Narrow a TupleType using length restrictions."""
         unpack_index = find_unpack_in_list(typ.items)
         if unpack_index is None:
@@ -7013,8 +7017,8 @@ def refine_tuple_type_with_len(
             # depending on the current length, expected length, and the comparison op.
             method = int_op_to_method[op]
             if method(typ.length(), size):
-                return typ, None
-            return None, typ
+                return typ, UninhabitedType()
+            return UninhabitedType(), typ
         unpack = typ.items[unpack_index]
         assert isinstance(unpack, UnpackType)
         unpacked = get_proper_type(unpack.type)
@@ -7026,7 +7030,7 @@ def refine_tuple_type_with_len(
             if op in ("==", "is"):
                 if min_len <= size:
                     return typ, typ
-                return None, typ
+                return UninhabitedType(), typ
             elif op in ("<", "<="):
                 if op == "<=":
                     size += 1
@@ -7036,7 +7040,7 @@ def refine_tuple_type_with_len(
                     # TODO: also record max_len to avoid false negatives?
                     unpack = UnpackType(unpacked.copy_modified(min_len=size - typ.length() + 1))
                     return typ, typ.copy_modified(items=prefix + [unpack] + suffix)
-                return None, typ
+                return UninhabitedType(), typ
             else:
                 yes_type, no_type = self.refine_tuple_type_with_len(typ, neg_ops[op], size)
                 return no_type, yes_type
@@ -7051,7 +7055,7 @@ def refine_tuple_type_with_len(
             if min_len <= size:
                 # TODO: return fixed union + prefixed variadic tuple for no_type?
                 return typ.copy_modified(items=prefix + [arg] * (size - min_len) + suffix), typ
-            return None, typ
+            return UninhabitedType(), typ
         elif op in ("<", "<="):
             if op == "<=":
                 size += 1
@@ -7066,14 +7070,14 @@ def refine_tuple_type_with_len(
                 for n in range(size - min_len):
                     yes_items.append(typ.copy_modified(items=prefix + [arg] * n + suffix))
                 return UnionType.make_union(yes_items, typ.line, typ.column), no_type
-            return None, typ
+            return UninhabitedType(), typ
         else:
             yes_type, no_type = self.refine_tuple_type_with_len(typ, neg_ops[op], size)
             return no_type, yes_type
 
     def refine_instance_type_with_len(
         self, typ: Instance, op: str, size: int
-    ) -> tuple[Type | None, Type | None]:
+    ) -> tuple[Type, Type]:
         """Narrow a homogeneous tuple using length restrictions."""
         base = map_instance_to_supertype(typ, self.lookup_typeinfo("builtins.tuple"))
         arg = base.args[0]
@@ -7089,14 +7093,14 @@ def refine_instance_type_with_len(
                 size += 1
             if allow_precise:
                 unpack = UnpackType(self.named_generic_type("builtins.tuple", [arg]))
-                no_type: Type | None = TupleType(items=[arg] * size + [unpack], fallback=typ)
+                no_type: Type = TupleType(items=[arg] * size + [unpack], fallback=typ)
             else:
                 no_type = typ
             if allow_precise:
                 items = []
                 for n in range(size):
                     items.append(TupleType([arg] * n, fallback=typ))
-                yes_type: Type | None = UnionType.make_union(items, typ.line, typ.column)
+                yes_type: Type = UnionType.make_union(items, typ.line, typ.column)
             else:
                 yes_type = typ
             return yes_type, no_type
@@ -7551,7 +7555,9 @@ def note(
         self.msg.note(msg, context, offset=offset, code=code)
 
     def iterable_item_type(
-        self, it: Instance | CallableType | TypeType | Overloaded, context: Context
+        self,
+        it: Instance | CallableType | TypeType | Overloaded | UninhabitedType,
+        context: Context,
     ) -> Type:
         if isinstance(it, Instance):
             iterable = map_instance_to_supertype(it, self.lookup_typeinfo("typing.Iterable"))
@@ -8000,9 +8006,7 @@ def conditional_types_to_typemaps(
     maps: list[TypeMap] = []
     for typ in (yes_type, no_type):
         proper_type = get_proper_type(typ)
-        if isinstance(proper_type, UninhabitedType):
-            maps.append(None)
-        elif proper_type is None:
+        if proper_type is None:
             maps.append({})
         else:
             assert typ is not None
@@ -8130,7 +8134,9 @@ def and_conditional_maps(m1: TypeMap, m2: TypeMap, use_meet: bool = False) -> Ty
     result = m2.copy()
     m2_keys = {literal_hash(n2) for n2 in m2}
     for n1 in m1:
-        if literal_hash(n1) not in m2_keys or isinstance(get_proper_type(m1[n1]), AnyType):
+        if literal_hash(n1) not in m2_keys or isinstance(
+            get_proper_type(m1[n1]), (UninhabitedType, AnyType)
+        ):
             result[n1] = m1[n1]
     if use_meet:
         # For now, meet common keys only if specifically requested.
@@ -8150,9 +8156,9 @@ def or_conditional_maps(m1: TypeMap, m2: TypeMap, coalesce_any: bool = False) ->
     joining restrictions.
     """
 
-    if m1 is None:
+    if m1 is None or any(isinstance(get_proper_type(t1), UninhabitedType) for t1 in m1.values()):
         return m2
-    if m2 is None:
+    if m2 is None or any(isinstance(get_proper_type(t2), UninhabitedType) for t2 in m2.values()):
         return m1
     # Both conditions can be true. Combine information about
     # expressions whose type is refined by both conditions. (We do not
@@ -8216,11 +8222,16 @@ def convert_to_typetype(type_map: TypeMap) -> TypeMap:
         t = typ
         if isinstance(t, TypeVarType):
             t = t.upper_bound
+
+        if isinstance(get_proper_type(t), UninhabitedType):
+            converted_type_map[expr] = UninhabitedType()
+            continue
         # TODO: should we only allow unions of instances as per PEP 484?
-        if not isinstance(get_proper_type(t), (UnionType, Instance, NoneType)):
+        elif not isinstance(get_proper_type(t), (UnionType, Instance, NoneType)):
             # unknown type; error was likely reported earlier
             return {}
         converted_type_map[expr] = TypeType.make_normalized(typ)
+
     return converted_type_map
 
 
@@ -8489,7 +8500,7 @@ def is_valid_inferred_type(typ: Type, is_lvalue_final: bool = False) -> bool:
         # the context. This resolution happens in leave_partial_types when
         # we pop a partial types scope.
         return is_lvalue_final
-    elif isinstance(proper_type, UninhabitedType):
+    elif isinstance(proper_type, UninhabitedType) and proper_type.ambiguous:
         return False
     return not typ.accept(InvalidInferredTypes())
 
diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 4078d447dab8..49989506d390 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -1638,6 +1638,9 @@ def check_call(
                 object_type,
                 original_type=callee,
             )
+        elif isinstance(callee, UninhabitedType):
+            self.infer_arg_types_in_empty_context(args)
+            return (UninhabitedType(), UninhabitedType())
         else:
             return self.msg.not_callable(callee, context), AnyType(TypeOfAny.from_error)
 
@@ -1795,9 +1798,20 @@ def check_callable_call(
             callable_name,
         )
 
-        self.check_argument_types(
-            arg_types, arg_kinds, args, callee, formal_to_actual, context, object_type=object_type
-        )
+        if not (
+            isinstance(callable_node, RefExpr)
+            and callable_node.fullname in ("typing.assert_never", "typing_extensions.assert_never")
+            and self.chk.binder.is_unreachable()
+        ):
+            self.check_argument_types(
+                arg_types,
+                arg_kinds,
+                args,
+                callee,
+                formal_to_actual,
+                context,
+                object_type=object_type,
+            )
 
         if (
             callee.is_type_obj()
@@ -4273,11 +4287,18 @@ def check_boolean_op(self, e: OpExpr, context: Context) -> Type:
         elif e.op == "or":
             left_map, right_map = self.chk.find_isinstance_check(e.left)
 
+        left_impossible = left_map is None or any(
+            isinstance(get_proper_type(v), UninhabitedType) for v in left_map.values()
+        )
+        right_impossible = right_map is None or any(
+            isinstance(get_proper_type(v), UninhabitedType) for v in right_map.values()
+        )
+
         # If left_map is None then we know mypy considers the left expression
         # to be redundant.
         if (
             codes.REDUNDANT_EXPR in self.chk.options.enabled_error_codes
-            and left_map is None
+            and left_impossible
             # don't report an error if it's intentional
             and not e.right_always
         ):
@@ -4285,7 +4306,7 @@ def check_boolean_op(self, e: OpExpr, context: Context) -> Type:
 
         if (
             self.chk.should_report_unreachable_issues()
-            and right_map is None
+            and right_impossible
             # don't report an error if it's intentional
             and not e.right_unreachable
         ):
@@ -4293,14 +4314,14 @@ def check_boolean_op(self, e: OpExpr, context: Context) -> Type:
 
         right_type = self.analyze_cond_branch(right_map, e.right, expanded_left_type)
 
-        if left_map is None and right_map is None:
+        if left_impossible and right_impossible:
             return UninhabitedType()
 
-        if right_map is None:
+        if right_impossible:
             # The boolean expression is statically known to be the left value
             assert left_map is not None
             return left_type
-        if left_map is None:
+        if left_impossible:
             # The boolean expression is statically known to be the right value
             assert right_map is not None
             return right_type
@@ -5798,9 +5819,13 @@ def check_for_comp(self, e: GeneratorExpr | DictionaryComprehension) -> None:
                     self.chk.push_type_map(true_map)
 
                 if codes.REDUNDANT_EXPR in self.chk.options.enabled_error_codes:
-                    if true_map is None:
+                    if true_map is None or any(
+                        isinstance(get_proper_type(t), UninhabitedType) for t in true_map.values()
+                    ):
                         self.msg.redundant_condition_in_comprehension(False, condition)
-                    elif false_map is None:
+                    elif false_map is None or any(
+                        isinstance(get_proper_type(t), UninhabitedType) for t in false_map.values()
+                    ):
                         self.msg.redundant_condition_in_comprehension(True, condition)
 
     def visit_conditional_expr(self, e: ConditionalExpr, allow_none_return: bool = False) -> Type:
@@ -5811,9 +5836,13 @@ def visit_conditional_expr(self, e: ConditionalExpr, allow_none_return: bool = F
         # but only for the current expression
         if_map, else_map = self.chk.find_isinstance_check(e.cond)
         if codes.REDUNDANT_EXPR in self.chk.options.enabled_error_codes:
-            if if_map is None:
+            if if_map is None or any(
+                isinstance(get_proper_type(t), UninhabitedType) for t in if_map.values()
+            ):
                 self.msg.redundant_condition_in_if(False, e.cond)
-            elif else_map is None:
+            elif else_map is None or any(
+                isinstance(get_proper_type(t), UninhabitedType) for t in else_map.values()
+            ):
                 self.msg.redundant_condition_in_if(True, e.cond)
 
         if_type = self.analyze_cond_branch(
@@ -5890,17 +5919,28 @@ def analyze_cond_branch(
         node: Expression,
         context: Type | None,
         allow_none_return: bool = False,
-        suppress_unreachable_errors: bool = True,
+        suppress_unreachable_errors: bool | None = None,
     ) -> Type:
+        # TODO: default based on flag (default to `True` if flag is not passed)
+        unreachable_errors_suppressed = (
+            suppress_unreachable_errors
+            if suppress_unreachable_errors is not None
+            else self.chk.binder.is_unreachable_warning_suppressed()
+        )
         with self.chk.binder.frame_context(can_skip=True, fall_through=0):
-            if map is None:
+            self.chk.push_type_map(map)
+
+            if map is None or any(
+                isinstance(get_proper_type(t), UninhabitedType) for t in map.values()
+            ):
                 # We still need to type check node, in case we want to
                 # process it for isinstance checks later. Since the branch was
                 # determined to be unreachable, any errors should be suppressed.
-                with self.msg.filter_errors(filter_errors=suppress_unreachable_errors):
+
+                with self.msg.filter_errors(filter_errors=unreachable_errors_suppressed):
                     self.accept(node, type_context=context, allow_none_return=allow_none_return)
                 return UninhabitedType()
-            self.chk.push_type_map(map)
+
             return self.accept(node, type_context=context, allow_none_return=allow_none_return)
 
     #
diff --git a/mypy/checkmember.py b/mypy/checkmember.py
index 0994d0df400b..20d512c7c6bb 100644
--- a/mypy/checkmember.py
+++ b/mypy/checkmember.py
@@ -70,6 +70,7 @@
     TypeVarLikeType,
     TypeVarTupleType,
     TypeVarType,
+    UninhabitedType,
     UnionType,
     get_proper_type,
 )
@@ -253,6 +254,8 @@ def _analyze_member_access(
     elif isinstance(typ, DeletedType):
         mx.msg.deleted_as_rvalue(typ, mx.context)
         return AnyType(TypeOfAny.from_error)
+    elif isinstance(typ, UninhabitedType):
+        return UninhabitedType()
     return report_missing_attribute(mx.original_type, typ, name, mx)
 
 
diff --git a/mypy/checkpattern.py b/mypy/checkpattern.py
index 2a8620482d87..3f646e699524 100644
--- a/mypy/checkpattern.py
+++ b/mypy/checkpattern.py
@@ -140,12 +140,11 @@ def visit_as_pattern(self, o: AsPattern) -> PatternType:
         else:
             typ, rest_type, type_map = current_type, UninhabitedType(), {}
 
-        if not is_uninhabited(typ) and o.name is not None:
+        if o.name is not None:
             typ, _ = self.chk.conditional_types_with_intersection(
                 current_type, [get_type_range(typ)], o, default=current_type
             )
-            if not is_uninhabited(typ):
-                type_map[o.name] = typ
+            type_map[o.name] = typ
 
         return PatternType(typ, rest_type, type_map)
 
@@ -470,14 +469,14 @@ def visit_mapping_pattern(self, o: MappingPattern) -> PatternType:
         captures: dict[Expression, Type] = {}
         for key, value in zip(o.keys, o.values):
             inner_type = self.get_mapping_item_type(o, current_type, key)
-            if inner_type is None:
+            if is_uninhabited(inner_type):
                 can_match = False
-                inner_type = self.chk.named_type("builtins.object")
+
             pattern_type = self.accept(value, inner_type)
             if is_uninhabited(pattern_type.type):
                 can_match = False
-            else:
-                self.update_type_map(captures, pattern_type.captures)
+
+            self.update_type_map(captures, pattern_type.captures)
 
         if o.rest is not None:
             mapping = self.chk.named_type("typing.Mapping")
@@ -502,13 +501,13 @@ def visit_mapping_pattern(self, o: MappingPattern) -> PatternType:
 
     def get_mapping_item_type(
         self, pattern: MappingPattern, mapping_type: Type, key: Expression
-    ) -> Type | None:
+    ) -> Type:
         mapping_type = get_proper_type(mapping_type)
         if isinstance(mapping_type, TypedDictType):
             with self.msg.filter_errors() as local_errors:
-                result: Type | None = self.chk.expr_checker.visit_typeddict_index_expr(
-                    mapping_type, key
-                )[0]
+                result: Type = self.chk.expr_checker.visit_typeddict_index_expr(mapping_type, key)[
+                    0
+                ]
                 has_local_errors = local_errors.has_new_errors()
             # If we can't determine the type statically fall back to treating it as a normal
             # mapping
@@ -517,7 +516,7 @@ def get_mapping_item_type(
                     result = self.get_simple_mapping_item_type(pattern, mapping_type, key)
 
                     if local_errors.has_new_errors():
-                        result = None
+                        result = UninhabitedType()
         else:
             with self.msg.filter_errors():
                 result = self.get_simple_mapping_item_type(pattern, mapping_type, key)
diff --git a/mypyc/ir/pprint.py b/mypyc/ir/pprint.py
index ac0e791290ab..9bbc5679d248 100644
--- a/mypyc/ir/pprint.py
+++ b/mypyc/ir/pprint.py
@@ -222,15 +222,16 @@ def visit_call_c(self, op: CallC) -> str:
     def visit_primitive_op(self, op: PrimitiveOp) -> str:
         args = []
         arg_index = 0
-        type_arg_index = 0
+        # type_arg_index = 0
         for arg_type in zip(op.desc.arg_types):
             if arg_type:
                 args.append(self.format("%r", op.args[arg_index]))
                 arg_index += 1
             else:
-                assert op.type_args
-                args.append(self.format("%r", op.type_args[type_arg_index]))
-                type_arg_index += 1
+                assert False
+                # assert op.type_args
+                # args.append(self.format("%r", op.type_args[type_arg_index]))
+                # type_arg_index += 1
 
         args_str = ", ".join(args)
         if op.is_void:
diff --git a/mypyc/test-data/irbuild-match.test b/mypyc/test-data/irbuild-match.test
index 28aff3dcfc45..4b09afd9cf9d 100644
--- a/mypyc/test-data/irbuild-match.test
+++ b/mypyc/test-data/irbuild-match.test
@@ -1765,10 +1765,8 @@ def f(x):
     r10 :: object
     r11 :: object[1]
     r12 :: object_ptr
-    r13, r14 :: object
-    r15 :: i32
-    r16 :: bit
-    r17, r18 :: bool
+    r13 :: object
+    r14 :: bool
 L0:
     r0 = __main__.Foo :: type
     r1 = PyObject_IsInstance(x, r0)
@@ -1792,13 +1790,9 @@ L2:
     goto L8
 L3:
 L4:
-    r14 = box(bool, 0)
-    r15 = PyObject_IsTrue(r14)
-    r16 = r15 >= 0 :: signed
-    r17 = truncate r15: i32 to builtins.bool
-    if r17 goto L6 else goto L5 :: bool
+    if 0 goto L6 else goto L5 :: bool
 L5:
-    r18 = raise AssertionError('Unreachable')
+    r14 = raise AssertionError('Unreachable')
     unreachable
 L6:
     goto L8
diff --git a/mypyc/test-data/run-singledispatch.test b/mypyc/test-data/run-singledispatch.test
index 61e4897c96d6..9a0f20b7db5a 100644
--- a/mypyc/test-data/run-singledispatch.test
+++ b/mypyc/test-data/run-singledispatch.test
@@ -347,11 +347,6 @@ def verify_typeinfo(stub: TypeInfo, a: MaybeMissing[Type[Any]], b: List[str]) ->
     yield Error('in TypeInfo')
     yield Error('hello')
 
-@verify.register(TypeVarExpr)
-def verify_typevarexpr(stub: TypeVarExpr, a: MaybeMissing[Any], b: List[str]) -> Iterator[Error]:
-    if False:
-        yield None
-
 def verify_list(stub, a, b) -> List[str]:
     """Helper function that converts iterator of errors to list of messages"""
     return list(err.msg for err in verify(stub, a, b))
@@ -361,7 +356,6 @@ def test_verify() -> None:
     assert verify_list(MypyFile(), MISSING, ['a', 'b']) == ["shouldn't be missing"]
     assert verify_list(MypyFile(), 5, ['a', 'b']) == ['in TypeInfo', 'hello']
     assert verify_list(TypeInfo(), str, ['a', 'b']) == ['in TypeInfo', 'hello']
-    assert verify_list(TypeVarExpr(), 'a', ['x', 'y']) == []
 
 
 [case testArgsInRegisteredImplNamedDifferentlyFromMainFunction]
diff --git a/test-data/unit/check-callable.test b/test-data/unit/check-callable.test
index 39e6c4fa3ff1..300fd7bf0816 100644
--- a/test-data/unit/check-callable.test
+++ b/test-data/unit/check-callable.test
@@ -1,20 +1,22 @@
 [case testCallableDef]
+# flags: --warn-unreachable
 def f() -> None: pass
 
 if callable(f):
     f()
 else:
-    f += 5
+    _ = "unreachable"  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
 [case testCallableLambda]
+# flags: --warn-unreachable
 f = lambda: None
 
 if callable(f):
     f()
 else:
-    f += 5
+    _ = "unreachable"  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
@@ -194,6 +196,7 @@ else:
 [builtins fixtures/callable.pyi]
 
 [case testCallableCallableClasses]
+# flags: --warn-unreachable
 from typing import Union
 
 
@@ -214,7 +217,7 @@ if callable(a):
     5 + 'test'  # E: Unsupported operand types for + ("int" and "str")
 
 if not callable(b):
-    5 + 'test'
+    _ = "unreachable"  # E: Statement is unreachable
 
 if callable(c):
     reveal_type(c)  # N: Revealed type is "__main__.B"
@@ -224,6 +227,7 @@ else:
 [builtins fixtures/callable.pyi]
 
 [case testDecoratedCallMethods]
+# flags: --warn-unreachable
 from typing import Any, Callable, Union, TypeVar
 
 F = TypeVar('F', bound=Callable)
@@ -258,11 +262,11 @@ s4: Some4
 if callable(s1):
     1 + 'a'  # E: Unsupported operand types for + ("int" and "str")
 else:
-    2 + 'b'
+    _ = "unreachable"  # E: Statement is unreachable
 if callable(s2):
     1 + 'a'  # E: Unsupported operand types for + ("int" and "str")
 else:
-    2 + 'b'
+    _ = "unreachable"  # E: Statement is unreachable
 if callable(s3):
     1 + 'a'  # E: Unsupported operand types for + ("int" and "str")
 else:
@@ -306,15 +310,17 @@ T = TypeVar('T', int, Callable[[], int], Union[str, Callable[[], str]])
 
 def f(t: T) -> None:
     if callable(t):
-        reveal_type(t())  # N: Revealed type is "Any"  \
-            # N: Revealed type is "builtins.int"  \
-            # N: Revealed type is "builtins.str"
+        reveal_type(t())  # N: Revealed type is "Any" \
+                          # N: Revealed type is "builtins.int" \
+                          # N: Revealed type is "builtins.str"
     else:
-        reveal_type(t)  # N: Revealed type is "builtins.int"  # N: Revealed type is "builtins.str"
+        reveal_type(t)  # N: Revealed type is "builtins.int" \
+                        # N: Revealed type is "builtins.str"
 
 [builtins fixtures/callable.pyi]
 
 [case testCallableTypeVarBound]
+# flags: --warn-unreachable
 from typing import TypeVar
 
 
@@ -329,11 +335,12 @@ def f(t: T) -> str:
     if callable(t):
         return t()
     else:
-        return 5
+        return t()  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
 [case testCallableTypeType]
+# flags: --warn-unreachable
 from typing import Type
 
 
@@ -347,11 +354,12 @@ def f(t: T) -> A:
     if callable(t):
         return t()
     else:
-        return 5
+        return t()  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
 [case testCallableTypeUnion]
+# flags: --warn-unreachable
 from abc import ABCMeta, abstractmethod
 from typing import Type, Union
 
@@ -371,11 +379,12 @@ if callable(x):
     # Abstract classes raise an error when called, but are indeed `callable`
     pass
 else:
-    'test' + 5
+    _ = "unreachable"  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
 [case testCallableUnionOfTypes]
+# flags: --warn-unreachable
 from abc import ABCMeta, abstractmethod
 from typing import Type, Union
 
@@ -395,7 +404,7 @@ if callable(x):
     # Abstract classes raise an error when called, but are indeed `callable`
     pass
 else:
-    'test' + 5
+    _ = "unreachable"  # E: Statement is unreachable
 
 [builtins fixtures/callable.pyi]
 
@@ -501,10 +510,11 @@ if callable():  # E: Missing positional argument "x" in call to "callable"
 [builtins fixtures/callable.pyi]
 
 [case testCallableWithNoneArgs]
-
+# flags: --warn-unreachable
 fn = None
 if callable(fn):
-  fn()
+    _ = "unreachable"  # E: Statement is unreachable
+    fn()
 
 [builtins fixtures/callable.pyi]
 
diff --git a/test-data/unit/check-enum.test b/test-data/unit/check-enum.test
index a3abf53e29ac..33ba1e39bbcf 100644
--- a/test-data/unit/check-enum.test
+++ b/test-data/unit/check-enum.test
@@ -871,6 +871,7 @@ main:2: note: Revealed type is "Literal[1]?"
 main:2: note: Revealed type is "Literal['foo']?"
 
 [case testEnumReachabilityChecksBasic]
+# flags: --warn-unreachable
 from enum import Enum
 from typing import Literal
 
@@ -887,7 +888,8 @@ elif x is Foo.B:
 elif x is Foo.C:
     reveal_type(x)  # N: Revealed type is "Literal[__main__.Foo.C]"
 else:
-    reveal_type(x)  # No output here: this branch is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 reveal_type(x) # N: Revealed type is "Union[Literal[__main__.Foo.A], Literal[__main__.Foo.B], Literal[__main__.Foo.C]]"
 
 if Foo.A is x:
@@ -897,7 +899,8 @@ elif Foo.B is x:
 elif Foo.C is x:
     reveal_type(x)  # N: Revealed type is "Literal[__main__.Foo.C]"
 else:
-    reveal_type(x)  # No output here: this branch is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 reveal_type(x) # N: Revealed type is "Union[Literal[__main__.Foo.A], Literal[__main__.Foo.B], Literal[__main__.Foo.C]]"
 
 y: Foo
@@ -908,7 +911,8 @@ elif y is Foo.B:
 elif y is Foo.C:
     reveal_type(y)  # N: Revealed type is "Literal[__main__.Foo.C]"
 else:
-    reveal_type(y)  # No output here: this branch is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 reveal_type(y) # N: Revealed type is "__main__.Foo"
 
 if Foo.A is y:
@@ -918,11 +922,13 @@ elif Foo.B is y:
 elif Foo.C is y:
     reveal_type(y)  # N: Revealed type is "Literal[__main__.Foo.C]"
 else:
-    reveal_type(y)  # No output here: this branch is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 reveal_type(y) # N: Revealed type is "__main__.Foo"
 [builtins fixtures/bool.pyi]
 
 [case testEnumReachabilityChecksWithOrdering]
+# flags: --warn-unreachable
 from enum import Enum
 from typing import Literal
 
@@ -939,7 +945,8 @@ if x is Foo.A:
 elif x is Foo.B:
     reveal_type(x)  # N: Revealed type is "Literal[__main__.Foo.B]"
 else:
-    reveal_type(x)  # No output here: this branch is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 
 class Bar(Enum):
     __order__ = "A B"
@@ -954,7 +961,8 @@ if y is Bar.A:
 elif y is Bar.B:
     reveal_type(y)  # N: Revealed type is "Literal[__main__.Bar.B]"
 else:
-    reveal_type(y)  # No output here: this branch is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 
 x2: Foo
 if x2 is Foo.A:
@@ -962,7 +970,8 @@ if x2 is Foo.A:
 elif x2 is Foo.B:
     reveal_type(x2)  # N: Revealed type is "Literal[__main__.Foo.B]"
 else:
-    reveal_type(x2)  # No output here: this branch is unreachable
+    reveal_type(x2)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 
 y2: Bar
 if y2 is Bar.A:
@@ -970,10 +979,12 @@ if y2 is Bar.A:
 elif y2 is Bar.B:
     reveal_type(y2)  # N: Revealed type is "Literal[__main__.Bar.B]"
 else:
-    reveal_type(y2)  # No output here: this branch is unreachable
+    reveal_type(y2)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 [builtins fixtures/tuple.pyi]
 
 [case testEnumReachabilityChecksIndirect]
+# flags: --warn-unreachable
 from enum import Enum
 from typing import Final, Literal
 
@@ -1027,15 +1038,17 @@ if y is z:
     reveal_type(z)  # N: Revealed type is "Literal[__main__.Foo.A]?"
     accepts_foo_a(z)
 else:
-    reveal_type(y)  # No output: this branch is unreachable
-    reveal_type(z)  # No output: this branch is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
+    reveal_type(z)  # N: Revealed type is "Literal[__main__.Foo.A]?"
 if z is y:
     reveal_type(y)  # N: Revealed type is "Literal[__main__.Foo.A]"
     reveal_type(z)  # N: Revealed type is "Literal[__main__.Foo.A]?"
     accepts_foo_a(z)
 else:
-    reveal_type(y)  # No output: this branch is unreachable
-    reveal_type(z)  # No output: this branch is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Literal[__main__.Foo.A]"
+    reveal_type(z)  # N: Revealed type is "Never"
 [builtins fixtures/bool.pyi]
 
 [case testEnumReachabilityNoNarrowingForUnionMessiness]
@@ -1311,14 +1324,16 @@ reveal_type(y)      # N: Revealed type is "__main__.Foo"
 
 # The standard output when we end up inferring two disjoint facts about the same expr
 if x is Foo.A and x is Foo.B:
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "__main__.Foo"
 reveal_type(x)      # N: Revealed type is "__main__.Foo"
 
 # ..and we get the same result if we have two disjoint groups within the same comp expr
 if x is Foo.A < x is Foo.B:
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "__main__.Foo"
 reveal_type(x)      # N: Revealed type is "__main__.Foo"
@@ -1336,7 +1351,8 @@ class Foo(Enum):
 
 x: Foo
 if x is Foo.A is Foo.B:
-   reveal_type(x)   # E: Statement is unreachable
+   reveal_type(x)   # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
    reveal_type(x)   # N: Revealed type is "__main__.Foo"
 reveal_type(x)      # N: Revealed type is "__main__.Foo"
@@ -1344,7 +1360,8 @@ reveal_type(x)      # N: Revealed type is "__main__.Foo"
 literal_a: Literal[Foo.A]
 literal_b: Literal[Foo.B]
 if x is literal_a is literal_b:
-   reveal_type(x)   # E: Statement is unreachable
+   reveal_type(x)   # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
    reveal_type(x)   # N: Revealed type is "__main__.Foo"
 reveal_type(x)      # N: Revealed type is "__main__.Foo"
@@ -1352,7 +1369,8 @@ reveal_type(x)      # N: Revealed type is "__main__.Foo"
 final_a: Final = Foo.A
 final_b: Final = Foo.B
 if x is final_a is final_b:
-   reveal_type(x)   # E: Statement is unreachable
+   reveal_type(x)   # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
    reveal_type(x)   # N: Revealed type is "__main__.Foo"
 reveal_type(x)      # N: Revealed type is "__main__.Foo"
@@ -2286,7 +2304,8 @@ if e == MyEnum.A:
 elif e == MyEnum.B:
     reveal_type(e)  # N: Revealed type is "Literal[__main__.MyEnum.B]"
 else:
-    reveal_type(e)  # E: Statement is unreachable
+    reveal_type(e)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/dict.pyi]
 
 
diff --git a/test-data/unit/check-errorcodes.test b/test-data/unit/check-errorcodes.test
index 6ec246fb3a13..f25e2e8f0b06 100644
--- a/test-data/unit/check-errorcodes.test
+++ b/test-data/unit/check-errorcodes.test
@@ -519,6 +519,11 @@ if int() != str():  # E: Non-overlapping equality check (left operand type: "int
     pass
 if int() is str():  # E: Non-overlapping identity check (left operand type: "int", right operand type: "str")  [comparison-overlap]
     pass
+
+x = int()
+while True:
+    if x is str():  # E: Non-overlapping identity check (left operand type: "int", right operand type: "str")  [comparison-overlap]
+        pass
 [builtins fixtures/primitives.pyi]
 
 [case testErrorCodeMissingModule]
diff --git a/test-data/unit/check-functions.test b/test-data/unit/check-functions.test
index a0a6e9d60920..8494060ff909 100644
--- a/test-data/unit/check-functions.test
+++ b/test-data/unit/check-functions.test
@@ -1532,7 +1532,7 @@ def bar() -> None:
     if False:
         foo = 1
     else:
-        def foo(obj): ...
+        def foo(obj): ...  # E: Incompatible redefinition (redefinition with type "Callable[[Any], Any]", original type "int")
 
 def baz() -> None:
     if False:
diff --git a/test-data/unit/check-incremental.test b/test-data/unit/check-incremental.test
index 0c7e67e5444d..50de2c6dbc11 100644
--- a/test-data/unit/check-incremental.test
+++ b/test-data/unit/check-incremental.test
@@ -5415,10 +5415,9 @@ reveal_type(z)
 [out]
 tmp/c.py:2: note: Revealed type is "a.<subclass of "a.A" and "a.B">"
 [out2]
-tmp/b.py:2: error: Cannot determine type of "y"
-tmp/c.py:2: note: Revealed type is "Any"
+tmp/c.py:2: note: Revealed type is "Never"
 
-[case testIsInstanceAdHocIntersectionIncrementalUnreachaableToIntersection]
+[case testIsInstanceAdHocIntersectionIncrementalUnreachableToIntersection]
 import c
 [file a.py]
 class A:
@@ -5447,8 +5446,7 @@ from b import z
 reveal_type(z)
 [builtins fixtures/isinstance.pyi]
 [out]
-tmp/b.py:2: error: Cannot determine type of "y"
-tmp/c.py:2: note: Revealed type is "Any"
+tmp/c.py:2: note: Revealed type is "Never"
 [out2]
 tmp/c.py:2: note: Revealed type is "a.<subclass of "a.A" and "a.B">"
 
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 49140bf52b8d..a44419efa56f 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -378,6 +378,7 @@ while 2:
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnionTryFinally5]
+# flags: --warn-unreachable
 class A: pass
 
 class B(A):
@@ -391,7 +392,7 @@ while 2:
     finally:
         x.b    # E: "A" has no attribute "b"
         break
-        x.b
+        _ = "unreachable"  # E: Statement is unreachable
     x.b
 
 [case testUnionTryFinally6]
@@ -722,6 +723,7 @@ x + [1]               # E: Unsupported operand types for + ("int" and "List[int]
 [builtins fixtures/isinstancelist.pyi]
 
 [case testIsInstanceThreeUnion3]
+# flags: --warn-unreachable
 from typing import Union, List
 
 while bool():
@@ -731,11 +733,11 @@ while bool():
     if isinstance(x, int):
         x + 1
         break
-    elif isinstance(x, str):
+    elif isinstance(x, str):  # E: Statement is unreachable
+        _ = "unreachable"
         x + 'a'
         break
-    x + [1]           # These lines aren't reached because x was an int
-    x + 'a'
+    _ = "unreachable"  # E: Statement is unreachable
 x + [1]               # E: Unsupported operand types for + ("int" and "List[int]") \
                       # E: Unsupported operand types for + ("str" and "List[int]") \
                       # N: Left operand is of type "Union[int, str, List[int]]"
@@ -1048,9 +1050,10 @@ def last(x: LinkedList) -> Nil:
 [builtins fixtures/isinstance.pyi]
 
 [case testReturnAndFlow]
+# flags: --warn-unreachable
 def foo() -> int:
     return 1 and 2
-    return 'a'
+    _ = "unreachable"  # E: Statement is unreachable
 [case testCastIsinstance]
 from typing import Union
 
@@ -1066,15 +1069,17 @@ x + 'a'   # E: Unsupported operand types for + ("int" and "str")
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableCode]
+# flags: --warn-unreachable
 x = 1 # type: int
 
 while bool():
     x = 'a'           # E: Incompatible types in assignment (expression has type "str", variable has type "int")
     break
-    x = 'a'           # Note: no error because unreachable code
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableCode2]
+# flags: --warn-unreachable
 x = 1
 while bool():
     try:
@@ -1083,50 +1088,56 @@ while bool():
         continue
     else:
         continue
-    x + 'a'
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/isinstance.pyi]
 
 [case testUnreachableWhileTrue]
+# flags: --warn-unreachable
 def f(x: int) -> None:
     while True:
         if x:
             return
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/bool.pyi]
 
 [case testUnreachableAssertFalse]
+# flags: --warn-unreachable
 def f() -> None:
     assert False
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/bool.pyi]
 
 [case testUnreachableAssertFalse2]
+# flags: --warn-unreachable
 def f() -> None:
     # The old parser doesn't understand the syntax below
     assert False, "hi"
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/bool.pyi]
 
 [case testUnreachableReturnOrAssertFalse]
+# flags: --warn-unreachable
 def f(x: int) -> int:
     if x:
         return x
     else:
         assert False
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/bool.pyi]
 
 [case testUnreachableTryExcept]
+# flags: --warn-unreachable
 def f() -> None:
     try:
         f()
         return
     except BaseException:
         return
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/exception.pyi]
 
 [case testUnreachableTryExceptElse]
+# flags: --warn-unreachable
 def f() -> None:
     try:
         f()
@@ -1134,39 +1145,43 @@ def f() -> None:
         return
     else:
         return
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/exception.pyi]
 
 [case testUnreachableTryReturnFinally1]
+# flags: --warn-unreachable
 def f() -> None:
     try:
         return
     finally:
         pass
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 
 [case testUnreachableTryReturnFinally2]
+# flags: --warn-unreachable
 def f() -> None:
     try:
         pass
     finally:
         return
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 
 [case testUnreachableTryReturnExceptRaise]
+# flags: --warn-unreachable
 def f() -> None:
     try:
         return
     except:
         raise
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 
 [case testUnreachableReturnLambda]
+# flags: --warn-unreachable
 from typing import Callable
 def g(t: Callable[[int], int]) -> int: pass
 def f() -> int:
     return g(lambda x: x)
-    1()
+    _ = "unreachable"  # E: Statement is unreachable
 
 [case testIsinstanceAnd]
 class A: pass
@@ -1236,6 +1251,7 @@ else:
 [builtins fixtures/isinstancelist.pyi]
 
 [case testIsinstanceMultiAndSpecialCase]
+# flags: --warn-unreachable
 class A:
     # Ensure A.__add__ and int.__add__ are different to
     # force 'isinstance(y, int)' checks below to never succeed.
@@ -1250,12 +1266,14 @@ class C(A):
 x = B() # type: A
 y = C() # type: A
 
-if isinstance(x, B) and isinstance(y, int):
-    1() # type checking skipped
-if isinstance(y, int) and isinstance(x, B):
-    1() # type checking skipped
-if isinstance(y, int) and y > 42:
-    1() # type checking skipped
+if isinstance(x, B) and isinstance(y, int):  # E: Subclass of "A" and "int" cannot exist: would have incompatible method signatures
+    _ = "unreachable"  # E: Statement is unreachable
+if isinstance(y, int) and isinstance(x, B):  # E: Subclass of "A" and "int" cannot exist: would have incompatible method signatures \
+                                             # E: Right operand of "and" is never evaluated
+    _ = "unreachable"  # E: Statement is unreachable
+if isinstance(y, int) and y > 42:  # E: Subclass of "A" and "int" cannot exist: would have incompatible method signatures \
+                                   # E: Right operand of "and" is never evaluated
+    _ = "unreachable"  # E: Statement is unreachable
 [builtins fixtures/isinstancelist.pyi]
 
 [case testReturnWithCallExprAndIsinstance]
@@ -1341,6 +1359,7 @@ def f2(x: Union[FloatLike, IntLike]) -> None:
 [builtins fixtures/isinstance.pyi]
 
 [case testIsinstanceOfSuperclass]
+# flags: --warn-unreachable
 class A: pass
 class B(A): pass
 
@@ -1348,8 +1367,9 @@ x = B()
 if isinstance(x, A):
     reveal_type(x)  # N: Revealed type is "__main__.B"
 if not isinstance(x, A):
-    reveal_type(x)  # unreachable
-    x = A()
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
+    x = A()  # E: Incompatible types in assignment (expression has type "A", variable has type "B")
 reveal_type(x)  # N: Revealed type is "__main__.B"
 [builtins fixtures/isinstance.pyi]
 
@@ -1401,6 +1421,7 @@ def f(x: Union[List[int], str]) -> None:
 [builtins fixtures/isinstancelist.pyi]
 
 [case testIsinstanceOrIsinstance]
+# flags: --warn-unreachable
 class A: pass
 
 class B(A):
@@ -1418,12 +1439,13 @@ else:
     f = 0
 reveal_type(x1) # N: Revealed type is "__main__.A"
 x2 = A()
-if isinstance(x2, A) or isinstance(x2, C):
+if isinstance(x2, A) or isinstance(x2, C):  # E: Right operand of "or" is never evaluated
     reveal_type(x2) # N: Revealed type is "__main__.A"
     f = x2.flag # E: "A" has no attribute "flag"
 else:
     # unreachable
-    1()
+    reveal_type(x2)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 reveal_type(x2) # N: Revealed type is "__main__.A"
 [builtins fixtures/isinstance.pyi]
 
@@ -1508,11 +1530,13 @@ def f(x: Union[int, A], a: Type[A]) -> None:
 [builtins fixtures/isinstancelist.pyi]
 
 [case testIssubclassUnreachable]
+# flags: --warn-unreachable
 from typing import Type, Sequence, Union
 
 x: Type[str]
-if issubclass(x, int):
-    reveal_type(x)  # unreachable block
+if issubclass(x, int):  # E: Subclass of "str" and "int" cannot exist: would have incompatible method signatures
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 
 class X: pass
 class Y(X): pass
@@ -1522,7 +1546,8 @@ a: Union[Type[Y], Type[Z]]
 if issubclass(a, X):
     reveal_type(a)  # N: Revealed type is "Union[Type[__main__.Y], Type[__main__.Z]]"
 else:
-    reveal_type(a)  # unreachable block
+    reveal_type(a)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testIssubclasDestructuringUnions1]
@@ -1858,12 +1883,14 @@ def f(x: T) -> T:
 [builtins fixtures/isinstance.pyi]
 
 [case testIsinstanceAndTypeType]
+# flags: --warn-unreachable
 from typing import Type
 def f(x: Type[int]) -> None:
     if isinstance(x, type):
         reveal_type(x) # N: Revealed type is "Type[builtins.int]"
     else:
-        reveal_type(x)  # Unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     reveal_type(x) # N: Revealed type is "Type[builtins.int]"
 [builtins fixtures/isinstance.pyi]
 
@@ -2363,7 +2390,8 @@ class C:
 class Example(A, B): pass  # E: Definition of "f" in base class "A" is incompatible with definition in base class "B"
 x: A
 if isinstance(x, B):  # E: Subclass of "A" and "B" cannot exist: would have incompatible method signatures
-    reveal_type(x)    # E: Statement is unreachable
+    reveal_type(x)    # E: Statement is unreachable \
+                      # N: Revealed type is "Never"
 else:
     reveal_type(x)    # N: Revealed type is "__main__.A"
 
@@ -2371,7 +2399,8 @@ y: C
 if isinstance(y, B):
     reveal_type(y)        # N: Revealed type is "__main__.<subclass of "__main__.C" and "__main__.B">"
     if isinstance(y, A):  # E: Subclass of "C", "B", and "A" cannot exist: would have incompatible method signatures
-        reveal_type(y)    # E: Statement is unreachable
+        reveal_type(y)    # E: Statement is unreachable \
+                          # N: Revealed type is "Never"
 [builtins fixtures/isinstance.pyi]
 
 [case testIsInstanceAdHocIntersectionReversed]
@@ -2436,7 +2465,8 @@ class B:
 
 x: A[int]
 if isinstance(x, B):    # E: Subclass of "A[int]" and "B" cannot exist: would have incompatible method signatures
-    reveal_type(x)      # E: Statement is unreachable
+    reveal_type(x)      # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 else:
     reveal_type(x)      # N: Revealed type is "__main__.A[builtins.int]"
 
@@ -2606,7 +2636,8 @@ class B(Y, X): pass
 
 foo: A
 if isinstance(foo, B):  # E: Subclass of "A" and "B" cannot exist: would have inconsistent method resolution order
-    reveal_type(foo)    # E: Statement is unreachable
+    reveal_type(foo)    # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 [builtins fixtures/isinstance.pyi]
 
 [case testIsInstanceAdHocIntersectionAmbiguousClass]
@@ -2640,7 +2671,8 @@ x: Type[A]
 if issubclass(x, B):
     reveal_type(x)        # N: Revealed type is "Type[__main__.<subclass of "__main__.A" and "__main__.B">]"
     if issubclass(x, C):  # E: Subclass of "A", "B", and "C" cannot exist: would have incompatible method signatures
-        reveal_type(x)    # E: Statement is unreachable
+        reveal_type(x)    # E: Statement is unreachable \
+                          # N: Revealed type is "Never"
     else:
         reveal_type(x)    # N: Revealed type is "Type[__main__.<subclass of "__main__.A" and "__main__.B">]"
 else:
diff --git a/test-data/unit/check-literal.test b/test-data/unit/check-literal.test
index 88c02f70488c..e5dfe7e17832 100644
--- a/test-data/unit/check-literal.test
+++ b/test-data/unit/check-literal.test
@@ -2837,8 +2837,8 @@ w: Union[Truth, AlsoTruth]
 if w:
     reveal_type(w)  # N: Revealed type is "Union[__main__.Truth, __main__.AlsoTruth]"
 else:
-    reveal_type(w)  # E: Statement is unreachable
-
+    reveal_type(w)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/bool.pyi]
 
 [case testLiteralAndInstanceSubtyping]
diff --git a/test-data/unit/check-narrowing.test b/test-data/unit/check-narrowing.test
index 1856ca26f736..c1f1ae069c7b 100644
--- a/test-data/unit/check-narrowing.test
+++ b/test-data/unit/check-narrowing.test
@@ -263,7 +263,8 @@ else:
     reveal_type(x)  # N: Revealed type is "Union[__main__.Object1, __main__.Object2]"
 
 if x.key is Key.D:
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "Union[__main__.Object1, __main__.Object2]"
 [builtins fixtures/tuple.pyi]
@@ -289,7 +290,8 @@ else:
     reveal_type(x)  # N: Revealed type is "Union[TypedDict('__main__.TypedDict1', {'key': Union[Literal['A'], Literal['C']]}), TypedDict('__main__.TypedDict2', {'key': Union[Literal['B'], Literal['C']]})]"
 
 if x['key'] == 'D':
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "Union[TypedDict('__main__.TypedDict1', {'key': Union[Literal['A'], Literal['C']]}), TypedDict('__main__.TypedDict2', {'key': Union[Literal['B'], Literal['C']]})]"
 [builtins fixtures/primitives.pyi]
@@ -316,7 +318,8 @@ else:
     reveal_type(x)  # N: Revealed type is "Union[TypedDict('__main__.TypedDict1', {'key'?: Union[Literal['A'], Literal['C']]}), TypedDict('__main__.TypedDict2', {'key'?: Union[Literal['B'], Literal['C']]})]"
 
 if x['key'] == 'D':
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "Union[TypedDict('__main__.TypedDict1', {'key'?: Union[Literal['A'], Literal['C']]}), TypedDict('__main__.TypedDict2', {'key'?: Union[Literal['B'], Literal['C']]})]"
 [builtins fixtures/primitives.pyi]
@@ -606,8 +609,9 @@ else:
 
 y: Union[Parent1, Parent2]
 if y["model"]["key"] is Key.C:
-    reveal_type(y)              # E: Statement is unreachable
-    reveal_type(y["model"])
+    reveal_type(y)              # E: Statement is unreachable \
+                                # N: Revealed type is "Never"
+    reveal_type(y["model"])  # N: Revealed type is "Never"
 else:
     reveal_type(y)              # N: Revealed type is "Union[TypedDict('__main__.Parent1', {'model': TypedDict('__main__.Model1', {'key': Literal[__main__.Key.A]}), 'foo': builtins.int}), TypedDict('__main__.Parent2', {'model': TypedDict('__main__.Model2', {'key': Literal[__main__.Key.B]}), 'bar': builtins.str})]"
     reveal_type(y["model"])     # N: Revealed type is "Union[TypedDict('__main__.Model1', {'key': Literal[__main__.Key.A]}), TypedDict('__main__.Model2', {'key': Literal[__main__.Key.B]})]"
@@ -642,8 +646,9 @@ else:
 
 y: Union[Parent1, Parent2]
 if y["model"]["key"] == 'C':
-    reveal_type(y)              # E: Statement is unreachable
-    reveal_type(y["model"])
+    reveal_type(y)              # E: Statement is unreachable \
+                                # N: Revealed type is "Never"
+    reveal_type(y["model"])  # N: Revealed type is "Never"
 else:
     reveal_type(y)              # N: Revealed type is "Union[TypedDict('__main__.Parent1', {'model': TypedDict('__main__.Model1', {'key': Literal['A']}), 'foo': builtins.int}), TypedDict('__main__.Parent2', {'model': TypedDict('__main__.Model2', {'key': Literal['B']}), 'bar': builtins.str})]"
     reveal_type(y["model"])     # N: Revealed type is "Union[TypedDict('__main__.Model1', {'key': Literal['A']}), TypedDict('__main__.Model2', {'key': Literal['B']})]"
@@ -721,7 +726,8 @@ def test2(switch: FlipFlopEnum) -> None:
     switch.mutate()
 
     assert switch.state == State.B     # E: Non-overlapping equality check (left operand type: "Literal[State.A]", right operand type: "Literal[State.B]")
-    reveal_type(switch.state)          # E: Statement is unreachable
+    reveal_type(switch.state)          # E: Statement is unreachable \
+                                       # N: Revealed type is "Never"
 
 def test3(switch: FlipFlopEnum) -> None:
     # Same thing, but using 'is' comparisons. Previously mypy's behaviour differed
@@ -733,7 +739,8 @@ def test3(switch: FlipFlopEnum) -> None:
     switch.mutate()
 
     assert switch.state is State.B     # E: Non-overlapping identity check (left operand type: "Literal[State.A]", right operand type: "Literal[State.B]")
-    reveal_type(switch.state)          # E: Statement is unreachable
+    reveal_type(switch.state)          # E: Statement is unreachable \
+                                       # N: Revealed type is "Never"
 [builtins fixtures/primitives.pyi]
 
 [case testNarrowingEqualityRequiresExplicitStrLiteral]
@@ -893,8 +900,9 @@ else:
 
 # No contamination here
 if 1 == x == z:      # E: Non-overlapping equality check (left operand type: "Optional[Literal[1, 2]]", right operand type: "Default")
-    reveal_type(x)   # E: Statement is unreachable
-    reveal_type(z)
+    reveal_type(x)   # E: Statement is unreachable \
+                     # N: Revealed type is "Literal[1]"
+    reveal_type(z)  # N: Revealed type is "Never"
 else:
     reveal_type(x)   # N: Revealed type is "Union[Literal[1], Literal[2], None]"
     reveal_type(z)   # N: Revealed type is "__main__.Default"
@@ -909,9 +917,10 @@ b: Literal[1, 2]
 c: Literal[2, 3]
 
 if a == b == c:
-    reveal_type(a)  # E: Statement is unreachable
-    reveal_type(b)
-    reveal_type(c)
+    reveal_type(a)  # E: Statement is unreachable \
+                    # N: Revealed type is "Literal[1]"
+    reveal_type(b)  # N: Revealed type is "Literal[1]"
+    reveal_type(c)  # N: Revealed type is "Never"
 else:
     reveal_type(a)  # N: Revealed type is "Literal[1]"
     reveal_type(b)  # N: Revealed type is "Union[Literal[1], Literal[2]]"
@@ -920,7 +929,8 @@ else:
 if a == a == a:
     reveal_type(a)  # N: Revealed type is "Literal[1]"
 else:
-    reveal_type(a)  # E: Statement is unreachable
+    reveal_type(a)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 
 if a == a == b:
     reveal_type(a)  # N: Revealed type is "Literal[1]"
@@ -982,8 +992,9 @@ elif a == a == 4:
 else:
     # In contrast, this branch must be unreachable: we assume (maybe naively)
     # that 'a' won't be mutated in the middle of the expression.
-    reveal_type(a)  # E: Statement is unreachable
-    reveal_type(b)
+    reveal_type(a)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
+    reveal_type(b)  # N: Revealed type is "Union[Literal[1], Literal[2], Literal[3], Literal[4]]"
 [builtins fixtures/primitives.pyi]
 
 [case testNarrowingLiteralTruthiness]
@@ -1038,21 +1049,25 @@ f1: F1
 if isinstance(f1, F1):
     reveal_type(f1)  # N: Revealed type is "__main__.F1"
 else:
-    reveal_type(f1)  # E: Statement is unreachable
+    reveal_type(f1)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 
 if isinstance(n, F1):  # E: Subclass of "N" and "F1" cannot exist: "F1" is final
-    reveal_type(n)  # E: Statement is unreachable
+    reveal_type(n)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(n)  # N: Revealed type is "__main__.N"
 
 if isinstance(f1, N):  # E: Subclass of "F1" and "N" cannot exist: "F1" is final
-    reveal_type(f1)  # E: Statement is unreachable
+    reveal_type(f1)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 else:
     reveal_type(f1)  # N: Revealed type is "__main__.F1"
 
 if isinstance(f1, F2):  # E: Subclass of "F1" and "F2" cannot exist: "F1" is final \
                         # E: Subclass of "F1" and "F2" cannot exist: "F2" is final
-    reveal_type(f1)  # E: Statement is unreachable
+    reveal_type(f1)  # E: Statement is unreachable \
+                     # N: Revealed type is "Never"
 else:
     reveal_type(f1)  # N: Revealed type is "__main__.F1"
 [builtins fixtures/isinstance.pyi]
@@ -1081,7 +1096,8 @@ else:
 if isinstance(n_f2, F1):  # E: Subclass of "N" and "F1" cannot exist: "F1" is final \
                           # E: Subclass of "F2" and "F1" cannot exist: "F2" is final \
                           # E: Subclass of "F2" and "F1" cannot exist: "F1" is final
-    reveal_type(n_f2)  # E: Statement is unreachable
+    reveal_type(n_f2)  # E: Statement is unreachable \
+                       # N: Revealed type is "Never"
 else:
     reveal_type(n_f2)  # N: Revealed type is "Union[__main__.N, __main__.F2]"
 
@@ -1317,6 +1333,7 @@ else:
 [typing fixtures/typing-typeddict.pyi]
 
 [case testNarrowingRuntimeCover]
+# flags: --warn-unreachable
 from typing import Dict, List, Union
 
 def unreachable(x: Union[str, List[str]]) -> None:
@@ -1325,7 +1342,8 @@ def unreachable(x: Union[str, List[str]]) -> None:
     elif isinstance(x, list):
         reveal_type(x)  # N: Revealed type is "builtins.list[builtins.str]"
     else:
-        reveal_type(x)  # No output: this branch is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 def all_parts_covered(x: Union[str, List[str], List[int], int]) -> None:
     if isinstance(x, str):
@@ -1645,12 +1663,14 @@ from typing import Tuple, Union
 
 x: Union[Tuple[int, int], Tuple[int, int, int]]
 if len(x) >= 4:
-    reveal_type(x) # E: Statement is unreachable
+    reveal_type(x) # E: Statement is unreachable \
+                   # N: Revealed type is "Never"
 else:
     reveal_type(x) # N: Revealed type is "Union[Tuple[builtins.int, builtins.int], Tuple[builtins.int, builtins.int, builtins.int]]"
 
 if len(x) < 2:
-    reveal_type(x) # E: Statement is unreachable
+    reveal_type(x) # E: Statement is unreachable \
+                   # N: Revealed type is "Never"
 else:
     reveal_type(x) # N: Revealed type is "Union[Tuple[builtins.int, builtins.int], Tuple[builtins.int, builtins.int, builtins.int]]"
 [builtins fixtures/len.pyi]
@@ -1728,23 +1748,27 @@ from typing_extensions import TypeVarTuple, Unpack
 Ts = TypeVarTuple("Ts")
 def foo(x: Tuple[int, Unpack[Ts], str]) -> None:
     if len(x) == 1:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     else:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[Ts`-1], builtins.str]"
 
     if len(x) != 1:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[Ts`-1], builtins.str]"
     else:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 def bar(x: Tuple[int, Unpack[Ts], str]) -> None:
     if len(x) >= 2:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[Ts`-1], builtins.str]"
     else:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
     if len(x) < 2:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     else:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[Ts`-1], builtins.str]"
 [builtins fixtures/len.pyi]
@@ -1790,23 +1814,27 @@ from typing_extensions import Unpack
 
 def foo(x: Tuple[int, Unpack[Tuple[float, ...]], str]) -> None:
     if len(x) == 1:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     else:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[builtins.tuple[builtins.float, ...]], builtins.str]"
 
     if len(x) != 1:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[builtins.tuple[builtins.float, ...]], builtins.str]"
     else:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 def bar(x: Tuple[int, Unpack[Tuple[float, ...]], str]) -> None:
     if len(x) >= 2:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[builtins.tuple[builtins.float, ...]], builtins.str]"
     else:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
     if len(x) < 2:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     else:
         reveal_type(x)  # N: Revealed type is "Tuple[builtins.int, Unpack[builtins.tuple[builtins.float, ...]], builtins.str]"
 [builtins fixtures/len.pyi]
@@ -2081,8 +2109,8 @@ if isinstance(x, (Y, Z, NoneType)):
     reveal_type(x)  # N: Revealed type is "__main__.<subclass of "__main__.X" and "__main__.Y">"
 if isinstance(x, (Z, NoneType)):  # E: Subclass of "X" and "Z" cannot exist: "Z" is final \
                                   # E: Subclass of "X" and "NoneType" cannot exist: "NoneType" is final
-    reveal_type(x)  # E: Statement is unreachable
-
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/isinstance.pyi]
 
 [case testTypeNarrowingReachableNegative]
@@ -2413,3 +2441,22 @@ def foo(x: T) -> T:
     reveal_type(x)  # N: Revealed type is "T`-1"
     return x
 [builtins fixtures/isinstance.pyi]
+
+[case testNarrowingToClassWithNeverProperty]
+# flags: --warn-unreachable
+from typing import Never, Union
+
+class X:
+    a: Never
+
+class B:
+    a: str
+
+x: Union[X, B]
+# TODO: this should not be unreachable (`Never & int` is just `Never`)
+if isinstance(x.a, int):  # E: Subclass of "str" and "int" cannot exist: would have incompatible method signatures
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "__main__.X"
+else:
+    reveal_type(x)  # N: Revealed type is "Union[__main__.X, __main__.B]"
+[builtins fixtures/isinstancelist.pyi]
diff --git a/test-data/unit/check-overloading.test b/test-data/unit/check-overloading.test
index 243568c54253..481383671eec 100644
--- a/test-data/unit/check-overloading.test
+++ b/test-data/unit/check-overloading.test
@@ -3705,7 +3705,7 @@ reveal_type(mymap(f3, seq))  # N: Revealed type is "Union[typing.Iterable[builti
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowTypeNoStrictOptional1]
-# flags: --no-strict-optional
+# flags: --no-strict-optional --warn-unreachable
 from typing import overload, Union, NoReturn
 
 @overload
@@ -3730,13 +3730,14 @@ def test_narrow_int() -> None:
     c: str
     if int():
         c = narrow_int(c)
-        reveal_type(c)  # Note: branch is now dead, so no type is revealed
-                        # TODO: maybe we should make mypy report a warning instead?
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowTypeWithStrictOptional1]
+# flags: --warn-unreachable
 from typing import overload, Union, NoReturn
 
 @overload
@@ -3761,14 +3762,14 @@ def test_narrow_int() -> None:
     c: str
     if int():
         c = narrow_int(c)
-        reveal_type(c)  # Note: branch is now dead, so no type is revealed
-                        # TODO: maybe we should make mypy report a warning instead?
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowTypeNoStrictOptional2]
-# flags: --no-strict-optional
+# flags: --no-strict-optional --warn-unreachable
 from typing import overload, Union, TypeVar, NoReturn, Optional
 
 T = TypeVar('T')
@@ -3794,12 +3795,14 @@ def test_narrow_none() -> None:
     c: None
     if int():
         c = narrow_none(c)
-        reveal_type(c)  # Note: branch is now dead, so no type is revealed
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowTypeWithStrictOptional2]
+# flags: --warn-unreachable
 from typing import overload, Union, TypeVar, NoReturn, Optional
 
 T = TypeVar('T')
@@ -3825,14 +3828,15 @@ def test_narrow_none() -> None:
     c: None
     if int():
         c = narrow_none(c)
-        reveal_type(c)  # Branch is now dead
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 
 [case testOverloadsAndNoReturnNarrowTypeNoStrictOptional3]
-# flags: --no-strict-optional
+# flags: --no-strict-optional --warn-unreachable
 from typing import overload, TypeVar, NoReturn, Optional
 
 @overload
@@ -3857,12 +3861,14 @@ def test_narrow_none_v2() -> None:
     c: None
     if int():
         c = narrow_none_v2(c)
-        reveal_type(c)  # Note: branch is now dead, so no type is revealed
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowTypeWithStrictOptional3]
+# flags: --warn-unreachable
 from typing import overload, TypeVar, NoReturn, Optional
 
 @overload
@@ -3887,12 +3893,14 @@ def test_narrow_none_v2() -> None:
     c: None
     if int():
         c = narrow_none_v2(c)
-        reveal_type(c)  # Note: branch is now dead, so no type is revealed
+        reveal_type(c)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowWhenBlacklistingSubtype]
+# flags: --warn-unreachable
 from typing import TypeVar, NoReturn, Union, overload
 
 class Parent: ...
@@ -3917,12 +3925,14 @@ def test() -> None:
     val2: A
     if int():
         val2 = narrow_to_not_a(val2)
-        reveal_type(val2)  # Branch now dead
+        reveal_type(val2)  # E: Statement is unreachable \
+                           # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
 
 [case testOverloadsAndNoReturnNarrowWhenBlacklistingSubtype2]
+# flags: --warn-unreachable
 from typing import TypeVar, NoReturn, Union, overload
 
 class Parent: ...
@@ -3945,7 +3955,8 @@ def test_v2(val: Union[A, B], val2: A) -> None:
 
     if int():
         val2 = narrow_to_not_a_v2(val2)
-        reveal_type(val2)  # Branch now dead
+        reveal_type(val2)  # E: Statement is unreachable \
+                           # N: Revealed type is "Never"
 
 [builtins fixtures/isinstance.pyi]
 [typing fixtures/typing-medium.pyi]
diff --git a/test-data/unit/check-protocols.test b/test-data/unit/check-protocols.test
index a7124b7a83d3..287082e94d23 100644
--- a/test-data/unit/check-protocols.test
+++ b/test-data/unit/check-protocols.test
@@ -1714,6 +1714,7 @@ if isinstance(x, Iterable):
 [typing fixtures/typing-full.pyi]
 
 [case testConcreteClassesInProtocolsIsInstance]
+# flags: --warn-unreachable
 from typing import Protocol, runtime_checkable, TypeVar, Generic
 
 T = TypeVar('T')
@@ -1742,25 +1743,29 @@ c = C()
 if isinstance(c, P1):
     reveal_type(c) # N: Revealed type is "__main__.C"
 else:
-    reveal_type(c) # Unreachable
+    reveal_type(c)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 if isinstance(c, P):
     reveal_type(c) # N: Revealed type is "__main__.C"
 else:
-    reveal_type(c) # Unreachable
+    reveal_type(c)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 
 c1i: C1[int]
 if isinstance(c1i, P1):
     reveal_type(c1i) # N: Revealed type is "__main__.C1[builtins.int]"
 else:
-    reveal_type(c1i) # Unreachable
+    reveal_type(c1i)  # E: Statement is unreachable \
+                      # N: Revealed type is "Never"
 if isinstance(c1i, P):
     reveal_type(c1i) # N: Revealed type is "__main__.<subclass of "__main__.C1[builtins.int]" and "__main__.P">"
 else:
     reveal_type(c1i) # N: Revealed type is "__main__.C1[builtins.int]"
 
 c1s: C1[str]
-if isinstance(c1s, P1):
-    reveal_type(c1s) # Unreachable
+if isinstance(c1s, P1):  # E: Subclass of "C1[str]" and "P1" cannot exist: would have incompatible method signatures
+    reveal_type(c1s)  # E: Statement is unreachable \
+                      # N: Revealed type is "Never"
 else:
     reveal_type(c1s) # N: Revealed type is "__main__.C1[builtins.str]"
 
diff --git a/test-data/unit/check-python310.test b/test-data/unit/check-python310.test
index 016f50552a5f..7ececb6c823b 100644
--- a/test-data/unit/check-python310.test
+++ b/test-data/unit/check-python310.test
@@ -26,12 +26,14 @@ match m:
 [builtins fixtures/primitives.pyi]
 
 [case testMatchLiteralPatternUnreachable]
+# flags: --warn-unreachable
 # primitives are needed because otherwise mypy doesn't see that int and str are incompatible
 m: int
 
 match m:
     case "str":
-        reveal_type(m)
+        reveal_type(m)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 [builtins fixtures/primitives.pyi]
 
 -- Value Pattern --
@@ -70,14 +72,16 @@ class B: ...
 b: B
 
 [case testMatchValuePatternUnreachable]
+# flags: --warn-unreachable
 # primitives are needed because otherwise mypy doesn't see that int and str are incompatible
 import b
 
 m: int
 
 match m:
-    case b.b:
-        reveal_type(m)
+    case b.b:  # E: Subclass of "int" and "str" cannot exist: would have incompatible method signatures
+        reveal_type(m)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 [file b.py]
 b: str
 [builtins fixtures/primitives.pyi]
@@ -169,6 +173,7 @@ match m:
 [builtins fixtures/list.pyi]
 
 [case testMatchSequencePatternMatches]
+# flags: --warn-unreachable
 import array, collections
 from typing import Sequence, Iterable
 
@@ -219,15 +224,21 @@ match m8:
 
 match m9:
     case [i]:
-        reveal_type(i)
+        reveal_type(i)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "i" \
+                        # N: Revealed type is "Any"
 
 match m10:
     case [j]:
-        reveal_type(j)
+        reveal_type(j)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "j" \
+                        # N: Revealed type is "Any"
 
 match m11:
     case [k]:
-        reveal_type(k)
+        reveal_type(k)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "k" \
+                        # N: Revealed type is "Any"
 [builtins fixtures/primitives.pyi]
 [typing fixtures/typing-full.pyi]
 
@@ -244,24 +255,33 @@ match m:
 [builtins fixtures/list.pyi]
 
 [case testMatchSequencePatternTupleTooLong]
+# flags: --warn-unreachable
 from typing import Tuple
 m: Tuple[int, str]
 
 match m:
     case [a, b, c]:
-        reveal_type(a)
-        reveal_type(b)
-        reveal_type(c)
+        reveal_type(a)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "a" \
+                        # N: Revealed type is "Any"
+        reveal_type(b)  # E: Cannot determine type of "b" \
+                        # N: Revealed type is "Any"
+        reveal_type(c)  # E: Cannot determine type of "c" \
+                        # N: Revealed type is "Any"
 [builtins fixtures/list.pyi]
 
 [case testMatchSequencePatternTupleTooShort]
+# flags: --warn-unreachable
 from typing import Tuple
 m: Tuple[int, str, bool]
 
 match m:
     case [a, b]:
-        reveal_type(a)
-        reveal_type(b)
+        reveal_type(a)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "a" \
+                        # N: Revealed type is "Any"
+        reveal_type(b)  # E: Cannot determine type of "b" \
+                        # N: Revealed type is "Any"
 [builtins fixtures/list.pyi]
 
 [case testMatchSequencePatternTupleNarrows]
@@ -298,15 +318,20 @@ match m:
 [builtins fixtures/list.pyi]
 
 [case testMatchSequencePatternTupleStarredTooShort]
+# flags: --warn-unreachable
 from typing import Tuple
 m: Tuple[int]
 reveal_type(m)  # N: Revealed type is "Tuple[builtins.int]"
 
 match m:
     case [a, *b, c]:
-        reveal_type(a)
-        reveal_type(b)
-        reveal_type(c)
+        reveal_type(a)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "a" \
+                        # N: Revealed type is "Any"
+        reveal_type(b)  # E: Cannot determine type of "b" \
+                        # N: Revealed type is "Any"
+        reveal_type(c)  # E: Cannot determine type of "c" \
+                        # N: Revealed type is "Any"
 [builtins fixtures/list.pyi]
 
 [case testMatchNonMatchingSequencePattern]
@@ -505,6 +530,7 @@ a: str
 [typing fixtures/typing-typeddict.pyi]
 
 [case testMatchMappingPatternCapturesTypedDictUnreachable]
+# flags: --warn-unreachable
 # TypedDict keys are always str, so this is actually unreachable
 from typing import TypedDict
 import b
@@ -517,9 +543,11 @@ m: A
 
 match m:
     case {1: v}:
-        reveal_type(v)
+        reveal_type(v)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     case {b.b: v2}:
-        reveal_type(v2)
+        reveal_type(v2)  # E: Statement is unreachable \
+                         # N: Revealed type is "Never"
 [file b.py]
 b: int
 [typing fixtures/typing-typeddict.pyi]
@@ -831,6 +859,7 @@ match m:
         reveal_type(i)  # N: Revealed type is "builtins.int"
 
 [case testMatchClassPatternCaptureFilledGenericTypeAlias]
+# flags: --warn-unreachable
 from typing import Generic, TypeVar
 
 T = TypeVar('T')
@@ -844,7 +873,9 @@ m: object
 
 match m:
     case B(a=i):  # E: Class pattern class must not be a type alias with type parameters
-        reveal_type(i)
+        reveal_type(i)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "i" \
+                        # N: Revealed type is "Any"
 
 [case testMatchClassPatternCaptureGenericTypeAlias]
 from typing import Generic, TypeVar
@@ -1003,13 +1034,17 @@ match m:
 [builtins fixtures/tuple.pyi]
 
 [case testMatchClassPatternIsNotType]
+# flags: --warn-unreachable
 a = 1
 m: object
 
 match m:
     case a(i, j):  # E: Expected type in class pattern; found "builtins.int"
-        reveal_type(i)
-        reveal_type(j)
+        reveal_type(i)  # E: Statement is unreachable \
+                        # E: Cannot determine type of "i" \
+                        # N: Revealed type is "Any"
+        reveal_type(j)  # E: Cannot determine type of "j" \
+                        # N: Revealed type is "Any"
 
 [case testMatchClassPatternAny]
 from typing import Any
@@ -1288,11 +1323,13 @@ match m:
         reveal_type(a)  # N: Revealed type is "builtins.str"
 
 [case testMatchAlwaysFalsePatternGuard]
+# flags: --warn-unreachable
 m: str
 
 match m:
     case a if False:
-        reveal_type(a)
+        reveal_type(a)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 [case testMatchRedefiningPatternGuard]
 m: str
@@ -1328,11 +1365,13 @@ match m:
 [builtins fixtures/isinstancelist.pyi]
 
 [case testMatchUnreachablePatternGuard]
+# flags: --warn-unreachable
 m: str
 
 match m:
-    case a if isinstance(a, int):
-        reveal_type(a)
+    case a if isinstance(a, int):  # E: Subclass of "str" and "int" cannot exist: would have incompatible method signatures
+        reveal_type(a)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 -- Exhaustiveness --
@@ -2297,6 +2336,7 @@ def f4(e: int | str | bytes) -> int:
 [builtins fixtures/primitives.pyi]
 
 [case testMatchSequencePatternVariadicTupleNotTooShort]
+# flags: --warn-unreachable
 from typing import Tuple
 from typing_extensions import Unpack
 
@@ -2310,8 +2350,11 @@ match fm1:
 fm2: Tuple[int, int, Unpack[Tuple[str, ...]], int]
 match fm2:
     case [fa2, fb2]:
-        reveal_type(fa2)
-        reveal_type(fb2)
+        reveal_type(fa2)  # E: Statement is unreachable \
+                          # E: Cannot determine type of "fa2" \
+                          # N: Revealed type is "Any"
+        reveal_type(fb2)  # E: Cannot determine type of "fb2" \
+                          # N: Revealed type is "Any"
 
 fm3: Tuple[int, int, Unpack[Tuple[str, ...]], int]
 match fm3:
@@ -2347,6 +2390,7 @@ match m3:
 [builtins fixtures/tuple.pyi]
 
 [case testMatchSequencePatternTypeVarTupleNotTooShort]
+# flags: --warn-unreachable
 from typing import Tuple
 from typing_extensions import Unpack, TypeVarTuple
 
@@ -2362,8 +2406,11 @@ def test(xs: Tuple[Unpack[Ts]]) -> None:
     fm2: Tuple[int, int, Unpack[Ts], int]
     match fm2:
         case [fa2, fb2]:
-            reveal_type(fa2)
-            reveal_type(fb2)
+            reveal_type(fa2)  # E: Statement is unreachable \
+                              # E: Cannot determine type of "fa2" \
+                              # N: Revealed type is "Any"
+            reveal_type(fb2)  # E: Cannot determine type of "fb2" \
+                              # N: Revealed type is "Any"
 
     fm3: Tuple[int, int, Unpack[Ts], int]
     match fm3:
diff --git a/test-data/unit/check-python38.test b/test-data/unit/check-python38.test
index f90baed0eb16..1643cec1d749 100644
--- a/test-data/unit/check-python38.test
+++ b/test-data/unit/check-python38.test
@@ -459,7 +459,8 @@ def check_partial_list() -> None:
 # flags: --warn-unreachable
 
 if (x := 0):
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(x)  # N: Revealed type is "Literal[0]"
 
@@ -485,7 +486,8 @@ else:
 reveal_type(x)  # N: Revealed type is "builtins.str"
 
 if y := wrapper.always_false:
-    reveal_type(y)  # E: Statement is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(y)  # N: Revealed type is "Literal[False]"
 
@@ -508,7 +510,8 @@ reveal_type(x)  # N: Revealed type is "builtins.str"
 def always_false() -> Literal[False]: ...
 
 if y := always_false():
-    reveal_type(y)  # E: Statement is unreachable
+    reveal_type(y)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(y)  # N: Revealed type is "Literal[False]"
 
@@ -517,7 +520,8 @@ reveal_type(y)  # N: Revealed type is "Literal[False]"
 def always_false_with_parameter(x: int) -> Literal[False]: ...
 
 if z := always_false_with_parameter(5):
-    reveal_type(z)  # E: Statement is unreachable
+    reveal_type(z)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 else:
     reveal_type(z)  # N: Revealed type is "Literal[False]"
 
diff --git a/test-data/unit/check-reports.test b/test-data/unit/check-reports.test
index 423cbcc49289..fc29e61a5cb5 100644
--- a/test-data/unit/check-reports.test
+++ b/test-data/unit/check-reports.test
@@ -41,7 +41,7 @@ def f(x: int) -> None:
 [outfile out/lineprecision.txt]
 Name      Lines  Precise  Imprecise  Any  Empty  Unanalyzed
 -------------------------------------------------------------
-__main__     10        5          0    0      2           3
+__main__     10        7          0    0      2           1
 
 [case testLinePrecisionEmptyLines]
 # flags: --lineprecision-report out
diff --git a/test-data/unit/check-tuples.test b/test-data/unit/check-tuples.test
index d675a35c4aae..8197825be6ee 100644
--- a/test-data/unit/check-tuples.test
+++ b/test-data/unit/check-tuples.test
@@ -940,7 +940,7 @@ for x in t:
 [case testForLoopOverEmptyTuple]
 import typing
 t = ()
-for x in t: pass  # E: Need type annotation for "x"
+for x in t: pass
 [builtins fixtures/for.pyi]
 
 [case testForLoopOverNoneValuedTuple]
@@ -1604,7 +1604,6 @@ t5: Tuple[int, int] = (1, 2, "s", 4)  # E: Incompatible types in assignment (exp
 
 # long initializer assignment with mismatched pairs
 t6: Tuple[int, int, int, int, int, int, int, int, int, int, int, int] = (1, 2, 3, 4, 5, 6, 7, 8, "str", "str", "str", "str", 1, 1, 1, 1, 1) # E: Incompatible types in assignment (expression has type Tuple[int, int, ... <15 more items>], variable has type Tuple[int, int, ... <10 more items>])
-
 [builtins fixtures/tuple.pyi]
 
 [case testTupleWithStarExpr]
diff --git a/test-data/unit/check-typeis.test b/test-data/unit/check-typeis.test
index e70c71a4b62e..24613af16e93 100644
--- a/test-data/unit/check-typeis.test
+++ b/test-data/unit/check-typeis.test
@@ -454,7 +454,10 @@ def g(x: object) -> None: ...
 def test(x: List[Any]) -> None:
     if not(f(x) or isinstance(x, A)):
         return
-    g(reveal_type(x))  # N: Revealed type is "Union[builtins.list[builtins.str], __main__.<subclass of "List[Any]" and "__main__.A">]"
+
+    g(reveal_type(x))  # N: Revealed type is "builtins.list[Any]"
+    # explanation: `if f(x): ...` is assumed always true!
+    # so there's no narrowing here.
 [builtins fixtures/tuple.pyi]
 
 [case testTypeIsMultipleCondition]
@@ -819,6 +822,7 @@ accept_typeguard(typeguard)
 [builtins fixtures/tuple.pyi]
 
 [case testTypeIsInOverloads]
+# flags: --warn-unreachable
 from typing import Any, overload, Union
 from typing_extensions import TypeIs
 
@@ -843,13 +847,15 @@ def func3(val: Union[int, str]):
     if func1(val):
         reveal_type(val)  # N: Revealed type is "Union[builtins.int, builtins.str]"
     else:
-        reveal_type(val)
+        reveal_type(val)  # E: Statement is unreachable \
+                          # N: Revealed type is "Never"
 
 def func4(val: int):
     if func1(val):
         reveal_type(val)  # N: Revealed type is "builtins.int"
     else:
-        reveal_type(val)
+        reveal_type(val)  # E: Statement is unreachable \
+                          # N: Revealed type is "Never"
 [builtins fixtures/tuple.pyi]
 
 [case testTypeIsInOverloadsSameReturn]
diff --git a/test-data/unit/check-typevar-tuple.test b/test-data/unit/check-typevar-tuple.test
index 2cc84c8e6b15..b442cdefeff7 100644
--- a/test-data/unit/check-typevar-tuple.test
+++ b/test-data/unit/check-typevar-tuple.test
@@ -1273,7 +1273,8 @@ def test(d: A[int, str]) -> None:
     if isinstance(d, A):
         reveal_type(d)  # N: Revealed type is "Tuple[builtins.int, builtins.str, fallback=__main__.A[builtins.int, builtins.str]]"
     else:
-        reveal_type(d)  # E: Statement is unreachable
+        reveal_type(d)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 
 class B(Generic[Unpack[TP]]): ...
 
@@ -1281,7 +1282,8 @@ def test2(d: B[int, str]) -> None:
     if isinstance(d, B):
         reveal_type(d)  # N: Revealed type is "__main__.B[builtins.int, builtins.str]"
     else:
-        reveal_type(d)  # E: Statement is unreachable
+        reveal_type(d)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testVariadicTupleSubtyping]
diff --git a/test-data/unit/check-typevar-values.test b/test-data/unit/check-typevar-values.test
index 36ab3af6d3e9..d69b44f52947 100644
--- a/test-data/unit/check-typevar-values.test
+++ b/test-data/unit/check-typevar-values.test
@@ -123,7 +123,6 @@ def h(x: T) -> T:
         return '' # E: Incompatible return value type (got "str", expected "int")
     return x
 [builtins fixtures/isinstance.pyi]
-[out]
 
 [case testIsinstanceAndTypeVarValues2]
 from typing import TypeVar
@@ -140,7 +139,6 @@ def g(x: T) -> T:
         return 2  # E: Incompatible return value type (got "int", expected "str")
     return x
 [builtins fixtures/isinstance.pyi]
-[out]
 
 [case testIsinstanceAndTypeVarValues3]
 from typing import TypeVar
@@ -163,7 +161,6 @@ def f(x: T) -> T:
         y = object()
     return y # E: Incompatible return value type (got "object", expected "str")
 [builtins fixtures/isinstance.pyi]
-[out]
 
 [case testIsinstanceAndTypeVarValues5]
 from typing import TypeVar
@@ -215,7 +212,6 @@ def g(x: S) -> None:
     if isinstance(x, int):
         x = y
 [builtins fixtures/isinstance.pyi]
-[out]
 
 [case testIsinstanceWithUserDefinedTypeAndTypeVarValues2]
 from typing import TypeVar
@@ -233,7 +229,6 @@ def f(x: T) -> None:
         x = 1
         x = S() # E: Incompatible types in assignment (expression has type "S", variable has type "int")
 [builtins fixtures/isinstance.pyi]
-[out]
 
 [case testTypeVarValuesAndNestedCalls]
 from typing import TypeVar
@@ -745,3 +740,24 @@ def fn(w: W) -> W:
         reveal_type(w)  # N: Revealed type is "builtins.int"
     return w
 [builtins fixtures/isinstance.pyi]
+
+[case testTypeVarValuesPropagateUnreachabilitySilence]
+# flags: --warn-unreachable
+from typing import Any, Callable, TypeVar
+
+from typing_extensions import Concatenate, ParamSpec
+
+T = TypeVar("T", int, str)
+P = ParamSpec("P")
+
+def accepts_mapping(
+    func: Callable[P, Any]
+) -> Callable[Concatenate[T, P], T]:
+    def wrapper(data: T, /, *args: P.args, **kwargs: P.kwargs) -> T:
+        if isinstance(data, str):
+            return ""
+        else:
+            return 1
+
+    return wrapper
+[builtins fixtures/isinstance.pyi]
diff --git a/test-data/unit/check-unreachable-code.test b/test-data/unit/check-unreachable-code.test
index a40aa21ff26a..994f2e28d22a 100644
--- a/test-data/unit/check-unreachable-code.test
+++ b/test-data/unit/check-unreachable-code.test
@@ -615,6 +615,7 @@ reveal_type(x)  # N: Revealed type is "__main__.B"
 [typing fixtures/typing-medium.pyi]
 
 [case testUnreachableWhenSuperclassIsAny]
+# flags: --warn-unreachable
 from typing import Any
 
 # This can happen if we're importing a class from a missing module
@@ -623,8 +624,9 @@ class Child(Parent):
     def foo(self) -> int:
         reveal_type(self)       # N: Revealed type is "__main__.Child"
         if self is None:
-            reveal_type(self)
-            return None
+            reveal_type(self)  # E: Statement is unreachable \
+                               # N: Revealed type is "Never"
+            return None  # E: Incompatible return value type (got "None", expected "int")
         reveal_type(self)       # N: Revealed type is "__main__.Child"
         return 3
 
@@ -633,8 +635,9 @@ class Child(Parent):
             self = super(Child, self).something()
             reveal_type(self)       # N: Revealed type is "__main__.Child"
             if self is None:
-                reveal_type(self)
-                return None
+                reveal_type(self)  # E: Statement is unreachable \
+                                   # N: Revealed type is "Never"
+                return None  # E: Incompatible return value type (got "None", expected "int")
             reveal_type(self)       # N: Revealed type is "__main__.Child"
             return 3
 [builtins fixtures/isinstance.pyi]
@@ -716,7 +719,8 @@ a: int
 if isinstance(a, int):
     reveal_type(a)  # N: Revealed type is "builtins.int"
 else:
-    reveal_type(a)  # E: Statement is unreachable
+    reveal_type(a)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableFlagWithBadControlFlow2]
@@ -725,7 +729,8 @@ b: int
 while isinstance(b, int):
     reveal_type(b)  # N: Revealed type is "builtins.int"
 else:
-    reveal_type(b)  # E: Statement is unreachable
+    reveal_type(b)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableFlagWithBadControlFlow3]
@@ -733,14 +738,16 @@ else:
 def foo(c: int) -> None:
     reveal_type(c)  # N: Revealed type is "builtins.int"
     assert not isinstance(c, int)
-    reveal_type(c)  # E: Statement is unreachable
+    reveal_type(c)  # E: Statement is unreachable \
+                    # N: Revealed type is "Never"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableFlagWithBadControlFlow4]
 # flags: --warn-unreachable
 d: int
 if False:
-    reveal_type(d)  # E: Statement is unreachable
+    reveal_type(d)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableFlagWithBadControlFlow5]
@@ -749,7 +756,8 @@ e: int
 if True:
     reveal_type(e)  # N: Revealed type is "builtins.int"
 else:
-    reveal_type(e)  # E: Statement is unreachable
+    reveal_type(e)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 [builtins fixtures/isinstancelist.pyi]
 
 [case testUnreachableFlagStatementAfterReturn]
@@ -757,7 +765,8 @@ else:
 def foo(x: int) -> None:
     reveal_type(x)  # N: Revealed type is "builtins.int"
     return
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 
 [case testUnreachableFlagTryBlocks]
 # flags: --warn-unreachable
@@ -766,24 +775,28 @@ def foo(x: int) -> int:
     try:
         reveal_type(x)      # N: Revealed type is "builtins.int"
         return x
-        reveal_type(x)      # E: Statement is unreachable
+        reveal_type(x)      # E: Statement is unreachable \
+                            # N: Revealed type is "builtins.int"
     finally:
         reveal_type(x)      # N: Revealed type is "builtins.int"
         if True:
             reveal_type(x)  # N: Revealed type is "builtins.int"
         else:
-            reveal_type(x)  # E: Statement is unreachable
+            reveal_type(x)  # E: Statement is unreachable \
+                            # N: Revealed type is "builtins.int"
 
 def bar(x: int) -> int:
     try:
         if True:
             raise Exception()
-        reveal_type(x)      # E: Statement is unreachable
+        reveal_type(x)      # E: Statement is unreachable \
+                            # N: Revealed type is "builtins.int"
     except:
         reveal_type(x)      # N: Revealed type is "builtins.int"
         return x
     else:
-        reveal_type(x)      # E: Statement is unreachable
+        reveal_type(x)      # E: Statement is unreachable \
+                            # N: Revealed type is "builtins.int"
 
 def baz(x: int) -> int:
     try:
@@ -862,6 +875,8 @@ d = [x for x in lst if FOOBAR]
 [case testUnreachableFlagOkWithDeadStatements]
 # flags: --warn-unreachable
 from typing import NoReturn
+from typing_extensions import assert_never as typing_assert_never
+
 def assert_never(x: NoReturn) -> NoReturn:
     assert False
 
@@ -872,24 +887,39 @@ def expect_str(x: str) -> str: pass
 x: int
 if False:
     assert False
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 
 if False:
     raise Exception()
-    reveal_type(x)  # E: Statement is unreachable
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 
 if False:
-    assert_never(x)
-    reveal_type(x)  # E: Statement is unreachable
+    assert_never(x)  # E: Argument 1 to "assert_never" has incompatible type "int"; expected "Never"
+    typing_assert_never(x)
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 
 if False:
-    nonthrowing_assert_never(x)  # E: Statement is unreachable
-    reveal_type(x)
+    nonthrowing_assert_never(x)  # E: Statement is unreachable \
+                                 # E: Argument 1 to "nonthrowing_assert_never" has incompatible type "int"; expected "Never"
+    reveal_type(x)  # N: Revealed type is "builtins.int"
 
 if False:
     # Ignore obvious type errors
-    assert_never(expect_str(x))
-    reveal_type(x)  # E: Statement is unreachable
+    assert_never(expect_str(x))  # E: Argument 1 to "assert_never" has incompatible type "str"; expected "Never" \
+                                 # E: Argument 1 to "expect_str" has incompatible type "int"; expected "str"
+    typing_assert_never(expect_str(x))  # E: Argument 1 to "expect_str" has incompatible type "int"; expected "str"
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
+
+if True:
+    typing_assert_never(x)  # E: Argument 1 to "assert_never" has incompatible type "int"; expected "Never"
+    assert_never(x)  # E: Argument 1 to "assert_never" has incompatible type "int"; expected "Never"
+    typing_assert_never(x)
+    reveal_type(x)  # E: Statement is unreachable \
+                    # N: Revealed type is "builtins.int"
 [builtins fixtures/exception.pyi]
 
 [case testNeverVariants]
@@ -932,11 +962,13 @@ k = [x for x in lst if isinstance(x, int) or foo()]  # E: Right operand of "or"
 
 class Case1:
     def test1(self) -> bool:
-        return False and self.missing()  # E: Right operand of "and" is never evaluated
+        return False and self.missing()  # E: Right operand of "and" is never evaluated \
+                                         # E: "Case1" has no attribute "missing"
 
     def test2(self) -> bool:
         return not self.property_decorator_missing and self.missing()  # E: Function "property_decorator_missing" could always be true in boolean context \
-            # E: Right operand of "and" is never evaluated
+                                                                       # E: Right operand of "and" is never evaluated \
+                                                                       # E: "Case1" has no attribute "missing"
 
     def property_decorator_missing(self) -> bool:
         return True
@@ -954,7 +986,8 @@ def test1(x: T1) -> T1:
     if isinstance(x, int):
         reveal_type(x)  # N: Revealed type is "T1`-1"
     else:
-        reveal_type(x)  # E: Statement is unreachable
+        reveal_type(x)  # E: Statement is unreachable \
+                        # N: Revealed type is "Never"
     return x
 
 def test2(x: T2) -> T2:
@@ -1332,8 +1365,12 @@ def test_untyped_fn(obj):
     obj.update(prop=False)
     obj.reload()
 
+    reveal_type(obj.prop)  # N: Revealed type is "Any" \
+                           # N: 'reveal_type' always outputs 'Any' in unchecked functions
+
     assert obj.prop is False
-    reveal_type(obj.prop)
+    reveal_type(obj.prop)  # N: Revealed type is "Any" \
+                           # N: 'reveal_type' always outputs 'Any' in unchecked functions
 
 def test_typed_fn(obj) -> None:
     assert obj.prop is True
@@ -1342,7 +1379,8 @@ def test_typed_fn(obj) -> None:
     obj.reload()
 
     assert obj.prop is False
-    reveal_type(obj.prop)  # E: Statement is unreachable
+    reveal_type(obj.prop)  # E: Statement is unreachable \
+                           # N: Revealed type is "Never"
 
 [case testUnreachableCheckedUntypedFunction]
 # flags: --warn-unreachable --check-untyped-defs
@@ -1354,7 +1392,8 @@ def test_untyped_fn(obj):
     obj.reload()
 
     assert obj.prop is False
-    reveal_type(obj.prop)  # E: Statement is unreachable
+    reveal_type(obj.prop)  # E: Statement is unreachable \
+                           # N: Revealed type is "Never"
 
 [case testConditionalTypeVarException]
 # every part of this test case was necessary to trigger the crash
@@ -1511,3 +1550,26 @@ x = 0  # not unreachable
 
 f2: Callable[[], NoReturn] = lambda: foo()
 x = 0  # not unreachable
+
+[case testUnpackNever]
+x: str
+if isinstance(x, int):
+    y, *ys = x
+    reveal_type(y)  # N: Revealed type is "Never"
+    reveal_type(ys)  # N: Revealed type is "builtins.list[Never]"
+[builtins fixtures/isinstancelist.pyi]
+
+[case testUnusedConditionalBranchesDoNotAffectType]
+# flags: --enable-error-code redundant-expr
+def foo(var: str) -> str:
+    return "aa" if isinstance(var, str) else 0  # E: If condition is always true
+[builtins fixtures/isinstancelist.pyi]
+
+[case testMypyDoesntNarrowBasedOnLies]
+x: int
+if isinstance(x, int):
+    assert False
+
+reveal_type(x)  # N: Revealed type is "builtins.int"
+# mypy should not narrow this ^
+[builtins fixtures/isinstancelist.pyi]
diff --git a/test-data/unit/daemon.test b/test-data/unit/daemon.test
index 7dfddd8f74df..af8124dd7cfc 100644
--- a/test-data/unit/daemon.test
+++ b/test-data/unit/daemon.test
@@ -463,8 +463,7 @@ $ dmypy inspect foo.py:1:2:3:4
 Can't find expression at span 1:2:3:4
 == Return code: 1
 $ dmypy inspect foo.py:17:5:17:5
-No known type available for "NameExpr" (maybe unreachable or try --force-reload)
-== Return code: 1
+"int"
 
 [file foo.py]
 from typing import Optional
@@ -523,9 +522,8 @@ $ dmypy inspect foo.py:1:2
 Can't find any expressions at position 1:2
 == Return code: 1
 $ dmypy inspect foo.py:11:5 --force-reload
-No known type available for "NameExpr" (maybe unreachable)
-No known type available for "OpExpr" (maybe unreachable)
-== Return code: 1
+"int"
+"int"
 
 [file foo.py]
 from typing import Optional
@@ -547,8 +545,7 @@ $ dmypy check foo.py bar.py --export-types
 $ dmypy inspect foo.py:9:1 --show attrs --include-span --include-kind -vv
 NameExpr:9:1:9:1 -> {"foo.C": ["a", "x", "y"], "foo.B": ["a", "b"]}
 $ dmypy inspect foo.py:11:10 --show attrs
-No known type available for "StrExpr" (maybe unreachable or try --force-reload)
-== Return code: 1
+{"str": ["__add__", "__contains__", "__eq__", "__ge__", "__getitem__", "__getnewargs__", "__gt__", "__hash__", "__iter__", "__le__", "__len__", "__lt__", "__mod__", "__mul__", "__ne__", "__new__", "__rmul__", "capitalize", "casefold", "center", "count", "encode", "endswith", "expandtabs", "find", "format", "format_map", "index", "isalnum", "isalpha", "isascii", "isdecimal", "isdigit", "isidentifier", "islower", "isnumeric", "isprintable", "isspace", "istitle", "isupper", "join", "ljust", "lower", "lstrip", "maketrans", "partition", "removeprefix", "removesuffix", "replace", "rfind", "rindex", "rjust", "rpartition", "rsplit", "rstrip", "split", "splitlines", "startswith", "strip", "swapcase", "title", "translate", "upper", "zfill"], "Sequence": ["__contains__", "__getitem__", "__iter__", "__reversed__", "count", "index"], "Reversible": ["__reversed__"], "Collection": ["__len__"], "Iterable": ["__iter__"], "Container": ["__contains__"]}
 $ dmypy inspect foo.py:1:1 --show attrs
 Can't find any expressions at position 1:1
 == Return code: 1
diff --git a/test-data/unit/deps-classes.test b/test-data/unit/deps-classes.test
index a8fc5d629491..4e9eb9f94b88 100644
--- a/test-data/unit/deps-classes.test
+++ b/test-data/unit/deps-classes.test
@@ -84,19 +84,23 @@ class A: pass
 <a> -> m
 
 [case testIfFalseInClassBody]
+from typing import Any
+
 class A:
     if False:
-        x = None  # type: str
+        x: Any = None
         x.foo()
 [builtins fixtures/bool.pyi]
 [out]
 <m.A> -> m.A
 
 [case testAlwaysFalseIsinstanceInClassBody]
+from typing import Any
+
 class A:
     x: int
     if isinstance(x, str):
-        y: str = None
+        y: Any = None
         y.foo()
 [builtins fixtures/isinstance.pyi]
 [out]
diff --git a/test-data/unit/deps.test b/test-data/unit/deps.test
index 2c231c9afff6..793624c22ca5 100644
--- a/test-data/unit/deps.test
+++ b/test-data/unit/deps.test
@@ -582,7 +582,7 @@ def f(a: A) -> None:
 [case testUnreachableAssignment]
 from typing import List, Tuple
 
-def f() -> None: pass
+def f() -> int: pass
 
 class C:
     def __init__(self, x: int) -> None:
diff --git a/test-data/unit/fine-grained.test b/test-data/unit/fine-grained.test
index d2b1a8a92b80..248206e09c24 100644
--- a/test-data/unit/fine-grained.test
+++ b/test-data/unit/fine-grained.test
@@ -9692,10 +9692,9 @@ reveal_type(z)
 [out]
 c.py:2: note: Revealed type is "a.<subclass of "a.A" and "a.B">"
 ==
-c.py:2: note: Revealed type is "Any"
-b.py:2: error: Cannot determine type of "y"
+c.py:2: note: Revealed type is "Never"
 
-[case testIsInstanceAdHocIntersectionFineGrainedIncrementalUnreachaableToIntersection]
+[case testIsInstanceAdHocIntersectionFineGrainedIncrementalUnreachableToIntersection]
 import c
 [file a.py]
 class A:
@@ -9724,8 +9723,7 @@ from b import z
 reveal_type(z)
 [builtins fixtures/isinstance.pyi]
 [out]
-b.py:2: error: Cannot determine type of "y"
-c.py:2: note: Revealed type is "Any"
+c.py:2: note: Revealed type is "Never"
 ==
 c.py:2: note: Revealed type is "a.<subclass of "a.A" and "a.B">"
 
diff --git a/test-data/unit/lib-stub/typing_extensions.pyi b/test-data/unit/lib-stub/typing_extensions.pyi
index cb054b0e6b4f..fddc0203eef7 100644
--- a/test-data/unit/lib-stub/typing_extensions.pyi
+++ b/test-data/unit/lib-stub/typing_extensions.pyi
@@ -81,6 +81,7 @@ def TypedDict(typename: str, fields: Dict[str, Type[_T]], *, total: Any = ...) -
 
 def reveal_type(__obj: _T) -> _T: pass
 def assert_type(__val: _T, __typ: Any) -> _T: pass
+def assert_never(__val: Never) -> Never: pass
 
 def dataclass_transform(
     *,
diff --git a/test-data/unit/pythoneval.test b/test-data/unit/pythoneval.test
index 0e0e2b1f344d..ff760ddfdaa4 100644
--- a/test-data/unit/pythoneval.test
+++ b/test-data/unit/pythoneval.test
@@ -1481,8 +1481,10 @@ if isinstance(x, int):
 [out]
 _testIsInstanceAdHocIntersectionWithStrAndBytes.py:3: error: Subclass of "str" and "bytes" cannot exist: would have incompatible method signatures
 _testIsInstanceAdHocIntersectionWithStrAndBytes.py:4: error: Statement is unreachable
+_testIsInstanceAdHocIntersectionWithStrAndBytes.py:4: note: Revealed type is "Never"
 _testIsInstanceAdHocIntersectionWithStrAndBytes.py:6: error: Subclass of "str" and "int" cannot exist: would have incompatible method signatures
 _testIsInstanceAdHocIntersectionWithStrAndBytes.py:7: error: Statement is unreachable
+_testIsInstanceAdHocIntersectionWithStrAndBytes.py:7: note: Revealed type is "Never"
 
 [case testAsyncioFutureWait]
 # mypy: strict-optional
@@ -1553,6 +1555,7 @@ if isinstance(obj, Awaitable):
 [out]
 _testSpecialTypingProtocols.py:6: note: Revealed type is "Tuple[builtins.int]"
 _testSpecialTypingProtocols.py:8: error: Statement is unreachable
+_testSpecialTypingProtocols.py:8: note: Revealed type is "Never"
 
 [case testTypeshedRecursiveTypesExample]
 from typing import List, Union
diff --git a/test-data/unit/reports.test b/test-data/unit/reports.test
index 82c3869bb855..8975d6323fe8 100644
--- a/test-data/unit/reports.test
+++ b/test-data/unit/reports.test
@@ -235,7 +235,8 @@ def bar(x):
 <span class="line-any" title="Any Types on this line:
 Explicit (x1)">    any_f(x)</span>
 <span class="line-precise" title="No Anys on this line!">    assert False</span>
-<span class="line-unanalyzed" title="No Anys on this line!">    any_f(x)</span>
+<span class="line-any" title="Any Types on this line:
+Explicit (x1)">    any_f(x)</span>
 </pre></td>
 </tr></tbody>
 </table>
@@ -296,10 +297,10 @@ def bar(x):
 [outfile report/any-exprs.txt]
  Name   Anys   Exprs   Coverage
 ---------------------------------
-    i      1       6     83.33%
+    i      0       8    100.00%
     j      0       5    100.00%
 ---------------------------------
-Total      1      11     90.91%
+Total      0      13    100.00%
 
 [case testAnyExprReportHigherKindedTypesAreNotAny]
 # cmd: mypy --any-exprs-report report i.py