[ty] Evaluate reachability of non-definitely-bound to Ambiguous (astral-sh#19579)

## Summary

closes astral-sh/ty#692

If the expression (or any child expressions) is not definitely bound the
reachability constraint evaluation is determined as ambiguous.

This fixes the infinite cycles panic in the following code:

```py
from typing import Literal

class Toggle:
    def __init__(self: "Toggle"):
        if not self.x:
            self.x: Literal[True] = True
```

Credit of this solution is for David.

## Test Plan

- Added a test case with too many cycle iterations panic.
- Previous tests.

---------

Co-authored-by: David Peter <mail@david-peter.de>

Author: 2 people

crates/ty_python_semantic/resources/mdtest/attributes.md

@@ -2288,6 +2288,26 @@ class H:
         self.x = other.x or self.x
 ```
 
+An attribute definition can be guarded by a condition involving that attribute. This is a regression
+test for <https://github.com/astral-sh/ty/issues/692>:
+
+```py
+from typing import Literal
+
+def check(x) -> Literal[False]:
+    return False
+
+class Toggle:
+    def __init__(self: "Toggle"):
+        if not self.x:
+            self.x: Literal[True] = True
+        if check(self.y):
+            self.y = True
+
+reveal_type(Toggle().x)  # revealed: Literal[True]
+reveal_type(Toggle().y)  # revealed:  Unknown | Literal[True]
+```
+
 ### Builtin types attributes
 
 This test can probably be removed eventually, but we currently include it because we do not yet

crates/ty_python_semantic/resources/mdtest/statically_known_branches.md

@@ -1564,6 +1564,24 @@ if True:
 from module import symbol
 ```
 
+## Non-definitely bound symbols in conditions
+
+When a non-definitely bound symbol is used as a (part of a) condition, we always infer an ambiguous
+truthiness. If we didn't do that, `x` would be considered definitely bound in the following example:
+
+```py
+def _(flag: bool):
+    if flag:
+        ALWAYS_TRUE_IF_BOUND = True
+
+    # error: [possibly-unresolved-reference] "Name `ALWAYS_TRUE_IF_BOUND` used when possibly not defined"
+    if True and ALWAYS_TRUE_IF_BOUND:
+        x = 1
+
+    # error: [possibly-unresolved-reference] "Name `x` used when possibly not defined"
+    x
+```
+
 ## Unreachable code
 
 A closely related feature is the ability to detect unreachable code. For example, we do not emit a

crates/ty_python_semantic/src/place.rs

@@ -135,6 +135,10 @@ impl<'db> Place<'db> {
             Place::Unbound => Place::Unbound,
         }
     }
+
+    pub(crate) const fn is_definitely_bound(&self) -> bool {
+        matches!(self, Place::Type(_, Boundness::Bound))
+    }
 }
 
 impl<'db> From<LookupResult<'db>> for PlaceAndQualifiers<'db> {

crates/ty_python_semantic/src/semantic_index/reachability_constraints.rs

@@ -209,6 +209,7 @@ use crate::semantic_index::predicate::{
 };
 use crate::types::{
     IntersectionBuilder, Truthiness, Type, UnionBuilder, UnionType, infer_expression_type,
+    static_expression_truthiness,
 };
 
 /// A ternary formula that defines under what conditions a binding is visible. (A ternary formula
@@ -821,8 +822,7 @@ impl ReachabilityConstraints {
     fn analyze_single(db: &dyn Db, predicate: &Predicate) -> Truthiness {
         match predicate.node {
             PredicateNode::Expression(test_expr) => {
-                let ty = infer_expression_type(db, test_expr);
-                ty.bool(db).negate_if(!predicate.is_positive)
+                static_expression_truthiness(db, test_expr).negate_if(!predicate.is_positive)
             }
             PredicateNode::ReturnsNever(CallableAndCallExpr {
                 callable,

crates/ty_python_semantic/src/semantic_index/use_def.rs

@@ -598,7 +598,7 @@ impl<'db> UseDefMap<'db> {
             .is_always_false()
     }
 
-    pub(crate) fn is_declaration_reachable(
+    pub(crate) fn declaration_reachability(
         &self,
         db: &dyn crate::Db,
         declaration: &DeclarationWithConstraint<'db>,
@@ -610,7 +610,7 @@ impl<'db> UseDefMap<'db> {
         )
     }
 
-    pub(crate) fn is_binding_reachable(
+    pub(crate) fn binding_reachability(
         &self,
         db: &dyn crate::Db,
         binding: &BindingWithConstraints<'_, 'db>,

crates/ty_python_semantic/src/types.rs

@@ -24,7 +24,7 @@ pub use self::diagnostic::TypeCheckDiagnostics;
 pub(crate) use self::diagnostic::register_lints;
 pub(crate) use self::infer::{
     infer_deferred_types, infer_definition_types, infer_expression_type, infer_expression_types,
-    infer_scope_types,
+    infer_scope_types, static_expression_truthiness,
 };
 pub(crate) use self::signatures::{CallableSignature, Signature};
 pub(crate) use self::subclass_of::{SubclassOfInner, SubclassOfType};
@@ -6910,6 +6910,10 @@ bitflags! {
         const NOT_REQUIRED = 1 << 4;
         /// `typing_extensions.ReadOnly`
         const READ_ONLY = 1 << 5;
+        /// An implicit instance attribute which is possibly unbound according
+        /// to local control flow within the method it is defined in. This flag
+        /// overrules the `Boundness` information on `PlaceAndQualifiers`.
+        const POSSIBLY_UNBOUND_IMPLICIT_ATTRIBUTE = 1 << 6;
     }
 }
 
@@ -8620,7 +8624,7 @@ impl TypeRelation {
     }
 }
 
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, get_size2::GetSize)]
 pub enum Truthiness {
     /// For an object `x`, `bool(x)` will always return `True`
     AlwaysTrue,

crates/ty_python_semantic/src/types/class.rs

@@ -2736,17 +2736,20 @@ impl<'db> ClassLiteral<'db> {
                 //     self.name: <annotation>
                 //     self.name: <annotation> = …
 
-                if use_def_map(db, method_scope)
-                    .is_declaration_reachable(db, &attribute_declaration)
-                    .is_always_false()
-                {
+                let reachability = use_def_map(db, method_scope)
+                    .declaration_reachability(db, &attribute_declaration);
+
+                if reachability.is_always_false() {
                     continue;
                 }
 
                 let annotation = declaration_type(db, declaration);
-                let annotation =
+                let mut annotation =
                     Place::bound(annotation.inner).with_qualifiers(annotation.qualifiers);
 
+                if reachability.is_ambiguous() {
+                    annotation.qualifiers |= TypeQualifiers::POSSIBLY_UNBOUND_IMPLICIT_ATTRIBUTE;
+                }
                 if let Some(all_qualifiers) = annotation.is_bare_final() {
                     if let Some(value) = assignment.value(&module) {
                         // If we see an annotated assignment with a bare `Final` as in
@@ -2789,7 +2792,7 @@ impl<'db> ClassLiteral<'db> {
                         .all_reachable_symbol_bindings(method_place)
                         .find_map(|bind| {
                             (bind.binding.is_defined_and(|def| def == method))
-                                .then(|| class_map.is_binding_reachable(db, &bind))
+                                .then(|| class_map.binding_reachability(db, &bind))
                         })
                         .unwrap_or(Truthiness::AlwaysFalse)
                 } else {
@@ -2818,11 +2821,15 @@ impl<'db> ClassLiteral<'db> {
                     continue;
                 };
                 match method_map
-                    .is_binding_reachable(db, &attribute_assignment)
+                    .binding_reachability(db, &attribute_assignment)
                     .and(is_method_reachable)
                 {
-                    Truthiness::AlwaysTrue | Truthiness::Ambiguous => {
+                    Truthiness::AlwaysTrue => {
+                        is_attribute_bound = true;
+                    }
+                    Truthiness::Ambiguous => {
                         is_attribute_bound = true;
+                        qualifiers |= TypeQualifiers::POSSIBLY_UNBOUND_IMPLICIT_ATTRIBUTE;
                     }
                     Truthiness::AlwaysFalse => {
                         continue;
@@ -2834,7 +2841,7 @@ impl<'db> ClassLiteral<'db> {
                 // TODO: this is incomplete logic since the attributes bound after termination are considered reachable.
                 let unbound_reachability = unbound_binding
                     .as_ref()
-                    .map(|binding| method_map.is_binding_reachable(db, binding))
+                    .map(|binding| method_map.binding_reachability(db, binding))
                     .unwrap_or(Truthiness::AlwaysFalse);
 
                 if unbound_reachability

crates/ty_python_semantic/src/types/infer.rs

@@ -337,6 +337,45 @@ fn single_expression_cycle_initial<'db>(
     Type::Never
 }
 
+/// Returns the statically-known truthiness of a given expression.
+///
+/// Returns [`Truthiness::Ambiguous`] in case any non-definitely bound places
+/// were encountered while inferring the type of the expression.
+#[salsa::tracked(cycle_fn=static_expression_truthiness_cycle_recover, cycle_initial=static_expression_truthiness_cycle_initial, heap_size=get_size2::GetSize::get_heap_size)]
+pub(crate) fn static_expression_truthiness<'db>(
+    db: &'db dyn Db,
+    expression: Expression<'db>,
+) -> Truthiness {
+    let inference = infer_expression_types(db, expression);
+
+    if !inference.all_places_definitely_bound() {
+        return Truthiness::Ambiguous;
+    }
+
+    let file = expression.file(db);
+    let module = parsed_module(db, file).load(db);
+    let node = expression.node_ref(db, &module);
+
+    inference.expression_type(node).bool(db)
+}
+
+#[expect(clippy::trivially_copy_pass_by_ref)]
+fn static_expression_truthiness_cycle_recover<'db>(
+    _db: &'db dyn Db,
+    _value: &Truthiness,
+    _count: u32,
+    _expression: Expression<'db>,
+) -> salsa::CycleRecoveryAction<Truthiness> {
+    salsa::CycleRecoveryAction::Iterate
+}
+
+fn static_expression_truthiness_cycle_initial<'db>(
+    _db: &'db dyn Db,
+    _expression: Expression<'db>,
+) -> Truthiness {
+    Truthiness::Ambiguous
+}
+
 /// Infer the types for an [`Unpack`] operation.
 ///
 /// This infers the expression type and performs structural match against the target expression
@@ -657,6 +696,9 @@ struct ExpressionInferenceExtra<'db> {
     ///
     /// Falls back to `Type::Never` if an expression is missing.
     cycle_fallback: bool,
+
+    /// `true` if all places in this expression are definitely bound
+    all_definitely_bound: bool,
 }
 
 impl<'db> ExpressionInference<'db> {
@@ -665,6 +707,7 @@ impl<'db> ExpressionInference<'db> {
         Self {
             extra: Some(Box::new(ExpressionInferenceExtra {
                 cycle_fallback: true,
+                all_definitely_bound: true,
                 ..ExpressionInferenceExtra::default()
             })),
             expressions: FxHashMap::default(),
@@ -698,6 +741,14 @@ impl<'db> ExpressionInference<'db> {
     fn fallback_type(&self) -> Option<Type<'db>> {
         self.is_cycle_callback().then_some(Type::Never)
     }
+
+    /// Returns true if all places in this expression are definitely bound.
+    pub(crate) fn all_places_definitely_bound(&self) -> bool {
+        self.extra
+            .as_ref()
+            .map(|e| e.all_definitely_bound)
+            .unwrap_or(true)
+    }
 }
 
 /// Whether the intersection type is on the left or right side of the comparison.
@@ -847,6 +898,9 @@ pub(super) struct TypeInferenceBuilder<'db, 'ast> {
     ///
     /// This is used only when constructing a cycle-recovery `TypeInference`.
     cycle_fallback: bool,
+
+    /// `true` if all places in this expression are definitely bound
+    all_definitely_bound: bool,
 }
 
 impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
@@ -880,6 +934,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             deferred: VecSet::default(),
             undecorated_type: None,
             cycle_fallback: false,
+            all_definitely_bound: true,
         }
     }
 
@@ -6614,7 +6669,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
         let (resolved, constraint_keys) =
             self.infer_place_load(PlaceExprRef::from(&expr), ast::ExprRef::Name(name_node));
 
-        resolved
+        let resolved_after_fallback = resolved
             // Not found in the module's explicitly declared global symbols?
             // Check the "implicit globals" such as `__doc__`, `__file__`, `__name__`, etc.
             // These are looked up as attributes on `types.ModuleType`.
@@ -6650,8 +6705,14 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 } else {
                     Place::Unbound.into()
                 }
-            })
-            .unwrap_with_diagnostic(|lookup_error| match lookup_error {
+            });
+
+        if !resolved_after_fallback.place.is_definitely_bound() {
+            self.all_definitely_bound = false;
+        }
+
+        let ty =
+            resolved_after_fallback.unwrap_with_diagnostic(|lookup_error| match lookup_error {
                 LookupError::Unbound(qualifiers) => {
                     self.report_unresolved_reference(name_node);
                     TypeAndQualifiers::new(Type::unknown(), qualifiers)
@@ -6662,8 +6723,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     }
                     type_when_bound
                 }
-            })
-            .inner_type()
+            });
+
+        ty.inner_type()
     }
 
     fn infer_local_place_load(
@@ -7093,7 +7155,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
     }
 
     fn narrow_expr_with_applicable_constraints<'r>(
-        &self,
+        &mut self,
         target: impl Into<ast::ExprRef<'r>>,
         target_ty: Type<'db>,
         constraint_keys: &[(FileScopeId, ConstraintKey)],
@@ -7136,11 +7198,19 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 assigned_type = Some(ty);
             }
         }
+        let fallback_place = value_type.member(db, &attr.id);
+        if !fallback_place.place.is_definitely_bound()
+            || fallback_place
+                .qualifiers
+                .contains(TypeQualifiers::POSSIBLY_UNBOUND_IMPLICIT_ATTRIBUTE)
+        {
+            self.all_definitely_bound = false;
+        }
 
-        let resolved_type = value_type
-            .member(db, &attr.id)
-            .map_type(|ty| self.narrow_expr_with_applicable_constraints(attribute, ty, &constraint_keys))
-            .unwrap_with_diagnostic(|lookup_error| match lookup_error {
+        let resolved_type =
+            fallback_place.map_type(|ty| {
+            self.narrow_expr_with_applicable_constraints(attribute, ty, &constraint_keys)
+        }).unwrap_with_diagnostic(|lookup_error| match lookup_error {
                 LookupError::Unbound(_) => {
                     let report_unresolved_attribute = self.is_reachable(attribute);
 
@@ -9248,6 +9318,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             declarations,
             deferred,
             cycle_fallback,
+            all_definitely_bound,
 
             // Ignored; only relevant to definition regions
             undecorated_type: _,
@@ -9274,7 +9345,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
         );
 
         let extra =
-            (cycle_fallback || !bindings.is_empty() || !diagnostics.is_empty()).then(|| {
+            (cycle_fallback || !bindings.is_empty() || !diagnostics.is_empty() || !all_definitely_bound).then(|| {
                 if bindings.len() > 20 {
                     tracing::debug!(
                         "Inferred expression region `{:?}` contains {} bindings. Lookups by linear scan might be slow.",
@@ -9287,6 +9358,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     bindings: bindings.into_boxed_slice(),
                     diagnostics,
                     cycle_fallback,
+                    all_definitely_bound,
                 })
             });
 
@@ -9312,7 +9384,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             deferred,
             cycle_fallback,
             undecorated_type,
-
+            all_definitely_bound: _,
             // builder only state
             typevar_binding_context: _,
             deferred_state: _,
@@ -9379,6 +9451,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
             deferred: _,
             bindings: _,
             declarations: _,
+            all_definitely_bound: _,
 
             // Ignored; only relevant to definition regions
             undecorated_type: _,