diff --git a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
index b757b0d820..016ab3d655 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -654,9 +654,7 @@ def f(cond: bool) -> str:
         reveal_type(x)  # revealed: Literal["before"]
         return "a"
         x = "after-return"
-        # TODO: no unresolved-reference error
-        # error: [unresolved-reference]
-        reveal_type(x)  # revealed: Unknown
+        reveal_type(x)  # revealed: Never
     else:
         x = "else"
     return reveal_type(x)  # revealed: Literal["else"]
diff --git a/crates/red_knot_python_semantic/resources/mdtest/unreachable.md b/crates/red_knot_python_semantic/resources/mdtest/unreachable.md
index fdeebf49aa..e7cdcf0668 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/unreachable.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/unreachable.md
@@ -211,9 +211,6 @@ def f():
 
     print("unreachable")
 
-    # TODO: we should not emit an error here; we currently do, since there is no control flow path from this
-    # use of 'x' to any definition of 'x'.
-    # error: [unresolved-reference]
     print(x)
 ```
 
@@ -228,8 +225,6 @@ def outer():
     x = 1
 
     def inner():
-        # TODO: we should not emit an error here
-        # error: [unresolved-reference]
         return x  # Name `x` used when not defined
     while True:
         pass
diff --git a/crates/red_knot_python_semantic/src/symbol.rs b/crates/red_knot_python_semantic/src/symbol.rs
index 53b2c88b15..e7fc55e7a5 100644
--- a/crates/red_knot_python_semantic/src/symbol.rs
+++ b/crates/red_knot_python_semantic/src/symbol.rs
@@ -679,6 +679,53 @@ fn symbol_from_bindings_impl<'db>(
                 visibility_constraints.evaluate(db, predicates, visibility_constraint);
 
             if static_visibility.is_always_false() {
+                // We found a binding that we have statically determined to not be visible from
+                // the use of the symbol that we are investigating. There are three interesting
+                // cases to consider:
+                //
+                // ```py
+                // def f1():
+                //     if False:
+                //         x = 1
+                //     use(x)
+                //
+                // def f2():
+                //     y = 1
+                //     return
+                //     use(y)
+                //
+                // def f3(flag: bool):
+                //     z = 1
+                //     if flag:
+                //         z = 2
+                //         return
+                //     use(z)
+                // ```
+                //
+                // In the first case, there is a single binding for `x`, and due to the statically
+                // known `False` condition, it is not visible at the use of `x`. However, we *can*
+                // see/reach the start of the scope from `use(x)`. This means that `x` is unbound
+                // and we should return `None`.
+                //
+                // In the second case, `y` is also not visible at the use of `y`, but here, we can
+                // not see/reach the start of the scope. There is only one path of control flow,
+                // and it passes through that binding of `y` (which we can not see). This implies
+                // that we are in an unreachable section of code. We return `Never` in order to
+                // silence the `unresolve-reference` diagnostic that would otherwise be emitted at
+                // the use of `y`.
+                //
+                // In the third case, we have two bindings for `z`. The first one is visible, so we
+                // consider the case that we now encounter the second binding `z = 2`, which is not
+                // visible due to the early return. We *also* can not see the start of the scope
+                // from `use(z)` because both paths of control flow pass through a binding of `z`.
+                // The `z = 1` binding is visible, and so we are *not* in an unreachable section of
+                // code. However, it is still okay to return `Never` in this case, because we will
+                // union the types of all bindings, and `Never` will be eliminated automatically.
+
+                if unbound_visibility.is_always_false() {
+                    // The scope-start is not visible
+                    return Some(Type::Never);
+                }
                 return None;
             }