[ty] Fix narrowing and reachability of class patterns with arguments (#19512)

## Summary I noticed that our type narrowing and reachability analysis was incorrect for class patterns that are not irrefutable. The test cases below compare the old and the new behavior: ```py from dataclasses import dataclass @DataClass class Point: x: int y: int class Other: ... def _(target: Point): y = 1 match target: case Point(0, 0): y = 2 case Point(x=0, y=1): y = 3 case Point(x=1, y=0): y = 4 reveal_type(y) # revealed: Literal[1, 2, 3, 4] (previously: Literal[2]) def _(target: Point | Other): match target: case Point(0, 0): reveal_type(target) # revealed: Point case Point(x=0, y=1): reveal_type(target) # revealed: Point (previously: Never) case Point(x=1, y=0): reveal_type(target) # revealed: Point (previously: Never) case Other(): reveal_type(target) # revealed: Other (previously: Other & ~Point) ``` ## Test Plan New Markdown test

Author: sharkdp

crates/ty_python_semantic/resources/mdtest/conditional/match.md

@@ -80,6 +80,8 @@ def _(subject: C):
 A `case` branch with a class pattern is taken if the subject is an instance of the given class, and
 all subpatterns in the class pattern match.
 
+### Without arguments
+
 ```py
 from typing import final
 
@@ -136,6 +138,51 @@ def _(target: FooSub | str):
  reveal_type(y) # revealed: Literal[1, 3, 4]
 ```
 
+### With arguments
+
+```py
+from typing_extensions import assert_never
+from dataclasses import dataclass
+
+@dataclass
+class Point:
+ x: int
+ y: int
+
+class Other: ...
+
+def _(target: Point):
+ y = 1
+
+ match target:
+ case Point(0, 0):
+ y = 2
+ case Point(x=0, y=1):
+ y = 3
+ case Point(x=1, y=0):
+ y = 4
+
+ reveal_type(y) # revealed: Literal[1, 2, 3, 4]
+
+def _(target: Point):
+ match target:
+ case Point(x, y): # irrefutable sub-patterns
+ pass
+ case _:
+ assert_never(target)
+
+def _(target: Point | Other):
+ match target:
+ case Point(0, 0):
+ reveal_type(target) # revealed: Point
+ case Point(x=0, y=1):
+ reveal_type(target) # revealed: Point
+ case Point(x=1, y=0):
+ reveal_type(target) # revealed: Point
+ case Other():
+ reveal_type(target) # revealed: Other
+```
+
 ## Singleton match
 
 Singleton patterns are matched based on identity, not equality comparisons or `isinstance()` checks.

crates/ty_python_semantic/src/semantic_index/builder.rs

@@ -35,8 +35,8 @@ use crate::semantic_index::place::{
  PlaceExprWithFlags, PlaceTableBuilder, Scope, ScopeId, ScopeKind, ScopedPlaceId,
 };
 use crate::semantic_index::predicate::{
- CallableAndCallExpr, PatternPredicate, PatternPredicateKind, Predicate, PredicateNode,
- PredicateOrLiteral, ScopedPredicateId, StarImportPlaceholderPredicate,
+ CallableAndCallExpr, ClassPatternKind, PatternPredicate, PatternPredicateKind, Predicate,
+ PredicateNode, PredicateOrLiteral, ScopedPredicateId, StarImportPlaceholderPredicate,
 };
 use crate::semantic_index::re_exports::exported_names;
 use crate::semantic_index::reachability_constraints::{
@@ -697,7 +697,25 @@ impl<'db, 'ast> SemanticIndexBuilder<'db, 'ast> {
  }
  ast::Pattern::MatchClass(pattern) => {
  let cls = self.add_standalone_expression(&pattern.cls);
- PatternPredicateKind::Class(cls)
+
+ PatternPredicateKind::Class(
+ cls,
+ if pattern
+ .arguments
+ .patterns
+ .iter()
+ .all(ast::Pattern::is_irrefutable)
+ && pattern
+ .arguments
+ .keywords
+ .iter()
+ .all(|kw| kw.pattern.is_irrefutable())
+ {
+ ClassPatternKind::Irrefutable
+ } else {
+ ClassPatternKind::Refutable
+ },
+ )
  }
  ast::Pattern::MatchOr(pattern) => {
  let predicates = pattern

crates/ty_python_semantic/src/semantic_index/predicate.rs

@@ -116,13 +116,25 @@ pub(crate) enum PredicateNode<'db> {
  StarImportPlaceholder(StarImportPlaceholderPredicate<'db>),
 }
 
+#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, salsa::Update)]
+pub(crate) enum ClassPatternKind {
+ Irrefutable,
+ Refutable,
+}
+
+impl ClassPatternKind {
+ pub(crate) fn is_irrefutable(self) -> bool {
+ matches!(self, ClassPatternKind::Irrefutable)
+ }
+}
+
 /// Pattern kinds for which we support type narrowing and/or static reachability analysis.
 #[derive(Debug, Clone, Hash, PartialEq, salsa::Update)]
 pub(crate) enum PatternPredicateKind<'db> {
  Singleton(Singleton),
  Value(Expression<'db>),
  Or(Vec<PatternPredicateKind<'db>>),
- Class(Expression<'db>),
+ Class(Expression<'db>, ClassPatternKind),
  Unsupported,
 }
 

crates/ty_python_semantic/src/semantic_index/reachability_constraints.rs

@@ -689,13 +689,20 @@ impl ReachabilityConstraints {
  });
  truthiness
  }
- PatternPredicateKind::Class(class_expr) => {
+ PatternPredicateKind::Class(class_expr, kind) => {
  let subject_ty = infer_expression_type(db, subject);
  let class_ty = infer_expression_type(db, *class_expr).to_instance(db);
 
  class_ty.map_or(Truthiness::Ambiguous, |class_ty| {
  if subject_ty.is_subtype_of(db, class_ty) {
- Truthiness::AlwaysTrue
+ if kind.is_irrefutable() {
+ Truthiness::AlwaysTrue
+ } else {
+ // A class pattern like `case Point(x=0, y=0)` is not irrefutable,
+ // i.e. it does not match all instances of `Point`. This means that
+ // we can't tell for sure if this pattern will match or not.
+ Truthiness::Ambiguous
+ }
  } else if subject_ty.is_disjoint_from(db, class_ty) {
  Truthiness::AlwaysFalse
  } else {

crates/ty_python_semantic/src/types/narrow.rs

@@ -3,7 +3,8 @@ use crate::semantic_index::expression::Expression;
 use crate::semantic_index::place::{PlaceExpr, PlaceTable, ScopeId, ScopedPlaceId};
 use crate::semantic_index::place_table;
 use crate::semantic_index::predicate::{
- CallableAndCallExpr, PatternPredicate, PatternPredicateKind, Predicate, PredicateNode,
+ CallableAndCallExpr, ClassPatternKind, PatternPredicate, PatternPredicateKind, Predicate,
+ PredicateNode,
 };
 use crate::types::enums::{enum_member_literals, enum_metadata};
 use crate::types::function::KnownFunction;
@@ -398,15 +399,18 @@ impl<'db, 'ast> NarrowingConstraintsBuilder<'db, 'ast> {
  &mut self,
  pattern_predicate_kind: &PatternPredicateKind<'db>,
  subject: Expression<'db>,
+ is_positive: bool,
  ) -> Option<NarrowingConstraints<'db>> {
  match pattern_predicate_kind {
  PatternPredicateKind::Singleton(singleton) => {
  self.evaluate_match_pattern_singleton(subject, *singleton)
  }
- PatternPredicateKind::Class(cls) => self.evaluate_match_pattern_class(subject, *cls),
+ PatternPredicateKind::Class(cls, kind) => {
+ self.evaluate_match_pattern_class(subject, *cls, *kind, is_positive)
+ }
  PatternPredicateKind::Value(expr) => self.evaluate_match_pattern_value(subject, *expr),
  PatternPredicateKind::Or(predicates) => {
- self.evaluate_match_pattern_or(subject, predicates)
+ self.evaluate_match_pattern_or(subject, predicates, is_positive)
  }
  PatternPredicateKind::Unsupported => None,
  }
@@ -418,7 +422,7 @@ impl<'db, 'ast> NarrowingConstraintsBuilder<'db, 'ast> {
  is_positive: bool,
  ) -> Option<NarrowingConstraints<'db>> {
  let subject = pattern.subject(self.db);
- self.evaluate_pattern_predicate_kind(pattern.kind(self.db), subject)
+ self.evaluate_pattern_predicate_kind(pattern.kind(self.db), subject, is_positive)
  .map(|mut constraints| {
  negate_if(&mut constraints, self.db, !is_positive);
  constraints
@@ -905,7 +909,16 @@ impl<'db, 'ast> NarrowingConstraintsBuilder<'db, 'ast> {
  &mut self,
  subject: Expression<'db>,
  cls: Expression<'db>,
+ kind: ClassPatternKind,
+ is_positive: bool,
  ) -> Option<NarrowingConstraints<'db>> {
+ if !kind.is_irrefutable() && !is_positive {
+ // A class pattern like `case Point(x=0, y=0)` is not irrefutable. In the positive case,
+ // we can still narrow the type of the match subject to `Point`. But in the negative case,
+ // we cannot exclude `Point` as a possibility.
+ return None;
+ }
+
  let subject = place_expr(subject.node_ref(self.db, self.module))?;
  let place = self.expect_place(&subject);
 
@@ -930,12 +943,15 @@ impl<'db, 'ast> NarrowingConstraintsBuilder<'db, 'ast> {
  &mut self,
  subject: Expression<'db>,
  predicates: &Vec<PatternPredicateKind<'db>>,
+ is_positive: bool,
  ) -> Option<NarrowingConstraints<'db>> {
  let db = self.db;
 
  predicates
  .iter()
- .filter_map(|predicate| self.evaluate_pattern_predicate_kind(predicate, subject))
+ .filter_map(|predicate| {
+ self.evaluate_pattern_predicate_kind(predicate, subject, is_positive)
+ })
  .reduce(|mut constraints, constraints_| {
  merge_constraints_or(&mut constraints, &constraints_, db);
  constraints