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

[markselby9]

Summary

Closes #3883.

A match arm whose sequence pattern has a literal element — e.g. case ("b", _) against the union member tuple[Literal["b"], int] — is irrefutable for that member, but the member was not subtracted from the subject in the fall-through / exhaustiveness branch. A full-capture pattern (case (k, v)) did subtract correctly. So this match left a non-Never remainder when it should have been exhaustive:

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)  # was: error, `tuple[...] | tuple[...]` not `Never`

Root cause

The MatchSequence arm already emits the right scope narrow — And(IsSequence, LenEq(n), <element narrows>), where a value element contributes an Eq(v) narrow on the element facet Index(i). But NarrowOps::and_all appends an AtomicNarrowOp::Placeholder for the subject whenever a sub-pattern contributes no narrow, which is exactly what an irrefutable element like _ does. Negating And(..., Placeholder) gives Or(..., Placeholder), and Placeholder narrows to the full type — so the union re-includes the member and nothing is subtracted. Placeholders were only stripped when every element was irrefutable, which a literal element defeats.

Fix

Strip the placeholders for any star-free sequence pattern whose elements are all irrefutable, value, or singleton patterns (this is the maintainer's suggestion on the issue: treat variable bindings like wildcards, and let the literal element contribute its condition).

This is sound because the subtraction is gated by the type-directed facet narrowing (atomic_narrow_for_facet's NotEq/IsNot arms), which removes a union member only when the element type guarantees the match (exact literal/singleton) and preserves it otherwise:

• ("b", _) vs tuple[Literal["b"], int] → subtracted ✓
• ("b", _) vs tuple[str, int] (wider) → preserved ✓
• (1.0, 2.0) vs tuple[float, float] → preserved ✓ (unchanged)

Star patterns are excluded (post-star elements get no facet subject), and nested/OR/class sub-patterns fall to the existing conservative path — no behavior change there. Guarded arms (case ("b", _) if cond:) still don't subtract, because the guard re-introduces a placeholder.

Test plan

• New tests in pyrefly/lib/test/pattern_match.rs:
  • test_match_sequence_literal_element_narrows_out_of_union — the issue repro (assert_never reached)
  • test_match_sequence_literal_element_with_capture_narrows — the case ("b", v) capture form
  • test_match_sequence_literal_element_wider_type_no_strip — over-narrow guard: ("b", _) vs tuple[str, int] is preserved
• Existing test_match_sequence_refutable_subpattern_no_strip and test_match_sequence_star_pattern_narrows still pass.
• Full lib suite: cargo test -p pyrefly --lib — 5978 passed, 0 failed.
• python3 test.py --no-test --no-tensor-shapes --no-conformance --no-jsonschema — clean.

[github-actions]

According to mypy_primer, this change doesn't affect type check results on a corpus of open source code. ✅