diff --git a/crates/red_knot_python_semantic/resources/mdtest/annotations/never.md b/crates/red_knot_python_semantic/resources/mdtest/annotations/never.md
index f3aeb7d5d6ff4..81efd2d864ed1 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/annotations/never.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/annotations/never.md
@@ -47,7 +47,9 @@ def f():
 
 ## `typing.Never`
 
-`typing.Never` is only available in Python 3.11 and later:
+`typing.Never` is only available in Python 3.11 and later.
+
+### Python 3.11
 
 ```toml
 [environment]
@@ -57,8 +59,17 @@ python-version = "3.11"
 ```py
 from typing import Never
 
-x: Never
+reveal_type(Never)  # revealed: typing.Never
+```
 
-def f():
-    reveal_type(x)  # revealed: Never
+### Python 3.10
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+```py
+# error: [unresolved-import]
+from typing import Never
 ```
diff --git a/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md b/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md
index c3977ed46b6c4..f696cd4ea414f 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md
@@ -33,8 +33,6 @@ b: tuple[int] = (42,)
 c: tuple[str, int] = ("42", 42)
 d: tuple[tuple[str, str], tuple[int, int]] = (("foo", "foo"), (42, 42))
 e: tuple[str, ...] = ()
-# TODO: we should not emit this error
-# error: [call-possibly-unbound-method] "Method `__class_getitem__` of type `Literal[tuple]` is possibly unbound"
 f: tuple[str, *tuple[int, ...], bytes] = ("42", b"42")
 g: tuple[str, Unpack[tuple[int, ...]], bytes] = ("42", b"42")
 h: tuple[list[int], list[int]] = ([], [])
diff --git a/crates/red_knot_python_semantic/resources/mdtest/boolean/short_circuit.md b/crates/red_knot_python_semantic/resources/mdtest/boolean/short_circuit.md
index 9ee078606d5cd..6ad75f185bb35 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/boolean/short_circuit.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/boolean/short_circuit.md
@@ -32,13 +32,10 @@ def _(flag: bool):
 
 ```py
 if True or (x := 1):
-    # TODO: infer that the second arm is never executed, and raise `unresolved-reference`.
-    # error: [possibly-unresolved-reference]
-    reveal_type(x)  # revealed: Literal[1]
+    # error: [unresolved-reference]
+    reveal_type(x)  # revealed: Unknown
 
 if True and (x := 1):
-    # TODO: infer that the second arm is always executed, do not raise a diagnostic
-    # error: [possibly-unresolved-reference]
     reveal_type(x)  # revealed: Literal[1]
 ```
 
diff --git a/crates/red_knot_python_semantic/resources/mdtest/call/callable_instance.md b/crates/red_knot_python_semantic/resources/mdtest/call/callable_instance.md
index 635082de5dfa2..746aee725f547 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/call/callable_instance.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/call/callable_instance.md
@@ -67,6 +67,6 @@ def _(flag: bool):
             def __call__(self) -> int: ...
 
     a = NonCallable()
-    # error: "Object of type `Literal[__call__] | Literal[1]` is not callable (due to union element `Literal[1]`)"
-    reveal_type(a())  # revealed: int | Unknown
+    # error: "Object of type `Literal[1] | Literal[__call__]` is not callable (due to union element `Literal[1]`)"
+    reveal_type(a())  # revealed: Unknown | int
 ```
diff --git a/crates/red_knot_python_semantic/resources/mdtest/expression/if.md b/crates/red_knot_python_semantic/resources/mdtest/expression/if.md
index 79faa45426855..6461522cefa46 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/expression/if.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/expression/if.md
@@ -7,7 +7,7 @@ def _(flag: bool):
     reveal_type(1 if flag else 2)  # revealed: Literal[1, 2]
 ```
 
-## Statically known branches
+## Statically known conditions in if-expressions
 
 ```py
 reveal_type(1 if True else 2)  # revealed: Literal[1]
diff --git a/crates/red_knot_python_semantic/resources/mdtest/literal/ellipsis.md b/crates/red_knot_python_semantic/resources/mdtest/literal/ellipsis.md
index 2b7bb7c61d9b1..241b498372d49 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/literal/ellipsis.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/literal/ellipsis.md
@@ -1,7 +1,23 @@
 # Ellipsis literals
 
-## Simple
+## Python 3.9
+
+```toml
+[environment]
+python-version = "3.9"
+```
+
+```py
+reveal_type(...)  # revealed: ellipsis
+```
+
+## Python 3.10
+
+```toml
+[environment]
+python-version = "3.10"
+```
 
 ```py
-reveal_type(...)  # revealed: EllipsisType | ellipsis
+reveal_type(...)  # revealed: EllipsisType
 ```
diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/issubclass.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/issubclass.md
index 7da1ad3e36126..b1099a1f7ae83 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/narrow/issubclass.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/issubclass.md
@@ -95,10 +95,14 @@ def _(t: type[object]):
 
 ### Handling of `None`
 
+`types.NoneType` is only available in Python 3.10 and later:
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
 ```py
-# TODO: this error should ideally go away once we (1) understand `sys.version_info` branches,
-# and (2) set the target Python version for this test to 3.10.
-# error: [possibly-unbound-import] "Member `NoneType` of module `types` is possibly unbound"
 from types import NoneType
 
 def _(flag: bool):
diff --git a/crates/red_knot_python_semantic/resources/mdtest/statically_known_branches.md b/crates/red_knot_python_semantic/resources/mdtest/statically_known_branches.md
new file mode 100644
index 0000000000000..46ccf784d68bc
--- /dev/null
+++ b/crates/red_knot_python_semantic/resources/mdtest/statically_known_branches.md
@@ -0,0 +1,1499 @@
+# Statically-known branches
+
+## Introduction
+
+We have the ability to infer precise types and boundness information for symbols that are defined in
+branches whose conditions we can statically determine to be always true or always false. This is
+useful for `sys.version_info` branches, which can make new features available based on the Python
+version:
+
+```py path=module1.py
+import sys
+
+if sys.version_info >= (3, 9):
+    SomeFeature = "available"
+```
+
+If we can statically determine that the condition is always true, then we can also understand that
+`SomeFeature` is always bound, without raising any errors:
+
+```py path=test1.py
+from module1 import SomeFeature
+
+# SomeFeature is unconditionally available here, because we are on Python 3.9 or newer:
+reveal_type(SomeFeature)  # revealed: Literal["available"]
+```
+
+Another scenario where this is useful is for `typing.TYPE_CHECKING` branches, which are often used
+for conditional imports:
+
+```py path=module2.py
+class SomeType: ...
+```
+
+```py path=test2.py
+import typing
+
+if typing.TYPE_CHECKING:
+    from module2 import SomeType
+
+# `SomeType` is unconditionally available here for type checkers:
+def f(s: SomeType) -> None: ...
+```
+
+## Common use cases
+
+This section makes sure that we can handle all commonly encountered patterns of static conditions.
+
+### `sys.version_info`
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+```py
+import sys
+
+if sys.version_info >= (3, 11):
+    greater_equals_311 = True
+elif sys.version_info >= (3, 9):
+    greater_equals_309 = True
+else:
+    less_than_309 = True
+
+if sys.version_info[0] == 2:
+    python2 = True
+
+# error: [unresolved-reference]
+greater_equals_311
+
+# no error
+greater_equals_309
+
+# error: [unresolved-reference]
+less_than_309
+
+# error: [unresolved-reference]
+python2
+```
+
+### `sys.platform`
+
+```toml
+[environment]
+python-platform = "linux"
+```
+
+```py
+import sys
+
+if sys.platform == "linux":
+    linux = True
+elif sys.platform == "darwin":
+    darwin = True
+else:
+    other = True
+
+# no error
+linux
+
+# error: [unresolved-reference]
+darwin
+
+# error: [unresolved-reference]
+other
+```
+
+### `typing.TYPE_CHECKING`
+
+```py
+import typing
+
+if typing.TYPE_CHECKING:
+    type_checking = True
+else:
+    runtime = True
+
+# no error
+type_checking
+
+# error: [unresolved-reference]
+runtime
+```
+
+### Combination of `sys.platform` check and `sys.version_info` check
+
+```toml
+[environment]
+python-version = "3.10"
+python-platform = "darwin"
+```
+
+```py
+import sys
+
+if sys.platform == "darwin" and sys.version_info >= (3, 11):
+    only_platform_check_true = True
+elif sys.platform == "win32" and sys.version_info >= (3, 10):
+    only_version_check_true = True
+elif sys.platform == "linux" and sys.version_info >= (3, 11):
+    both_checks_false = True
+elif sys.platform == "darwin" and sys.version_info >= (3, 10):
+    both_checks_true = True
+else:
+    other = True
+
+# error: [unresolved-reference]
+only_platform_check_true
+
+# error: [unresolved-reference]
+only_version_check_true
+
+# error: [unresolved-reference]
+both_checks_false
+
+# no error
+both_checks_true
+
+# error: [unresolved-reference]
+other
+```
+
+## Based on type inference
+
+For the the rest of this test suite, we will mostly use `True` and `False` literals to indicate
+statically known conditions, but here, we show that the results are truly based on type inference,
+not some special handling of specific conditions in semantic index building. We use two modules to
+demonstrate this, since semantic index building is inherently single-module:
+
+```py path=module.py
+class AlwaysTrue:
+    def __bool__(self) -> Literal[True]:
+        return True
+```
+
+```py
+from module import AlwaysTrue
+
+if AlwaysTrue():
+    yes = True
+else:
+    no = True
+
+# no error
+yes
+
+# error: [unresolved-reference]
+no
+```
+
+## If statements
+
+The rest of this document contains tests for various control flow elements. This section tests `if`
+statements.
+
+### Always false
+
+#### If
+
+```py
+x = 1
+
+if False:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+#### Else
+
+```py
+x = 1
+
+if True:
+    pass
+else:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+### Always true
+
+#### If
+
+```py
+x = 1
+
+if True:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+#### Else
+
+```py
+x = 1
+
+if False:
+    pass
+else:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+### Ambiguous
+
+Just for comparison, we still infer the combined type if the condition is not statically known:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+### Combination of always true and always false
+
+```py
+x = 1
+
+if True:
+    x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+### `elif` branches
+
+#### Always false
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif False:
+    x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 4]
+```
+
+#### Always true
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif True:
+    x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 3]
+```
+
+#### Ambiguous
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif flag():
+    x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 3, 4]
+```
+
+#### Multiple `elif` branches, always false
+
+Make sure that we include bindings from all non-`False` branches:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif flag():
+    x = 3
+elif False:
+    x = 4
+elif False:
+    x = 5
+elif flag():
+    x = 6
+elif flag():
+    x = 7
+else:
+    x = 8
+
+reveal_type(x)  # revealed: Literal[2, 3, 6, 7, 8]
+```
+
+#### Multiple `elif` branches, always true
+
+Make sure that we only include the binding from the first `elif True` branch:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif flag():
+    x = 3
+elif True:
+    x = 4
+elif True:
+    x = 5
+elif flag():
+    x = 6
+else:
+    x = 7
+
+reveal_type(x)  # revealed: Literal[2, 3, 4]
+```
+
+#### `elif` without `else` branch, always true
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif True:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[2, 3]
+```
+
+#### `elif` without `else` branch, always false
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    x = 2
+elif False:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+### Nested conditionals
+
+#### `if True` inside `if True`
+
+```py
+x = 1
+
+if True:
+    if True:
+        x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+#### `if False` inside `if True`
+
+```py
+x = 1
+
+if True:
+    if False:
+        x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+#### `if <bool>` inside `if True`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if True:
+    if flag():
+        x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+#### `if True` inside `if <bool>`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    if True:
+        x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[2, 3]
+```
+
+#### `if True` inside `if False` ... `else`
+
+```py
+x = 1
+
+if False:
+    x = 2
+else:
+    if True:
+        x = 3
+
+reveal_type(x)  # revealed: Literal[3]
+```
+
+#### `if False` inside `if False` ... `else`
+
+```py
+x = 1
+
+if False:
+    x = 2
+else:
+    if False:
+        x = 3
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+#### `if <bool>` inside `if False` ... `else`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if False:
+    x = 2
+else:
+    if flag():
+        x = 3
+
+reveal_type(x)  # revealed: Literal[1, 3]
+```
+
+### Nested conditionals (with inner `else`)
+
+#### `if True` inside `if True`
+
+```py
+x = 1
+
+if True:
+    if True:
+        x = 2
+    else:
+        x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+#### `if False` inside `if True`
+
+```py
+x = 1
+
+if True:
+    if False:
+        x = 2
+    else:
+        x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[3]
+```
+
+#### `if <bool>` inside `if True`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if True:
+    if flag():
+        x = 2
+    else:
+        x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 3]
+```
+
+#### `if True` inside `if <bool>`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if flag():
+    if True:
+        x = 2
+    else:
+        x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 4]
+```
+
+#### `if True` inside `if False` ... `else`
+
+```py
+x = 1
+
+if False:
+    x = 2
+else:
+    if True:
+        x = 3
+    else:
+        x = 4
+
+reveal_type(x)  # revealed: Literal[3]
+```
+
+#### `if False` inside `if False` ... `else`
+
+```py
+x = 1
+
+if False:
+    x = 2
+else:
+    if False:
+        x = 3
+    else:
+        x = 4
+
+reveal_type(x)  # revealed: Literal[4]
+```
+
+#### `if <bool>` inside `if False` ... `else`
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+if False:
+    x = 2
+else:
+    if flag():
+        x = 3
+    else:
+        x = 4
+
+reveal_type(x)  # revealed: Literal[3, 4]
+```
+
+### Combination with non-conditional control flow
+
+#### `try` ... `except`
+
+##### `if True` inside `try`
+
+```py
+def may_raise() -> None: ...
+
+x = 1
+
+try:
+    may_raise()
+    if True:
+        x = 2
+    else:
+        x = 3
+except:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[2, 4]
+```
+
+##### `try` inside `if True`
+
+```py
+def may_raise() -> None: ...
+
+x = 1
+
+if True:
+    try:
+        may_raise()
+        x = 2
+    except KeyError:
+        x = 3
+    except ValueError:
+        x = 4
+else:
+    x = 5
+
+reveal_type(x)  # revealed: Literal[2, 3, 4]
+```
+
+##### `try` with `else` inside `if True`
+
+```py
+def may_raise() -> None: ...
+
+x = 1
+
+if True:
+    try:
+        may_raise()
+        x = 2
+    except KeyError:
+        x = 3
+    else:
+        x = 4
+else:
+    x = 5
+
+reveal_type(x)  # revealed: Literal[3, 4]
+```
+
+##### `try` with `finally` inside `if True`
+
+```py
+def may_raise() -> None: ...
+
+x = 1
+
+if True:
+    try:
+        may_raise()
+        x = 2
+    except KeyError:
+        x = 3
+    else:
+        x = 4
+    finally:
+        x = 5
+else:
+    x = 6
+
+reveal_type(x)  # revealed: Literal[5]
+```
+
+#### `for` loops
+
+##### `if True` inside `for`
+
+```py
+def iterable() -> list[object]:
+    return [1, ""]
+
+x = 1
+
+for _ in iterable():
+    x = 2
+    if True:
+        x = 3
+
+reveal_type(x)  # revealed: Literal[1, 3]
+```
+
+##### `if True` inside `for` ... `else`
+
+```py
+def iterable() -> list[object]:
+    return [1, ""]
+
+x = 1
+
+for _ in iterable():
+    x = 2
+else:
+    if True:
+        x = 3
+    else:
+        x = 4
+
+reveal_type(x)  # revealed: Literal[3]
+```
+
+##### `for` inside `if True`
+
+```py
+def iterable() -> list[object]:
+    return [1, ""]
+
+x = 1
+
+if True:
+    for _ in iterable():
+        x = 2
+else:
+    x = 3
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+##### `for` ... `else` inside `if True`
+
+```py
+def iterable() -> list[object]:
+    return [1, ""]
+
+x = 1
+
+if True:
+    for _ in iterable():
+        x = 2
+    else:
+        x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[3]
+```
+
+##### `for` loop with `break` inside `if True`
+
+```py
+def iterable() -> list[object]:
+    return [1, ""]
+
+x = 1
+
+if True:
+    x = 2
+    for _ in iterable():
+        x = 3
+        break
+    else:
+        x = 4
+else:
+    x = 5
+
+reveal_type(x)  # revealed: Literal[3, 4]
+```
+
+## If expressions
+
+Note that the result type of an `if`-expression can be precisely inferred if the condition is
+statically known. This is a plain type inference feature that does not need support for statically
+known branches. The tests for this feature are in [expression/if.md](expression/if.md).
+
+The tests here make sure that we also handle assignment expressions inside `if`-expressions
+correctly.
+
+### Type inference
+
+### Always true
+
+```py
+x = (y := 1) if True else (y := 2)
+
+reveal_type(x)  # revealed: Literal[1]
+reveal_type(y)  # revealed: Literal[1]
+```
+
+### Always false
+
+```py
+x = (y := 1) if False else (y := 2)
+
+reveal_type(x)  # revealed: Literal[2]
+reveal_type(y)  # revealed: Literal[2]
+```
+
+## Boolean expressions
+
+### Always true, `or`
+
+```py
+(x := 1) or (x := 2)
+
+reveal_type(x)  # revealed: Literal[1]
+
+(y := 1) or (y := 2) or (y := 3) or (y := 4)
+
+reveal_type(y)  # revealed: Literal[1]
+```
+
+### Always true, `and`
+
+```py
+(x := 1) and (x := 2)
+
+reveal_type(x)  # revealed: Literal[2]
+
+(y := 1) and (y := 2) and (y := 3) and (y := 4)
+
+reveal_type(y)  # revealed: Literal[4]
+```
+
+### Always false, `or`
+
+```py
+(x := 0) or (x := 1)
+
+reveal_type(x)  # revealed: Literal[1]
+
+(y := 0) or (y := 0) or (y := 1) or (y := 2)
+
+reveal_type(y)  # revealed: Literal[1]
+```
+
+### Always false, `and`
+
+```py
+(x := 0) and (x := 1)
+
+reveal_type(x)  # revealed: Literal[0]
+
+(y := 0) and (y := 1) and (y := 2) and (y := 3)
+
+reveal_type(y)  # revealed: Literal[0]
+```
+
+## While loops
+
+### Always false
+
+```py
+x = 1
+
+while False:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+### Always true
+
+```py
+x = 1
+
+while True:
+    x = 2
+    break
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+### Ambiguous
+
+Make sure that we still infer the combined type if the condition is not statically known:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+while flag():
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+### `while` ... `else`
+
+#### `while False`
+
+```py
+while False:
+    x = 1
+else:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+#### `while False` with `break`
+
+```py
+x = 1
+while False:
+    x = 2
+    break
+    x = 3
+else:
+    x = 4
+
+reveal_type(x)  # revealed: Literal[4]
+```
+
+#### `while True`
+
+```py
+while True:
+    x = 1
+    break
+else:
+    x = 2
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+## `match` statements
+
+### Single-valued types, always true
+
+```py
+x = 1
+
+match "a":
+    case "a":
+        x = 2
+    case "b":
+        x = 3
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+### Single-valued types, always true, with wildcard pattern
+
+```py
+x = 1
+
+match "a":
+    case "a":
+        x = 2
+    case "b":
+        x = 3
+    case _:
+        pass
+
+reveal_type(x)  # revealed: Literal[2]
+```
+
+### Single-valued types, always true, with guard
+
+Make sure we don't infer a static truthiness in case there is a case guard:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+match "a":
+    case "a" if flag():
+        x = 2
+    case "b":
+        x = 3
+    case _:
+        pass
+
+reveal_type(x)  # revealed: Literal[1, 2]
+```
+
+### Single-valued types, always false
+
+```py
+x = 1
+
+match "something else":
+    case "a":
+        x = 2
+    case "b":
+        x = 3
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+### Single-valued types, always false, with wildcard pattern
+
+```py
+x = 1
+
+match "something else":
+    case "a":
+        x = 2
+    case "b":
+        x = 3
+    case _:
+        pass
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+### Single-valued types, always false, with guard
+
+For definitely-false cases, the presence of a guard has no influence:
+
+```py
+def flag() -> bool:
+    return True
+
+x = 1
+
+match "something else":
+    case "a" if flag():
+        x = 2
+    case "b":
+        x = 3
+    case _:
+        pass
+
+reveal_type(x)  # revealed: Literal[1]
+```
+
+### Non-single-valued types
+
+```py
+def _(s: str):
+    match s:
+        case "a":
+            x = 1
+        case "b":
+            x = 2
+        case _:
+            x = 3
+
+    reveal_type(x)  # revealed: Literal[1, 2, 3]
+```
+
+### Matching on `sys.platform`
+
+```toml
+[environment]
+python-platform = "darwin"
+```
+
+```py
+import sys
+
+match sys.platform:
+    case "linux":
+        linux = True
+    case "darwin":
+        darwin = True
+    case "win32":
+        win32 = True
+    case _:
+        other = True
+
+# error: [unresolved-reference]
+linux
+
+# no error
+darwin
+
+# error: [unresolved-reference]
+win32
+
+# error: [unresolved-reference]
+other
+```
+
+### Matching on `sys.version_info`
+
+```toml
+[environment]
+python-version = "3.13"
+```
+
+```py
+import sys
+
+minor = "too old"
+
+match sys.version_info.minor:
+    case 12:
+        minor = 12
+    case 13:
+        minor = 13
+    case _:
+        pass
+
+reveal_type(minor)  # revealed: Literal[13]
+```
+
+## Conditional declarations
+
+### Always false
+
+#### `if False`
+
+```py
+x: str
+
+if False:
+    x: int
+
+def f() -> None:
+    reveal_type(x)  # revealed: str
+```
+
+#### `if True … else`
+
+```py
+x: str
+
+if True:
+    pass
+else:
+    x: int
+
+def f() -> None:
+    reveal_type(x)  # revealed: str
+```
+
+### Always true
+
+#### `if True`
+
+```py
+x: str
+
+if True:
+    x: int
+
+def f() -> None:
+    reveal_type(x)  # revealed: int
+```
+
+#### `if False … else`
+
+```py
+x: str
+
+if False:
+    pass
+else:
+    x: int
+
+def f() -> None:
+    reveal_type(x)  # revealed: int
+```
+
+### Ambiguous
+
+```py
+def flag() -> bool:
+    return True
+
+x: str
+
+if flag():
+    x: int
+
+def f() -> None:
+    reveal_type(x)  # revealed: str | int
+```
+
+## Conditional function definitions
+
+```py
+def f() -> int:
+    return 1
+
+def g() -> int:
+    return 1
+
+if True:
+    def f() -> str:
+        return ""
+
+else:
+    def g() -> str:
+        return ""
+
+reveal_type(f())  # revealed: str
+reveal_type(g())  # revealed: int
+```
+
+## Conditional class definitions
+
+```py
+if True:
+    class C:
+        x: int = 1
+
+else:
+    class C:
+        x: str = "a"
+
+reveal_type(C.x)  # revealed: int
+```
+
+## Conditional class attributes
+
+```py
+class C:
+    if True:
+        x: int = 1
+    else:
+        x: str = "a"
+
+reveal_type(C.x)  # revealed: int
+```
+
+## (Un)boundness
+
+### Unbound, `if False`
+
+```py
+if False:
+    x = 1
+
+# error: [unresolved-reference]
+x
+```
+
+### Unbound, `if True … else`
+
+```py
+if True:
+    pass
+else:
+    x = 1
+
+# error: [unresolved-reference]
+x
+```
+
+### Bound, `if True`
+
+```py
+if True:
+    x = 1
+
+# x is always bound, no error
+x
+```
+
+### Bound, `if False … else`
+
+```py
+if False:
+    pass
+else:
+    x = 1
+
+# x is always bound, no error
+x
+```
+
+### Ambiguous, possibly unbound
+
+For comparison, we still detect definitions inside non-statically known branches as possibly
+unbound:
+
+```py
+def flag() -> bool:
+    return True
+
+if flag():
+    x = 1
+
+# error: [possibly-unresolved-reference]
+x
+```
+
+### Nested conditionals
+
+```py
+def flag() -> bool:
+    return True
+
+if False:
+    if True:
+        unbound1 = 1
+
+if True:
+    if False:
+        unbound2 = 1
+
+if False:
+    if False:
+        unbound3 = 1
+
+if False:
+    if flag():
+        unbound4 = 1
+
+if flag():
+    if False:
+        unbound5 = 1
+
+# error: [unresolved-reference]
+# error: [unresolved-reference]
+# error: [unresolved-reference]
+# error: [unresolved-reference]
+# error: [unresolved-reference]
+(unbound1, unbound2, unbound3, unbound4, unbound5)
+```
+
+### Chained conditionals
+
+```py
+if False:
+    x = 1
+if True:
+    x = 2
+
+# x is always bound, no error
+x
+
+if False:
+    y = 1
+if True:
+    y = 2
+
+# y is always bound, no error
+y
+
+if False:
+    z = 1
+if False:
+    z = 2
+
+# z is never bound:
+# error: [unresolved-reference]
+z
+```
+
+### Public boundness
+
+```py
+if True:
+    x = 1
+
+def f():
+    # x is always bound, no error
+    x
+```
+
+### Imports of conditionally defined symbols
+
+#### Always false, unbound
+
+```py path=module.py
+if False:
+    symbol = 1
+```
+
+```py
+# error: [unresolved-import]
+from module import symbol
+```
+
+#### Always true, bound
+
+```py path=module.py
+if True:
+    symbol = 1
+```
+
+```py
+# no error
+from module import symbol
+```
+
+#### Ambiguous, possibly unbound
+
+```py path=module.py
+def flag() -> bool:
+    return True
+
+if flag():
+    symbol = 1
+```
+
+```py
+# error: [possibly-unbound-import]
+from module import symbol
+```
+
+#### Always false, undeclared
+
+```py path=module.py
+if False:
+    symbol: int
+```
+
+```py
+# error: [unresolved-import]
+from module import symbol
+
+reveal_type(symbol)  # revealed: Unknown
+```
+
+#### Always true, declared
+
+```py path=module.py
+if True:
+    symbol: int
+```
+
+```py
+# no error
+from module import symbol
+```
+
+## Unsupported features
+
+We do not support full unreachable code analysis yet. We also raise diagnostics from
+statically-known to be false branches:
+
+```py
+if False:
+    # error: [unresolved-reference]
+    x
+```
diff --git a/crates/red_knot_python_semantic/resources/mdtest/subscript/tuple.md b/crates/red_knot_python_semantic/resources/mdtest/subscript/tuple.md
index 1d27885567df2..88dd39144a6ae 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/subscript/tuple.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/subscript/tuple.md
@@ -81,10 +81,7 @@ python-version = "3.9"
 ```
 
 ```py
-# TODO:
-#  * `tuple.__class_getitem__` is always bound on 3.9 (`sys.version_info`)
-#  * `tuple[int, str]` is a valid base (generics)
-# error: [call-possibly-unbound-method] "Method `__class_getitem__` of type `Literal[tuple]` is possibly unbound"
+# TODO: `tuple[int, str]` is a valid base (generics)
 # error: [invalid-base] "Invalid class base with type `GenericAlias` (all bases must be a class, `Any`, `Unknown` or `Todo`)"
 class A(tuple[int, str]): ...
 
diff --git a/crates/red_knot_python_semantic/resources/mdtest/sys_platform.md b/crates/red_knot_python_semantic/resources/mdtest/sys_platform.md
new file mode 100644
index 0000000000000..637230efaad5d
--- /dev/null
+++ b/crates/red_knot_python_semantic/resources/mdtest/sys_platform.md
@@ -0,0 +1,71 @@
+# `sys.platform`
+
+## Default value
+
+When no target platform is specified, we fall back to the type of `sys.platform` declared in
+typeshed:
+
+```toml
+[environment]
+# No python-platform entry
+```
+
+```py
+import sys
+
+reveal_type(sys.platform)  # revealed: str
+```
+
+## Explicit selection of `all` platforms
+
+```toml
+[environment]
+python-platform = "all"
+```
+
+```py
+import sys
+
+reveal_type(sys.platform)  # revealed: str
+```
+
+## Explicit selection of a specific platform
+
+```toml
+[environment]
+python-platform = "linux"
+```
+
+```py
+import sys
+
+reveal_type(sys.platform)  # revealed: Literal["linux"]
+```
+
+## Testing for a specific platform
+
+### Exact comparison
+
+```toml
+[environment]
+python-platform = "freebsd8"
+```
+
+```py
+import sys
+
+reveal_type(sys.platform == "freebsd8")  # revealed: Literal[True]
+reveal_type(sys.platform == "linux")  # revealed: Literal[False]
+```
+
+### Substring comparison
+
+It is [recommended](https://docs.python.org/3/library/sys.html#sys.platform) to use
+`sys.platform.startswith(...)` for platform checks. This is not yet supported in type inference:
+
+```py
+import sys
+
+reveal_type(sys.platform.startswith("freebsd"))  # revealed: @Todo(instance attributes)
+reveal_type(sys.platform.startswith("linux"))  # revealed: @Todo(instance attributes)
+```
diff --git a/crates/red_knot_python_semantic/src/db.rs b/crates/red_knot_python_semantic/src/db.rs
index 1e40d7ad1377b..e3677f816c37d 100644
--- a/crates/red_knot_python_semantic/src/db.rs
+++ b/crates/red_knot_python_semantic/src/db.rs
@@ -16,7 +16,7 @@ pub(crate) mod tests {
 
     use crate::program::{Program, SearchPathSettings};
     use crate::python_version::PythonVersion;
-    use crate::{default_lint_registry, ProgramSettings};
+    use crate::{default_lint_registry, ProgramSettings, PythonPlatform};
 
     use super::Db;
     use crate::lint::RuleSelection;
@@ -127,6 +127,8 @@ pub(crate) mod tests {
     pub(crate) struct TestDbBuilder<'a> {
         /// Target Python version
         python_version: PythonVersion,
+        /// Target Python platform
+        python_platform: PythonPlatform,
         /// Path to a custom typeshed directory
         custom_typeshed: Option<SystemPathBuf>,
         /// Path and content pairs for files that should be present
@@ -137,6 +139,7 @@ pub(crate) mod tests {
         pub(crate) fn new() -> Self {
             Self {
                 python_version: PythonVersion::default(),
+                python_platform: PythonPlatform::default(),
                 custom_typeshed: None,
                 files: vec![],
             }
@@ -173,6 +176,7 @@ pub(crate) mod tests {
                 &db,
                 &ProgramSettings {
                     python_version: self.python_version,
+                    python_platform: self.python_platform,
                     search_paths,
                 },
             )
diff --git a/crates/red_knot_python_semantic/src/lib.rs b/crates/red_knot_python_semantic/src/lib.rs
index 324d2756b8c55..0a83fd713995e 100644
--- a/crates/red_knot_python_semantic/src/lib.rs
+++ b/crates/red_knot_python_semantic/src/lib.rs
@@ -7,6 +7,7 @@ pub use db::Db;
 pub use module_name::ModuleName;
 pub use module_resolver::{resolve_module, system_module_search_paths, KnownModule, Module};
 pub use program::{Program, ProgramSettings, SearchPathSettings, SitePackages};
+pub use python_platform::PythonPlatform;
 pub use python_version::PythonVersion;
 pub use semantic_model::{HasTy, SemanticModel};
 
@@ -17,6 +18,7 @@ mod module_name;
 mod module_resolver;
 mod node_key;
 mod program;
+mod python_platform;
 mod python_version;
 pub mod semantic_index;
 mod semantic_model;
@@ -26,6 +28,7 @@ pub(crate) mod symbol;
 pub mod types;
 mod unpack;
 mod util;
+mod visibility_constraints;
 
 type FxOrderSet<V> = ordermap::set::OrderSet<V, BuildHasherDefault<FxHasher>>;
 
diff --git a/crates/red_knot_python_semantic/src/module_resolver/resolver.rs b/crates/red_knot_python_semantic/src/module_resolver/resolver.rs
index 990fc01a51106..954ded42620bb 100644
--- a/crates/red_knot_python_semantic/src/module_resolver/resolver.rs
+++ b/crates/red_knot_python_semantic/src/module_resolver/resolver.rs
@@ -721,8 +721,8 @@ mod tests {
     use crate::module_name::ModuleName;
     use crate::module_resolver::module::ModuleKind;
     use crate::module_resolver::testing::{FileSpec, MockedTypeshed, TestCase, TestCaseBuilder};
-    use crate::ProgramSettings;
     use crate::PythonVersion;
+    use crate::{ProgramSettings, PythonPlatform};
 
     use super::*;
 
@@ -1262,7 +1262,7 @@ mod tests {
     fn symlink() -> anyhow::Result<()> {
         use anyhow::Context;
 
-        use crate::program::Program;
+        use crate::{program::Program, PythonPlatform};
         use ruff_db::system::{OsSystem, SystemPath};
 
         use crate::db::tests::TestDb;
@@ -1296,6 +1296,7 @@ mod tests {
             &db,
             &ProgramSettings {
                 python_version: PythonVersion::PY38,
+                python_platform: PythonPlatform::default(),
                 search_paths: SearchPathSettings {
                     extra_paths: vec![],
                     src_root: src.clone(),
@@ -1801,6 +1802,7 @@ not_a_directory
             &db,
             &ProgramSettings {
                 python_version: PythonVersion::default(),
+                python_platform: PythonPlatform::default(),
                 search_paths: SearchPathSettings {
                     extra_paths: vec![],
                     src_root: SystemPathBuf::from("/src"),
diff --git a/crates/red_knot_python_semantic/src/module_resolver/testing.rs b/crates/red_knot_python_semantic/src/module_resolver/testing.rs
index 75d66835f5f1a..365dec2893690 100644
--- a/crates/red_knot_python_semantic/src/module_resolver/testing.rs
+++ b/crates/red_knot_python_semantic/src/module_resolver/testing.rs
@@ -4,7 +4,7 @@ use ruff_db::vendored::VendoredPathBuf;
 use crate::db::tests::TestDb;
 use crate::program::{Program, SearchPathSettings};
 use crate::python_version::PythonVersion;
-use crate::{ProgramSettings, SitePackages};
+use crate::{ProgramSettings, PythonPlatform, SitePackages};
 
 /// A test case for the module resolver.
 ///
@@ -101,6 +101,7 @@ pub(crate) struct UnspecifiedTypeshed;
 pub(crate) struct TestCaseBuilder<T> {
     typeshed_option: T,
     python_version: PythonVersion,
+    python_platform: PythonPlatform,
     first_party_files: Vec<FileSpec>,
     site_packages_files: Vec<FileSpec>,
 }
@@ -147,6 +148,7 @@ impl TestCaseBuilder<UnspecifiedTypeshed> {
         Self {
             typeshed_option: UnspecifiedTypeshed,
             python_version: PythonVersion::default(),
+            python_platform: PythonPlatform::default(),
             first_party_files: vec![],
             site_packages_files: vec![],
         }
@@ -157,12 +159,14 @@ impl TestCaseBuilder<UnspecifiedTypeshed> {
         let TestCaseBuilder {
             typeshed_option: _,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         } = self;
         TestCaseBuilder {
             typeshed_option: VendoredTypeshed,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         }
@@ -176,6 +180,7 @@ impl TestCaseBuilder<UnspecifiedTypeshed> {
         let TestCaseBuilder {
             typeshed_option: _,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         } = self;
@@ -183,6 +188,7 @@ impl TestCaseBuilder<UnspecifiedTypeshed> {
         TestCaseBuilder {
             typeshed_option: typeshed,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         }
@@ -212,6 +218,7 @@ impl TestCaseBuilder<MockedTypeshed> {
         let TestCaseBuilder {
             typeshed_option,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         } = self;
@@ -227,6 +234,7 @@ impl TestCaseBuilder<MockedTypeshed> {
             &db,
             &ProgramSettings {
                 python_version,
+                python_platform,
                 search_paths: SearchPathSettings {
                     extra_paths: vec![],
                     src_root: src.clone(),
@@ -269,6 +277,7 @@ impl TestCaseBuilder<VendoredTypeshed> {
         let TestCaseBuilder {
             typeshed_option: VendoredTypeshed,
             python_version,
+            python_platform,
             first_party_files,
             site_packages_files,
         } = self;
@@ -283,6 +292,7 @@ impl TestCaseBuilder<VendoredTypeshed> {
             &db,
             &ProgramSettings {
                 python_version,
+                python_platform,
                 search_paths: SearchPathSettings {
                     site_packages: SitePackages::Known(vec![site_packages.clone()]),
                     ..SearchPathSettings::new(src.clone())
diff --git a/crates/red_knot_python_semantic/src/program.rs b/crates/red_knot_python_semantic/src/program.rs
index cf85fd7cf41eb..54147cfccfb63 100644
--- a/crates/red_knot_python_semantic/src/program.rs
+++ b/crates/red_knot_python_semantic/src/program.rs
@@ -1,3 +1,4 @@
+use crate::python_platform::PythonPlatform;
 use crate::python_version::PythonVersion;
 use anyhow::Context;
 use salsa::Durability;
@@ -12,6 +13,8 @@ use crate::Db;
 pub struct Program {
     pub python_version: PythonVersion,
 
+    pub python_platform: PythonPlatform,
+
     #[return_ref]
     pub(crate) search_paths: SearchPaths,
 }
@@ -20,6 +23,7 @@ impl Program {
     pub fn from_settings(db: &dyn Db, settings: &ProgramSettings) -> anyhow::Result<Self> {
         let ProgramSettings {
             python_version,
+            python_platform,
             search_paths,
         } = settings;
 
@@ -28,9 +32,11 @@ impl Program {
         let search_paths = SearchPaths::from_settings(db, search_paths)
             .with_context(|| "Invalid search path settings")?;
 
-        Ok(Program::builder(settings.python_version, search_paths)
-            .durability(Durability::HIGH)
-            .new(db))
+        Ok(
+            Program::builder(*python_version, python_platform.clone(), search_paths)
+                .durability(Durability::HIGH)
+                .new(db),
+        )
     }
 
     pub fn update_search_paths(
@@ -57,6 +63,7 @@ impl Program {
 #[cfg_attr(feature = "serde", derive(serde::Serialize))]
 pub struct ProgramSettings {
     pub python_version: PythonVersion,
+    pub python_platform: PythonPlatform,
     pub search_paths: SearchPathSettings,
 }
 
diff --git a/crates/red_knot_python_semantic/src/python_platform.rs b/crates/red_knot_python_semantic/src/python_platform.rs
new file mode 100644
index 0000000000000..672db29459b16
--- /dev/null
+++ b/crates/red_knot_python_semantic/src/python_platform.rs
@@ -0,0 +1,19 @@
+/// The target platform to assume when resolving types.
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+#[cfg_attr(
+    feature = "serde",
+    derive(serde::Serialize, serde::Deserialize),
+    serde(rename_all = "kebab-case")
+)]
+pub enum PythonPlatform {
+    /// Do not make any assumptions about the target platform.
+    #[default]
+    All,
+    /// Assume a specific target platform like `linux`, `darwin` or `win32`.
+    ///
+    /// We use a string (instead of individual enum variants), as the set of possible platforms
+    /// may change over time. See <https://docs.python.org/3/library/sys.html#sys.platform> for
+    /// some known platform identifiers.
+    #[cfg_attr(feature = "serde", serde(untagged))]
+    Identifier(String),
+}
diff --git a/crates/red_knot_python_semantic/src/semantic_index.rs b/crates/red_knot_python_semantic/src/semantic_index.rs
index 0c6ce231d1ac3..c9b05a4dd2b9e 100644
--- a/crates/red_knot_python_semantic/src/semantic_index.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index.rs
@@ -29,7 +29,8 @@ pub mod symbol;
 mod use_def;
 
 pub(crate) use self::use_def::{
-    BindingWithConstraints, BindingWithConstraintsIterator, DeclarationsIterator,
+    BindingWithConstraints, BindingWithConstraintsIterator, DeclarationWithConstraint,
+    DeclarationsIterator,
 };
 
 type SymbolMap = hashbrown::HashMap<ScopedSymbolId, (), FxBuildHasher>;
@@ -155,7 +156,7 @@ impl<'db> SemanticIndex<'db> {
     /// Use the Salsa cached [`use_def_map()`] query if you only need the
     /// use-def map for a single scope.
     #[track_caller]
-    pub(super) fn use_def_map(&self, scope_id: FileScopeId) -> Arc<UseDefMap> {
+    pub(super) fn use_def_map(&'db self, scope_id: FileScopeId) -> Arc<UseDefMap<'db>> {
         self.use_def_maps[scope_id].clone()
     }
 
@@ -378,14 +379,12 @@ mod tests {
     impl UseDefMap<'_> {
         fn first_public_binding(&self, symbol: ScopedSymbolId) -> Option<Definition<'_>> {
             self.public_bindings(symbol)
-                .next()
-                .map(|constrained_binding| constrained_binding.binding)
+                .find_map(|constrained_binding| constrained_binding.binding)
         }
 
         fn first_binding_at_use(&self, use_id: ScopedUseId) -> Option<Definition<'_>> {
             self.bindings_at_use(use_id)
-                .next()
-                .map(|constrained_binding| constrained_binding.binding)
+                .find_map(|constrained_binding| constrained_binding.binding)
         }
     }
 
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 fdd6d11534195..7781662a663ab 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder.rs
@@ -6,15 +6,16 @@ use rustc_hash::{FxHashMap, FxHashSet};
 use ruff_db::files::File;
 use ruff_db::parsed::ParsedModule;
 use ruff_index::IndexVec;
-use ruff_python_ast as ast;
 use ruff_python_ast::name::Name;
 use ruff_python_ast::visitor::{walk_expr, walk_pattern, walk_stmt, Visitor};
+use ruff_python_ast::{self as ast, Pattern};
 use ruff_python_ast::{BoolOp, Expr};
 
 use crate::ast_node_ref::AstNodeRef;
 use crate::module_name::ModuleName;
 use crate::semantic_index::ast_ids::node_key::ExpressionNodeKey;
 use crate::semantic_index::ast_ids::AstIdsBuilder;
+use crate::semantic_index::constraint::PatternConstraintKind;
 use crate::semantic_index::definition::{
     AssignmentDefinitionNodeRef, ComprehensionDefinitionNodeRef, Definition, DefinitionNodeKey,
     DefinitionNodeRef, ForStmtDefinitionNodeRef, ImportFromDefinitionNodeRef,
@@ -27,6 +28,7 @@ use crate::semantic_index::symbol::{
 use crate::semantic_index::use_def::{FlowSnapshot, UseDefMapBuilder};
 use crate::semantic_index::SemanticIndex;
 use crate::unpack::Unpack;
+use crate::visibility_constraints::VisibilityConstraint;
 use crate::Db;
 
 use super::constraint::{Constraint, ConstraintNode, PatternConstraint};
@@ -63,9 +65,9 @@ pub(super) struct SemanticIndexBuilder<'db> {
     current_match_case: Option<CurrentMatchCase<'db>>,
 
     /// Flow states at each `break` in the current loop.
-    loop_break_states: Vec<FlowSnapshot>,
+    loop_break_states: Vec<FlowSnapshot<'db>>,
     /// Per-scope contexts regarding nested `try`/`except` statements
-    try_node_context_stack_manager: TryNodeContextStackManager,
+    try_node_context_stack_manager: TryNodeContextStackManager<'db>,
 
     /// Flags about the file's global scope
     has_future_annotations: bool,
@@ -157,7 +159,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());
@@ -200,16 +202,17 @@ impl<'db> SemanticIndexBuilder<'db> {
         &mut self.ast_ids[scope_id]
     }
 
-    fn flow_snapshot(&self) -> FlowSnapshot {
+    fn flow_snapshot(&'db self) -> FlowSnapshot<'db> {
         self.current_use_def_map().snapshot()
     }
 
-    fn flow_restore(&mut self, state: FlowSnapshot) {
+    fn flow_restore(&'db mut self, state: FlowSnapshot<'db>) {
         self.current_use_def_map_mut().restore(state);
     }
 
-    fn flow_merge(&mut self, state: FlowSnapshot) {
-        self.current_use_def_map_mut().merge(state);
+    fn flow_merge(&mut self, state: FlowSnapshot<'db>) {
+        let db = self.db;
+        self.current_use_def_map_mut().merge(db, state);
     }
 
     fn add_symbol(&mut self, name: Name) -> ScopedSymbolId {
@@ -233,7 +236,8 @@ impl<'db> SemanticIndexBuilder<'db> {
     }
 
     fn add_definition(
-        &mut self,
+        &'db mut self,
+        db: &'db dyn Db,
         symbol: ScopedSymbolId,
         definition_node: impl Into<DefinitionNodeRef<'db>>,
     ) -> Definition<'db> {
@@ -266,10 +270,10 @@ impl<'db> SemanticIndexBuilder<'db> {
         let use_def = self.current_use_def_map_mut();
         match category {
             DefinitionCategory::DeclarationAndBinding => {
-                use_def.record_declaration_and_binding(symbol, definition);
+                use_def.record_declaration_and_binding(db, symbol, definition);
             }
-            DefinitionCategory::Declaration => use_def.record_declaration(symbol, definition),
-            DefinitionCategory::Binding => use_def.record_binding(symbol, definition),
+            DefinitionCategory::Declaration => use_def.record_declaration(db, symbol, definition),
+            DefinitionCategory::Binding => use_def.record_binding(db, symbol, definition),
         }
 
         let mut try_node_stack_manager = std::mem::take(&mut self.try_node_context_stack_manager);
@@ -285,10 +289,6 @@ impl<'db> SemanticIndexBuilder<'db> {
         constraint
     }
 
-    fn record_constraint(&mut self, constraint: Constraint<'db>) {
-        self.current_use_def_map_mut().record_constraint(constraint);
-    }
-
     fn build_constraint(&mut self, constraint_node: &Expr) -> Constraint<'db> {
         let expression = self.add_standalone_expression(constraint_node);
         Constraint {
@@ -297,12 +297,69 @@ impl<'db> SemanticIndexBuilder<'db> {
         }
     }
 
-    fn record_negated_constraint(&mut self, constraint: Constraint<'db>) {
+    fn add_constraint(&mut self, constraint: Constraint<'db>) -> Constraint<'db> {
+        self.current_use_def_map_mut().add_constraint(constraint);
+        constraint
+    }
+
+    fn add_negated_constraint(&mut self, constraint: Constraint<'db>) -> Constraint<'db> {
+        let negated = Constraint {
+            node: constraint.node,
+            is_positive: false,
+        };
+        self.current_use_def_map_mut().add_constraint(negated);
+        negated
+    }
+
+    fn record_constraint(&mut self, constraint: Constraint<'db>) {
+        self.current_use_def_map_mut().record_constraint(constraint);
+    }
+
+    fn record_negated_constraint(&mut self, constraint: Constraint<'db>) -> Constraint<'db> {
+        let negated = self.add_negated_constraint(constraint);
+        self.record_constraint(negated);
+        negated
+    }
+
+    fn record_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) {
         self.current_use_def_map_mut()
-            .record_constraint(Constraint {
-                node: constraint.node,
-                is_positive: false,
-            });
+            .record_visibility_constraint(db, constraint);
+    }
+
+    fn create_and_record_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: Constraint<'db>,
+    ) -> VisibilityConstraint<'db> {
+        let constraint = VisibilityConstraint::visible_if(db, constraint);
+        self.current_use_def_map_mut()
+            .record_visibility_constraint(db, constraint);
+        constraint
+    }
+
+    fn record_ambiguous_visibility(&mut self, db: &'db dyn Db) {
+        self.current_use_def_map_mut()
+            .record_visibility_constraint(db, VisibilityConstraint::ambiguous(db));
+    }
+
+    fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot<'db>) {
+        self.current_use_def_map_mut()
+            .simplify_visibility_constraints(snapshot);
+    }
+
+    fn record_negated_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) -> VisibilityConstraint<'db> {
+        let constraint = VisibilityConstraint::visible_if_not(db, constraint);
+        self.current_use_def_map_mut()
+            .record_visibility_constraint(db, constraint);
+        constraint
     }
 
     fn push_assignment(&mut self, assignment: CurrentAssignment<'db>) {
@@ -324,30 +381,37 @@ impl<'db> SemanticIndexBuilder<'db> {
 
     fn add_pattern_constraint(
         &mut self,
-        subject: &ast::Expr,
+        subject: Expression<'db>,
         pattern: &ast::Pattern,
-    ) -> PatternConstraint<'db> {
-        #[allow(unsafe_code)]
-        let (subject, pattern) = unsafe {
-            (
-                AstNodeRef::new(self.module.clone(), subject),
-                AstNodeRef::new(self.module.clone(), pattern),
-            )
+        guard: Option<&ast::Expr>,
+    ) -> Constraint<'db> {
+        let guard = guard.map(|guard| self.add_standalone_expression(guard));
+
+        let kind = match pattern {
+            Pattern::MatchValue(pattern) => {
+                let value = self.add_standalone_expression(&pattern.value);
+                PatternConstraintKind::Value(value, guard)
+            }
+            Pattern::MatchSingleton(singleton) => {
+                PatternConstraintKind::Singleton(singleton.value, guard)
+            }
+            _ => PatternConstraintKind::Unsupported,
         };
+
         let pattern_constraint = PatternConstraint::new(
             self.db,
             self.file,
             self.current_scope(),
             subject,
-            pattern,
+            kind,
             countme::Count::default(),
         );
-        self.current_use_def_map_mut()
-            .record_constraint(Constraint {
-                node: ConstraintNode::Pattern(pattern_constraint),
-                is_positive: true,
-            });
-        pattern_constraint
+        let constraint = Constraint {
+            node: ConstraintNode::Pattern(pattern_constraint),
+            is_positive: true,
+        };
+        self.current_use_def_map_mut().record_constraint(constraint);
+        constraint
     }
 
     /// Record an expression that needs to be a Salsa ingredient, because we need to infer its type
@@ -407,9 +471,11 @@ impl<'db> SemanticIndexBuilder<'db> {
                     self.visit_expr(default);
                 }
                 match type_param {
-                    ast::TypeParam::TypeVar(node) => self.add_definition(symbol, node),
-                    ast::TypeParam::ParamSpec(node) => self.add_definition(symbol, node),
-                    ast::TypeParam::TypeVarTuple(node) => self.add_definition(symbol, node),
+                    ast::TypeParam::TypeVar(node) => self.add_definition(self.db, symbol, node),
+                    ast::TypeParam::ParamSpec(node) => self.add_definition(self.db, symbol, node),
+                    ast::TypeParam::TypeVarTuple(node) => {
+                        self.add_definition(self.db, symbol, node)
+                    }
                 };
             }
         }
@@ -490,20 +556,25 @@ impl<'db> SemanticIndexBuilder<'db> {
         if let Some(vararg) = parameters.vararg.as_ref() {
             let symbol = self.add_symbol(vararg.name.id().clone());
             self.add_definition(
+                self.db,
                 symbol,
                 DefinitionNodeRef::VariadicPositionalParameter(vararg),
             );
         }
         if let Some(kwarg) = parameters.kwarg.as_ref() {
             let symbol = self.add_symbol(kwarg.name.id().clone());
-            self.add_definition(symbol, DefinitionNodeRef::VariadicKeywordParameter(kwarg));
+            self.add_definition(
+                self.db,
+                symbol,
+                DefinitionNodeRef::VariadicKeywordParameter(kwarg),
+            );
         }
     }
 
     fn declare_parameter(&mut self, parameter: &'db ast::ParameterWithDefault) {
         let symbol = self.add_symbol(parameter.parameter.name.id().clone());
 
-        let definition = self.add_definition(symbol, parameter);
+        let definition = self.add_definition(self.db, symbol, parameter);
 
         // Insert a mapping from the inner Parameter node to the same definition.
         // This ensures that calling `HasTy::ty` on the inner parameter returns
@@ -618,7 +689,7 @@ where
                 // at the end to match the runtime evaluation of parameter defaults
                 // and return-type annotations.
                 let symbol = self.add_symbol(name.id.clone());
-                self.add_definition(symbol, function_def);
+                self.add_definition(self.db, symbol, function_def);
             }
             ast::Stmt::ClassDef(class) => {
                 for decorator in &class.decorator_list {
@@ -626,7 +697,7 @@ where
                 }
 
                 let symbol = self.add_symbol(class.name.id.clone());
-                self.add_definition(symbol, class);
+                self.add_definition(self.db, symbol, class);
 
                 self.with_type_params(
                     NodeWithScopeRef::ClassTypeParameters(class),
@@ -651,7 +722,7 @@ where
                         .map(|name| name.id.clone())
                         .unwrap_or("<unknown>".into()),
                 );
-                self.add_definition(symbol, type_alias);
+                self.add_definition(self.db, symbol, type_alias);
                 self.visit_expr(&type_alias.name);
 
                 self.with_type_params(
@@ -679,7 +750,7 @@ where
                     };
 
                     let symbol = self.add_symbol(symbol_name);
-                    self.add_definition(symbol, alias);
+                    self.add_definition(self.db, symbol, alias);
                 }
             }
             ast::Stmt::ImportFrom(node) => {
@@ -700,7 +771,11 @@ where
 
                     let symbol = self.add_symbol(symbol_name.clone());
 
-                    self.add_definition(symbol, ImportFromDefinitionNodeRef { node, alias_index });
+                    self.add_definition(
+                        self.db,
+                        symbol,
+                        ImportFromDefinitionNodeRef { node, alias_index },
+                    );
                 }
             }
             ast::Stmt::Assign(node) => {
@@ -799,6 +874,11 @@ where
                 let constraint = self.record_expression_constraint(&node.test);
                 let mut constraints = vec![constraint];
                 self.visit_body(&node.body);
+
+                let visibility_constraint_id =
+                    self.create_and_record_visibility_constraint(self.db, constraint);
+                let mut vis_constraints = vec![visibility_constraint_id];
+
                 let mut post_clauses: Vec<FlowSnapshot> = vec![];
                 let elif_else_clauses = node
                     .elif_else_clauses
@@ -825,15 +905,32 @@ where
                     for constraint in &constraints {
                         self.record_negated_constraint(*constraint);
                     }
-                    if let Some(elif_test) = clause_test {
+
+                    let elif_constraint = if let Some(elif_test) = clause_test {
                         self.visit_expr(elif_test);
-                        constraints.push(self.record_expression_constraint(elif_test));
-                    }
+                        let constraint = self.record_expression_constraint(elif_test);
+                        constraints.push(constraint);
+                        Some(constraint)
+                    } else {
+                        None
+                    };
                     self.visit_body(clause_body);
+
+                    for id in &vis_constraints {
+                        self.record_negated_visibility_constraint(self.db, *id);
+                    }
+                    if let Some(elif_constraint) = elif_constraint {
+                        let id =
+                            self.create_and_record_visibility_constraint(self.db, elif_constraint);
+                        vis_constraints.push(id);
+                    }
                 }
+
                 for post_clause_state in post_clauses {
                     self.flow_merge(post_clause_state);
                 }
+
+                self.simplify_visibility_constraints(pre_if);
             }
             ast::Stmt::While(ast::StmtWhile {
                 test,
@@ -856,6 +953,9 @@ where
                 self.visit_body(body);
                 self.set_inside_loop(outer_loop_state);
 
+                let vis_constraint_id =
+                    self.create_and_record_visibility_constraint(self.db, constraint);
+
                 // Get the break states from the body of this loop, and restore the saved outer
                 // ones.
                 let break_states =
@@ -863,15 +963,21 @@ where
 
                 // We may execute the `else` clause without ever executing the body, so merge in
                 // the pre-loop state before visiting `else`.
-                self.flow_merge(pre_loop);
+                self.flow_merge(pre_loop.clone());
                 self.record_negated_constraint(constraint);
                 self.visit_body(orelse);
+                self.record_negated_visibility_constraint(self.db, vis_constraint_id);
 
                 // Breaking out of a while loop bypasses the `else` clause, so merge in the break
                 // states after visiting `else`.
                 for break_state in break_states {
-                    self.flow_merge(break_state);
+                    let snapshot = self.flow_snapshot();
+                    self.flow_restore(break_state);
+                    self.create_and_record_visibility_constraint(self.db, constraint);
+                    self.flow_merge(snapshot);
                 }
+
+                self.simplify_visibility_constraints(pre_loop);
             }
             ast::Stmt::With(ast::StmtWith {
                 items,
@@ -912,6 +1018,8 @@ where
                 self.add_standalone_expression(iter);
                 self.visit_expr(iter);
 
+                self.record_ambiguous_visibility(self.db);
+
                 let pre_loop = self.flow_snapshot();
                 let saved_break_states = std::mem::take(&mut self.loop_break_states);
 
@@ -947,32 +1055,64 @@ where
                 cases,
                 range: _,
             }) => {
-                self.add_standalone_expression(subject);
+                let subject_expr = self.add_standalone_expression(subject);
                 self.visit_expr(subject);
 
                 let after_subject = self.flow_snapshot();
                 let Some((first, remaining)) = cases.split_first() else {
                     return;
                 };
-                self.add_pattern_constraint(subject, &first.pattern);
+
+                let first_constraint_id = self.add_pattern_constraint(
+                    subject_expr,
+                    &first.pattern,
+                    first.guard.as_deref(),
+                );
+
                 self.visit_match_case(first);
 
+                let first_vis_constraint_id =
+                    self.create_and_record_visibility_constraint(self.db, first_constraint_id);
+                let mut vis_constraints = vec![first_vis_constraint_id];
+
                 let mut post_case_snapshots = vec![];
                 for case in remaining {
                     post_case_snapshots.push(self.flow_snapshot());
                     self.flow_restore(after_subject.clone());
-                    self.add_pattern_constraint(subject, &case.pattern);
+                    let constraint_id = self.add_pattern_constraint(
+                        subject_expr,
+                        &case.pattern,
+                        case.guard.as_deref(),
+                    );
                     self.visit_match_case(case);
+
+                    for id in &vis_constraints {
+                        self.record_negated_visibility_constraint(self.db, *id);
+                    }
+                    let vis_constraint_id =
+                        self.create_and_record_visibility_constraint(self.db, constraint_id);
+                    vis_constraints.push(vis_constraint_id);
                 }
-                for post_clause_state in post_case_snapshots {
-                    self.flow_merge(post_clause_state);
-                }
+
+                // If there is no final wildcard match case, pretend there is one. This is similar to how
+                // we add an implicit `else` block in if-elif chains, in case it's not present.
                 if !cases
                     .last()
                     .is_some_and(|case| case.guard.is_none() && case.pattern.is_wildcard())
                 {
-                    self.flow_merge(after_subject);
+                    post_case_snapshots.push(self.flow_snapshot());
+                    self.flow_restore(after_subject.clone());
+
+                    for id in &vis_constraints {
+                        self.record_negated_visibility_constraint(self.db, *id);
+                    }
+                }
+
+                for post_clause_state in post_case_snapshots {
+                    self.flow_merge(post_clause_state);
                 }
+
+                self.simplify_visibility_constraints(after_subject);
             }
             ast::Stmt::Try(ast::StmtTry {
                 body,
@@ -982,6 +1122,8 @@ where
                 is_star,
                 range: _,
             }) => {
+                self.record_ambiguous_visibility(self.db);
+
                 // Save the state prior to visiting any of the `try` block.
                 //
                 // Potentially none of the `try` block could have been executed prior to executing
@@ -1039,6 +1181,7 @@ where
                             let symbol = self.add_symbol(symbol_name.id.clone());
 
                             self.add_definition(
+                                self.db,
                                 symbol,
                                 DefinitionNodeRef::ExceptHandler(ExceptHandlerDefinitionNodeRef {
                                     handler: except_handler,
@@ -1121,6 +1264,7 @@ where
                             unpack,
                         }) => {
                             self.add_definition(
+                                self.db,
                                 symbol,
                                 AssignmentDefinitionNodeRef {
                                     unpack,
@@ -1131,13 +1275,14 @@ where
                             );
                         }
                         Some(CurrentAssignment::AnnAssign(ann_assign)) => {
-                            self.add_definition(symbol, ann_assign);
+                            self.add_definition(self.db, symbol, ann_assign);
                         }
                         Some(CurrentAssignment::AugAssign(aug_assign)) => {
-                            self.add_definition(symbol, aug_assign);
+                            self.add_definition(self.db, symbol, aug_assign);
                         }
                         Some(CurrentAssignment::For(node)) => {
                             self.add_definition(
+                                self.db,
                                 symbol,
                                 ForStmtDefinitionNodeRef {
                                     iterable: &node.iter,
@@ -1150,10 +1295,11 @@ where
                             // TODO(dhruvmanila): If the current scope is a comprehension, then the
                             // named expression is implicitly nonlocal. This is yet to be
                             // implemented.
-                            self.add_definition(symbol, named);
+                            self.add_definition(self.db, symbol, named);
                         }
                         Some(CurrentAssignment::Comprehension { node, first }) => {
                             self.add_definition(
+                                self.db,
                                 symbol,
                                 ComprehensionDefinitionNodeRef {
                                     iterable: &node.iter,
@@ -1165,6 +1311,7 @@ where
                         }
                         Some(CurrentAssignment::WithItem { item, is_async }) => {
                             self.add_definition(
+                                self.db,
                                 symbol,
                                 WithItemDefinitionNodeRef {
                                     node: item,
@@ -1222,19 +1369,20 @@ where
             ast::Expr::If(ast::ExprIf {
                 body, test, orelse, ..
             }) => {
-                // TODO detect statically known truthy or falsy test (via type inference, not naive
-                // AST inspection, so we can't simplify here, need to record test expression for
-                // later checking)
                 self.visit_expr(test);
                 let pre_if = self.flow_snapshot();
                 let constraint = self.record_expression_constraint(test);
                 self.visit_expr(body);
+                let visibility_constraint =
+                    self.create_and_record_visibility_constraint(self.db, constraint);
                 let post_body = self.flow_snapshot();
-                self.flow_restore(pre_if);
+                self.flow_restore(pre_if.clone());
 
                 self.record_negated_constraint(constraint);
                 self.visit_expr(orelse);
+                self.record_negated_visibility_constraint(self.db, visibility_constraint);
                 self.flow_merge(post_body);
+                self.simplify_visibility_constraints(pre_if);
             }
             ast::Expr::ListComp(
                 list_comprehension @ ast::ExprListComp {
@@ -1291,27 +1439,55 @@ where
                 range: _,
                 op,
             }) => {
-                // TODO detect statically known truthy or falsy values (via type inference, not naive
-                // AST inspection, so we can't simplify here, need to record test expression for
-                // later checking)
+                let pre_op = self.flow_snapshot();
+
                 let mut snapshots = vec![];
+                let mut visibility_constraints = vec![];
 
                 for (index, value) in values.iter().enumerate() {
                     self.visit_expr(value);
-                    // In the last value we don't need to take a snapshot nor add a constraint
+
+                    for vid in &visibility_constraints {
+                        self.record_visibility_constraint(self.db, *vid);
+                    }
+
+                    // For the last value, we don't need to model control flow. There is short-circuiting
+                    // anymore.
                     if index < values.len() - 1 {
-                        // Snapshot is taken after visiting the expression but before adding the constraint.
-                        snapshots.push(self.flow_snapshot());
                         let constraint = self.build_constraint(value);
-                        match op {
-                            BoolOp::And => self.record_constraint(constraint),
-                            BoolOp::Or => self.record_negated_constraint(constraint),
+                        let constraint = match op {
+                            BoolOp::And => self.add_constraint(constraint),
+                            BoolOp::Or => self.add_negated_constraint(constraint),
+                        };
+                        let visibility_constraint =
+                            VisibilityConstraint::visible_if(self.db, constraint);
+
+                        let after_expr = self.flow_snapshot();
+
+                        // We first model the short-circuiting behavior. We take the short-circuit
+                        // path here if all of the previous short-circuit paths were not taken, so
+                        // we record all previously existing visibility constraints, and negate the
+                        // one for the current expression.
+                        for vid in &visibility_constraints {
+                            self.record_visibility_constraint(*vid);
                         }
+                        self.record_negated_visibility_constraint(self.db, visibility_constraint);
+                        snapshots.push(self.flow_snapshot());
+
+                        // Then we model the non-short-circuiting behavior. Here, we need to delay
+                        // the application of the visibility constraint until after the expression
+                        // has been evaluated, so we only push it onto the stack here.
+                        self.flow_restore(after_expr);
+                        self.record_constraint(constraint);
+                        visibility_constraints.push(visibility_constraint);
                     }
                 }
+
                 for snapshot in snapshots {
                     self.flow_merge(snapshot);
                 }
+
+                self.simplify_visibility_constraints(pre_op);
             }
             _ => {
                 walk_expr(self, expr);
@@ -1348,6 +1524,7 @@ where
             let symbol = self.add_symbol(name.id().clone());
             let state = self.current_match_case.as_ref().unwrap();
             self.add_definition(
+                self.db,
                 symbol,
                 MatchPatternDefinitionNodeRef {
                     pattern: state.pattern,
@@ -1369,6 +1546,7 @@ where
             let symbol = self.add_symbol(name.id().clone());
             let state = self.current_match_case.as_ref().unwrap();
             self.add_definition(
+                self.db,
                 symbol,
                 MatchPatternDefinitionNodeRef {
                     pattern: state.pattern,
diff --git a/crates/red_knot_python_semantic/src/semantic_index/builder/except_handlers.rs b/crates/red_knot_python_semantic/src/semantic_index/builder/except_handlers.rs
index 6438d1996f3d1..5f286a7cbc657 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/builder/except_handlers.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/builder/except_handlers.rs
@@ -4,9 +4,9 @@ use super::SemanticIndexBuilder;
 
 /// An abstraction over the fact that each scope should have its own [`TryNodeContextStack`]
 #[derive(Debug, Default)]
-pub(super) struct TryNodeContextStackManager(Vec<TryNodeContextStack>);
+pub(super) struct TryNodeContextStackManager<'db>(Vec<TryNodeContextStack<'db>>);
 
-impl TryNodeContextStackManager {
+impl<'db> TryNodeContextStackManager<'db> {
     /// Push a new [`TryNodeContextStack`] onto the stack of stacks.
     ///
     /// Each [`TryNodeContextStack`] is only valid for a single scope
@@ -46,7 +46,7 @@ impl TryNodeContextStackManager {
     }
 
     /// Retrieve the [`TryNodeContextStack`] that is relevant for the current scope.
-    fn current_try_context_stack(&mut self) -> &mut TryNodeContextStack {
+    fn current_try_context_stack(&'db mut self) -> &'db mut TryNodeContextStack<'db> {
         self.0
             .last_mut()
             .expect("There should always be at least one `TryBlockContexts` on the stack")
@@ -55,9 +55,9 @@ impl TryNodeContextStackManager {
 
 /// The contexts of nested `try`/`except` blocks for a single scope
 #[derive(Debug, Default)]
-struct TryNodeContextStack(Vec<TryNodeContext>);
+struct TryNodeContextStack<'db>(Vec<TryNodeContext<'db>>);
 
-impl TryNodeContextStack {
+impl<'db> TryNodeContextStack<'db> {
     /// Push a new [`TryNodeContext`] for recording intermediate states
     /// while visiting a [`ruff_python_ast::StmtTry`] node that has a `finally` branch.
     fn push_context(&mut self) {
@@ -90,11 +90,11 @@ impl TryNodeContextStack {
 /// It will likely be necessary to add more fields to this struct in the future
 /// when we add more advanced handling of `finally` branches.
 #[derive(Debug, Default)]
-struct TryNodeContext {
-    try_suite_snapshots: Vec<FlowSnapshot>,
+struct TryNodeContext<'db> {
+    try_suite_snapshots: Vec<FlowSnapshot<'db>>,
 }
 
-impl TryNodeContext {
+impl<'db> TryNodeContext<'db> {
     /// Take a record of what the internal state looked like after a definition
     fn record_definition(&mut self, snapshot: FlowSnapshot) {
         self.try_suite_snapshots.push(snapshot);
diff --git a/crates/red_knot_python_semantic/src/semantic_index/constraint.rs b/crates/red_knot_python_semantic/src/semantic_index/constraint.rs
index 44b542f0e90ac..b1861c0c6f5ef 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/constraint.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/constraint.rs
@@ -1,23 +1,30 @@
 use ruff_db::files::File;
-use ruff_python_ast as ast;
+use ruff_python_ast::Singleton;
 
-use crate::ast_node_ref::AstNodeRef;
 use crate::db::Db;
 use crate::semantic_index::expression::Expression;
 use crate::semantic_index::symbol::{FileScopeId, ScopeId};
 
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
 pub(crate) struct Constraint<'db> {
     pub(crate) node: ConstraintNode<'db>,
     pub(crate) is_positive: bool,
 }
 
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
 pub(crate) enum ConstraintNode<'db> {
     Expression(Expression<'db>),
     Pattern(PatternConstraint<'db>),
 }
 
+/// Pattern kinds for which we support type narrowing and/or static visibility analysis.
+#[derive(Debug, Clone, PartialEq)]
+pub(crate) enum PatternConstraintKind<'db> {
+    Singleton(Singleton, Option<Expression<'db>>),
+    Value(Expression<'db>, Option<Expression<'db>>),
+    Unsupported,
+}
+
 #[salsa::tracked]
 pub(crate) struct PatternConstraint<'db> {
     #[id]
@@ -28,11 +35,11 @@ pub(crate) struct PatternConstraint<'db> {
 
     #[no_eq]
     #[return_ref]
-    pub(crate) subject: AstNodeRef<ast::Expr>,
+    pub(crate) subject: Expression<'db>,
 
     #[no_eq]
     #[return_ref]
-    pub(crate) pattern: AstNodeRef<ast::Pattern>,
+    pub(crate) kind: PatternConstraintKind<'db>,
 
     #[no_eq]
     count: countme::Count<PatternConstraint<'static>>,
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 9f3e197c74eee..e0444d75bda09 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
@@ -221,14 +221,16 @@
 //! snapshot, and merging a snapshot into the current state. The logic using these methods lives in
 //! [`SemanticIndexBuilder`](crate::semantic_index::builder::SemanticIndexBuilder), e.g. where it
 //! visits a `StmtIf` node.
+pub(crate) use self::symbol_state::ScopedConstraintId;
 use self::symbol_state::{
     BindingIdWithConstraintsIterator, ConstraintIdIterator, DeclarationIdIterator,
-    ScopedConstraintId, ScopedDefinitionId, SymbolBindings, SymbolDeclarations, SymbolState,
+    ScopedDefinitionId, SymbolBindings, SymbolDeclarations, SymbolState,
 };
 use crate::semantic_index::ast_ids::ScopedUseId;
 use crate::semantic_index::definition::Definition;
 use crate::semantic_index::symbol::ScopedSymbolId;
-use crate::symbol::Boundness;
+use crate::visibility_constraints::VisibilityConstraint;
+use crate::Db;
 use ruff_index::IndexVec;
 use rustc_hash::FxHashMap;
 
@@ -237,17 +239,19 @@ use super::constraint::Constraint;
 mod bitset;
 mod symbol_state;
 
+pub(crate) type AllConstraints<'db> = IndexVec<ScopedConstraintId, Constraint<'db>>;
+
 /// Applicable definitions and constraints for every use of a name.
 #[derive(Debug, PartialEq, Eq)]
 pub(crate) struct UseDefMap<'db> {
     /// Array of [`Definition`] in this scope.
-    all_definitions: IndexVec<ScopedDefinitionId, Definition<'db>>,
+    all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
 
     /// Array of [`Constraint`] in this scope.
-    all_constraints: IndexVec<ScopedConstraintId, Constraint<'db>>,
+    all_constraints: AllConstraints<'db>,
 
     /// [`SymbolBindings`] reaching a [`ScopedUseId`].
-    bindings_by_use: IndexVec<ScopedUseId, SymbolBindings>,
+    bindings_by_use: IndexVec<ScopedUseId, SymbolBindings<'db>>,
 
     /// [`SymbolBindings`] or [`SymbolDeclarations`] reaching a given [`Definition`].
     ///
@@ -261,10 +265,10 @@ pub(crate) struct UseDefMap<'db> {
     /// If the definition is both a declaration and a binding -- `x: int = 1` for example -- then
     /// we don't actually need anything here, all we'll need to validate is that our own RHS is a
     /// valid assignment to our own annotation.
-    definitions_by_definition: FxHashMap<Definition<'db>, SymbolDefinitions>,
+    definitions_by_definition: FxHashMap<Definition<'db>, SymbolDefinitions<'db>>,
 
     /// [`SymbolState`] visible at end of scope for each symbol.
-    public_symbols: IndexVec<ScopedSymbolId, SymbolState>,
+    public_symbols: IndexVec<ScopedSymbolId, SymbolState<'db>>,
 }
 
 impl<'db> UseDefMap<'db> {
@@ -275,29 +279,13 @@ impl<'db> UseDefMap<'db> {
         self.bindings_iterator(&self.bindings_by_use[use_id])
     }
 
-    pub(crate) fn use_boundness(&self, use_id: ScopedUseId) -> Boundness {
-        if self.bindings_by_use[use_id].may_be_unbound() {
-            Boundness::PossiblyUnbound
-        } else {
-            Boundness::Bound
-        }
-    }
-
     pub(crate) fn public_bindings(
-        &self,
+        &'db self,
         symbol: ScopedSymbolId,
-    ) -> BindingWithConstraintsIterator<'_, 'db> {
+    ) -> BindingWithConstraintsIterator<'map, 'db> {
         self.bindings_iterator(self.public_symbols[symbol].bindings())
     }
 
-    pub(crate) fn public_boundness(&self, symbol: ScopedSymbolId) -> Boundness {
-        if self.public_symbols[symbol].may_be_unbound() {
-            Boundness::PossiblyUnbound
-        } else {
-            Boundness::Bound
-        }
-    }
-
     pub(crate) fn bindings_at_declaration(
         &self,
         declaration: Definition<'db>,
@@ -310,10 +298,10 @@ impl<'db> UseDefMap<'db> {
         }
     }
 
-    pub(crate) fn declarations_at_binding(
-        &self,
+    pub(crate) fn declarations_at_binding<'map>(
+        &'map self,
         binding: Definition<'db>,
-    ) -> DeclarationsIterator<'_, 'db> {
+    ) -> DeclarationsIterator<'map, 'db> {
         if let SymbolDefinitions::Declarations(declarations) =
             &self.definitions_by_definition[&binding]
         {
@@ -323,22 +311,18 @@ impl<'db> UseDefMap<'db> {
         }
     }
 
-    pub(crate) fn public_declarations(
-        &self,
+    pub(crate) fn public_declarations<'map>(
+        &'map self,
         symbol: ScopedSymbolId,
-    ) -> DeclarationsIterator<'_, 'db> {
+    ) -> DeclarationsIterator<'map, 'db> {
         let declarations = self.public_symbols[symbol].declarations();
         self.declarations_iterator(declarations)
     }
 
-    pub(crate) fn has_public_declarations(&self, symbol: ScopedSymbolId) -> bool {
-        !self.public_symbols[symbol].declarations().is_empty()
-    }
-
-    fn bindings_iterator<'a>(
-        &'a self,
-        bindings: &'a SymbolBindings,
-    ) -> BindingWithConstraintsIterator<'a, 'db> {
+    fn bindings_iterator<'map>(
+        &'map self,
+        bindings: &'map SymbolBindings<'db>,
+    ) -> BindingWithConstraintsIterator<'map, 'db> {
         BindingWithConstraintsIterator {
             all_definitions: &self.all_definitions,
             all_constraints: &self.all_constraints,
@@ -346,44 +330,46 @@ impl<'db> UseDefMap<'db> {
         }
     }
 
-    fn declarations_iterator<'a>(
-        &'a self,
-        declarations: &'a SymbolDeclarations,
-    ) -> DeclarationsIterator<'a, 'db> {
+    fn declarations_iterator<'map>(
+        &'map self,
+        declarations: &'map SymbolDeclarations,
+    ) -> DeclarationsIterator<'map, 'db> {
         DeclarationsIterator {
             all_definitions: &self.all_definitions,
             inner: declarations.iter(),
-            may_be_undeclared: declarations.may_be_undeclared(),
         }
     }
 }
 
 /// Either live bindings or live declarations for a symbol.
 #[derive(Debug, PartialEq, Eq)]
-enum SymbolDefinitions {
-    Bindings(SymbolBindings),
-    Declarations(SymbolDeclarations),
+enum SymbolDefinitions<'db> {
+    Bindings(SymbolBindings<'db>),
+    Declarations(SymbolDeclarations<'db>),
 }
 
 #[derive(Debug)]
 pub(crate) struct BindingWithConstraintsIterator<'map, 'db> {
-    all_definitions: &'map IndexVec<ScopedDefinitionId, Definition<'db>>,
-    all_constraints: &'map IndexVec<ScopedConstraintId, Constraint<'db>>,
-    inner: BindingIdWithConstraintsIterator<'map>,
+    all_definitions: &'map IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
+    all_constraints: &'map AllConstraints<'db>,
+    inner: BindingIdWithConstraintsIterator<'map, 'db>,
 }
 
 impl<'map, 'db> Iterator for BindingWithConstraintsIterator<'map, 'db> {
     type Item = BindingWithConstraints<'map, 'db>;
 
     fn next(&mut self) -> Option<Self::Item> {
+        let all_constraints = self.all_constraints;
+
         self.inner
             .next()
-            .map(|def_id_with_constraints| BindingWithConstraints {
-                binding: self.all_definitions[def_id_with_constraints.definition],
+            .map(|binding_id_with_constraints| BindingWithConstraints {
+                binding: self.all_definitions[binding_id_with_constraints.definition],
                 constraints: ConstraintsIterator {
-                    all_constraints: self.all_constraints,
-                    constraint_ids: def_id_with_constraints.constraint_ids,
+                    all_constraints,
+                    constraint_ids: binding_id_with_constraints.constraint_ids,
                 },
+                visibility_constraint: binding_id_with_constraints.visibility_constraint,
             })
     }
 }
@@ -391,12 +377,13 @@ impl<'map, 'db> Iterator for BindingWithConstraintsIterator<'map, 'db> {
 impl std::iter::FusedIterator for BindingWithConstraintsIterator<'_, '_> {}
 
 pub(crate) struct BindingWithConstraints<'map, 'db> {
-    pub(crate) binding: Definition<'db>,
+    pub(crate) binding: Option<Definition<'db>>,
     pub(crate) constraints: ConstraintsIterator<'map, 'db>,
+    pub(crate) visibility_constraint: VisibilityConstraint<'db>,
 }
 
 pub(crate) struct ConstraintsIterator<'map, 'db> {
-    all_constraints: &'map IndexVec<ScopedConstraintId, Constraint<'db>>,
+    all_constraints: &'map AllConstraints<'db>,
     constraint_ids: ConstraintIdIterator<'map>,
 }
 
@@ -413,22 +400,25 @@ impl<'db> Iterator for ConstraintsIterator<'_, 'db> {
 impl std::iter::FusedIterator for ConstraintsIterator<'_, '_> {}
 
 pub(crate) struct DeclarationsIterator<'map, 'db> {
-    all_definitions: &'map IndexVec<ScopedDefinitionId, Definition<'db>>,
+    all_definitions: &'map IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
     inner: DeclarationIdIterator<'map>,
-    may_be_undeclared: bool,
 }
 
-impl DeclarationsIterator<'_, '_> {
-    pub(crate) fn may_be_undeclared(&self) -> bool {
-        self.may_be_undeclared
-    }
+pub(crate) struct DeclarationWithConstraint<'db> {
+    pub(crate) declaration: Option<Definition<'db>>,
+    pub(crate) visibility_constraint: VisibilityConstraint<'db>,
 }
 
-impl<'db> Iterator for DeclarationsIterator<'_, 'db> {
-    type Item = Definition<'db>;
+impl<'map, 'db> Iterator for DeclarationsIterator<'map, 'db> {
+    type Item = DeclarationWithConstraint<'db>;
 
     fn next(&mut self) -> Option<Self::Item> {
-        self.inner.next().map(|def_id| self.all_definitions[def_id])
+        self.inner.next().map(
+            |(def_id, visibility_constraint)| DeclarationWithConstraint {
+                declaration: self.all_definitions[def_id],
+                visibility_constraint,
+            },
+        )
     }
 }
 
@@ -436,78 +426,156 @@ impl std::iter::FusedIterator for DeclarationsIterator<'_, '_> {}
 
 /// A snapshot of the definitions and constraints state at a particular point in control flow.
 #[derive(Clone, Debug)]
-pub(super) struct FlowSnapshot {
-    symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
+pub(super) struct FlowSnapshot<'db> {
+    symbol_states: IndexVec<ScopedSymbolId, SymbolState<'db>>,
+    scope_start_visibility: VisibilityConstraint<'db>,
 }
 
-#[derive(Debug, Default)]
+#[derive(Debug)]
 pub(super) struct UseDefMapBuilder<'db> {
     /// Append-only array of [`Definition`].
-    all_definitions: IndexVec<ScopedDefinitionId, Definition<'db>>,
+    all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
 
     /// Append-only array of [`Constraint`].
-    all_constraints: IndexVec<ScopedConstraintId, Constraint<'db>>,
+    all_constraints: AllConstraints<'db>,
+
+    /// A constraint which describes the visibility of the unbound/undeclared state, i.e.
+    /// whether or not the start of the scope is visible. This is important for cases like
+    /// `if True: x = 1; use(x)` where we need to hide the implicit "x = unbound" binding
+    /// in the "else" branch.
+    scope_start_visibility: VisibilityConstraint<'db>,
 
     /// Live bindings at each so-far-recorded use.
-    bindings_by_use: IndexVec<ScopedUseId, SymbolBindings>,
+    bindings_by_use: IndexVec<ScopedUseId, SymbolBindings<'db>>,
 
     /// Live bindings or declarations for each so-far-recorded definition.
-    definitions_by_definition: FxHashMap<Definition<'db>, SymbolDefinitions>,
+    definitions_by_definition: FxHashMap<Definition<'db>, SymbolDefinitions<'db>>,
 
     /// Currently live bindings and declarations for each symbol.
-    symbol_states: IndexVec<ScopedSymbolId, SymbolState>,
+    symbol_states: IndexVec<ScopedSymbolId, SymbolState<'db>>,
 }
 
 impl<'db> UseDefMapBuilder<'db> {
+    pub(crate) fn new(db: &'db dyn Db) -> Self {
+        Self {
+            all_definitions: IndexVec::from_iter([None]),
+            all_constraints: IndexVec::new(),
+            scope_start_visibility: VisibilityConstraint::always_true(db),
+            bindings_by_use: IndexVec::new(),
+            definitions_by_definition: FxHashMap::default(),
+            symbol_states: IndexVec::new(),
+        }
+    }
+
     pub(super) fn add_symbol(&mut self, symbol: ScopedSymbolId) {
-        let new_symbol = self.symbol_states.push(SymbolState::undefined());
+        let new_symbol = self
+            .symbol_states
+            .push(SymbolState::undefined(self.scope_start_visibility));
         debug_assert_eq!(symbol, new_symbol);
     }
 
-    pub(super) fn record_binding(&mut self, symbol: ScopedSymbolId, binding: Definition<'db>) {
-        let def_id = self.all_definitions.push(binding);
+    pub(super) fn record_binding(
+        &'db mut self,
+        db: &'db dyn Db,
+        symbol: ScopedSymbolId,
+        binding: Definition<'db>,
+    ) {
+        let def_id = self.all_definitions.push(Some(binding));
         let symbol_state = &mut self.symbol_states[symbol];
         self.definitions_by_definition.insert(
             binding,
             SymbolDefinitions::Declarations(symbol_state.declarations().clone()),
         );
-        symbol_state.record_binding(def_id);
+        symbol_state.record_binding(db, def_id);
+    }
+
+    pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
+        self.all_constraints.push(constraint)
     }
 
     pub(super) fn record_constraint(&mut self, constraint: Constraint<'db>) {
-        let constraint_id = self.all_constraints.push(constraint);
+        let constraint_id = self.add_constraint(constraint);
         for state in &mut self.symbol_states {
             state.record_constraint(constraint_id);
         }
     }
 
-    pub(super) fn record_declaration(
+    pub(super) fn record_visibility_constraint(
         &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) {
+        for state in &mut self.symbol_states {
+            state.record_visibility_constraint(db, constraint);
+        }
+
+        self.scope_start_visibility =
+            VisibilityConstraint::kleene_and(db, self.scope_start_visibility, constraint);
+    }
+
+    /// This method resets the visibility constraints for all symbols to a previous state
+    /// *if* there have been no new declarations or bindings since then. Consider the
+    /// following example:
+    /// ```py
+    /// x = 0
+    /// y = 0
+    /// if test_a:
+    ///     y = 1
+    /// elif test_b:
+    ///     y = 2
+    /// elif test_c:
+    ///    y = 3
+    ///
+    /// # RESET
+    /// ```
+    /// We build a complex visibility constraint for the `y = 0` binding. We build the same
+    /// constraint for the `x = 0` binding as well, but at the `RESET` point, we can get rid
+    /// of it, as the `if`-`elif`-`elif` chain doesn't include any new bindings of `x`.
+    pub(super) fn simplify_visibility_constraints(&mut self, snapshot: FlowSnapshot<'db>) {
+        debug_assert!(self.symbol_states.len() >= snapshot.symbol_states.len());
+
+        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
+        // be subject to visibility constraints. We only simplify/reset visibility constraints
+        // for symbols that have the same bindings and declarations present compared to the
+        // snapshot.
+        for (current, snapshot) in self.symbol_states.iter_mut().zip(snapshot.symbol_states) {
+            current.simplify_visibility_constraints(snapshot);
+        }
+    }
+
+    pub(super) fn record_declaration(
+        &'db mut self,
+        db: &'db dyn Db,
         symbol: ScopedSymbolId,
         declaration: Definition<'db>,
     ) {
-        let def_id = self.all_definitions.push(declaration);
+        let def_id = self.all_definitions.push(Some(declaration));
         let symbol_state = &mut self.symbol_states[symbol];
         self.definitions_by_definition.insert(
             declaration,
             SymbolDefinitions::Bindings(symbol_state.bindings().clone()),
         );
-        symbol_state.record_declaration(def_id);
+        symbol_state.record_declaration(db, def_id);
     }
 
     pub(super) fn record_declaration_and_binding(
-        &mut self,
+        &'db mut self,
+        db: &'db dyn Db,
         symbol: ScopedSymbolId,
         definition: Definition<'db>,
     ) {
         // We don't need to store anything in self.definitions_by_definition.
-        let def_id = self.all_definitions.push(definition);
+        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_declaration(db, def_id);
+        symbol_state.record_binding(db, def_id);
     }
 
-    pub(super) fn record_use(&mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
+    pub(super) fn record_use(&'db mut self, symbol: ScopedSymbolId, use_id: ScopedUseId) {
         // We have a use of a symbol; clone the current bindings for that symbol, and record them
         // as the live bindings for this use.
         let new_use = self
@@ -517,14 +585,15 @@ impl<'db> UseDefMapBuilder<'db> {
     }
 
     /// Take a snapshot of the current visible-symbols state.
-    pub(super) fn snapshot(&self) -> FlowSnapshot {
+    pub(super) fn snapshot(&'db self) -> FlowSnapshot<'db> {
         FlowSnapshot {
             symbol_states: self.symbol_states.clone(),
+            scope_start_visibility: self.scope_start_visibility,
         }
     }
 
     /// Restore the current builder symbols state to the given snapshot.
-    pub(super) fn restore(&mut self, snapshot: FlowSnapshot) {
+    pub(super) fn restore(&mut self, snapshot: FlowSnapshot<'db>) {
         // 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
         // greater than the number of known symbols in a previously-taken snapshot.
@@ -533,18 +602,21 @@ 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;
 
         // 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
         // snapshot, the correct state to fill them in with is "undefined".
-        self.symbol_states
-            .resize(num_symbols, SymbolState::undefined());
+        self.symbol_states.resize(
+            num_symbols,
+            SymbolState::undefined(self.scope_start_visibility),
+        );
     }
 
     /// 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) {
+    pub(super) fn merge(&mut self, db: &'db dyn Db, snapshot: FlowSnapshot<'db>) {
         // 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
         // greater than the number of known symbols in a previously-taken snapshot.
@@ -553,13 +625,18 @@ impl<'db> UseDefMapBuilder<'db> {
         let mut snapshot_definitions_iter = snapshot.symbol_states.into_iter();
         for current in &mut self.symbol_states {
             if let Some(snapshot) = snapshot_definitions_iter.next() {
-                current.merge(snapshot);
+                current.merge(db, snapshot);
             } else {
+                current.merge(db, SymbolState::undefined(snapshot.scope_start_visibility));
                 // Symbol not present in snapshot, so it's unbound/undeclared from that path.
-                current.set_may_be_unbound();
-                current.set_may_be_undeclared();
             }
         }
+
+        self.scope_start_visibility = VisibilityConstraint::kleene_or(
+            db,
+            self.scope_start_visibility,
+            snapshot.scope_start_visibility,
+        );
     }
 
     pub(super) fn finish(mut self) -> UseDefMap<'db> {
diff --git a/crates/red_knot_python_semantic/src/semantic_index/use_def/bitset.rs b/crates/red_knot_python_semantic/src/semantic_index/use_def/bitset.rs
index 464f718e7b4f4..bf7bb01365c02 100644
--- a/crates/red_knot_python_semantic/src/semantic_index/use_def/bitset.rs
+++ b/crates/red_knot_python_semantic/src/semantic_index/use_def/bitset.rs
@@ -32,10 +32,6 @@ impl<const B: usize> BitSet<B> {
         bitset
     }
 
-    pub(super) fn is_empty(&self) -> bool {
-        self.blocks().iter().all(|&b| b == 0)
-    }
-
     /// Convert from Inline to Heap, if needed, and resize the Heap vector, if needed.
     fn resize(&mut self, value: u32) {
         let num_blocks_needed = (value / 64) + 1;
@@ -97,19 +93,6 @@ impl<const B: usize> BitSet<B> {
         }
     }
 
-    /// Union in-place with another [`BitSet`].
-    pub(super) fn union(&mut self, other: &BitSet<B>) {
-        let mut max_len = self.blocks().len();
-        let other_len = other.blocks().len();
-        if other_len > max_len {
-            max_len = other_len;
-            self.resize_blocks(max_len);
-        }
-        for (my_block, other_block) in self.blocks_mut().iter_mut().zip(other.blocks()) {
-            *my_block |= other_block;
-        }
-    }
-
     /// Return an iterator over the values (in ascending order) in this [`BitSet`].
     pub(super) fn iter(&self) -> BitSetIterator<'_, B> {
         let blocks = self.blocks();
@@ -239,59 +222,6 @@ mod tests {
         assert_bitset(&b1, &[89]);
     }
 
-    #[test]
-    fn union() {
-        let mut b1 = BitSet::<1>::with(2);
-        let b2 = BitSet::<1>::with(4);
-
-        b1.union(&b2);
-        assert_bitset(&b1, &[2, 4]);
-    }
-
-    #[test]
-    fn union_mixed_1() {
-        let mut b1 = BitSet::<1>::with(4);
-        let mut b2 = BitSet::<1>::with(4);
-        b1.insert(89);
-        b2.insert(5);
-
-        b1.union(&b2);
-        assert_bitset(&b1, &[4, 5, 89]);
-    }
-
-    #[test]
-    fn union_mixed_2() {
-        let mut b1 = BitSet::<1>::with(4);
-        let mut b2 = BitSet::<1>::with(4);
-        b1.insert(23);
-        b2.insert(89);
-
-        b1.union(&b2);
-        assert_bitset(&b1, &[4, 23, 89]);
-    }
-
-    #[test]
-    fn union_heap() {
-        let mut b1 = BitSet::<1>::with(4);
-        let mut b2 = BitSet::<1>::with(4);
-        b1.insert(89);
-        b2.insert(90);
-
-        b1.union(&b2);
-        assert_bitset(&b1, &[4, 89, 90]);
-    }
-
-    #[test]
-    fn union_heap_2() {
-        let mut b1 = BitSet::<1>::with(89);
-        let mut b2 = BitSet::<1>::with(89);
-        b1.insert(91);
-        b2.insert(90);
-
-        b1.union(&b2);
-        assert_bitset(&b1, &[89, 90, 91]);
-    }
-
     #[test]
     fn multiple_blocks() {
         let mut b = BitSet::<2>::with(120);
@@ -299,11 +229,4 @@ mod tests {
         assert!(matches!(b, BitSet::Inline(_)));
         assert_bitset(&b, &[45, 120]);
     }
-
-    #[test]
-    fn empty() {
-        let b = BitSet::<1>::default();
-
-        assert!(b.is_empty());
-    }
 }
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 506300067c952..a96c7697d00d2 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
@@ -43,6 +43,8 @@
 //!
 //! Tracking live declarations is simpler, since constraints are not involved, but otherwise very
 //! similar to tracking live bindings.
+use crate::{visibility_constraints::VisibilityConstraint, Db};
+
 use super::bitset::{BitSet, BitSetIterator};
 use ruff_index::newtype_index;
 use smallvec::SmallVec;
@@ -51,9 +53,13 @@ use smallvec::SmallVec;
 #[newtype_index]
 pub(super) struct ScopedDefinitionId;
 
+impl ScopedDefinitionId {
+    pub(super) const UNBOUND: ScopedDefinitionId = ScopedDefinitionId::from_u32(0);
+}
+
 /// A newtype-index for a constraint expression in a particular scope.
 #[newtype_index]
-pub(super) struct ScopedConstraintId;
+pub(crate) struct ScopedConstraintId;
 
 /// Can reference this * 64 total definitions inline; more will fall back to the heap.
 const INLINE_BINDING_BLOCKS: usize = 3;
@@ -75,60 +81,81 @@ const INLINE_CONSTRAINT_BLOCKS: usize = 2;
 /// Can keep inline this many live bindings per symbol at a given time; more will go to heap.
 const INLINE_BINDINGS_PER_SYMBOL: usize = 4;
 
-/// One [`BitSet`] of applicable [`ScopedConstraintId`] per live binding.
-type InlineConstraintArray = [BitSet<INLINE_CONSTRAINT_BLOCKS>; INLINE_BINDINGS_PER_SYMBOL];
-type Constraints = SmallVec<InlineConstraintArray>;
-type ConstraintsIterator<'a> = std::slice::Iter<'a, BitSet<INLINE_CONSTRAINT_BLOCKS>>;
+/// Which constraints apply to a given binding?
+type Constraints = BitSet<INLINE_CONSTRAINT_BLOCKS>;
+
+type InlineConstraintArray = [Constraints; INLINE_BINDINGS_PER_SYMBOL];
+
+/// One [`BitSet`] of applicable [`ScopedConstraintId`]s per live binding.
+type ConstraintsPerBinding = SmallVec<InlineConstraintArray>;
+
+/// Iterate over all constraints for a single binding.
+type ConstraintsIterator<'a> = std::slice::Iter<'a, Constraints>;
 type ConstraintsIntoIterator = smallvec::IntoIter<InlineConstraintArray>;
 
+/// Similar to what we have above, but for visibility constraints.
+
+const INLINE_VISIBILITY_CONSTRAINTS: usize = 4;
+type InlineVisibilityConstraintsArray<'db> =
+    [VisibilityConstraint<'db>; INLINE_VISIBILITY_CONSTRAINTS];
+type VisibilityConstraintPerDeclaration<'db> = SmallVec<InlineVisibilityConstraintsArray<'db>>;
+type VisibilityConstraintPerBinding<'db> = SmallVec<InlineVisibilityConstraintsArray<'db>>;
+type VisibilityConstraintsIterator<'db> = std::slice::Iter<'db, VisibilityConstraint<'db>>;
+type VisibilityConstraintsIntoIterator<'db> =
+    smallvec::IntoIter<InlineVisibilityConstraintsArray<'db>>;
+
 /// Live declarations for a single symbol at some point in control flow.
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub(super) struct SymbolDeclarations {
+pub(super) struct SymbolDeclarations<'db> {
     /// [`BitSet`]: which declarations (as [`ScopedDefinitionId`]) can reach the current location?
-    live_declarations: Declarations,
+    pub(crate) live_declarations: Declarations,
 
-    /// Could the symbol be un-declared at this point?
-    may_be_undeclared: bool,
+    /// For each live declaration, which visibility constraints apply to it?
+    pub(crate) visibility_constraints: VisibilityConstraintPerDeclaration<'db>,
 }
 
-impl SymbolDeclarations {
-    fn undeclared() -> Self {
+impl<'db> SymbolDeclarations<'db> {
+    fn undeclared(scope_start_visibility: VisibilityConstraint<'db>) -> Self {
         Self {
-            live_declarations: Declarations::default(),
-            may_be_undeclared: true,
+            live_declarations: Declarations::with(0),
+            visibility_constraints: VisibilityConstraintPerDeclaration::from_iter([
+                scope_start_visibility,
+            ]),
         }
     }
 
     /// Record a newly-encountered declaration for this symbol.
-    fn record_declaration(&mut self, declaration_id: ScopedDefinitionId) {
+    fn record_declaration(&mut self, db: &'db dyn Db, declaration_id: ScopedDefinitionId) {
         self.live_declarations = Declarations::with(declaration_id.into());
-        self.may_be_undeclared = false;
+
+        self.visibility_constraints = VisibilityConstraintPerDeclaration::with_capacity(1);
+        self.visibility_constraints
+            .push(VisibilityConstraint::always_true(db));
     }
 
-    /// Add undeclared as a possibility for this symbol.
-    fn set_may_be_undeclared(&mut self) {
-        self.may_be_undeclared = true;
+    /// Add given visibility constraint to all live bindings.
+    pub(super) fn record_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) {
+        for existing in &mut self.visibility_constraints {
+            *existing = VisibilityConstraint::kleene_and(db, *existing, constraint);
+        }
     }
 
     /// Return an iterator over live declarations for this symbol.
     pub(super) fn iter(&self) -> DeclarationIdIterator {
         DeclarationIdIterator {
-            inner: self.live_declarations.iter(),
+            declarations: self.live_declarations.iter(),
+            visibility_constraints: self.visibility_constraints.iter(),
         }
     }
-
-    pub(super) fn is_empty(&self) -> bool {
-        self.live_declarations.is_empty()
-    }
-
-    pub(super) fn may_be_undeclared(&self) -> bool {
-        self.may_be_undeclared
-    }
 }
 
 /// Live bindings and narrowing constraints for a single symbol at some point in control flow.
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub(super) struct SymbolBindings {
+pub(super) struct SymbolBindings<'db> {
     /// [`BitSet`]: which bindings (as [`ScopedDefinitionId`]) can reach the current location?
     live_bindings: Bindings,
 
@@ -136,34 +163,34 @@ pub(super) struct SymbolBindings {
     ///
     /// This is a [`smallvec::SmallVec`] which should always have one [`BitSet`] of constraints per
     /// binding in `live_bindings`.
-    constraints: Constraints,
+    constraints: ConstraintsPerBinding,
 
-    /// Could the symbol be unbound at this point?
-    may_be_unbound: bool,
+    /// For each live binding, which visibility constraints apply to it?
+    visibility_constraints: VisibilityConstraintPerBinding<'db>,
 }
 
-impl SymbolBindings {
-    fn unbound() -> Self {
+impl<'db> SymbolBindings<'db> {
+    fn unbound(scope_start_visibility: VisibilityConstraint<'db>) -> Self {
         Self {
-            live_bindings: Bindings::default(),
-            constraints: Constraints::default(),
-            may_be_unbound: true,
+            live_bindings: Bindings::with(0),
+            constraints: ConstraintsPerBinding::from_iter([Constraints::default()]),
+            visibility_constraints: VisibilityConstraintPerBinding::from_iter([
+                scope_start_visibility,
+            ]),
         }
     }
 
-    /// Add Unbound as a possibility for this symbol.
-    fn set_may_be_unbound(&mut self) {
-        self.may_be_unbound = true;
-    }
-
     /// 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, db: &'db dyn Db, 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());
-        self.constraints = Constraints::with_capacity(1);
-        self.constraints.push(BitSet::default());
-        self.may_be_unbound = false;
+        self.constraints = ConstraintsPerBinding::with_capacity(1);
+        self.constraints.push(Constraints::default());
+
+        self.visibility_constraints = VisibilityConstraintPerBinding::with_capacity(1);
+        self.visibility_constraints
+            .push(VisibilityConstraint::always_true(db));
     }
 
     /// Add given constraint to all live bindings.
@@ -173,42 +200,46 @@ impl SymbolBindings {
         }
     }
 
-    /// Iterate over currently live bindings for this symbol.
+    /// Add given visibility constraint to all live bindings.
+    pub(super) fn record_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) {
+        for existing in &mut self.visibility_constraints {
+            *existing = VisibilityConstraint::kleene_and(db, *existing, constraint);
+        }
+    }
+
+    /// Iterate over currently live bindings for this symbol
     pub(super) fn iter(&self) -> BindingIdWithConstraintsIterator {
         BindingIdWithConstraintsIterator {
             definitions: self.live_bindings.iter(),
             constraints: self.constraints.iter(),
+            visibility_constraints: self.visibility_constraints.iter(),
         }
     }
-
-    pub(super) fn may_be_unbound(&self) -> bool {
-        self.may_be_unbound
-    }
 }
 
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub(super) struct SymbolState {
-    declarations: SymbolDeclarations,
-    bindings: SymbolBindings,
+pub(super) struct SymbolState<'db> {
+    declarations: SymbolDeclarations<'db>,
+    bindings: SymbolBindings<'db>,
 }
 
-impl SymbolState {
+impl<'db> SymbolState<'db> {
     /// Return a new [`SymbolState`] representing an unbound, undeclared symbol.
-    pub(super) fn undefined() -> Self {
+    pub(super) fn undefined(scope_start_visibility: VisibilityConstraint<'db>) -> Self {
         Self {
-            declarations: SymbolDeclarations::undeclared(),
-            bindings: SymbolBindings::unbound(),
+            declarations: SymbolDeclarations::undeclared(scope_start_visibility),
+            bindings: SymbolBindings::unbound(scope_start_visibility),
         }
     }
 
-    /// Add Unbound as a possibility for this symbol.
-    pub(super) fn set_may_be_unbound(&mut self) {
-        self.bindings.set_may_be_unbound();
-    }
-
     /// Record a newly-encountered binding for this symbol.
-    pub(super) fn record_binding(&mut self, binding_id: ScopedDefinitionId) {
-        self.bindings.record_binding(binding_id);
+    pub(super) fn record_binding(&mut self, db: &'db dyn Db, binding_id: ScopedDefinitionId) {
+        debug_assert_ne!(binding_id, ScopedDefinitionId::UNBOUND);
+        self.bindings.record_binding(db, binding_id);
     }
 
     /// Add given constraint to all live bindings.
@@ -216,40 +247,58 @@ impl SymbolState {
         self.bindings.record_constraint(constraint_id);
     }
 
-    /// Add undeclared as a possibility for this symbol.
-    pub(super) fn set_may_be_undeclared(&mut self) {
-        self.declarations.set_may_be_undeclared();
+    /// Add given visibility constraint to all live bindings.
+    pub(super) fn record_visibility_constraint(
+        &mut self,
+        db: &'db dyn Db,
+        constraint: VisibilityConstraint<'db>,
+    ) {
+        self.bindings.record_visibility_constraint(db, constraint);
+        self.declarations
+            .record_visibility_constraint(db, constraint);
+    }
+
+    pub(super) fn simplify_visibility_constraints(&mut self, snapshot_state: SymbolState<'db>) {
+        if self.bindings.live_bindings == snapshot_state.bindings.live_bindings {
+            self.bindings.visibility_constraints = snapshot_state.bindings.visibility_constraints;
+        }
+        if self.declarations.live_declarations == snapshot_state.declarations.live_declarations {
+            self.declarations.visibility_constraints =
+                snapshot_state.declarations.visibility_constraints;
+        }
     }
 
     /// Record a newly-encountered declaration of this symbol.
-    pub(super) fn record_declaration(&mut self, declaration_id: ScopedDefinitionId) {
-        self.declarations.record_declaration(declaration_id);
+    pub(super) fn record_declaration(
+        &mut self,
+        db: &'db dyn Db,
+        declaration_id: ScopedDefinitionId,
+    ) {
+        self.declarations.record_declaration(db, declaration_id);
     }
 
     /// Merge another [`SymbolState`] into this one.
-    pub(super) fn merge(&mut self, b: SymbolState) {
+    pub(super) fn merge(&mut self, db: &'db dyn Db, b: SymbolState<'db>) {
         let mut a = Self {
             bindings: SymbolBindings {
                 live_bindings: Bindings::default(),
-                constraints: Constraints::default(),
-                may_be_unbound: self.bindings.may_be_unbound || b.bindings.may_be_unbound,
+                constraints: ConstraintsPerBinding::default(),
+                visibility_constraints: VisibilityConstraintPerBinding::default(),
             },
             declarations: SymbolDeclarations {
                 live_declarations: self.declarations.live_declarations.clone(),
-                may_be_undeclared: self.declarations.may_be_undeclared
-                    || b.declarations.may_be_undeclared,
+                visibility_constraints: VisibilityConstraintPerDeclaration::default(),
             },
         };
 
         std::mem::swap(&mut a, self);
-        self.declarations
-            .live_declarations
-            .union(&b.declarations.live_declarations);
 
         let mut a_defs_iter = a.bindings.live_bindings.iter();
         let mut b_defs_iter = b.bindings.live_bindings.iter();
         let mut a_constraints_iter = a.bindings.constraints.into_iter();
         let mut b_constraints_iter = b.bindings.constraints.into_iter();
+        let mut a_vis_constraints_iter = a.bindings.visibility_constraints.into_iter();
+        let mut b_vis_constraints_iter = b.bindings.visibility_constraints.into_iter();
 
         let mut opt_a_def: Option<u32> = a_defs_iter.next();
         let mut opt_b_def: Option<u32> = b_defs_iter.next();
@@ -261,7 +310,10 @@ impl SymbolState {
         // path is irrelevant.
 
         // Helper to push `def`, with constraints in `constraints_iter`, onto `self`.
-        let push = |def, constraints_iter: &mut ConstraintsIntoIterator, merged: &mut Self| {
+        let push = |def,
+                    constraints_iter: &mut ConstraintsIntoIterator,
+                    visibility_constraints_iter: &mut VisibilityConstraintsIntoIterator,
+                    merged: &mut Self| {
             merged.bindings.live_bindings.insert(def);
             // SAFETY: we only ever create SymbolState with either no definitions and no constraint
             // bitsets (`::unbound`) or one definition and one constraint bitset (`::with`), and
@@ -271,7 +323,14 @@ impl SymbolState {
             let constraints = constraints_iter
                 .next()
                 .expect("definitions and constraints length mismatch");
+            let visibility_constraints = visibility_constraints_iter
+                .next()
+                .expect("definitions and visibility_constraints length mismatch");
             merged.bindings.constraints.push(constraints);
+            merged
+                .bindings
+                .visibility_constraints
+                .push(visibility_constraints);
         };
 
         loop {
@@ -279,17 +338,32 @@ impl SymbolState {
                 (Some(a_def), Some(b_def)) => match a_def.cmp(&b_def) {
                     std::cmp::Ordering::Less => {
                         // Next definition ID is only in `a`, push it to `self` and advance `a`.
-                        push(a_def, &mut a_constraints_iter, self);
+                        push(
+                            a_def,
+                            &mut a_constraints_iter,
+                            &mut a_vis_constraints_iter,
+                            self,
+                        );
                         opt_a_def = a_defs_iter.next();
                     }
                     std::cmp::Ordering::Greater => {
                         // Next definition ID is only in `b`, push it to `self` and advance `b`.
-                        push(b_def, &mut b_constraints_iter, self);
+                        push(
+                            b_def,
+                            &mut b_constraints_iter,
+                            &mut b_vis_constraints_iter,
+                            self,
+                        );
                         opt_b_def = b_defs_iter.next();
                     }
                     std::cmp::Ordering::Equal => {
                         // Next definition is in both; push to `self` and intersect constraints.
-                        push(a_def, &mut b_constraints_iter, self);
+                        push(
+                            a_def,
+                            &mut b_constraints_iter,
+                            &mut b_vis_constraints_iter,
+                            self,
+                        );
                         // SAFETY: we only ever create SymbolState with either no definitions and
                         // no constraint bitsets (`::unbound`) or one definition and one constraint
                         // bitset (`::with`), and `::merge` always pushes one definition and one
@@ -298,6 +372,7 @@ impl SymbolState {
                         let a_constraints = a_constraints_iter
                             .next()
                             .expect("definitions and constraints length mismatch");
+
                         // If the same definition is visible through both paths, any constraint
                         // that applies on only one path is irrelevant to the resulting type from
                         // unioning the two paths, so we intersect the constraints.
@@ -306,80 +381,153 @@ impl SymbolState {
                             .last_mut()
                             .unwrap()
                             .intersect(&a_constraints);
+
+                        // TODO: documentation
+                        // SAFETY: See above
+                        let a_vis_constraint = a_vis_constraints_iter
+                            .next()
+                            .expect("visibility_constraints length mismatch");
+                        let current = self.bindings.visibility_constraints.last_mut().unwrap();
+                        *current = VisibilityConstraint::kleene_or(db, *current, a_vis_constraint);
+
                         opt_a_def = a_defs_iter.next();
                         opt_b_def = b_defs_iter.next();
                     }
                 },
                 (Some(a_def), None) => {
                     // We've exhausted `b`, just push the def from `a` and move on to the next.
-                    push(a_def, &mut a_constraints_iter, self);
+                    push(
+                        a_def,
+                        &mut a_constraints_iter,
+                        &mut a_vis_constraints_iter,
+                        self,
+                    );
                     opt_a_def = a_defs_iter.next();
                 }
                 (None, Some(b_def)) => {
                     // We've exhausted `a`, just push the def from `b` and move on to the next.
-                    push(b_def, &mut b_constraints_iter, self);
+                    push(
+                        b_def,
+                        &mut b_constraints_iter,
+                        &mut b_vis_constraints_iter,
+                        self,
+                    );
                     opt_b_def = b_defs_iter.next();
                 }
                 (None, None) => break,
             }
         }
-    }
 
-    pub(super) fn bindings(&self) -> &SymbolBindings {
-        &self.bindings
-    }
+        // Same as above, but for declarations.
+        let mut a_decls_iter = a.declarations.live_declarations.iter();
+        let mut b_decls_iter = b.declarations.live_declarations.iter();
+        let mut a_vis_constraints_iter = a.declarations.visibility_constraints.into_iter();
+        let mut b_vis_constraints_iter = b.declarations.visibility_constraints.into_iter();
 
-    pub(super) fn declarations(&self) -> &SymbolDeclarations {
-        &self.declarations
+        let mut opt_a_decl: Option<u32> = a_decls_iter.next();
+        let mut opt_b_decl: Option<u32> = b_decls_iter.next();
+
+        let push = |decl,
+                    vis_constraints_iter: &mut VisibilityConstraintsIntoIterator,
+                    merged: &mut Self| {
+            merged.declarations.live_declarations.insert(decl);
+            let vis_constraints = vis_constraints_iter
+                .next()
+                .expect("declarations and visibility_constraints length mismatch");
+            merged
+                .declarations
+                .visibility_constraints
+                .push(vis_constraints);
+        };
+
+        loop {
+            match (opt_a_decl, opt_b_decl) {
+                (Some(a_decl), Some(b_decl)) => match a_decl.cmp(&b_decl) {
+                    std::cmp::Ordering::Less => {
+                        push(a_decl, &mut a_vis_constraints_iter, self);
+                        opt_a_decl = a_decls_iter.next();
+                    }
+                    std::cmp::Ordering::Greater => {
+                        push(b_decl, &mut b_vis_constraints_iter, self);
+                        opt_b_decl = b_decls_iter.next();
+                    }
+                    std::cmp::Ordering::Equal => {
+                        push(a_decl, &mut b_vis_constraints_iter, self);
+
+                        let a_vis_constraint = a_vis_constraints_iter
+                            .next()
+                            .expect("declarations and visibility_constraints length mismatch");
+                        let current = self.declarations.visibility_constraints.last_mut().unwrap();
+                        *current = VisibilityConstraint::kleene_or(db, *current, a_vis_constraint);
+
+                        opt_a_decl = a_decls_iter.next();
+                        opt_b_decl = b_decls_iter.next();
+                    }
+                },
+                (Some(a_decl), None) => {
+                    push(a_decl, &mut a_vis_constraints_iter, self);
+                    opt_a_decl = a_decls_iter.next();
+                }
+                (None, Some(b_decl)) => {
+                    push(b_decl, &mut b_vis_constraints_iter, self);
+                    opt_b_decl = b_decls_iter.next();
+                }
+                (None, None) => break,
+            }
+        }
     }
 
-    /// Could the symbol be unbound?
-    pub(super) fn may_be_unbound(&self) -> bool {
-        self.bindings.may_be_unbound()
+    pub(super) fn bindings(&'db self) -> &'db SymbolBindings<'db> {
+        &self.bindings
     }
-}
 
-/// The default state of a symbol, if we've seen no definitions of it, is undefined (that is,
-/// both unbound and undeclared).
-impl Default for SymbolState {
-    fn default() -> Self {
-        SymbolState::undefined()
+    pub(super) fn declarations(&'db self) -> &'db SymbolDeclarations<'db> {
+        &self.declarations
     }
 }
 
 /// A single binding (as [`ScopedDefinitionId`]) with an iterator of its applicable
 /// [`ScopedConstraintId`].
 #[derive(Debug)]
-pub(super) struct BindingIdWithConstraints<'a> {
+pub(super) struct BindingIdWithConstraints<'map, 'db> {
     pub(super) definition: ScopedDefinitionId,
-    pub(super) constraint_ids: ConstraintIdIterator<'a>,
+    pub(super) constraint_ids: ConstraintIdIterator<'map>,
+    pub(super) visibility_constraint: VisibilityConstraint<'db>,
 }
 
 #[derive(Debug)]
-pub(super) struct BindingIdWithConstraintsIterator<'a> {
-    definitions: BindingsIterator<'a>,
-    constraints: ConstraintsIterator<'a>,
+pub(super) struct BindingIdWithConstraintsIterator<'map, 'db> {
+    definitions: BindingsIterator<'map>,
+    constraints: ConstraintsIterator<'map>,
+    visibility_constraints: VisibilityConstraintsIterator<'db>,
 }
 
-impl<'a> Iterator for BindingIdWithConstraintsIterator<'a> {
-    type Item = BindingIdWithConstraints<'a>;
+impl<'map, 'db> Iterator for BindingIdWithConstraintsIterator<'map, 'db> {
+    type Item = BindingIdWithConstraints<'map, 'db>;
 
     fn next(&mut self) -> Option<Self::Item> {
-        match (self.definitions.next(), self.constraints.next()) {
-            (None, None) => None,
-            (Some(def), Some(constraints)) => Some(BindingIdWithConstraints {
-                definition: ScopedDefinitionId::from_u32(def),
-                constraint_ids: ConstraintIdIterator {
-                    wrapped: constraints.iter(),
-                },
-            }),
+        match (
+            self.definitions.next(),
+            self.constraints.next(),
+            self.visibility_constraints.next(),
+        ) {
+            (None, None, None) => None,
+            (Some(def), Some(constraints), Some(visibility_constraint_id)) => {
+                Some(BindingIdWithConstraints {
+                    definition: ScopedDefinitionId::from_u32(def),
+                    constraint_ids: ConstraintIdIterator {
+                        wrapped: constraints.iter(),
+                    },
+                    visibility_constraint: *visibility_constraint_id,
+                })
+            }
             // SAFETY: see above.
             _ => unreachable!("definitions and constraints length mismatch"),
         }
     }
 }
 
-impl std::iter::FusedIterator for BindingIdWithConstraintsIterator<'_> {}
+impl std::iter::FusedIterator for BindingIdWithConstraintsIterator<'_, '_> {}
 
 #[derive(Debug)]
 pub(super) struct ConstraintIdIterator<'a> {
@@ -396,193 +544,192 @@ impl Iterator for ConstraintIdIterator<'_> {
 
 impl std::iter::FusedIterator for ConstraintIdIterator<'_> {}
 
-#[derive(Debug)]
-pub(super) struct DeclarationIdIterator<'a> {
-    inner: DeclarationsIterator<'a>,
+pub(super) struct DeclarationIdIterator<'map> {
+    pub(crate) declarations: DeclarationsIterator<'map>,
+    pub(crate) visibility_constraints: VisibilityConstraintsIterator<'map>,
 }
 
-impl Iterator for DeclarationIdIterator<'_> {
-    type Item = ScopedDefinitionId;
+impl<'db> Iterator for DeclarationIdIterator<'db> {
+    type Item = (ScopedDefinitionId, VisibilityConstraint<'db>);
 
     fn next(&mut self) -> Option<Self::Item> {
-        self.inner.next().map(ScopedDefinitionId::from_u32)
+        match (self.declarations.next(), self.visibility_constraints.next()) {
+            (None, None) => None,
+            (Some(declaration), Some(visibility_constraints_id)) => Some((
+                ScopedDefinitionId::from_u32(declaration),
+                *visibility_constraints_id,
+            )),
+            // SAFETY: see above.
+            _ => unreachable!("declarations and visibility_constraints length mismatch"),
+        }
     }
 }
 
 impl std::iter::FusedIterator for DeclarationIdIterator<'_> {}
 
-#[cfg(test)]
-mod tests {
-    use super::{ScopedConstraintId, ScopedDefinitionId, SymbolState};
-
-    fn assert_bindings(symbol: &SymbolState, may_be_unbound: bool, expected: &[&str]) {
-        assert_eq!(symbol.may_be_unbound(), may_be_unbound);
-        let actual = symbol
-            .bindings()
-            .iter()
-            .map(|def_id_with_constraints| {
-                format!(
-                    "{}<{}>",
-                    def_id_with_constraints.definition.as_u32(),
-                    def_id_with_constraints
-                        .constraint_ids
-                        .map(ScopedConstraintId::as_u32)
-                        .map(|idx| idx.to_string())
-                        .collect::<Vec<_>>()
-                        .join(", ")
-                )
-            })
-            .collect::<Vec<_>>();
-        assert_eq!(actual, expected);
-    }
+// #[cfg(test)]
+// mod tests {
+//     use super::*;
+
+//     #[track_caller]
+//     fn assert_bindings(symbol: &SymbolState, expected: &[&str]) {
+//         let actual = symbol
+//             .bindings()
+//             .iter()
+//             .map(|def_id_with_constraints| {
+//                 let def_id = def_id_with_constraints.definition;
+//                 let def = if def_id == ScopedDefinitionId::UNBOUND {
+//                     "unbound".into()
+//                 } else {
+//                     def_id.as_u32().to_string()
+//                 };
+//                 let constraints = def_id_with_constraints
+//                     .constraint_ids
+//                     .map(ScopedConstraintId::as_u32)
+//                     .map(|idx| idx.to_string())
+//                     .collect::<Vec<_>>()
+//                     .join(", ");
+//                 format!("{def}<{constraints}>")
+//             })
+//             .collect::<Vec<_>>();
+//         assert_eq!(actual, expected);
+//     }
+
+//     #[track_caller]
+//     pub(crate) fn assert_declarations(symbol: &SymbolState, expected: &[&str]) {
+//         let actual = symbol
+//             .declarations()
+//             .iter()
+//             .map(|(def_id, _)| {
+//                 if def_id == ScopedDefinitionId::UNBOUND {
+//                     "undeclared".into()
+//                 } else {
+//                     def_id.as_u32().to_string()
+//                 }
+//             })
+//             .collect::<Vec<_>>();
+//         assert_eq!(actual, expected);
+//     }
+
+//     #[test]
+//     fn unbound() {
+//         let sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+
+//         assert_bindings(&sym, &["unbound<>"]);
+//     }
+
+//     #[test]
+//     fn with() {
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_binding(ScopedDefinitionId::from_u32(1));
+
+//         assert_bindings(&sym, &["1<>"]);
+//     }
+
+//     #[test]
+//     fn record_constraint() {
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_binding(ScopedDefinitionId::from_u32(1));
+//         sym.record_constraint(ScopedConstraintId::from_u32(0));
+
+//         assert_bindings(&sym, &["1<0>"]);
+//     }
+
+//     #[test]
+//     fn merge() {
+//         let mut visibility_constraints = VisibilityConstraints::default();
+
+//         // 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_constraint(ScopedConstraintId::from_u32(0));
+
+//         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym1b.record_binding(ScopedDefinitionId::from_u32(1));
+//         sym1b.record_constraint(ScopedConstraintId::from_u32(0));
+
+//         sym1a.merge(sym1b, &mut visibility_constraints);
+//         let mut sym1 = sym1a;
+//         assert_bindings(&sym1, &["1<0>"]);
+
+//         // 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_constraint(ScopedConstraintId::from_u32(1));
+
+//         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym1b.record_binding(ScopedDefinitionId::from_u32(2));
+//         sym1b.record_constraint(ScopedConstraintId::from_u32(2));
+
+//         sym2a.merge(sym1b, &mut visibility_constraints);
+//         let sym2 = sym2a;
+//         assert_bindings(&sym2, &["2<>"]);
+
+//         // 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_constraint(ScopedConstraintId::from_u32(3));
+
+//         let sym2b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+
+//         sym3a.merge(sym2b, &mut visibility_constraints);
+//         let sym3 = sym3a;
+//         assert_bindings(&sym3, &["unbound<>", "3<3>"]);
+
+//         // merging different definitions keeps them each with their existing constraints
+//         sym1.merge(sym3, &mut visibility_constraints);
+//         let sym = sym1;
+//         assert_bindings(&sym, &["unbound<>", "1<0>", "3<3>"]);
+//     }
+
+//     #[test]
+//     fn no_declaration() {
+//         let sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+
+//         assert_declarations(&sym, &["undeclared"]);
+//     }
+
+//     #[test]
+//     fn record_declaration() {
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_declaration(ScopedDefinitionId::from_u32(1));
+
+//         assert_declarations(&sym, &["1"]);
+//     }
+
+//     #[test]
+//     fn record_declaration_override() {
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_declaration(ScopedDefinitionId::from_u32(1));
+//         sym.record_declaration(ScopedDefinitionId::from_u32(2));
+
+//         assert_declarations(&sym, &["2"]);
+//     }
+
+//     #[test]
+//     fn record_declaration_merge() {
+//         let mut visibility_constraints = VisibilityConstraints::default();
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_declaration(ScopedDefinitionId::from_u32(1));
 
-    pub(crate) fn assert_declarations(
-        symbol: &SymbolState,
-        may_be_undeclared: bool,
-        expected: &[u32],
-    ) {
-        assert_eq!(symbol.declarations.may_be_undeclared(), may_be_undeclared);
-        let actual = symbol
-            .declarations()
-            .iter()
-            .map(ScopedDefinitionId::as_u32)
-            .collect::<Vec<_>>();
-        assert_eq!(actual, expected);
-    }
-
-    #[test]
-    fn unbound() {
-        let sym = SymbolState::undefined();
-
-        assert_bindings(&sym, true, &[]);
-    }
+//         let mut sym2 = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym2.record_declaration(ScopedDefinitionId::from_u32(2));
 
-    #[test]
-    fn with() {
-        let mut sym = SymbolState::undefined();
-        sym.record_binding(ScopedDefinitionId::from_u32(0));
+//         sym.merge(sym2, &mut visibility_constraints);
 
-        assert_bindings(&sym, false, &["0<>"]);
-    }
+//         assert_declarations(&sym, &["1", "2"]);
+//     }
 
-    #[test]
-    fn set_may_be_unbound() {
-        let mut sym = SymbolState::undefined();
-        sym.record_binding(ScopedDefinitionId::from_u32(0));
-        sym.set_may_be_unbound();
+//     #[test]
+//     fn record_declaration_merge_partial_undeclared() {
+//         let mut visibility_constraints = VisibilityConstraints::default();
+//         let mut sym = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
+//         sym.record_declaration(ScopedDefinitionId::from_u32(1));
 
-        assert_bindings(&sym, true, &["0<>"]);
-    }
+//         let sym2 = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
 
-    #[test]
-    fn record_constraint() {
-        let mut sym = SymbolState::undefined();
-        sym.record_binding(ScopedDefinitionId::from_u32(0));
-        sym.record_constraint(ScopedConstraintId::from_u32(0));
+//         sym.merge(sym2, &mut visibility_constraints);
 
-        assert_bindings(&sym, false, &["0<0>"]);
-    }
-
-    #[test]
-    fn merge() {
-        // merging the same definition with the same constraint keeps the constraint
-        let mut sym0a = SymbolState::undefined();
-        sym0a.record_binding(ScopedDefinitionId::from_u32(0));
-        sym0a.record_constraint(ScopedConstraintId::from_u32(0));
-
-        let mut sym0b = SymbolState::undefined();
-        sym0b.record_binding(ScopedDefinitionId::from_u32(0));
-        sym0b.record_constraint(ScopedConstraintId::from_u32(0));
-
-        sym0a.merge(sym0b);
-        let mut sym0 = sym0a;
-        assert_bindings(&sym0, false, &["0<0>"]);
-
-        // merging the same definition with differing constraints drops all constraints
-        let mut sym1a = SymbolState::undefined();
-        sym1a.record_binding(ScopedDefinitionId::from_u32(1));
-        sym1a.record_constraint(ScopedConstraintId::from_u32(1));
-
-        let mut sym1b = SymbolState::undefined();
-        sym1b.record_binding(ScopedDefinitionId::from_u32(1));
-        sym1b.record_constraint(ScopedConstraintId::from_u32(2));
-
-        sym1a.merge(sym1b);
-        let sym1 = sym1a;
-        assert_bindings(&sym1, false, &["1<>"]);
-
-        // merging a constrained definition with unbound keeps both
-        let mut sym2a = SymbolState::undefined();
-        sym2a.record_binding(ScopedDefinitionId::from_u32(2));
-        sym2a.record_constraint(ScopedConstraintId::from_u32(3));
-
-        let sym2b = SymbolState::undefined();
-
-        sym2a.merge(sym2b);
-        let sym2 = sym2a;
-        assert_bindings(&sym2, true, &["2<3>"]);
-
-        // merging different definitions keeps them each with their existing constraints
-        sym0.merge(sym2);
-        let sym = sym0;
-        assert_bindings(&sym, true, &["0<0>", "2<3>"]);
-    }
-
-    #[test]
-    fn no_declaration() {
-        let sym = SymbolState::undefined();
-
-        assert_declarations(&sym, true, &[]);
-    }
-
-    #[test]
-    fn record_declaration() {
-        let mut sym = SymbolState::undefined();
-        sym.record_declaration(ScopedDefinitionId::from_u32(1));
-
-        assert_declarations(&sym, false, &[1]);
-    }
-
-    #[test]
-    fn record_declaration_override() {
-        let mut sym = SymbolState::undefined();
-        sym.record_declaration(ScopedDefinitionId::from_u32(1));
-        sym.record_declaration(ScopedDefinitionId::from_u32(2));
-
-        assert_declarations(&sym, false, &[2]);
-    }
-
-    #[test]
-    fn record_declaration_merge() {
-        let mut sym = SymbolState::undefined();
-        sym.record_declaration(ScopedDefinitionId::from_u32(1));
-
-        let mut sym2 = SymbolState::undefined();
-        sym2.record_declaration(ScopedDefinitionId::from_u32(2));
-
-        sym.merge(sym2);
-
-        assert_declarations(&sym, false, &[1, 2]);
-    }
-
-    #[test]
-    fn record_declaration_merge_partial_undeclared() {
-        let mut sym = SymbolState::undefined();
-        sym.record_declaration(ScopedDefinitionId::from_u32(1));
-
-        let sym2 = SymbolState::undefined();
-
-        sym.merge(sym2);
-
-        assert_declarations(&sym, true, &[1]);
-    }
-
-    #[test]
-    fn set_may_be_undeclared() {
-        let mut sym = SymbolState::undefined();
-        sym.record_declaration(ScopedDefinitionId::from_u32(0));
-        sym.set_may_be_undeclared();
-
-        assert_declarations(&sym, true, &[0]);
-    }
-}
+//         assert_declarations(&sym, &["undeclared", "1"]);
+//     }
+// }
diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index d655e18d8f848..6e826e6bf5f19 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -23,7 +23,8 @@ use crate::semantic_index::definition::Definition;
 use crate::semantic_index::symbol::{self as symbol, ScopeId, ScopedSymbolId};
 use crate::semantic_index::{
     global_scope, imported_modules, semantic_index, symbol_table, use_def_map,
-    BindingWithConstraints, BindingWithConstraintsIterator, DeclarationsIterator,
+    BindingWithConstraints, BindingWithConstraintsIterator, DeclarationWithConstraint,
+    DeclarationsIterator,
 };
 use crate::stdlib::{builtins_symbol, known_module_symbol, typing_extensions_symbol};
 use crate::symbol::{Boundness, Symbol};
@@ -75,51 +76,60 @@ fn symbol_by_id<'db>(db: &'db dyn Db, scope: ScopeId<'db>, symbol: ScopedSymbolI
 
     // If the symbol is declared, the public type is based on declarations; otherwise, it's based
     // on inference from bindings.
-    if use_def.has_public_declarations(symbol) {
-        let declarations = use_def.public_declarations(symbol);
-        // If the symbol is undeclared in some paths, include the inferred type in the public type.
-        let undeclared_ty = if declarations.may_be_undeclared() {
-            Some(
-                bindings_ty(db, use_def.public_bindings(symbol))
-                    .map(|bindings_ty| Symbol::Type(bindings_ty, use_def.public_boundness(symbol)))
-                    .unwrap_or(Symbol::Unbound),
-            )
-        } else {
-            None
-        };
-        // Intentionally ignore conflicting declared types; that's not our problem, it's the
-        // problem of the module we are importing from.
-
-        // TODO: Our handling of boundness currently only depends on bindings, and ignores
-        // declarations. This is inconsistent, since we only look at bindings if the symbol
-        // may be undeclared. Consider the following example:
-        // ```py
-        // x: int
-        //
-        // if flag:
-        //     y: int
-        // else
-        //     y = 3
-        // ```
-        // If we import from this module, we will currently report `x` as a definitely-bound
-        // symbol (even though it has no bindings at all!) but report `y` as possibly-unbound
-        // (even though every path has either a binding or a declaration for it.)
-
-        match undeclared_ty {
-            Some(Symbol::Type(ty, boundness)) => Symbol::Type(
-                declarations_ty(db, declarations, Some(ty)).unwrap_or_else(|(ty, _)| ty),
-                boundness,
-            ),
-            None | Some(Symbol::Unbound) => Symbol::Type(
-                declarations_ty(db, declarations, None).unwrap_or_else(|(ty, _)| ty),
-                Boundness::Bound,
-            ),
+
+    let declarations = use_def.public_declarations(symbol);
+    let declared = declarations_ty(db, declarations);
+
+    match declared {
+        // Symbol is declared, trust the declared type
+        Ok(symbol @ Symbol::Type(_, Boundness::Bound)) => symbol,
+        // Symbol is possibly declared
+        Ok(Symbol::Type(declared_ty, Boundness::PossiblyUnbound)) => {
+            let bindings = use_def.public_bindings(symbol);
+            let inferred = bindings_ty(db, bindings);
+
+            match inferred {
+                // Symbol is possibly undeclared and definitely unbound
+                Symbol::Unbound => {
+                    // TODO: We probably don't want to report `Bound` here. This requires a bit of
+                    // design work though as we might want a different behavior for stubs and for
+                    // normal modules.
+                    Symbol::Type(declared_ty, Boundness::Bound)
+                }
+                // Symbol is possibly undeclared and (possibly) bound
+                Symbol::Type(inferred_ty, boundness) => Symbol::Type(
+                    UnionType::from_elements(db, [inferred_ty, declared_ty].iter().copied()),
+                    boundness,
+                ),
+            }
+        }
+        // Symbol is undeclared, return the inferred type
+        Ok(Symbol::Unbound) => {
+            let bindings = use_def.public_bindings(symbol);
+            bindings_ty(db, bindings)
+        }
+        // Symbol is possibly undeclared
+        Err((declared_ty, _)) => {
+            // Intentionally ignore conflicting declared types; that's not our problem,
+            // it's the problem of the module we are importing from.
+            declared_ty.into()
         }
-    } else {
-        bindings_ty(db, use_def.public_bindings(symbol))
-            .map(|bindings_ty| Symbol::Type(bindings_ty, use_def.public_boundness(symbol)))
-            .unwrap_or(Symbol::Unbound)
     }
+
+    // TODO (ticket: https://github.com/astral-sh/ruff/issues/14297) Our handling of boundness
+    // currently only depends on bindings, and ignores declarations. This is inconsistent, since
+    // we only look at bindings if the symbol may be undeclared. Consider the following example:
+    // ```py
+    // x: int
+    //
+    // if flag:
+    //     y: int
+    // else
+    //     y = 3
+    // ```
+    // If we import from this module, we will currently report `x` as a definitely-bound symbol
+    // (even though it has no bindings at all!) but report `y` as possibly-unbound (even though
+    // every path has either a binding or a declaration for it.)
 }
 
 /// Shorthand for `symbol_by_id` that takes a symbol name instead of an ID.
@@ -132,6 +142,22 @@ fn symbol<'db>(db: &'db dyn Db, scope: ScopeId<'db>, name: &str) -> Symbol<'db>
     {
         return Symbol::Type(Type::BooleanLiteral(true), Boundness::Bound);
     }
+    if name == "platform"
+        && file_to_module(db, scope.file(db))
+            .is_some_and(|module| module.is_known(KnownModule::Sys))
+    {
+        match Program::get(db).python_platform(db) {
+            crate::PythonPlatform::Identifier(platform) => {
+                return Symbol::Type(
+                    Type::StringLiteral(StringLiteralType::new(db, platform.as_str())),
+                    Boundness::Bound,
+                );
+            }
+            crate::PythonPlatform::All => {
+                // Fall through to the looked up type
+            }
+        }
+    }
 
     let table = symbol_table(db, scope);
     table
@@ -247,46 +273,77 @@ fn definition_expression_ty<'db>(
 fn bindings_ty<'db>(
     db: &'db dyn Db,
     bindings_with_constraints: BindingWithConstraintsIterator<'_, 'db>,
-) -> Option<Type<'db>> {
-    let mut def_types = bindings_with_constraints.map(
+) -> Symbol<'db> {
+    let mut bindings_with_constraints = bindings_with_constraints.peekable();
+
+    let unbound_visibility = if let Some(BindingWithConstraints {
+        binding: None,
+        constraints: _,
+        visibility_constraint,
+    }) = bindings_with_constraints.peek()
+    {
+        crate::visibility_constraints::evaluate(db, *visibility_constraint)
+    } else {
+        Truthiness::AlwaysFalse
+    };
+
+    let mut types = bindings_with_constraints.filter_map(
         |BindingWithConstraints {
              binding,
              constraints,
+             visibility_constraint,
          }| {
+            let binding = binding?;
+            let static_visibility =
+                crate::visibility_constraints::evaluate(db, visibility_constraint);
+
+            if static_visibility.is_always_false() {
+                return None;
+            }
+
             let mut constraint_tys = constraints
                 .filter_map(|constraint| narrowing_constraint(db, constraint, binding))
                 .peekable();
 
             let binding_ty = binding_ty(db, binding);
             if constraint_tys.peek().is_some() {
-                constraint_tys
+                let intersection_ty = constraint_tys
                     .fold(
                         IntersectionBuilder::new(db).add_positive(binding_ty),
                         IntersectionBuilder::add_positive,
                     )
-                    .build()
+                    .build();
+                Some(intersection_ty)
             } else {
-                binding_ty
+                Some(binding_ty)
             }
         },
     );
 
-    if let Some(first) = def_types.next() {
-        if let Some(second) = def_types.next() {
-            Some(UnionType::from_elements(
-                db,
-                [first, second].into_iter().chain(def_types),
-            ))
+    if let Some(first) = types.next() {
+        let boundness = match unbound_visibility {
+            Truthiness::AlwaysTrue => {
+                unreachable!("If we have at least one binding, the scope-start should not be definitely visible")
+            }
+            Truthiness::AlwaysFalse => Boundness::Bound,
+            Truthiness::Ambiguous => Boundness::PossiblyUnbound,
+        };
+
+        if let Some(second) = types.next() {
+            Symbol::Type(
+                UnionType::from_elements(db, [first, second].into_iter().chain(types)),
+                boundness,
+            )
         } else {
-            Some(first)
+            Symbol::Type(first, boundness)
         }
     } else {
-        None
+        Symbol::Unbound
     }
 }
 
 /// The result of looking up a declared type from declarations; see [`declarations_ty`].
-type DeclaredTypeResult<'db> = Result<Type<'db>, (Type<'db>, Box<[Type<'db>]>)>;
+type DeclaredTypeResult<'db> = Result<Symbol<'db>, (Type<'db>, Box<[Type<'db>]>)>;
 
 /// Build a declared type from a [`DeclarationsIterator`].
 ///
@@ -304,40 +361,68 @@ type DeclaredTypeResult<'db> = Result<Type<'db>, (Type<'db>, Box<[Type<'db>]>)>;
 fn declarations_ty<'db>(
     db: &'db dyn Db,
     declarations: DeclarationsIterator<'_, 'db>,
-    undeclared_ty: Option<Type<'db>>,
 ) -> DeclaredTypeResult<'db> {
-    let mut declaration_types = declarations.map(|declaration| declaration_ty(db, declaration));
+    let mut declarations = declarations.peekable();
 
-    let Some(first) = declaration_types.next() else {
-        if let Some(undeclared_ty) = undeclared_ty {
-            // Short-circuit to return the undeclared type if there are no declarations.
-            return Ok(undeclared_ty);
-        }
-        panic!("declarations_ty must not be called with zero declarations and no undeclared_ty");
+    let undeclared_visibility = if let Some(DeclarationWithConstraint {
+        declaration: None,
+        visibility_constraint,
+    }) = declarations.peek()
+    {
+        crate::visibility_constraints::evaluate(db, *visibility_constraint)
+    } else {
+        Truthiness::AlwaysFalse
     };
 
-    let mut conflicting: Vec<Type<'db>> = vec![];
-    let mut builder = UnionBuilder::new(db).add(first);
-    for other in declaration_types {
-        if !first.is_equivalent_to(db, other) {
-            conflicting.push(other);
-        }
-        builder = builder.add(other);
-    }
-    // Avoid considering the undeclared type for the conflicting declaration diagnostics. It
-    // should still be part of the declared type.
-    if let Some(undeclared_ty) = undeclared_ty {
-        builder = builder.add(undeclared_ty);
-    }
-    let declared_ty = builder.build();
+    let mut types = declarations.filter_map(
+        |DeclarationWithConstraint {
+             declaration,
+             visibility_constraint,
+         }| {
+            let declaration = declaration?;
+            let static_visibility =
+                crate::visibility_constraints::evaluate(db, visibility_constraint);
+
+            if static_visibility.is_always_false() {
+                None
+            } else {
+                Some(declaration_ty(db, declaration))
+            }
+        },
+    );
 
-    if conflicting.is_empty() {
-        Ok(declared_ty)
+    if let Some(first) = types.next() {
+        let mut conflicting: Vec<Type<'db>> = vec![];
+        let declared_ty = if let Some(second) = types.next() {
+            let mut builder = UnionBuilder::new(db).add(first);
+            for other in std::iter::once(second).chain(types) {
+                if !first.is_equivalent_to(db, other) {
+                    conflicting.push(other);
+                }
+                builder = builder.add(other);
+            }
+            builder.build()
+        } else {
+            first
+        };
+        if conflicting.is_empty() {
+            let boundness = match undeclared_visibility {
+                Truthiness::AlwaysTrue => {
+                    unreachable!("If we have at least one declaration, the scope-start should not be definitely visible")
+                }
+                Truthiness::AlwaysFalse => Boundness::Bound,
+                Truthiness::Ambiguous => Boundness::PossiblyUnbound,
+            };
+
+            Ok(Symbol::Type(declared_ty, boundness))
+        } else {
+            Err((
+                declared_ty,
+                std::iter::once(first).chain(conflicting).collect(),
+            ))
+        }
     } else {
-        Err((
-            declared_ty,
-            [first].into_iter().chain(conflicting).collect(),
-        ))
+        Ok(Symbol::Unbound)
     }
 }
 
@@ -1580,7 +1665,7 @@ impl<'db> Type<'db> {
     ///
     /// This is used to determine the value that would be returned
     /// when `bool(x)` is called on an object `x`.
-    fn bool(&self, db: &'db dyn Db) -> Truthiness {
+    pub(crate) fn bool(&self, db: &'db dyn Db) -> Truthiness {
         match self {
             Type::Any | Type::Todo(_) | Type::Never | Type::Unknown => Truthiness::Ambiguous,
             Type::FunctionLiteral(_) => Truthiness::AlwaysTrue,
@@ -2859,11 +2944,19 @@ pub enum Truthiness {
 }
 
 impl Truthiness {
-    const fn is_ambiguous(self) -> bool {
+    pub(crate) const fn is_ambiguous(self) -> bool {
         matches!(self, Truthiness::Ambiguous)
     }
 
-    const fn negate(self) -> Self {
+    pub(crate) const fn is_always_false(self) -> bool {
+        matches!(self, Truthiness::AlwaysFalse)
+    }
+
+    pub(crate) const fn is_always_true(self) -> bool {
+        matches!(self, Truthiness::AlwaysTrue)
+    }
+
+    pub(crate) const fn negate(self) -> Self {
         match self {
             Self::AlwaysTrue => Self::AlwaysFalse,
             Self::AlwaysFalse => Self::AlwaysTrue,
@@ -2871,6 +2964,14 @@ impl Truthiness {
         }
     }
 
+    pub(crate) const fn negate_if(self, condition: bool) -> Self {
+        if condition {
+            self.negate()
+        } else {
+            self
+        }
+    }
+
     fn into_type(self, db: &dyn Db) -> Type {
         match self {
             Self::AlwaysTrue => Type::BooleanLiteral(true),
diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs
index 084451ee50d1d..3aafa78ae922b 100644
--- a/crates/red_knot_python_semantic/src/types/infer.rs
+++ b/crates/red_knot_python_semantic/src/types/infer.rs
@@ -824,14 +824,10 @@ impl<'db> TypeInferenceBuilder<'db> {
         debug_assert!(binding.is_binding(self.db()));
         let use_def = self.index.use_def_map(binding.file_scope(self.db()));
         let declarations = use_def.declarations_at_binding(binding);
-        let undeclared_ty = if declarations.may_be_undeclared() {
-            Some(Type::Unknown)
-        } else {
-            None
-        };
         let mut bound_ty = ty;
-        let declared_ty = declarations_ty(self.db(), declarations, undeclared_ty).unwrap_or_else(
-            |(ty, conflicting)| {
+        let declared_ty = declarations_ty(self.db(), declarations)
+            .map(|s| s.ignore_possibly_unbound().unwrap_or(Type::Unknown))
+            .unwrap_or_else(|(ty, conflicting)| {
                 // TODO point out the conflicting declarations in the diagnostic?
                 let symbol_table = self.index.symbol_table(binding.file_scope(self.db()));
                 let symbol_name = symbol_table.symbol(binding.symbol(self.db())).name();
@@ -844,8 +840,7 @@ impl<'db> TypeInferenceBuilder<'db> {
                     ),
                 );
                 ty
-            },
-        );
+            });
         if !bound_ty.is_assignable_to(self.db(), declared_ty) {
             report_invalid_assignment(&self.context, node, declared_ty, bound_ty);
             // allow declarations to override inference in case of invalid assignment
@@ -860,7 +855,9 @@ impl<'db> TypeInferenceBuilder<'db> {
         let use_def = self.index.use_def_map(declaration.file_scope(self.db()));
         let prior_bindings = use_def.bindings_at_declaration(declaration);
         // unbound_ty is Never because for this check we don't care about unbound
-        let inferred_ty = bindings_ty(self.db(), prior_bindings).unwrap_or(Type::Never);
+        let inferred_ty = bindings_ty(self.db(), prior_bindings)
+            .ignore_possibly_unbound()
+            .unwrap_or(Type::Never);
         let ty = if inferred_ty.is_assignable_to(self.db(), ty) {
             ty
         } else {
@@ -1739,7 +1736,9 @@ impl<'db> TypeInferenceBuilder<'db> {
                 guard,
             } = case;
             self.infer_match_pattern(pattern);
-            self.infer_optional_expression(guard.as_deref());
+            guard
+                .as_deref()
+                .map(|guard| self.infer_standalone_expression(guard));
             self.infer_body(body);
         }
     }
@@ -1764,13 +1763,24 @@ impl<'db> TypeInferenceBuilder<'db> {
     fn infer_match_pattern(&mut self, pattern: &ast::Pattern) {
         // TODO(dhruvmanila): Add a Salsa query for inferring pattern types and matching against
         // the subject expression: https://github.com/astral-sh/ruff/pull/13147#discussion_r1739424510
+        match pattern {
+            ast::Pattern::MatchValue(match_value) => {
+                self.infer_standalone_expression(&match_value.value);
+            }
+            _ => {
+                self.infer_match_pattern_impl(pattern);
+            }
+        }
+    }
+
+    fn infer_match_pattern_impl(&mut self, pattern: &ast::Pattern) {
         match pattern {
             ast::Pattern::MatchValue(match_value) => {
                 self.infer_expression(&match_value.value);
             }
             ast::Pattern::MatchSequence(match_sequence) => {
                 for pattern in &match_sequence.patterns {
-                    self.infer_match_pattern(pattern);
+                    self.infer_match_pattern_impl(pattern);
                 }
             }
             ast::Pattern::MatchMapping(match_mapping) => {
@@ -1784,7 +1794,7 @@ impl<'db> TypeInferenceBuilder<'db> {
                     self.infer_expression(key);
                 }
                 for pattern in patterns {
-                    self.infer_match_pattern(pattern);
+                    self.infer_match_pattern_impl(pattern);
                 }
             }
             ast::Pattern::MatchClass(match_class) => {
@@ -1794,21 +1804,21 @@ impl<'db> TypeInferenceBuilder<'db> {
                     arguments,
                 } = match_class;
                 for pattern in &arguments.patterns {
-                    self.infer_match_pattern(pattern);
+                    self.infer_match_pattern_impl(pattern);
                 }
                 for keyword in &arguments.keywords {
-                    self.infer_match_pattern(&keyword.pattern);
+                    self.infer_match_pattern_impl(&keyword.pattern);
                 }
                 self.infer_expression(cls);
             }
             ast::Pattern::MatchAs(match_as) => {
                 if let Some(pattern) = &match_as.pattern {
-                    self.infer_match_pattern(pattern);
+                    self.infer_match_pattern_impl(pattern);
                 }
             }
             ast::Pattern::MatchOr(match_or) => {
                 for pattern in &match_or.patterns {
-                    self.infer_match_pattern(pattern);
+                    self.infer_match_pattern_impl(pattern);
                 }
             }
             ast::Pattern::MatchStar(_) | ast::Pattern::MatchSingleton(_) => {}
@@ -3094,28 +3104,24 @@ impl<'db> TypeInferenceBuilder<'db> {
         let use_def = self.index.use_def_map(file_scope_id);
 
         // If we're inferring types of deferred expressions, always treat them as public symbols
-        let (bindings_ty, boundness) = if self.is_deferred() {
+        let bindings_ty = if self.is_deferred() {
             if let Some(symbol) = self.index.symbol_table(file_scope_id).symbol_id_by_name(id) {
-                (
-                    bindings_ty(self.db(), use_def.public_bindings(symbol)),
-                    use_def.public_boundness(symbol),
-                )
+                bindings_ty(self.db(), use_def.public_bindings(symbol))
             } else {
                 assert!(
                     self.deferred_state.in_string_annotation(),
                     "Expected the symbol table to create a symbol for every Name node"
                 );
-                (None, Boundness::PossiblyUnbound)
+                Symbol::Unbound
             }
         } else {
             let use_id = name.scoped_use_id(self.db(), self.scope());
-            (
-                bindings_ty(self.db(), use_def.bindings_at_use(use_id)),
-                use_def.use_boundness(use_id),
-            )
+            bindings_ty(self.db(), use_def.bindings_at_use(use_id))
         };
 
-        if boundness == Boundness::PossiblyUnbound {
+        if let Symbol::Type(ty, Boundness::Bound) = bindings_ty {
+            ty
+        } else {
             match self.lookup_name(name) {
                 Symbol::Type(looked_up_ty, looked_up_boundness) => {
                     if looked_up_boundness == Boundness::PossiblyUnbound {
@@ -3123,20 +3129,22 @@ impl<'db> TypeInferenceBuilder<'db> {
                     }
 
                     bindings_ty
+                        .ignore_possibly_unbound()
                         .map(|ty| UnionType::from_elements(self.db(), [ty, looked_up_ty]))
                         .unwrap_or(looked_up_ty)
                 }
-                Symbol::Unbound => {
-                    if bindings_ty.is_some() {
+                Symbol::Unbound => match bindings_ty {
+                    Symbol::Type(ty, Boundness::PossiblyUnbound) => {
                         report_possibly_unresolved_reference(&self.context, name);
-                    } else {
+                        ty
+                    }
+                    Symbol::Unbound => {
                         report_unresolved_reference(&self.context, name);
+                        Type::Unknown
                     }
-                    bindings_ty.unwrap_or(Type::Unknown)
-                }
+                    Symbol::Type(_, Boundness::Bound) => unreachable!("Handled above"),
+                },
             }
-        } else {
-            bindings_ty.unwrap_or(Type::Unknown)
         }
     }
 
@@ -6353,14 +6361,13 @@ mod tests {
     }
 
     // Incremental inference tests
-
+    #[track_caller]
     fn first_public_binding<'db>(db: &'db TestDb, file: File, name: &str) -> Definition<'db> {
         let scope = global_scope(db, file);
         use_def_map(db, scope)
             .public_bindings(symbol_table(db, scope).symbol_id_by_name(name).unwrap())
-            .next()
-            .unwrap()
-            .binding
+            .find_map(|b| b.binding)
+            .expect("no binding found")
     }
 
     #[test]
diff --git a/crates/red_knot_python_semantic/src/types/narrow.rs b/crates/red_knot_python_semantic/src/types/narrow.rs
index 53476cdbb4949..ef1d6293037ba 100644
--- a/crates/red_knot_python_semantic/src/types/narrow.rs
+++ b/crates/red_knot_python_semantic/src/types/narrow.rs
@@ -1,5 +1,7 @@
 use crate::semantic_index::ast_ids::HasScopedExpressionId;
-use crate::semantic_index::constraint::{Constraint, ConstraintNode, PatternConstraint};
+use crate::semantic_index::constraint::{
+    Constraint, ConstraintNode, PatternConstraint, PatternConstraintKind,
+};
 use crate::semantic_index::definition::Definition;
 use crate::semantic_index::expression::Expression;
 use crate::semantic_index::symbol::{ScopeId, ScopedSymbolId, SymbolTable};
@@ -216,31 +218,12 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
     ) -> Option<NarrowingConstraints<'db>> {
         let subject = pattern.subject(self.db);
 
-        match pattern.pattern(self.db).node() {
-            ast::Pattern::MatchValue(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchSingleton(singleton_pattern) => {
-                self.evaluate_match_pattern_singleton(subject, singleton_pattern)
-            }
-            ast::Pattern::MatchSequence(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchMapping(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchClass(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchStar(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchAs(_) => {
-                None // TODO
-            }
-            ast::Pattern::MatchOr(_) => {
-                None // TODO
+        match pattern.kind(self.db) {
+            PatternConstraintKind::Singleton(singleton, _guard) => {
+                self.evaluate_match_pattern_singleton(*subject, *singleton)
             }
+            // TODO: support more pattern kinds
+            PatternConstraintKind::Value(..) | PatternConstraintKind::Unsupported => None,
         }
     }
 
@@ -483,14 +466,14 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
 
     fn evaluate_match_pattern_singleton(
         &mut self,
-        subject: &ast::Expr,
-        pattern: &ast::PatternMatchSingleton,
+        subject: Expression<'db>,
+        singleton: ast::Singleton,
     ) -> Option<NarrowingConstraints<'db>> {
-        if let Some(ast::ExprName { id, .. }) = subject.as_name_expr() {
+        if let Some(ast::ExprName { id, .. }) = subject.node_ref(self.db).as_name_expr() {
             // SAFETY: we should always have a symbol for every Name node.
             let symbol = self.symbols().symbol_id_by_name(id).unwrap();
 
-            let ty = match pattern.value {
+            let ty = match singleton {
                 ast::Singleton::None => Type::none(self.db),
                 ast::Singleton::True => Type::BooleanLiteral(true),
                 ast::Singleton::False => Type::BooleanLiteral(false),
diff --git a/crates/red_knot_python_semantic/src/visibility_constraints.rs b/crates/red_knot_python_semantic/src/visibility_constraints.rs
new file mode 100644
index 0000000000000..616b1ef3709ea
--- /dev/null
+++ b/crates/red_knot_python_semantic/src/visibility_constraints.rs
@@ -0,0 +1,161 @@
+use crate::semantic_index::{
+    ast_ids::HasScopedExpressionId,
+    constraint::{Constraint, ConstraintNode, PatternConstraintKind},
+};
+use crate::types::{infer_expression_types, Truthiness};
+use crate::Db;
+
+const MAX_RECURSION_DEPTH: usize = 10;
+
+#[salsa::interned]
+pub(crate) struct VisibilityConstraint<'db> {
+    kind: VisibilityConstraintKind<'db>,
+}
+
+impl<'db> VisibilityConstraint<'db> {
+    pub(crate) fn always_true(db: &'db dyn Db) -> Self {
+        Self::new(db, VisibilityConstraintKind::AlwaysTrue)
+    }
+
+    pub(crate) fn ambiguous(db: &'db dyn Db) -> Self {
+        Self::new(db, VisibilityConstraintKind::Ambiguous)
+    }
+
+    pub(crate) fn visible_if(db: &'db dyn Db, constraint: Constraint<'db>) -> Self {
+        Self::new(db, VisibilityConstraintKind::VisibleIf(constraint))
+    }
+
+    pub(crate) fn visible_if_not(db: &'db dyn Db, constraint: VisibilityConstraint<'db>) -> Self {
+        Self::new(db, VisibilityConstraintKind::VisibleIfNot(constraint))
+    }
+
+    pub(crate) fn kleene_and(
+        db: &'db dyn Db,
+        lhs: VisibilityConstraint<'db>,
+        rhs: VisibilityConstraint<'db>,
+    ) -> Self {
+        Self::new(db, VisibilityConstraintKind::KleeneAnd(lhs, rhs))
+    }
+
+    pub(crate) fn kleene_or(
+        db: &'db dyn Db,
+        lhs: VisibilityConstraint<'db>,
+        rhs: VisibilityConstraint<'db>,
+    ) -> Self {
+        Self::new(db, VisibilityConstraintKind::KleeneOr(lhs, rhs))
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub(crate) enum VisibilityConstraintKind<'db> {
+    AlwaysTrue,
+    Ambiguous,
+    VisibleIf(Constraint<'db>),
+    VisibleIfNot(VisibilityConstraint<'db>),
+    KleeneAnd(VisibilityConstraint<'db>, VisibilityConstraint<'db>),
+    KleeneOr(VisibilityConstraint<'db>, VisibilityConstraint<'db>),
+}
+
+/// Analyze the statically known visibility for a given visibility constraint.
+pub(crate) fn evaluate<'db>(db: &'db dyn Db, constraint: VisibilityConstraint<'db>) -> Truthiness {
+    evaluate_impl(db, constraint, MAX_RECURSION_DEPTH)
+}
+
+fn evaluate_impl<'db>(
+    db: &'db dyn Db,
+    constraint: VisibilityConstraint<'db>,
+    max_depth: usize,
+) -> Truthiness {
+    if max_depth == 0 {
+        return Truthiness::Ambiguous;
+    }
+
+    match constraint.kind(db) {
+        VisibilityConstraintKind::AlwaysTrue => Truthiness::AlwaysTrue,
+        VisibilityConstraintKind::Ambiguous => Truthiness::Ambiguous,
+        VisibilityConstraintKind::VisibleIf(constraint) => analyze_single(db, &constraint),
+        VisibilityConstraintKind::VisibleIfNot(negated) => {
+            evaluate_impl(db, negated, max_depth - 1).negate()
+        }
+        VisibilityConstraintKind::KleeneAnd(lhs, rhs) => {
+            let lhs = evaluate_impl(db, lhs, max_depth - 1);
+
+            if lhs == Truthiness::AlwaysFalse {
+                return Truthiness::AlwaysFalse;
+            }
+
+            let rhs = evaluate_impl(db, rhs, max_depth - 1);
+
+            if rhs == Truthiness::AlwaysFalse {
+                Truthiness::AlwaysFalse
+            } else if lhs == Truthiness::AlwaysTrue && rhs == Truthiness::AlwaysTrue {
+                Truthiness::AlwaysTrue
+            } else {
+                Truthiness::Ambiguous
+            }
+        }
+        VisibilityConstraintKind::KleeneOr(lhs, rhs) => {
+            let lhs = evaluate_impl(db, lhs, max_depth - 1);
+
+            if lhs == Truthiness::AlwaysTrue {
+                return Truthiness::AlwaysTrue;
+            }
+
+            let rhs = evaluate_impl(db, rhs, max_depth - 1);
+
+            if rhs == Truthiness::AlwaysTrue {
+                Truthiness::AlwaysTrue
+            } else if lhs == Truthiness::AlwaysFalse && rhs == Truthiness::AlwaysFalse {
+                Truthiness::AlwaysFalse
+            } else {
+                Truthiness::Ambiguous
+            }
+        }
+    }
+}
+
+fn analyze_single(db: &dyn Db, constraint: &Constraint) -> Truthiness {
+    match constraint.node {
+        ConstraintNode::Expression(test_expr) => {
+            let inference = infer_expression_types(db, test_expr);
+            let scope = test_expr.scope(db);
+            let ty =
+                inference.expression_ty(test_expr.node_ref(db).scoped_expression_id(db, scope));
+
+            ty.bool(db).negate_if(!constraint.is_positive)
+        }
+        ConstraintNode::Pattern(inner) => match inner.kind(db) {
+            PatternConstraintKind::Value(value, guard) => {
+                let subject_expression = inner.subject(db);
+                let inference = infer_expression_types(db, *subject_expression);
+                let scope = subject_expression.scope(db);
+                let subject_ty = inference.expression_ty(
+                    subject_expression
+                        .node_ref(db)
+                        .scoped_expression_id(db, scope),
+                );
+
+                let inference = infer_expression_types(db, *value);
+                let scope = value.scope(db);
+                let value_ty =
+                    inference.expression_ty(value.node_ref(db).scoped_expression_id(db, scope));
+
+                if subject_ty.is_single_valued(db) {
+                    let truthiness = Truthiness::from(subject_ty.is_equivalent_to(db, value_ty));
+
+                    if truthiness.is_always_true() && guard.is_some() {
+                        // Fall back to ambiguous, the guard might change the result.
+                        Truthiness::Ambiguous
+                    } else {
+                        truthiness
+                    }
+                } else {
+                    Truthiness::Ambiguous
+                }
+            }
+            PatternConstraintKind::Singleton(..) | PatternConstraintKind::Unsupported => {
+                Truthiness::Ambiguous
+            }
+        },
+    }
+}
diff --git a/crates/red_knot_test/src/config.rs b/crates/red_knot_test/src/config.rs
index cf677c485c3da..a2fe51226e34a 100644
--- a/crates/red_knot_test/src/config.rs
+++ b/crates/red_knot_test/src/config.rs
@@ -9,7 +9,7 @@
 //! ```
 
 use anyhow::Context;
-use red_knot_python_semantic::PythonVersion;
+use red_knot_python_semantic::{PythonPlatform, PythonVersion};
 use serde::Deserialize;
 
 #[derive(Deserialize, Debug, Default, Clone)]
@@ -28,13 +28,22 @@ impl MarkdownTestConfig {
     pub(crate) fn python_version(&self) -> Option<PythonVersion> {
         self.environment.as_ref().and_then(|env| env.python_version)
     }
+
+    pub(crate) fn python_platform(&self) -> Option<PythonPlatform> {
+        self.environment
+            .as_ref()
+            .and_then(|env| env.python_platform.clone())
+    }
 }
 
 #[derive(Deserialize, Debug, Default, Clone)]
 #[serde(rename_all = "kebab-case", deny_unknown_fields)]
 pub(crate) struct Environment {
-    /// Python version to assume when resolving types.
+    /// Target Python version to assume when resolving types.
     pub(crate) python_version: Option<PythonVersion>,
+
+    /// Target platform to assume when resolving types.
+    pub(crate) python_platform: Option<PythonPlatform>,
 }
 
 #[derive(Deserialize, Debug, Clone)]
diff --git a/crates/red_knot_test/src/db.rs b/crates/red_knot_test/src/db.rs
index df1cfc503e9f9..d6e3d82090e03 100644
--- a/crates/red_knot_test/src/db.rs
+++ b/crates/red_knot_test/src/db.rs
@@ -1,7 +1,7 @@
 use red_knot_python_semantic::lint::RuleSelection;
 use red_knot_python_semantic::{
-    default_lint_registry, Db as SemanticDb, Program, ProgramSettings, PythonVersion,
-    SearchPathSettings,
+    default_lint_registry, Db as SemanticDb, Program, ProgramSettings, PythonPlatform,
+    PythonVersion, SearchPathSettings,
 };
 use ruff_db::files::{File, Files};
 use ruff_db::system::{DbWithTestSystem, System, SystemPath, SystemPathBuf, TestSystem};
@@ -40,6 +40,7 @@ impl Db {
             &db,
             &ProgramSettings {
                 python_version: PythonVersion::default(),
+                python_platform: PythonPlatform::default(),
                 search_paths: SearchPathSettings::new(db.workspace_root.clone()),
             },
         )
diff --git a/crates/red_knot_test/src/lib.rs b/crates/red_knot_test/src/lib.rs
index f2a7639e29ec7..9b39048a572af 100644
--- a/crates/red_knot_test/src/lib.rs
+++ b/crates/red_knot_test/src/lib.rs
@@ -52,6 +52,9 @@ pub fn run(path: &Utf8Path, long_title: &str, short_title: &str, test_name: &str
         Program::get(&db)
             .set_python_version(&mut db)
             .to(test.configuration().python_version().unwrap_or_default());
+        Program::get(&db)
+            .set_python_platform(&mut db)
+            .to(test.configuration().python_platform().unwrap_or_default());
 
         // Remove all files so that the db is in a "fresh" state.
         db.memory_file_system().remove_all();
diff --git a/crates/red_knot_workspace/src/workspace/settings.rs b/crates/red_knot_workspace/src/workspace/settings.rs
index 66493f441d265..c924e9ec9b1d4 100644
--- a/crates/red_knot_workspace/src/workspace/settings.rs
+++ b/crates/red_knot_workspace/src/workspace/settings.rs
@@ -1,5 +1,7 @@
 use crate::workspace::PackageMetadata;
-use red_knot_python_semantic::{ProgramSettings, PythonVersion, SearchPathSettings, SitePackages};
+use red_knot_python_semantic::{
+    ProgramSettings, PythonPlatform, PythonVersion, SearchPathSettings, SitePackages,
+};
 use ruff_db::system::{SystemPath, SystemPathBuf};
 
 /// The resolved configurations.
@@ -40,6 +42,7 @@ impl Configuration {
         WorkspaceSettings {
             program: ProgramSettings {
                 python_version: self.python_version.unwrap_or_default(),
+                python_platform: PythonPlatform::default(),
                 search_paths: self.search_paths.to_settings(workspace_root),
             },
         }
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_file.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_file.snap
index d4a37a5d96369..804be9349a23c 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_file.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_file.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: "&workspace"
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -23,6 +22,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_hidden_folder.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_hidden_folder.snap
index ab387f9a4c834..3aabf1ceb2e35 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_hidden_folder.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__member_pattern_matching_hidden_folder.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: workspace
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -23,6 +22,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__package_without_pyproject.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__package_without_pyproject.snap
index bbc5c1247c548..73329a8552048 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__package_without_pyproject.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__package_without_pyproject.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: workspace
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -23,6 +22,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__single_package.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__single_package.snap
index 4c0f26977bc24..6255e408683d9 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__single_package.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__single_package.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: workspace
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -23,6 +22,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_excluded.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_excluded.snap
index 8429a787eb208..4c68fd87142b2 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_excluded.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_excluded.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: workspace
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -36,6 +35,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_members.snap b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_members.snap
index 74e5ced627f17..4f3c74ba34c8f 100644
--- a/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_members.snap
+++ b/crates/red_knot_workspace/src/workspace/snapshots/red_knot_workspace__workspace__metadata__tests__workspace_members.snap
@@ -1,7 +1,6 @@
 ---
 source: crates/red_knot_workspace/src/workspace/metadata.rs
 expression: workspace
-snapshot_kind: text
 ---
 WorkspaceMetadata(
   root: "/app",
@@ -49,6 +48,7 @@ WorkspaceMetadata(
   settings: WorkspaceSettings(
     program: ProgramSettings(
       python_version: "3.9",
+      python_platform: all,
       search_paths: SearchPathSettings(
         extra_paths: [],
         src_root: "/app",
diff --git a/crates/ruff_graph/src/db.rs b/crates/ruff_graph/src/db.rs
index a70ae6d91e7b8..9e3d1b6f3f58d 100644
--- a/crates/ruff_graph/src/db.rs
+++ b/crates/ruff_graph/src/db.rs
@@ -3,7 +3,9 @@ use std::sync::Arc;
 use zip::CompressionMethod;
 
 use red_knot_python_semantic::lint::RuleSelection;
-use red_knot_python_semantic::{Db, Program, ProgramSettings, PythonVersion, SearchPathSettings};
+use red_knot_python_semantic::{
+    Db, Program, ProgramSettings, PythonPlatform, PythonVersion, SearchPathSettings,
+};
 use ruff_db::files::{File, Files};
 use ruff_db::system::{OsSystem, System, SystemPathBuf};
 use ruff_db::vendored::{VendoredFileSystem, VendoredFileSystemBuilder};
@@ -49,6 +51,7 @@ impl ModuleDb {
             &db,
             &ProgramSettings {
                 python_version,
+                python_platform: PythonPlatform::default(),
                 search_paths,
             },
         )?;
diff --git a/fuzz/fuzz_targets/red_knot_check_invalid_syntax.rs b/fuzz/fuzz_targets/red_knot_check_invalid_syntax.rs
index 1259b8c33687d..f547a7c4760c8 100644
--- a/fuzz/fuzz_targets/red_knot_check_invalid_syntax.rs
+++ b/fuzz/fuzz_targets/red_knot_check_invalid_syntax.rs
@@ -10,7 +10,7 @@ use libfuzzer_sys::{fuzz_target, Corpus};
 use red_knot_python_semantic::types::check_types;
 use red_knot_python_semantic::{
     default_lint_registry, lint::RuleSelection, Db as SemanticDb, Program, ProgramSettings,
-    PythonVersion, SearchPathSettings,
+    PythonPlatform, PythonVersion, SearchPathSettings,
 };
 use ruff_db::files::{system_path_to_file, File, Files};
 use ruff_db::system::{DbWithTestSystem, System, SystemPathBuf, TestSystem};
@@ -112,6 +112,7 @@ fn setup_db() -> TestDb {
         &db,
         &ProgramSettings {
             python_version: PythonVersion::default(),
+            python_platform: PythonPlatform::default(),
             search_paths: SearchPathSettings::new(src_root),
         },
     )