Sequence pattern in `match`/`case` with a literal element does not narrow a type out of a union

[kkom]

Describe the Bug

A match arm with a sequence pattern whose element is a literal (case "b", v) doesn't get subtracted from the union after the match. The same code with a capture (case k, v) narrows to Never correctly. (Different from the fixed #3147, which used a wildcard case (_, _).)

from typing import Literal, reveal_type

type MyUnion = Literal["a"] | tuple[Literal["b"], int] | tuple[Literal["c"], int]


def broken(value: MyUnion) -> str:  # Function declared to return `str`, but one or more paths are missing an explicit `return`
    match value:
        case "a":
            return "a"
        case "b", v:
            reveal_type(v)  # revealed type: int
            return "b"
        case "c", v:
            reveal_type(v)  # revealed type: int
            return "c"
    reveal_type(value)  # revealed type: tuple[Literal['b'], int] | tuple[Literal['c'], int]


def works(value: MyUnion) -> str:
    match value:
        case "a":
            return "a"
        case k, v:
            reveal_type(k)  # revealed type: Literal['b', 'c']
            reveal_type(v)  # revealed type: int
            return k
    reveal_type(value)  # revealed type: Never

broken is exhaustive, so value should narrow to Never like in works, and the bad-return is spurious.

pyrefly version: 1.1.1

Sandbox Link

https://pyrefly.org/sandbox/?project=N4IgZglgNgpgziAXKOBDAdgEwEYHsAeAdAA4CeS4ATrgLYAEALqcROgOZ0Q3G6UN0AZCAxiVUUADR1KMAG4xxAfSbEYAHXQaVMOgFlSAVXQRc6OgF5Bw0eIDaakKgcBdOgB9GAV2KxbQkWJQ9iDYLlKsDK4eDN6%2B-jZBDgDGYZzokRqZWDBgdNjUANYw6AAUsuKeMIh6hsamAJR0ALQAfHRwDJTVdADEdABinuhJDCZmmDBJUKgymIy40jAxlGYABh2Uq1LYnvymOrx0NLw6xKgMABZwdDM6NBBwcKwcGHQw%2BD4QScJ0qzLL6FWGjoIKO5ySFzo5SglUQwNBCKSqDgOgcTiQ8IRWMWALoaIcmKxSJReJCDiksjhZmxWJk8iU2jKjV6i3psDm2mqEUJNJxnhWpNCIB5oOJqJAKRAFKpvIRdIUUGUzBgTJBfXl4hgHOVXPSIux-35ZmSBOpII1isZ0MqzPVcgVWsYOq8PhgfmsgVsAHJsF7nOF0lEXXEPXYvUk-QGMpoYxNcgB3XgFOBlCpVGpGMaNVrtToy0E0cGQ61VfV0MWk9H52V8gX44VmonInQFaVluX2hnKkoFW2sh3a1TVeKen1eqThv3t0EWpWqVUsi2OzlpBjT81LI10AqE2dWtN9peD9MAOXtlClIDIMjAUFIhAYtCgFD6AAVSDe7%2B0MDgCOXTJAbD8ucYyEBofQAMowDoFwMAwxBwIgAD0SHXjkd6ELwbBIcUSGYLgSRwEhSQARAQFiKMphIXQYCHKg5TQKg2CwP%2B6CAcBlFmLgxCcXAYHoGQlymE08iUE8pgWKSADMhAAIwAEymrYojUGJzgaEMXA8HwWpNJgEAyCMEDyJJXpkegJxehoFkME0MgAI6eAZulFKQTSoEkSTwNclhevGMzoFZ6AgAAvhIjhGfI-TQDAFBoFgeBEGQoVAA

(Only applicable for extension issues) IDE Information

No response

[yangdanny97]

Yeah I think we can consider variable bindings similarly to wildcards w.r.t narrowing the match subject

"b", v should generate 2 conditions: the tuple has 2 elements + the first element is b

[markselby9]

Took a shot at this in #3967, following your suggestion (treat variable bindings like wildcards; let the literal element contribute its condition). The fix strips the spurious Placeholder that blocked negative narrowing for star-free patterns whose elements are all irrefutable/value/singleton — soundness stays gated on the type-directed facet narrowing, so ("b", _) against tuple[str, int] is still preserved. Full lib suite green.