From 02c4798159167f3662a28958a8c98765ae5a2974 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 29 Jan 2025 15:10:00 -0500
Subject: [PATCH 01/35] Add ALWAYS_FALSE

---
 .../semantic_index/use_def/symbol_state.rs    |  6 ++++
 .../src/visibility_constraints.rs             | 33 ++++++++++++++++---
 2 files changed, 34 insertions(+), 5 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
index 39ccd193cfc0d..4bf28f9957d90 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
@@ -109,6 +109,12 @@ impl ScopedVisibilityConstraintId {
     /// present at index 0.
     pub(crate) const ALWAYS_TRUE: ScopedVisibilityConstraintId =
         ScopedVisibilityConstraintId::from_u32(0);
+
+    /// A special ID that is used for an "always false" / "never visible" constraint.
+    /// When we create a new [`VisibilityConstraints`] object, this constraint is always
+    /// present at index 1.
+    pub(crate) const ALWAYS_FALSE: ScopedVisibilityConstraintId =
+        ScopedVisibilityConstraintId::from_u32(1);
 }
 
 const INLINE_VISIBILITY_CONSTRAINTS: usize = 4;
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index f19144fb5e072..18333504759af 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -186,7 +186,10 @@ pub(crate) struct VisibilityConstraints<'db> {
 impl Default for VisibilityConstraints<'_> {
     fn default() -> Self {
         Self {
-            constraints: IndexVec::from_iter([VisibilityConstraint::AlwaysTrue]),
+            constraints: IndexVec::from_iter([
+                VisibilityConstraint::AlwaysTrue,
+                VisibilityConstraint::VisibleIfNot(ScopedVisibilityConstraintId::ALWAYS_TRUE),
+            ]),
         }
     }
 }
@@ -204,6 +207,15 @@ impl<'db> VisibilityConstraints<'db> {
         a: ScopedVisibilityConstraintId,
         b: ScopedVisibilityConstraintId,
     ) -> ScopedVisibilityConstraintId {
+        if a == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+            return b;
+        } else if b == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+            return a;
+        } else if a == ScopedVisibilityConstraintId::ALWAYS_TRUE {
+            return ScopedVisibilityConstraintId::ALWAYS_TRUE;
+        } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE {
+            return ScopedVisibilityConstraintId::ALWAYS_TRUE;
+        }
         match (&self.constraints[a], &self.constraints[b]) {
             (_, VisibilityConstraint::VisibleIfNot(id)) if a == *id => {
                 ScopedVisibilityConstraintId::ALWAYS_TRUE
@@ -221,11 +233,22 @@ impl<'db> VisibilityConstraints<'db> {
         b: ScopedVisibilityConstraintId,
     ) -> ScopedVisibilityConstraintId {
         if a == ScopedVisibilityConstraintId::ALWAYS_TRUE {
-            b
+            return b;
         } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE {
-            a
-        } else {
-            self.add(VisibilityConstraint::KleeneAnd(a, b))
+            return a;
+        } else if a == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+            return ScopedVisibilityConstraintId::ALWAYS_FALSE;
+        } else if b == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+            return ScopedVisibilityConstraintId::ALWAYS_FALSE;
+        }
+        match (&self.constraints[a], &self.constraints[b]) {
+            (_, VisibilityConstraint::VisibleIfNot(id)) if a == *id => {
+                ScopedVisibilityConstraintId::ALWAYS_FALSE
+            }
+            (VisibilityConstraint::VisibleIfNot(id), _) if *id == b => {
+                ScopedVisibilityConstraintId::ALWAYS_FALSE
+            }
+            _ => self.add(VisibilityConstraint::KleeneAnd(a, b)),
         }
     }
 

From 2c0d577a55a52ebbd73edd2ae8121b34ad118574 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 29 Jan 2025 16:31:20 -0500
Subject: [PATCH 02/35] Mark return states

---
 .../src/semantic_index/builder.rs             | 23 ++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index 8b8a6b56a3e50..fa05792fe5edd 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -65,6 +65,7 @@ pub(super) struct SemanticIndexBuilder<'db> {
     /// The match case we're currently visiting.
     current_match_case: Option<CurrentMatchCase<'db>>,
 
+    return_states: Vec<FlowSnapshot>,
     /// Flow states at each `break` in the current loop.
     loop_break_states: Vec<FlowSnapshot>,
     /// Per-scope contexts regarding nested `try`/`except` statements
@@ -95,6 +96,7 @@ impl<'db> SemanticIndexBuilder<'db> {
             scope_stack: Vec::new(),
             current_assignments: vec![],
             current_match_case: None,
+            return_states: vec![],
             loop_break_states: vec![],
             try_node_context_stack_manager: TryNodeContextStackManager::default(),
 
@@ -703,10 +705,20 @@ where
                         }
 
                         builder.push_scope(NodeWithScopeRef::Function(function_def));
+                        let saved_return_states = std::mem::take(&mut builder.return_states);
 
                         builder.declare_parameters(parameters);
 
                         builder.visit_body(body);
+
+                        // Merge the flow state just before any `return` statements with the flow
+                        // state at the end of the function body.
+                        let return_states =
+                            std::mem::replace(&mut builder.return_states, saved_return_states);
+                        for return_state in return_states {
+                            builder.flow_merge(return_state);
+                        }
+
                         builder.pop_scope()
                     },
                 );
@@ -1272,12 +1284,21 @@ where
                 self.visit_body(finalbody);
             }
 
-            ast::Stmt::Raise(_) | ast::Stmt::Return(_) | ast::Stmt::Continue(_) => {
+            ast::Stmt::Raise(_) | ast::Stmt::Continue(_) => {
                 walk_stmt(self, stmt);
                 // Everything in the current block after a terminal statement is unreachable.
                 self.mark_unreachable();
             }
 
+            ast::Stmt::Return(_) => {
+                // Mark the flow state just before the `return` as one of the return states of the
+                // current function.
+                self.return_states.push(self.flow_snapshot());
+
+                // Everything in the current block after a terminal statement is unreachable.
+                self.mark_unreachable();
+            }
+
             ast::Stmt::Break(_) => {
                 if self.loop_state().is_inside() {
                     self.loop_break_states.push(self.flow_snapshot());

From e1988064318233158de478943ccc53be936130d0 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 29 Jan 2025 16:31:35 -0500
Subject: [PATCH 03/35] Mark live bindings as non-visible when flow is
 unreachable

---
 crates/red_knot_python_semantic/src/semantic_index/use_def.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 04120f8a67fa9..80bf1932a01cd 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -525,7 +525,8 @@ impl Default for UseDefMapBuilder<'_> {
 
 impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn mark_unreachable(&mut self) {
-        self.reachable = false;
+        //self.reachable = false;
+        self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
     }
 
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {

From 23b366d46cbc0389fc58dfa255e3e3fac7d6aab7 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 09:35:07 -0500
Subject: [PATCH 04/35] Revert "Mark return states"

This reverts commit 2c0d577a55a52ebbd73edd2ae8121b34ad118574.
---
 .../src/semantic_index/builder.rs             | 23 +------------------
 1 file changed, 1 insertion(+), 22 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index fa05792fe5edd..8b8a6b56a3e50 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -65,7 +65,6 @@ pub(super) struct SemanticIndexBuilder<'db> {
     /// The match case we're currently visiting.
     current_match_case: Option<CurrentMatchCase<'db>>,
 
-    return_states: Vec<FlowSnapshot>,
     /// Flow states at each `break` in the current loop.
     loop_break_states: Vec<FlowSnapshot>,
     /// Per-scope contexts regarding nested `try`/`except` statements
@@ -96,7 +95,6 @@ impl<'db> SemanticIndexBuilder<'db> {
             scope_stack: Vec::new(),
             current_assignments: vec![],
             current_match_case: None,
-            return_states: vec![],
             loop_break_states: vec![],
             try_node_context_stack_manager: TryNodeContextStackManager::default(),
 
@@ -705,20 +703,10 @@ where
                         }
 
                         builder.push_scope(NodeWithScopeRef::Function(function_def));
-                        let saved_return_states = std::mem::take(&mut builder.return_states);
 
                         builder.declare_parameters(parameters);
 
                         builder.visit_body(body);
-
-                        // Merge the flow state just before any `return` statements with the flow
-                        // state at the end of the function body.
-                        let return_states =
-                            std::mem::replace(&mut builder.return_states, saved_return_states);
-                        for return_state in return_states {
-                            builder.flow_merge(return_state);
-                        }
-
                         builder.pop_scope()
                     },
                 );
@@ -1284,21 +1272,12 @@ where
                 self.visit_body(finalbody);
             }
 
-            ast::Stmt::Raise(_) | ast::Stmt::Continue(_) => {
+            ast::Stmt::Raise(_) | ast::Stmt::Return(_) | ast::Stmt::Continue(_) => {
                 walk_stmt(self, stmt);
                 // Everything in the current block after a terminal statement is unreachable.
                 self.mark_unreachable();
             }
 
-            ast::Stmt::Return(_) => {
-                // Mark the flow state just before the `return` as one of the return states of the
-                // current function.
-                self.return_states.push(self.flow_snapshot());
-
-                // Everything in the current block after a terminal statement is unreachable.
-                self.mark_unreachable();
-            }
-
             ast::Stmt::Break(_) => {
                 if self.loop_state().is_inside() {
                     self.loop_break_states.push(self.flow_snapshot());

From 38f3d99d4caeaf1d7fc71ef69ee5d49ac3522bf3 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 10:07:28 -0500
Subject: [PATCH 05/35] Handle final return statement specially

---
 .../src/semantic_index/builder.rs             | 20 ++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index 8b8a6b56a3e50..2b95c46e971dd 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -706,7 +706,25 @@ where
 
                         builder.declare_parameters(parameters);
 
-                        builder.visit_body(body);
+                        // HACK: Visit the function body, but treat the last statement specially if
+                        // it is a return. If it is, this would cause all definitions in the
+                        // function to be marked as non-visible with our current treatment of
+                        // terminal statements. Since we currently model the externally visible
+                        // definitions in a function scope as the set of bindings that are visible
+                        // at the end of the body, we then consider this function to have no
+                        // externally visible definitions. To get around this, we take a flow
+                        // snapshot just before processing the return statement, and use _that_ as
+                        // the "end-of-body" state that we resolve external references against.
+                        if let Some((last_stmt, first_stmts)) = body.split_last() {
+                            builder.visit_body(first_stmts);
+                            let pre_return_state = matches!(last_stmt, ast::Stmt::Return(_))
+                                .then(|| builder.flow_snapshot());
+                            builder.visit_stmt(last_stmt);
+                            if let Some(pre_return_state) = pre_return_state {
+                                builder.flow_restore(pre_return_state);
+                            }
+                        }
+
                         builder.pop_scope()
                     },
                 );

From 5c1918af04861dbc52e11f7a1f72d21fa3f518d9 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 10:33:40 -0500
Subject: [PATCH 06/35] Customizable binding visibility

---
 .../src/semantic_index/use_def.rs             |  4 +-
 .../semantic_index/use_def/symbol_state.rs    | 52 ++++++++++++++-----
 2 files changed, 42 insertions(+), 14 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 80bf1932a01cd..9841363a7f872 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -543,7 +543,7 @@ impl<'db> UseDefMapBuilder<'db> {
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id);
+        symbol_state.record_binding(def_id, ScopedVisibilityConstraintId::ALWAYS_TRUE);
     }
 
     pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
@@ -648,7 +648,7 @@ impl<'db> UseDefMapBuilder<'db> {
         let def_id = self.all_definitions.push(Some(definition));
         let symbol_state = &mut self.symbol_states[symbol];
         symbol_state.record_declaration(def_id);
-        symbol_state.record_binding(def_id);
+        symbol_state.record_binding(def_id, ScopedVisibilityConstraintId::ALWAYS_TRUE);
     }
 
     pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
index 4bf28f9957d90..154cb223321a3 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
@@ -254,7 +254,11 @@ impl SymbolBindings {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
+    pub(super) fn record_binding(
+        &mut self,
+        binding_id: ScopedDefinitionId,
+        visibility: ScopedVisibilityConstraintId,
+    ) {
         // The new binding replaces all previous live bindings in this path, and has no
         // constraints.
         self.live_bindings = Bindings::with(binding_id.into());
@@ -262,8 +266,7 @@ impl SymbolBindings {
         self.constraints.push(Constraints::default());
 
         self.visibility_constraints = VisibilityConstraintPerBinding::with_capacity(1);
-        self.visibility_constraints
-            .push(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+        self.visibility_constraints.push(visibility);
     }
 
     /// Add given constraint to all live bindings.
@@ -366,9 +369,13 @@ impl SymbolState {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
+    pub(super) fn record_binding(
+        &mut self,
+        binding_id: ScopedDefinitionId,
+        visibility: ScopedVisibilityConstraintId,
+    ) {
         debug_assert_ne!(binding_id, ScopedDefinitionId::UNBOUND);
-        self.bindings.record_binding(binding_id);
+        self.bindings.record_binding(binding_id, visibility);
     }
 
     /// Add given constraint to all live bindings.
@@ -574,7 +581,10 @@ mod tests {
     #[test]
     fn with() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(ScopedDefinitionId::from_u32(1));
+        sym.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
 
         assert_bindings(&sym, &["1<>"]);
     }
@@ -582,7 +592,10 @@ mod tests {
     #[test]
     fn record_constraint() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(ScopedDefinitionId::from_u32(1));
+        sym.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym.record_constraint(ScopedConstraintId::from_u32(0));
 
         assert_bindings(&sym, &["1<0>"]);
@@ -594,11 +607,17 @@ mod tests {
 
         // merging the same definition with the same constraint keeps the constraint
         let mut sym1a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1a.record_binding(ScopedDefinitionId::from_u32(1));
+        sym1a.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1a.record_constraint(ScopedConstraintId::from_u32(0));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(ScopedDefinitionId::from_u32(1));
+        sym1b.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1b.record_constraint(ScopedConstraintId::from_u32(0));
 
         sym1a.merge(sym1b, &mut visibility_constraints);
@@ -607,11 +626,17 @@ mod tests {
 
         // merging the same definition with differing constraints drops all constraints
         let mut sym2a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym2a.record_binding(ScopedDefinitionId::from_u32(2));
+        sym2a.record_binding(
+            ScopedDefinitionId::from_u32(2),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym2a.record_constraint(ScopedConstraintId::from_u32(1));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(ScopedDefinitionId::from_u32(2));
+        sym1b.record_binding(
+            ScopedDefinitionId::from_u32(2),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1b.record_constraint(ScopedConstraintId::from_u32(2));
 
         sym2a.merge(sym1b, &mut visibility_constraints);
@@ -620,7 +645,10 @@ mod tests {
 
         // merging a constrained definition with unbound keeps both
         let mut sym3a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym3a.record_binding(ScopedDefinitionId::from_u32(3));
+        sym3a.record_binding(
+            ScopedDefinitionId::from_u32(3),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym3a.record_constraint(ScopedConstraintId::from_u32(3));
 
         let sym2b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);

From 7504fb742c6dfefb8746da0b85f48b9d0a209095 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 10:58:05 -0500
Subject: [PATCH 07/35] Reachability is now a vis constraint, not a bool

---
 .../src/semantic_index/builder.rs             |  2 +-
 .../src/semantic_index/use_def.rs             | 55 ++++++++++++-------
 .../src/visibility_constraints.rs             | 34 +++++++++---
 3 files changed, 61 insertions(+), 30 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index 2b95c46e971dd..fcf5cfe23570b 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -160,7 +160,7 @@ impl<'db> SemanticIndexBuilder<'db> {
 
         let file_scope_id = self.scopes.push(scope);
         self.symbol_tables.push(SymbolTableBuilder::default());
-        self.use_def_maps.push(UseDefMapBuilder::default());
+        self.use_def_maps.push(UseDefMapBuilder::new(self.db));
         let ast_id_scope = self.ast_ids.push(AstIdsBuilder::default());
 
         let scope_id = ScopeId::new(self.db, self.file, file_scope_id, countme::Count::default());
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 9841363a7f872..06ec797504476 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -265,6 +265,7 @@ use crate::semantic_index::definition::Definition;
 use crate::semantic_index::symbol::ScopedSymbolId;
 use crate::semantic_index::use_def::symbol_state::DeclarationIdWithConstraint;
 use crate::visibility_constraints::{VisibilityConstraint, VisibilityConstraints};
+use crate::Db;
 use ruff_index::IndexVec;
 use rustc_hash::FxHashMap;
 
@@ -476,11 +477,12 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
-    reachable: bool,
+    reachability: ScopedVisibilityConstraintId,
 }
 
-#[derive(Debug)]
 pub(super) struct UseDefMapBuilder<'db> {
+    db: &'db dyn Db,
+
     /// Append-only array of [`Definition`].
     all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
 
@@ -505,12 +507,13 @@ pub(super) struct UseDefMapBuilder<'db> {
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
 
-    reachable: bool,
+    reachability: ScopedVisibilityConstraintId,
 }
 
-impl Default for UseDefMapBuilder<'_> {
-    fn default() -> Self {
+impl<'db> UseDefMapBuilder<'db> {
+    pub(super) fn new(db: &'db dyn Db) -> Self {
         Self {
+            db,
             all_definitions: IndexVec::from_iter([None]),
             all_constraints: IndexVec::new(),
             visibility_constraints: VisibilityConstraints::default(),
@@ -518,14 +521,12 @@ impl Default for UseDefMapBuilder<'_> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
-            reachable: true,
+            reachability: ScopedVisibilityConstraintId::ALWAYS_TRUE,
         }
     }
-}
 
-impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn mark_unreachable(&mut self) {
-        //self.reachable = false;
+        self.reachability = ScopedVisibilityConstraintId::ALWAYS_FALSE;
         self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
     }
 
@@ -543,7 +544,7 @@ impl<'db> UseDefMapBuilder<'db> {
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id, ScopedVisibilityConstraintId::ALWAYS_TRUE);
+        symbol_state.record_binding(def_id, self.reachability);
     }
 
     pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
@@ -648,7 +649,7 @@ impl<'db> UseDefMapBuilder<'db> {
         let def_id = self.all_definitions.push(Some(definition));
         let symbol_state = &mut self.symbol_states[symbol];
         symbol_state.record_declaration(def_id);
-        symbol_state.record_binding(def_id, ScopedVisibilityConstraintId::ALWAYS_TRUE);
+        symbol_state.record_binding(def_id, self.reachability);
     }
 
     pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
@@ -665,7 +666,7 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
-            reachable: self.reachable,
+            reachability: self.reachability,
         }
     }
 
@@ -689,20 +690,32 @@ impl<'db> UseDefMapBuilder<'db> {
             SymbolState::undefined(self.scope_start_visibility),
         );
 
-        self.reachable = snapshot.reachable;
+        self.reachability = snapshot.reachability;
     }
 
     /// Merge the given snapshot into the current state, reflecting that we might have taken either
     /// path to get here. The new state for each symbol should include definitions from both the
     /// prior state and the snapshot.
     pub(super) fn merge(&mut self, snapshot: FlowSnapshot) {
-        // Unreachable snapshots should not be merged: If the current snapshot is unreachable, it
-        // should be completely overwritten by the snapshot we're merging in. If the other snapshot
-        // is unreachable, we should return without merging.
-        if !snapshot.reachable {
+        // As an optimization, if we know statically that either of the snapshots is always
+        // unreachable, we can leave it out of the merged result entirely. Note that we cannot
+        // perform any type inference at this point, so this is largely limited to unreachability
+        // via terminal statements. If a flow's reachability depends on an expression in the code,
+        // we will include the flow in the merged result; the visibility constraints of its
+        // bindings will include this reachability condition, so that later during type inference,
+        // we can determine whether any particular binding is non-visible due to unreachability.
+        if self
+            .visibility_constraints
+            .evaluate_without_inference(self.db, snapshot.reachability)
+            .is_always_false()
+        {
             return;
         }
-        if !self.reachable {
+        if self
+            .visibility_constraints
+            .evaluate_without_inference(self.db, self.reachability)
+            .is_always_false()
+        {
             self.restore(snapshot);
             return;
         }
@@ -729,8 +742,10 @@ impl<'db> UseDefMapBuilder<'db> {
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
 
-        // Both of the snapshots are reachable, so the merged result is too.
-        self.reachable = true;
+        // The merged result is reachability when either of the merged flows is.
+        self.reachability = self
+            .visibility_constraints
+            .add_or_constraint(self.reachability, snapshot.reachability);
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index 18333504759af..8ca395bf85e6d 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -252,12 +252,22 @@ impl<'db> VisibilityConstraints<'db> {
         }
     }
 
+    /// Analyze the statically known visibility for a given visibility constraint, without
+    /// performing any type inference.
+    pub(crate) fn evaluate_without_inference(
+        &self,
+        db: &'db dyn Db,
+        id: ScopedVisibilityConstraintId,
+    ) -> Truthiness {
+        self.evaluate_impl::<false>(db, id, MAX_RECURSION_DEPTH)
+    }
+
     /// Analyze the statically known visibility for a given visibility constraint.
     pub(crate) fn evaluate(&self, db: &'db dyn Db, id: ScopedVisibilityConstraintId) -> Truthiness {
-        self.evaluate_impl(db, id, MAX_RECURSION_DEPTH)
+        self.evaluate_impl::<true>(db, id, MAX_RECURSION_DEPTH)
     }
 
-    fn evaluate_impl(
+    fn evaluate_impl<const INFERENCE_ALLOWED: bool>(
         &self,
         db: &'db dyn Db,
         id: ScopedVisibilityConstraintId,
@@ -271,18 +281,24 @@ impl<'db> VisibilityConstraints<'db> {
         match visibility_constraint {
             VisibilityConstraint::AlwaysTrue => Truthiness::AlwaysTrue,
             VisibilityConstraint::Ambiguous => Truthiness::Ambiguous,
-            VisibilityConstraint::VisibleIf(constraint) => Self::analyze_single(db, constraint),
-            VisibilityConstraint::VisibleIfNot(negated) => {
-                self.evaluate_impl(db, *negated, max_depth - 1).negate()
+            VisibilityConstraint::VisibleIf(constraint) => {
+                if INFERENCE_ALLOWED {
+                    Self::analyze_single(db, constraint)
+                } else {
+                    Truthiness::Ambiguous
+                }
             }
+            VisibilityConstraint::VisibleIfNot(negated) => self
+                .evaluate_impl::<INFERENCE_ALLOWED>(db, *negated, max_depth - 1)
+                .negate(),
             VisibilityConstraint::KleeneAnd(lhs, rhs) => {
-                let lhs = self.evaluate_impl(db, *lhs, max_depth - 1);
+                let lhs = self.evaluate_impl::<INFERENCE_ALLOWED>(db, *lhs, max_depth - 1);
 
                 if lhs == Truthiness::AlwaysFalse {
                     return Truthiness::AlwaysFalse;
                 }
 
-                let rhs = self.evaluate_impl(db, *rhs, max_depth - 1);
+                let rhs = self.evaluate_impl::<INFERENCE_ALLOWED>(db, *rhs, max_depth - 1);
 
                 if rhs == Truthiness::AlwaysFalse {
                     Truthiness::AlwaysFalse
@@ -293,13 +309,13 @@ impl<'db> VisibilityConstraints<'db> {
                 }
             }
             VisibilityConstraint::KleeneOr(lhs_id, rhs_id) => {
-                let lhs = self.evaluate_impl(db, *lhs_id, max_depth - 1);
+                let lhs = self.evaluate_impl::<INFERENCE_ALLOWED>(db, *lhs_id, max_depth - 1);
 
                 if lhs == Truthiness::AlwaysTrue {
                     return Truthiness::AlwaysTrue;
                 }
 
-                let rhs = self.evaluate_impl(db, *rhs_id, max_depth - 1);
+                let rhs = self.evaluate_impl::<INFERENCE_ALLOWED>(db, *rhs_id, max_depth - 1);
 
                 if rhs == Truthiness::AlwaysTrue {
                     Truthiness::AlwaysTrue

From ee6f2538db222365212c75aac727c19f862fafbf Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 11:20:52 -0500
Subject: [PATCH 08/35] Fix ternary AND logic

---
 .../src/visibility_constraints.rs             | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index 8ca395bf85e6d..93845a6b1c248 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -233,22 +233,15 @@ impl<'db> VisibilityConstraints<'db> {
         b: ScopedVisibilityConstraintId,
     ) -> ScopedVisibilityConstraintId {
         if a == ScopedVisibilityConstraintId::ALWAYS_TRUE {
-            return b;
+            b
         } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE {
-            return a;
+            a
         } else if a == ScopedVisibilityConstraintId::ALWAYS_FALSE {
-            return ScopedVisibilityConstraintId::ALWAYS_FALSE;
+            ScopedVisibilityConstraintId::ALWAYS_FALSE
         } else if b == ScopedVisibilityConstraintId::ALWAYS_FALSE {
-            return ScopedVisibilityConstraintId::ALWAYS_FALSE;
-        }
-        match (&self.constraints[a], &self.constraints[b]) {
-            (_, VisibilityConstraint::VisibleIfNot(id)) if a == *id => {
-                ScopedVisibilityConstraintId::ALWAYS_FALSE
-            }
-            (VisibilityConstraint::VisibleIfNot(id), _) if *id == b => {
-                ScopedVisibilityConstraintId::ALWAYS_FALSE
-            }
-            _ => self.add(VisibilityConstraint::KleeneAnd(a, b)),
+            ScopedVisibilityConstraintId::ALWAYS_FALSE
+        } else {
+            self.add(VisibilityConstraint::KleeneAnd(a, b))
         }
     }
 

From 6b53554f4d3891a6aded2bfbdd13ab139e692176 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 11:34:15 -0500
Subject: [PATCH 09/35] These are now unresolved I guess?

---
 .../resources/mdtest/exception/basic.md                        | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
index 1c53bc754cc0a..1e938ede86e10 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
@@ -158,8 +158,9 @@ except KeyboardInterrupt as e:  # fine
 try:
     raise
 except int as e:  # error: [invalid-exception-caught]
+    # error: [unresolved-reference]
     reveal_type(e)  # revealed: Unknown
-    raise KeyError from e
+    raise KeyError from e  # error: [unresolved-reference]
 
 def _(e: Exception | type[Exception]):
     raise ModuleNotFoundError from e  # fine

From bb11cf8173cf025a7239412f07f731fa757041db Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 11:36:19 -0500
Subject: [PATCH 10/35] clippy

---
 .../src/visibility_constraints.rs                    | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index 93845a6b1c248..b8e09fc091b38 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -211,9 +211,9 @@ impl<'db> VisibilityConstraints<'db> {
             return b;
         } else if b == ScopedVisibilityConstraintId::ALWAYS_FALSE {
             return a;
-        } else if a == ScopedVisibilityConstraintId::ALWAYS_TRUE {
-            return ScopedVisibilityConstraintId::ALWAYS_TRUE;
-        } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE {
+        } else if a == ScopedVisibilityConstraintId::ALWAYS_TRUE
+            || b == ScopedVisibilityConstraintId::ALWAYS_TRUE
+        {
             return ScopedVisibilityConstraintId::ALWAYS_TRUE;
         }
         match (&self.constraints[a], &self.constraints[b]) {
@@ -236,9 +236,9 @@ impl<'db> VisibilityConstraints<'db> {
             b
         } else if b == ScopedVisibilityConstraintId::ALWAYS_TRUE {
             a
-        } else if a == ScopedVisibilityConstraintId::ALWAYS_FALSE {
-            ScopedVisibilityConstraintId::ALWAYS_FALSE
-        } else if b == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+        } else if a == ScopedVisibilityConstraintId::ALWAYS_FALSE
+            || b == ScopedVisibilityConstraintId::ALWAYS_FALSE
+        {
             ScopedVisibilityConstraintId::ALWAYS_FALSE
         } else {
             self.add(VisibilityConstraint::KleeneAnd(a, b))

From a2ef7028e297548018a30ab3f1e2f8e23aeb0b3c Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 11:55:41 -0500
Subject: [PATCH 11/35] Normalize negations of ALWAYS_{TRUE,FALSE}

---
 .../src/semantic_index/builder.rs                   |  2 +-
 .../src/semantic_index/use_def.rs                   |  9 +++++++++
 .../src/visibility_constraints.rs                   | 13 +++++++++++++
 3 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index fcf5cfe23570b..486cf3a0a1651 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -356,7 +356,7 @@ impl<'db> SemanticIndexBuilder<'db> {
         constraint: ScopedVisibilityConstraintId,
     ) -> ScopedVisibilityConstraintId {
         self.current_use_def_map_mut()
-            .record_visibility_constraint(VisibilityConstraint::VisibleIfNot(constraint))
+            .record_negated_visibility_constraint_id(constraint)
     }
 
     /// Records a visibility constraint by applying it to all live bindings and declarations.
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 06ec797504476..8f253393b636f 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -583,6 +583,15 @@ impl<'db> UseDefMapBuilder<'db> {
             .add_and_constraint(self.scope_start_visibility, constraint);
     }
 
+    pub(super) fn record_negated_visibility_constraint_id(
+        &mut self,
+        constraint: ScopedVisibilityConstraintId,
+    ) -> ScopedVisibilityConstraintId {
+        let new_constraint_id = self.visibility_constraints.add_not_constraint(constraint);
+        self.record_visibility_constraint_id(new_constraint_id);
+        new_constraint_id
+    }
+
     pub(super) fn record_visibility_constraint(
         &mut self,
         constraint: VisibilityConstraint<'db>,
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index b8e09fc091b38..b9492b60e9785 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -202,6 +202,19 @@ impl<'db> VisibilityConstraints<'db> {
         self.constraints.push(constraint)
     }
 
+    pub(crate) fn add_not_constraint(
+        &mut self,
+        a: ScopedVisibilityConstraintId,
+    ) -> ScopedVisibilityConstraintId {
+        if a == ScopedVisibilityConstraintId::ALWAYS_TRUE {
+            ScopedVisibilityConstraintId::ALWAYS_FALSE
+        } else if a == ScopedVisibilityConstraintId::ALWAYS_FALSE {
+            ScopedVisibilityConstraintId::ALWAYS_TRUE
+        } else {
+            self.add(VisibilityConstraint::VisibleIfNot(a))
+        }
+    }
+
     pub(crate) fn add_or_constraint(
         &mut self,
         a: ScopedVisibilityConstraintId,

From 1c42a2b598a35372cf0205093948b8c6dbeffe9a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 13:46:38 -0500
Subject: [PATCH 12/35] scope_start_visibility _is_ reachability

---
 .../src/semantic_index/use_def.rs             | 21 ++++---------------
 1 file changed, 4 insertions(+), 17 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 8f253393b636f..6136bc09f4ae4 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -477,7 +477,6 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
-    reachability: ScopedVisibilityConstraintId,
 }
 
 pub(super) struct UseDefMapBuilder<'db> {
@@ -506,8 +505,6 @@ pub(super) struct UseDefMapBuilder<'db> {
 
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
-
-    reachability: ScopedVisibilityConstraintId,
 }
 
 impl<'db> UseDefMapBuilder<'db> {
@@ -521,12 +518,10 @@ impl<'db> UseDefMapBuilder<'db> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
-            reachability: ScopedVisibilityConstraintId::ALWAYS_TRUE,
         }
     }
 
     pub(super) fn mark_unreachable(&mut self) {
-        self.reachability = ScopedVisibilityConstraintId::ALWAYS_FALSE;
         self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
     }
 
@@ -544,7 +539,7 @@ impl<'db> UseDefMapBuilder<'db> {
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id, self.reachability);
+        symbol_state.record_binding(def_id, self.scope_start_visibility);
     }
 
     pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
@@ -658,7 +653,7 @@ impl<'db> UseDefMapBuilder<'db> {
         let def_id = self.all_definitions.push(Some(definition));
         let symbol_state = &mut self.symbol_states[symbol];
         symbol_state.record_declaration(def_id);
-        symbol_state.record_binding(def_id, self.reachability);
+        symbol_state.record_binding(def_id, self.scope_start_visibility);
     }
 
     pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
@@ -675,7 +670,6 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
-            reachability: self.reachability,
         }
     }
 
@@ -698,8 +692,6 @@ impl<'db> UseDefMapBuilder<'db> {
             num_symbols,
             SymbolState::undefined(self.scope_start_visibility),
         );
-
-        self.reachability = snapshot.reachability;
     }
 
     /// Merge the given snapshot into the current state, reflecting that we might have taken either
@@ -715,14 +707,14 @@ impl<'db> UseDefMapBuilder<'db> {
         // we can determine whether any particular binding is non-visible due to unreachability.
         if self
             .visibility_constraints
-            .evaluate_without_inference(self.db, snapshot.reachability)
+            .evaluate_without_inference(self.db, snapshot.scope_start_visibility)
             .is_always_false()
         {
             return;
         }
         if self
             .visibility_constraints
-            .evaluate_without_inference(self.db, self.reachability)
+            .evaluate_without_inference(self.db, self.scope_start_visibility)
             .is_always_false()
         {
             self.restore(snapshot);
@@ -750,11 +742,6 @@ impl<'db> UseDefMapBuilder<'db> {
         self.scope_start_visibility = self
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
-
-        // The merged result is reachability when either of the merged flows is.
-        self.reachability = self
-            .visibility_constraints
-            .add_or_constraint(self.reachability, snapshot.reachability);
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {

From 289c0c65bfdf56a5e61692ad78adc641af76e025 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 13:47:54 -0500
Subject: [PATCH 13/35] No, bindings are always visible

---
 .../src/semantic_index/use_def.rs             |  4 +-
 .../semantic_index/use_def/symbol_state.rs    | 52 +++++--------------
 2 files changed, 14 insertions(+), 42 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 6136bc09f4ae4..dd0867e62f8b3 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -539,7 +539,7 @@ impl<'db> UseDefMapBuilder<'db> {
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id, self.scope_start_visibility);
+        symbol_state.record_binding(def_id);
     }
 
     pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
@@ -653,7 +653,7 @@ impl<'db> UseDefMapBuilder<'db> {
         let def_id = self.all_definitions.push(Some(definition));
         let symbol_state = &mut self.symbol_states[symbol];
         symbol_state.record_declaration(def_id);
-        symbol_state.record_binding(def_id, self.scope_start_visibility);
+        symbol_state.record_binding(def_id);
     }
 
     pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
index 154cb223321a3..4bf28f9957d90 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
@@ -254,11 +254,7 @@ impl SymbolBindings {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(
-        &mut self,
-        binding_id: ScopedDefinitionId,
-        visibility: ScopedVisibilityConstraintId,
-    ) {
+    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
         // The new binding replaces all previous live bindings in this path, and has no
         // constraints.
         self.live_bindings = Bindings::with(binding_id.into());
@@ -266,7 +262,8 @@ impl SymbolBindings {
         self.constraints.push(Constraints::default());
 
         self.visibility_constraints = VisibilityConstraintPerBinding::with_capacity(1);
-        self.visibility_constraints.push(visibility);
+        self.visibility_constraints
+            .push(ScopedVisibilityConstraintId::ALWAYS_TRUE);
     }
 
     /// Add given constraint to all live bindings.
@@ -369,13 +366,9 @@ impl SymbolState {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(
-        &mut self,
-        binding_id: ScopedDefinitionId,
-        visibility: ScopedVisibilityConstraintId,
-    ) {
+    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
         debug_assert_ne!(binding_id, ScopedDefinitionId::UNBOUND);
-        self.bindings.record_binding(binding_id, visibility);
+        self.bindings.record_binding(binding_id);
     }
 
     /// Add given constraint to all live bindings.
@@ -581,10 +574,7 @@ mod tests {
     #[test]
     fn with() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(
-            ScopedDefinitionId::from_u32(1),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym.record_binding(ScopedDefinitionId::from_u32(1));
 
         assert_bindings(&sym, &["1<>"]);
     }
@@ -592,10 +582,7 @@ mod tests {
     #[test]
     fn record_constraint() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(
-            ScopedDefinitionId::from_u32(1),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym.record_binding(ScopedDefinitionId::from_u32(1));
         sym.record_constraint(ScopedConstraintId::from_u32(0));
 
         assert_bindings(&sym, &["1<0>"]);
@@ -607,17 +594,11 @@ mod tests {
 
         // merging the same definition with the same constraint keeps the constraint
         let mut sym1a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1a.record_binding(
-            ScopedDefinitionId::from_u32(1),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym1a.record_binding(ScopedDefinitionId::from_u32(1));
         sym1a.record_constraint(ScopedConstraintId::from_u32(0));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(
-            ScopedDefinitionId::from_u32(1),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym1b.record_binding(ScopedDefinitionId::from_u32(1));
         sym1b.record_constraint(ScopedConstraintId::from_u32(0));
 
         sym1a.merge(sym1b, &mut visibility_constraints);
@@ -626,17 +607,11 @@ mod tests {
 
         // merging the same definition with differing constraints drops all constraints
         let mut sym2a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym2a.record_binding(
-            ScopedDefinitionId::from_u32(2),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym2a.record_binding(ScopedDefinitionId::from_u32(2));
         sym2a.record_constraint(ScopedConstraintId::from_u32(1));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(
-            ScopedDefinitionId::from_u32(2),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym1b.record_binding(ScopedDefinitionId::from_u32(2));
         sym1b.record_constraint(ScopedConstraintId::from_u32(2));
 
         sym2a.merge(sym1b, &mut visibility_constraints);
@@ -645,10 +620,7 @@ mod tests {
 
         // merging a constrained definition with unbound keeps both
         let mut sym3a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym3a.record_binding(
-            ScopedDefinitionId::from_u32(3),
-            ScopedVisibilityConstraintId::ALWAYS_TRUE,
-        );
+        sym3a.record_binding(ScopedDefinitionId::from_u32(3));
         sym3a.record_constraint(ScopedConstraintId::from_u32(3));
 
         let sym2b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);

From 8b0899f92a897e5bada54f6c552e864ad3639a4d Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 13:54:16 -0500
Subject: [PATCH 14/35] TODO for `raise`/`else` unreachability

---
 .../resources/mdtest/terminal_statements.md               | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

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 6a3427e211c84..57d3ff7f2a5db 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -452,12 +452,16 @@ def raise_in_both_branches(cond: bool):
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
         reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
     else:
+        # This should not be included below, but we do not currently model that control flows that
+        # terminate via `raise` cannot enter the `else` clause.
         x = "unreachable"
     finally:
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
-        reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
+        # TODO: Literal["before", "raise1", "raise2"]
+        reveal_type(x)  # revealed: Literal["before", "raise1", "raise2", "unreachable"]
     # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
-    reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
+    # TODO: Literal["before", "raise1", "raise2"]
+    reveal_type(x)  # revealed: Literal["before", "raise1", "raise2", "unreachable"]
 
 def raise_in_nested_then_branch(cond1: bool, cond2: bool):
     x = "before"

From 9cd8e6849720691fff47c23a6d821f59c1e5050a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 13:59:45 -0500
Subject: [PATCH 15/35] Fix test failure

---
 .../resources/mdtest/exception/basic.md                        | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
index 1e938ede86e10..1c53bc754cc0a 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
@@ -158,9 +158,8 @@ except KeyboardInterrupt as e:  # fine
 try:
     raise
 except int as e:  # error: [invalid-exception-caught]
-    # error: [unresolved-reference]
     reveal_type(e)  # revealed: Unknown
-    raise KeyError from e  # error: [unresolved-reference]
+    raise KeyError from e
 
 def _(e: Exception | type[Exception]):
     raise ModuleNotFoundError from e  # fine

From 1a80f819eccd5395beeab68e50dfe7843f30620b Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 14:00:48 -0500
Subject: [PATCH 16/35] Expected test case change

---
 .../resources/mdtest/terminal_statements.md                     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 57d3ff7f2a5db..4b90ae6160055 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -640,5 +640,5 @@ def _(cond: bool):
             return
 
     # TODO: Literal["a"]
-    reveal_type(x)  # revealed: Literal["a", "b"]
+    reveal_type(x)  # revealed: Literal["a"]
 ```

From f71325c23fb19d775294ad57582a8acb1a2ca69c Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 16:25:26 -0500
Subject: [PATCH 17/35] Try to skip simplification by checking
 scope_start_visibility

---
 .../src/semantic_index/use_def.rs                         | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index dd0867e62f8b3..9f594a1d8d3e3 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -617,6 +617,14 @@ impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) {
         debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
 
+        if !self
+            .visibility_constraints
+            .evaluate_without_inference(self.db, self.scope_start_visibility)
+            .is_always_true()
+        {
+            return;
+        }
+
         self.scope_start_visibility = snapshot.scope_start_visibility;
 
         // Note that this loop terminates when we reach a symbol not present in the snapshot.

From 0e0601200b26604e92f66b56cccbe84db12094b0 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 16:26:23 -0500
Subject: [PATCH 18/35] And try via a separate `always_reachable` boolean

---
 .../src/semantic_index/use_def.rs                | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 9f594a1d8d3e3..850330fea2ba1 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -477,6 +477,7 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
+    always_reachable: bool,
 }
 
 pub(super) struct UseDefMapBuilder<'db> {
@@ -505,6 +506,8 @@ pub(super) struct UseDefMapBuilder<'db> {
 
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
+
+    always_reachable: bool,
 }
 
 impl<'db> UseDefMapBuilder<'db> {
@@ -518,11 +521,13 @@ impl<'db> UseDefMapBuilder<'db> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
+            always_reachable: true,
         }
     }
 
     pub(super) fn mark_unreachable(&mut self) {
         self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
+        self.always_reachable = false;
     }
 
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {
@@ -617,11 +622,7 @@ impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) {
         debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
 
-        if !self
-            .visibility_constraints
-            .evaluate_without_inference(self.db, self.scope_start_visibility)
-            .is_always_true()
-        {
+        if !self.always_reachable {
             return;
         }
 
@@ -678,6 +679,7 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
+            always_reachable: self.always_reachable,
         }
     }
 
@@ -692,6 +694,7 @@ impl<'db> UseDefMapBuilder<'db> {
         // Restore the current visible-definitions state to the given snapshot.
         self.symbol_states = snapshot.symbol_states;
         self.scope_start_visibility = snapshot.scope_start_visibility;
+        self.always_reachable = snapshot.always_reachable;
 
         // If the snapshot we are restoring is missing some symbols we've recorded since, we need
         // to fill them in so the symbol IDs continue to line up. Since they don't exist in the
@@ -706,6 +709,7 @@ impl<'db> UseDefMapBuilder<'db> {
     /// path to get here. The new state for each symbol should include definitions from both the
     /// prior state and the snapshot.
     pub(super) fn merge(&mut self, snapshot: FlowSnapshot) {
+        /*
         // As an optimization, if we know statically that either of the snapshots is always
         // unreachable, we can leave it out of the merged result entirely. Note that we cannot
         // perform any type inference at this point, so this is largely limited to unreachability
@@ -728,6 +732,7 @@ impl<'db> UseDefMapBuilder<'db> {
             self.restore(snapshot);
             return;
         }
+        */
 
         // We never remove symbols from `symbol_states` (it's an IndexVec, and the symbol
         // IDs must line up), so the current number of known symbols must always be equal to or
@@ -750,6 +755,7 @@ impl<'db> UseDefMapBuilder<'db> {
         self.scope_start_visibility = self
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
+        self.always_reachable &= snapshot.always_reachable;
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {

From b3b4577bc11485b5cdcc2ea6012de5fd6cff31ec Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 16:56:22 -0500
Subject: [PATCH 19/35] Add AlwaysFalse as its own constraint variant

---
 .../src/visibility_constraints.rs                      | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index b9492b60e9785..f543339f13d5a 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -171,6 +171,7 @@ const MAX_RECURSION_DEPTH: usize = 24;
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub(crate) enum VisibilityConstraint<'db> {
     AlwaysTrue,
+    AlwaysFalse,
     Ambiguous,
     VisibleIf(Constraint<'db>),
     VisibleIfNot(ScopedVisibilityConstraintId),
@@ -188,7 +189,7 @@ impl Default for VisibilityConstraints<'_> {
         Self {
             constraints: IndexVec::from_iter([
                 VisibilityConstraint::AlwaysTrue,
-                VisibilityConstraint::VisibleIfNot(ScopedVisibilityConstraintId::ALWAYS_TRUE),
+                VisibilityConstraint::AlwaysFalse,
             ]),
         }
     }
@@ -199,7 +200,11 @@ impl<'db> VisibilityConstraints<'db> {
         &mut self,
         constraint: VisibilityConstraint<'db>,
     ) -> ScopedVisibilityConstraintId {
-        self.constraints.push(constraint)
+        match constraint {
+            VisibilityConstraint::AlwaysTrue => ScopedVisibilityConstraintId::ALWAYS_TRUE,
+            VisibilityConstraint::AlwaysFalse => ScopedVisibilityConstraintId::ALWAYS_FALSE,
+            _ => self.constraints.push(constraint),
+        }
     }
 
     pub(crate) fn add_not_constraint(
@@ -286,6 +291,7 @@ impl<'db> VisibilityConstraints<'db> {
         let visibility_constraint = &self.constraints[id];
         match visibility_constraint {
             VisibilityConstraint::AlwaysTrue => Truthiness::AlwaysTrue,
+            VisibilityConstraint::AlwaysFalse => Truthiness::AlwaysFalse,
             VisibilityConstraint::Ambiguous => Truthiness::Ambiguous,
             VisibilityConstraint::VisibleIf(constraint) => {
                 if INFERENCE_ALLOWED {

From 46b1ec2ba3bf8b3e53852323a2aff875ac3afaa6 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 17:01:28 -0500
Subject: [PATCH 20/35] Update always_reachable on merge correctly

---
 crates/red_knot_python_semantic/src/semantic_index/use_def.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 850330fea2ba1..fb4a144dd070f 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -709,7 +709,6 @@ impl<'db> UseDefMapBuilder<'db> {
     /// path to get here. The new state for each symbol should include definitions from both the
     /// prior state and the snapshot.
     pub(super) fn merge(&mut self, snapshot: FlowSnapshot) {
-        /*
         // As an optimization, if we know statically that either of the snapshots is always
         // unreachable, we can leave it out of the merged result entirely. Note that we cannot
         // perform any type inference at this point, so this is largely limited to unreachability
@@ -722,6 +721,7 @@ impl<'db> UseDefMapBuilder<'db> {
             .evaluate_without_inference(self.db, snapshot.scope_start_visibility)
             .is_always_false()
         {
+            self.always_reachable = false;
             return;
         }
         if self
@@ -730,9 +730,9 @@ impl<'db> UseDefMapBuilder<'db> {
             .is_always_false()
         {
             self.restore(snapshot);
+            self.always_reachable = false;
             return;
         }
-        */
 
         // We never remove symbols from `symbol_states` (it's an IndexVec, and the symbol
         // IDs must line up), so the current number of known symbols must always be equal to or

From 999188a1728c28aa5a31b8da2037ea15774476ff Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 17:02:45 -0500
Subject: [PATCH 21/35] Try checking if reachability contains AlwaysFalse in
 syntax tree

---
 .../src/semantic_index/use_def.rs             | 15 +++-----
 .../src/visibility_constraints.rs             | 34 +++++++++++++++++++
 2 files changed, 38 insertions(+), 11 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index fb4a144dd070f..b23341b1dee9b 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -477,7 +477,6 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
-    always_reachable: bool,
 }
 
 pub(super) struct UseDefMapBuilder<'db> {
@@ -506,8 +505,6 @@ pub(super) struct UseDefMapBuilder<'db> {
 
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
-
-    always_reachable: bool,
 }
 
 impl<'db> UseDefMapBuilder<'db> {
@@ -521,13 +518,11 @@ impl<'db> UseDefMapBuilder<'db> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
-            always_reachable: true,
         }
     }
 
     pub(super) fn mark_unreachable(&mut self) {
         self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
-        self.always_reachable = false;
     }
 
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {
@@ -622,7 +617,10 @@ impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) {
         debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
 
-        if !self.always_reachable {
+        if self
+            .visibility_constraints
+            .contains_always_false(self.scope_start_visibility)
+        {
             return;
         }
 
@@ -679,7 +677,6 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
-            always_reachable: self.always_reachable,
         }
     }
 
@@ -694,7 +691,6 @@ impl<'db> UseDefMapBuilder<'db> {
         // Restore the current visible-definitions state to the given snapshot.
         self.symbol_states = snapshot.symbol_states;
         self.scope_start_visibility = snapshot.scope_start_visibility;
-        self.always_reachable = snapshot.always_reachable;
 
         // If the snapshot we are restoring is missing some symbols we've recorded since, we need
         // to fill them in so the symbol IDs continue to line up. Since they don't exist in the
@@ -721,7 +717,6 @@ impl<'db> UseDefMapBuilder<'db> {
             .evaluate_without_inference(self.db, snapshot.scope_start_visibility)
             .is_always_false()
         {
-            self.always_reachable = false;
             return;
         }
         if self
@@ -730,7 +725,6 @@ impl<'db> UseDefMapBuilder<'db> {
             .is_always_false()
         {
             self.restore(snapshot);
-            self.always_reachable = false;
             return;
         }
 
@@ -755,7 +749,6 @@ impl<'db> UseDefMapBuilder<'db> {
         self.scope_start_visibility = self
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
-        self.always_reachable &= snapshot.always_reachable;
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index f543339f13d5a..e6256b5e8399b 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -273,6 +273,40 @@ impl<'db> VisibilityConstraints<'db> {
         self.evaluate_impl::<false>(db, id, MAX_RECURSION_DEPTH)
     }
 
+    pub(crate) fn contains_always_false(&self, id: ScopedVisibilityConstraintId) -> bool {
+        let visibility_constraint = &self.constraints[id];
+        match visibility_constraint {
+            VisibilityConstraint::AlwaysTrue => false,
+            VisibilityConstraint::AlwaysFalse => true,
+            VisibilityConstraint::Ambiguous => false,
+            VisibilityConstraint::VisibleIf(_) => false,
+            VisibilityConstraint::VisibleIfNot(negated) => self.contains_always_true(*negated),
+            VisibilityConstraint::KleeneAnd(lhs, rhs) => {
+                self.contains_always_false(*lhs) || self.contains_always_false(*rhs)
+            }
+            VisibilityConstraint::KleeneOr(lhs, rhs) => {
+                self.contains_always_false(*lhs) || self.contains_always_false(*rhs)
+            }
+        }
+    }
+
+    pub(crate) fn contains_always_true(&self, id: ScopedVisibilityConstraintId) -> bool {
+        let visibility_constraint = &self.constraints[id];
+        match visibility_constraint {
+            VisibilityConstraint::AlwaysTrue => true,
+            VisibilityConstraint::AlwaysFalse => false,
+            VisibilityConstraint::Ambiguous => false,
+            VisibilityConstraint::VisibleIf(_) => false,
+            VisibilityConstraint::VisibleIfNot(negated) => self.contains_always_false(*negated),
+            VisibilityConstraint::KleeneAnd(lhs, rhs) => {
+                self.contains_always_true(*lhs) || self.contains_always_true(*rhs)
+            }
+            VisibilityConstraint::KleeneOr(lhs, rhs) => {
+                self.contains_always_true(*lhs) || self.contains_always_true(*rhs)
+            }
+        }
+    }
+
     /// Analyze the statically known visibility for a given visibility constraint.
     pub(crate) fn evaluate(&self, db: &'db dyn Db, id: ScopedVisibilityConstraintId) -> Truthiness {
         self.evaluate_impl::<true>(db, id, MAX_RECURSION_DEPTH)

From 0f278dafc6546203113c48aa3831c96b8b714132 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Thu, 30 Jan 2025 17:02:58 -0500
Subject: [PATCH 22/35] But that doesn't work either

(because OR-ing reachability on merge throws away the AlwaysFalse)
---
 .../src/semantic_index/use_def.rs             | 15 +++++---
 .../src/visibility_constraints.rs             | 34 -------------------
 2 files changed, 11 insertions(+), 38 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index b23341b1dee9b..fb4a144dd070f 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -477,6 +477,7 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
+    always_reachable: bool,
 }
 
 pub(super) struct UseDefMapBuilder<'db> {
@@ -505,6 +506,8 @@ pub(super) struct UseDefMapBuilder<'db> {
 
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
+
+    always_reachable: bool,
 }
 
 impl<'db> UseDefMapBuilder<'db> {
@@ -518,11 +521,13 @@ impl<'db> UseDefMapBuilder<'db> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
+            always_reachable: true,
         }
     }
 
     pub(super) fn mark_unreachable(&mut self) {
         self.record_visibility_constraint_id(ScopedVisibilityConstraintId::ALWAYS_FALSE);
+        self.always_reachable = false;
     }
 
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {
@@ -617,10 +622,7 @@ impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) {
         debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
 
-        if self
-            .visibility_constraints
-            .contains_always_false(self.scope_start_visibility)
-        {
+        if !self.always_reachable {
             return;
         }
 
@@ -677,6 +679,7 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
+            always_reachable: self.always_reachable,
         }
     }
 
@@ -691,6 +694,7 @@ impl<'db> UseDefMapBuilder<'db> {
         // Restore the current visible-definitions state to the given snapshot.
         self.symbol_states = snapshot.symbol_states;
         self.scope_start_visibility = snapshot.scope_start_visibility;
+        self.always_reachable = snapshot.always_reachable;
 
         // If the snapshot we are restoring is missing some symbols we've recorded since, we need
         // to fill them in so the symbol IDs continue to line up. Since they don't exist in the
@@ -717,6 +721,7 @@ impl<'db> UseDefMapBuilder<'db> {
             .evaluate_without_inference(self.db, snapshot.scope_start_visibility)
             .is_always_false()
         {
+            self.always_reachable = false;
             return;
         }
         if self
@@ -725,6 +730,7 @@ impl<'db> UseDefMapBuilder<'db> {
             .is_always_false()
         {
             self.restore(snapshot);
+            self.always_reachable = false;
             return;
         }
 
@@ -749,6 +755,7 @@ impl<'db> UseDefMapBuilder<'db> {
         self.scope_start_visibility = self
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
+        self.always_reachable &= snapshot.always_reachable;
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
index e6256b5e8399b..f543339f13d5a 100644
--- a/crates/red_knot_python_semantic/src/visibility_constraints.rs
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -273,40 +273,6 @@ impl<'db> VisibilityConstraints<'db> {
         self.evaluate_impl::<false>(db, id, MAX_RECURSION_DEPTH)
     }
 
-    pub(crate) fn contains_always_false(&self, id: ScopedVisibilityConstraintId) -> bool {
-        let visibility_constraint = &self.constraints[id];
-        match visibility_constraint {
-            VisibilityConstraint::AlwaysTrue => false,
-            VisibilityConstraint::AlwaysFalse => true,
-            VisibilityConstraint::Ambiguous => false,
-            VisibilityConstraint::VisibleIf(_) => false,
-            VisibilityConstraint::VisibleIfNot(negated) => self.contains_always_true(*negated),
-            VisibilityConstraint::KleeneAnd(lhs, rhs) => {
-                self.contains_always_false(*lhs) || self.contains_always_false(*rhs)
-            }
-            VisibilityConstraint::KleeneOr(lhs, rhs) => {
-                self.contains_always_false(*lhs) || self.contains_always_false(*rhs)
-            }
-        }
-    }
-
-    pub(crate) fn contains_always_true(&self, id: ScopedVisibilityConstraintId) -> bool {
-        let visibility_constraint = &self.constraints[id];
-        match visibility_constraint {
-            VisibilityConstraint::AlwaysTrue => true,
-            VisibilityConstraint::AlwaysFalse => false,
-            VisibilityConstraint::Ambiguous => false,
-            VisibilityConstraint::VisibleIf(_) => false,
-            VisibilityConstraint::VisibleIfNot(negated) => self.contains_always_false(*negated),
-            VisibilityConstraint::KleeneAnd(lhs, rhs) => {
-                self.contains_always_true(*lhs) || self.contains_always_true(*rhs)
-            }
-            VisibilityConstraint::KleeneOr(lhs, rhs) => {
-                self.contains_always_true(*lhs) || self.contains_always_true(*rhs)
-            }
-        }
-    }
-
     /// Analyze the statically known visibility for a given visibility constraint.
     pub(crate) fn evaluate(&self, db: &'db dyn Db, id: ScopedVisibilityConstraintId) -> Truthiness {
         self.evaluate_impl::<true>(db, id, MAX_RECURSION_DEPTH)

From c882a9566f02898d76e68db151d2c4de3a2a03be Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 14:42:24 -0500
Subject: [PATCH 23/35] This is working again

---
 .../resources/mdtest/terminal_statements.md                 | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

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 4b90ae6160055..c2627beda6daf 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -457,11 +457,9 @@ def raise_in_both_branches(cond: bool):
         x = "unreachable"
     finally:
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
-        # TODO: Literal["before", "raise1", "raise2"]
-        reveal_type(x)  # revealed: Literal["before", "raise1", "raise2", "unreachable"]
+        reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
     # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
-    # TODO: Literal["before", "raise1", "raise2"]
-    reveal_type(x)  # revealed: Literal["before", "raise1", "raise2", "unreachable"]
+    reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
 
 def raise_in_nested_then_branch(cond1: bool, cond2: bool):
     x = "before"

From 33db6f1e589092026c7e8c7f8edb4038e6f8099d Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 14:48:59 -0500
Subject: [PATCH 24/35] Remove static bool

---
 .../src/semantic_index/use_def.rs                | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 7f30410152e19..efed05ec0af16 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -478,7 +478,6 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 pub(super) struct FlowSnapshot {
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
     scope_start_visibility: ScopedVisibilityConstraintId,
-    always_reachable: bool,
 }
 
 pub(super) struct UseDefMapBuilder<'db> {
@@ -505,8 +504,6 @@ pub(super) struct UseDefMapBuilder<'db> {
 
     /// Currently live bindings and declarations for each symbol.
     symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
-
-    always_reachable: bool,
 }
 
 impl Default for UseDefMapBuilder<'_> {
@@ -519,7 +516,6 @@ impl Default for UseDefMapBuilder<'_> {
             bindings_by_use: IndexVec::new(),
             definitions_by_definition: FxHashMap::default(),
             symbol_states: IndexVec::new(),
-            always_reachable: true,
         }
     }
 }
@@ -527,7 +523,6 @@ impl Default for UseDefMapBuilder<'_> {
 impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn mark_unreachable(&mut self) {
         self.record_visibility_constraint(ScopedVisibilityConstraintId::ALWAYS_FALSE);
-        self.always_reachable = false;
     }
 
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {
@@ -596,12 +591,12 @@ impl<'db> UseDefMapBuilder<'db> {
     pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot) {
         debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
 
-        if !self.always_reachable {
+        // If there are any control flow paths that have become unreachable between `snapshot` and
+        // now, then it's not valid to simplify any visibility constraints to `snapshot`.
+        if self.scope_start_visibility != snapshot.scope_start_visibility {
             return;
         }
 
-        self.scope_start_visibility = snapshot.scope_start_visibility;
-
         // Note that this loop terminates when we reach a symbol not present in the snapshot.
         // This means we keep visibility constraints for all new symbols, which is intended,
         // since these symbols have been introduced in the corresponding branch, which might
@@ -653,7 +648,6 @@ impl<'db> UseDefMapBuilder<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
             scope_start_visibility: self.scope_start_visibility,
-            always_reachable: self.always_reachable,
         }
     }
 
@@ -668,7 +662,6 @@ impl<'db> UseDefMapBuilder<'db> {
         // Restore the current visible-definitions state to the given snapshot.
         self.symbol_states = snapshot.symbol_states;
         self.scope_start_visibility = snapshot.scope_start_visibility;
-        self.always_reachable = snapshot.always_reachable;
 
         // If the snapshot we are restoring is missing some symbols we've recorded since, we need
         // to fill them in so the symbol IDs continue to line up. Since they don't exist in the
@@ -691,12 +684,10 @@ impl<'db> UseDefMapBuilder<'db> {
         // bindings will include this reachability condition, so that later during type inference,
         // we can determine whether any particular binding is non-visible due to unreachability.
         if snapshot.scope_start_visibility == ScopedVisibilityConstraintId::ALWAYS_FALSE {
-            self.always_reachable = false;
             return;
         }
         if self.scope_start_visibility == ScopedVisibilityConstraintId::ALWAYS_FALSE {
             self.restore(snapshot);
-            self.always_reachable = false;
             return;
         }
 
@@ -721,7 +712,6 @@ impl<'db> UseDefMapBuilder<'db> {
         self.scope_start_visibility = self
             .visibility_constraints
             .add_or_constraint(self.scope_start_visibility, snapshot.scope_start_visibility);
-        self.always_reachable &= snapshot.always_reachable;
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {

From b49916d61360ef2e3b463da9d1d8b0e7324a98e9 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 14:50:46 -0500
Subject: [PATCH 25/35] Remove moot comment

---
 .../resources/mdtest/terminal_statements.md                     | 2 --
 1 file changed, 2 deletions(-)

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 c2627beda6daf..878c01fb9bdcb 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -452,8 +452,6 @@ def raise_in_both_branches(cond: bool):
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
         reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
     else:
-        # This should not be included below, but we do not currently model that control flows that
-        # terminate via `raise` cannot enter the `else` clause.
         x = "unreachable"
     finally:
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities

From c80f27e3d7cbb4beaf3a095e6e067608a4f6bdc5 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 14:51:04 -0500
Subject: [PATCH 26/35] And another

---
 .../resources/mdtest/terminal_statements.md                      | 1 -
 1 file changed, 1 deletion(-)

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 878c01fb9bdcb..5888847b84f7d 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -635,6 +635,5 @@ def _(cond: bool):
         if True:
             return
 
-    # TODO: Literal["a"]
     reveal_type(x)  # revealed: Literal["a"]
 ```

From 0d50385c9a897b23c4ce74d4d218546d55b22745 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 15:18:50 -0500
Subject: [PATCH 27/35] New bindings are visible only if control flow is
 reachable

---
 .../resources/mdtest/exception/basic.md       |  3 +-
 .../src/semantic_index/use_def.rs             |  4 +-
 .../semantic_index/use_def/symbol_state.rs    | 53 ++++++++++++++-----
 3 files changed, 45 insertions(+), 15 deletions(-)

diff --git a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
index 1c53bc754cc0a..1e938ede86e10 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
@@ -158,8 +158,9 @@ except KeyboardInterrupt as e:  # fine
 try:
     raise
 except int as e:  # error: [invalid-exception-caught]
+    # error: [unresolved-reference]
     reveal_type(e)  # revealed: Unknown
-    raise KeyError from e
+    raise KeyError from e  # error: [unresolved-reference]
 
 def _(e: Exception | type[Exception]):
     raise ModuleNotFoundError from e  # fine
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index efed05ec0af16..1dfac3a5a4d79 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -539,7 +539,7 @@ impl<'db> UseDefMapBuilder<'db> {
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id);
+        symbol_state.record_binding(def_id, self.scope_start_visibility);
     }
 
     pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
@@ -631,7 +631,7 @@ impl<'db> UseDefMapBuilder<'db> {
         let def_id = self.all_definitions.push(Some(definition));
         let symbol_state = &mut self.symbol_states[symbol];
         symbol_state.record_declaration(def_id);
-        symbol_state.record_binding(def_id);
+        symbol_state.record_binding(def_id, self.scope_start_visibility);
     }
 
     pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
index 4c0c72bc6226a..487632908a8af 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs
@@ -237,7 +237,11 @@ impl SymbolBindings {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
+    pub(super) fn record_binding(
+        &mut self,
+        binding_id: ScopedDefinitionId,
+        visibility_constraint: ScopedVisibilityConstraintId,
+    ) {
         // The new binding replaces all previous live bindings in this path, and has no
         // constraints.
         self.live_bindings = Bindings::with(binding_id.into());
@@ -245,8 +249,7 @@ impl SymbolBindings {
         self.constraints.push(Constraints::default());
 
         self.visibility_constraints = VisibilityConstraintPerBinding::with_capacity(1);
-        self.visibility_constraints
-            .push(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+        self.visibility_constraints.push(visibility_constraint);
     }
 
     /// Add given constraint to all live bindings.
@@ -349,9 +352,14 @@ impl SymbolState {
     }
 
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
+    pub(super) fn record_binding(
+        &mut self,
+        binding_id: ScopedDefinitionId,
+        visibility_constraint: ScopedVisibilityConstraintId,
+    ) {
         debug_assert_ne!(binding_id, ScopedDefinitionId::UNBOUND);
-        self.bindings.record_binding(binding_id);
+        self.bindings
+            .record_binding(binding_id, visibility_constraint);
     }
 
     /// Add given constraint to all live bindings.
@@ -557,7 +565,10 @@ mod tests {
     #[test]
     fn with() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(ScopedDefinitionId::from_u32(1));
+        sym.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
 
         assert_bindings(&sym, &["1<>"]);
     }
@@ -565,7 +576,10 @@ mod tests {
     #[test]
     fn record_constraint() {
         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym.record_binding(ScopedDefinitionId::from_u32(1));
+        sym.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym.record_constraint(ScopedConstraintId::from_u32(0));
 
         assert_bindings(&sym, &["1<0>"]);
@@ -577,11 +591,17 @@ mod tests {
 
         // merging the same definition with the same constraint keeps the constraint
         let mut sym1a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1a.record_binding(ScopedDefinitionId::from_u32(1));
+        sym1a.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1a.record_constraint(ScopedConstraintId::from_u32(0));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(ScopedDefinitionId::from_u32(1));
+        sym1b.record_binding(
+            ScopedDefinitionId::from_u32(1),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1b.record_constraint(ScopedConstraintId::from_u32(0));
 
         sym1a.merge(sym1b, &mut visibility_constraints);
@@ -590,11 +610,17 @@ mod tests {
 
         // merging the same definition with differing constraints drops all constraints
         let mut sym2a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym2a.record_binding(ScopedDefinitionId::from_u32(2));
+        sym2a.record_binding(
+            ScopedDefinitionId::from_u32(2),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym2a.record_constraint(ScopedConstraintId::from_u32(1));
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym1b.record_binding(ScopedDefinitionId::from_u32(2));
+        sym1b.record_binding(
+            ScopedDefinitionId::from_u32(2),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym1b.record_constraint(ScopedConstraintId::from_u32(2));
 
         sym2a.merge(sym1b, &mut visibility_constraints);
@@ -603,7 +629,10 @@ mod tests {
 
         // merging a constrained definition with unbound keeps both
         let mut sym3a = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
-        sym3a.record_binding(ScopedDefinitionId::from_u32(3));
+        sym3a.record_binding(
+            ScopedDefinitionId::from_u32(3),
+            ScopedVisibilityConstraintId::ALWAYS_TRUE,
+        );
         sym3a.record_constraint(ScopedConstraintId::from_u32(3));
 
         let sym2b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);

From c42490cb7142e5d6c51dec49d408ff819e350c9a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Tue, 4 Feb 2025 16:02:30 -0500
Subject: [PATCH 28/35] Add xfail for RET503

---
 crates/red_knot_project/tests/check.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crates/red_knot_project/tests/check.rs b/crates/red_knot_project/tests/check.rs
index 6cdd13f32f16a..711cec75f2d23 100644
--- a/crates/red_knot_project/tests/check.rs
+++ b/crates/red_knot_project/tests/check.rs
@@ -270,6 +270,8 @@ impl SourceOrderVisitor<'_> for PullTypesVisitor<'_> {
 /// Whether or not the .py/.pyi version of this file is expected to fail
 #[rustfmt::skip]
 const KNOWN_FAILURES: &[(&str, bool, bool)] = &[
+    // related to circular references in nested functions
+    ("crates/ruff_linter/resources/test/fixtures/flake8_return/RET503.py", false, true),
     // related to circular references in class definitions
     ("crates/ruff_linter/resources/test/fixtures/pyflakes/F821_26.py", true, true),
     ("crates/ruff_linter/resources/test/fixtures/pyflakes/F821_27.py", true, true),

From 26f842b44daadd59a0b335d7e0e9f13a1d3dd762 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 09:36:20 -0500
Subject: [PATCH 29/35] Update terminal statement comment

---
 .../resources/mdtest/terminal_statements.md                 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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 5888847b84f7d..f22587a4c422e 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -623,9 +623,9 @@ def return_from_nested_if(cond1: bool, cond2: bool):
 
 ## Statically known terminal statements
 
-Terminal statements do not yet interact correctly with statically known bounds. In this example, we
-should see that the `return` statement is always executed, and therefore that the `"b"` assignment
-is not visible to the `reveal_type`.
+We model reachability using the same visibility constraints that we use to model statically known
+bounds. In this example, we see that the `return` statement is always executed, and therefore that
+the `"b"` assignment is not visible to the `reveal_type`.
 
 ```py
 def _(cond: bool):

From e5b6c4ac132c6d2f6b14a98488288162942edc7d Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 09:42:11 -0500
Subject: [PATCH 30/35] Add shorter example for bindings after terminal
 statement

---
 .../resources/mdtest/terminal_statements.md   | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

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 f22587a4c422e..513a6eee4704e 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -452,6 +452,9 @@ def raise_in_both_branches(cond: bool):
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
         reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
     else:
+        # This branch is unreachable, since all control flows in the `try` clause raise exceptions.
+        # As a result, this binding should never be reachable, since new bindings are visibile only
+        # when they are reachable.
         x = "unreachable"
     finally:
         # Exceptions can occur anywhere, so "before" and "raise" are valid possibilities
@@ -637,3 +640,21 @@ def _(cond: bool):
 
     reveal_type(x)  # revealed: Literal["a"]
 ```
+
+## Bindings after a terminal statement are unreachable
+
+Any bindings introduced after a terminal statement are unreachable, and are considered not visible.
+
+```py
+def f(cond: bool) -> str:
+    x = "before"
+    if cond:
+        reveal_type(x)  # revealed: Literal["before"]
+        return
+        x = "after-return"
+        # error: [unresolved-reference]
+        reveal_type(x)  # revealed: Unknown
+    else:
+        x = "else"
+    reveal_type(x)  # revealed: Literal["else"]
+```

From 00e236fac40e25f2037785693413416f856e50b4 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 09:44:55 -0500
Subject: [PATCH 31/35] Add back debug derive

---
 crates/red_knot_python_semantic/src/semantic_index/use_def.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
index 1dfac3a5a4d79..4d46c79152fad 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def.rs
@@ -480,6 +480,7 @@ pub(super) struct FlowSnapshot {
     scope_start_visibility: ScopedVisibilityConstraintId,
 }
 
+#[derive(Debug)]
 pub(super) struct UseDefMapBuilder<'db> {
     /// Append-only array of [`Definition`].
     all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,

From 1d936504ffbf4d835bc11fd23e6b17a97bb1ab48 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 09:46:35 -0500
Subject: [PATCH 32/35] Add TODO to function symbol comment

---
 .../src/semantic_index/builder.rs                     | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder.rs b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
index 88fcc9b6b8199..ad0655818aaf5 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -794,10 +794,13 @@ where
                             &mut first_parameter_name,
                         );
 
-                        // HACK: Visit the function body, but treat the last statement specially if
-                        // it is a return. If it is, this would cause all definitions in the
-                        // function to be marked as non-visible with our current treatment of
-                        // terminal statements. Since we currently model the externally visible
+                        // TODO: Fix how we determine the public types of symbols in a
+                        // function-like scope: https://github.com/astral-sh/ruff/issues/15777
+                        //
+                        // In the meantime, visit the function body, but treat the last statement
+                        // specially if it is a return. If it is, this would cause all definitions
+                        // in the function to be marked as non-visible with our current treatment
+                        // of terminal statements. Since we currently model the externally visible
                         // definitions in a function scope as the set of bindings that are visible
                         // at the end of the body, we then consider this function to have no
                         // externally visible definitions. To get around this, we take a flow

From ae837410464076d86fe2390f6520389ae90f46ff Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 14:57:35 -0500
Subject: [PATCH 33/35] Wrap try examples in functions to bound reachability

---
 .../resources/mdtest/exception/basic.md       | 68 ++++++++++---------
 1 file changed, 37 insertions(+), 31 deletions(-)

diff --git a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
index 1e938ede86e10..f313532303f7d 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/exception/basic.md
@@ -124,43 +124,49 @@ def _(e: Exception | type[Exception] | None):
 ## Exception cause is not an exception
 
 ```py
-try:
-    raise EOFError() from GeneratorExit  # fine
-except:
-    ...
+def _():
+    try:
+        raise EOFError() from GeneratorExit  # fine
+    except:
+        ...
 
-try:
-    raise StopIteration from MemoryError()  # fine
-except:
-    ...
+def _():
+    try:
+        raise StopIteration from MemoryError()  # fine
+    except:
+        ...
 
-try:
-    raise BufferError() from None  # fine
-except:
-    ...
+def _():
+    try:
+        raise BufferError() from None  # fine
+    except:
+        ...
 
-try:
-    raise ZeroDivisionError from False  # error: [invalid-raise]
-except:
-    ...
+def _():
+    try:
+        raise ZeroDivisionError from False  # error: [invalid-raise]
+    except:
+        ...
 
-try:
-    raise SystemExit from bool()  # error: [invalid-raise]
-except:
-    ...
+def _():
+    try:
+        raise SystemExit from bool()  # error: [invalid-raise]
+    except:
+        ...
 
-try:
-    raise
-except KeyboardInterrupt as e:  # fine
-    reveal_type(e)  # revealed: KeyboardInterrupt
-    raise LookupError from e  # fine
+def _():
+    try:
+        raise
+    except KeyboardInterrupt as e:  # fine
+        reveal_type(e)  # revealed: KeyboardInterrupt
+        raise LookupError from e  # fine
 
-try:
-    raise
-except int as e:  # error: [invalid-exception-caught]
-    # error: [unresolved-reference]
-    reveal_type(e)  # revealed: Unknown
-    raise KeyError from e  # error: [unresolved-reference]
+def _():
+    try:
+        raise
+    except int as e:  # error: [invalid-exception-caught]
+        reveal_type(e)  # revealed: Unknown
+        raise KeyError from e
 
 def _(e: Exception | type[Exception]):
     raise ModuleNotFoundError from e  # fine

From f13a6a6a1ae4e4952612b5f458bb32c69f2bf419 Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 15:01:06 -0500
Subject: [PATCH 34/35] Spelling typo

---
 .../resources/mdtest/terminal_statements.md                     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 513a6eee4704e..c0122f63b0765 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -453,7 +453,7 @@ def raise_in_both_branches(cond: bool):
         reveal_type(x)  # revealed: Literal["before", "raise1", "raise2"]
     else:
         # This branch is unreachable, since all control flows in the `try` clause raise exceptions.
-        # As a result, this binding should never be reachable, since new bindings are visibile only
+        # As a result, this binding should never be reachable, since new bindings are visible only
         # when they are reachable.
         x = "unreachable"
     finally:

From 7423de29d010e0ebed807005d4467d4b2337a4eb Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Wed, 5 Feb 2025 15:07:50 -0500
Subject: [PATCH 35/35] Add TODO for unreachable code example

---
 .../resources/mdtest/terminal_statements.md                  | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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 c0122f63b0765..9918d8082e0c4 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/terminal_statements.md
@@ -643,7 +643,9 @@ def _(cond: bool):
 
 ## Bindings after a terminal statement are unreachable
 
-Any bindings introduced after a terminal statement are unreachable, and are considered not visible.
+Any bindings introduced after a terminal statement are unreachable, and are currently considered not
+visible. We [anticipate](https://github.com/astral-sh/ruff/issues/15797) that we want to provide a
+more useful analysis for code after terminal statements.
 
 ```py
 def f(cond: bool) -> str:
@@ -652,6 +654,7 @@ def f(cond: bool) -> str:
         reveal_type(x)  # revealed: Literal["before"]
         return
         x = "after-return"
+        # TODO: no unresolved-reference error
         # error: [unresolved-reference]
         reveal_type(x)  # revealed: Unknown
     else: