False positive unreachable code hint for base case when matching on variables, coerced to Literal annotation

[ekorchmar]

Describe the bug When explicitly declaring an typing.Any variable (which, since we are talking about Python, is ANY variable) as an enum of typing.Literal values, exhaustive pattern matching with "_" will be reported as unreachable code. This is wrong, as demonstrated in the code example below.

At least one of two things are expected to happen, or probably both:

1. A warning on line 11 when "coercing" Any to a Literal type without any assertions.
2. Detection of "dirty" Literal types stated by developer, not inferred statically, and raising warnings on non-exhaustive match statements, rather than hints on exhaustive ones.

In any case, current behavior is wrong, as declared Literal values enumerations should not be relied upon, and exhaustively handling a base case (if only to raise an Exception) is a good practice.

Code or Screenshots

from typing import Literal, Any

# Declare something of type Any to be type Literal
something: Any = 'blueberry'
fruit: Literal['apple', 'banana', 'cherry'] = something

# Match structurally
match fruit:
    case 'apple':
        print('You entered an apple')
    case 'banana':
        print('You entered a banana')
    case 'cherry':
        print('You entered a cherry')
    case _:  # But we are still Any!
        print('You entered something else')

This code successfully prints "You entered something else".

This, of course, may happen more subtly, as, for example, when parsing inputs from external APIs or users.

Developer may be tricked into removing exhaustive matching pattern and not handling a base case; thus, causing a security issue by not terminating early on malformed input, and everyone will have a bad day.

VS Code extension or command-line Using LSP version 1.1.378 in Neovim.

[erictraut]

Pyright is working as designed here, so I don't consider this a bug.

You are assigning the value of something to the variable fruit. This is allowed because the type of something is Any, so it's possible that something has a value that is compatible with fruit. From that point on, pyright assumes that the value of fruit is consistent with its type definition — that is, it contains a value that is one of the three specified literal strings.

One could argue that the narrowed value of fruit should be Any & Literal["apple", "banana", "cherry"] after the assignment (where & represents an intersection type). However, the Python type system doesn't currently support intersections. Also, the behavior of narrowing on assignment isn't spelled out by the Python typing spec, so type checkers are free to do what they want here.

Changing the narrowing-on-assignment behavior to narrow the type to Any in this case would have implications that would be really bad for type checking in general. It would also really harm language server functionality like completion suggestions. This is why pyright doesn't do this. Nor do other Python type checkers like mypy. So it's unlikely we'd change this behavior as you're suggesting.