[ty] Fix narrowing and reachability of class patterns with arguments

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