Subtract a union member matched by a literal sequence-pattern element

pyrefly/lib/binding/pattern.rs

@@ -234,6 +234,20 @@ impl<'a> BindingsBuilder<'a> {
                     .patterns
                     .iter()
                     .all(|p| p.is_irrefutable() || p.is_wildcard());
+                // Strip the spurious Placeholders that `and_all` adds for sub-patterns with
+                // no narrow ops, so negative narrowing can subtract a matched member. Safe
+                // for a star-free pattern whose elements are all irrefutable (wildcards,
+                // captures) or value / singleton patterns: those emit `Eq`/`Is` facet
+                // narrows whose negation removes a union member only when the element type
+                // guarantees the match, so refutable members are preserved.
+                // https://github.com/facebook/pyrefly/issues/3883
+                let strip_placeholders = all_subpatterns_irrefutable
+                    || (num_patterns == num_non_star_patterns
+                        && x.patterns.iter().all(|p| {
+                            p.is_irrefutable()
+                                || p.is_wildcard()
+                                || matches!(p, Pattern::MatchValue(_) | Pattern::MatchSingleton(_))
+                        }));
                 let mut subject_idx = subject_idx;
                 let synthesized_len = Expr::NumberLiteral(ExprNumberLiteral {
                     node_index: AtomicNodeIndex::default(),
@@ -377,7 +391,7 @@ impl<'a> BindingsBuilder<'a> {
                     KeyExpect::UnpackedLength(x.range),
                     BindingExpect::UnpackedLength(subject_idx, x.range, expect),
                 );
-                if all_subpatterns_irrefutable
+                if strip_placeholders
                     && let Some(subject) = match_subject.as_single()
                     && let Some((op, _)) = narrow_ops.scope.0.get_mut(subject.name())
                 {

pyrefly/lib/test/pattern_match.rs

@@ -306,6 +306,71 @@ def f(value: float | tuple[float, float]) -> float | tuple[float, float]:
 "#,
 );
 
+testcase!(
+    // https://github.com/facebook/pyrefly/issues/3883: a sequence pattern whose
+    // element is a literal matching the member's element type exactly (e.g.
+    // `("b", _)` against `tuple[Literal["b"], int]`) is irrefutable for that
+    // member, so the member is subtracted from the subject union.
+    test_match_sequence_literal_element_narrows_out_of_union,
+    r#"
+from typing import Literal, assert_never
+
+def f(
+    value: Literal["a"] | tuple[Literal["b"], int] | tuple[Literal["c"], int],
+) -> None:
+    match value:
+        case "a":
+            pass
+        case ("b", _):
+            pass
+        case ("c", _):
+            pass
+        case _ as unreachable:
+            assert_never(unreachable)
+"#,
+);
+
+testcase!(
+    // A capture after the literal element is irrefutable for that element, so the
+    // member is still subtracted (the maintainer's "treat bindings like wildcards"
+    // case). https://github.com/facebook/pyrefly/issues/3883
+    test_match_sequence_literal_element_with_capture_narrows,
+    r#"
+from typing import Literal, assert_never
+
+def f(
+    value: Literal["a"] | tuple[Literal["b"], int] | tuple[Literal["c"], int],
+) -> int:
+    match value:
+        case "a":
+            return 0
+        case ("b", v):
+            return v
+        case ("c", v):
+            return v
+        case _ as unreachable:
+            assert_never(unreachable)
+"#,
+);
+
+testcase!(
+    // The literal element only subtracts a member when the element type guarantees
+    // the match. Against a wider element type (`str`), `("b", _)` is refutable, so
+    // the type must be preserved.
+    test_match_sequence_literal_element_wider_type_no_strip,
+    r#"
+from typing import assert_type
+
+def f(value: tuple[str, int]) -> tuple[str, int]:
+    match value:
+        case ("b", _):
+            return value
+        case other:
+            assert_type(other, tuple[str, int])
+            return other
+"#,
+);
+
 testcase!(
     test_match_exhaustive_call_subject_assert_never,
     r#"