Feature proposal: Warn when narrowing to a mutable type

Feature

I often encourage people to use "immutable" types for function parameters, as a way to indicate that the passed data structures won't be mutated by the function. Of course that isn't a guarantee, but a nice indication that can make it easier to reason about code like this:

vals = [1, 2, 3]
operation(vals)
print(vals)  # What is vals here?

If operation is typed with Sequence we can usually assume that vals isn't mutated by it. However, right now it wouldn't be a type error for operation to be implemented like this, which breaks that indication.

def operation(vals: Sequence[int]) -> None:
    assert isinstance(vals, list)
    vals += [3, 4, 5]

Here's the above example on mypy playground.

Pitch

I think it would be a valuable feature for mypy to warn when it narrows from a known immutable type such as Sequence to a known mutable type such as list.

Start with the linked mypy playground example and review how narrowing from Sequence to list is currently handled. Done means mypy can identify this narrowing from a known immutable type to a known mutable type and emit the proposed warning without changing unrelated narrowing behavior.