Should type checkers trust assert statements with mutable values?

[randolf-scholz]

I tested the example below with multiple type checkers, and they all predict Never rather than Literal[False] after the last assert statement. But this is incorrect at runtime.

from typing import reveal_type

class Foo:
    def __init__(self) -> None:
        self.requires_fit: bool = True
    
    def fit(self) -> None:
        self.requires_fit = False

def test_foo() -> None:
    foo = Foo()
    reveal_type(foo.requires_fit)  # bool ✅️
    
    assert foo.requires_fit
    reveal_type(foo.requires_fit)  # Literal[True]
    
    foo.fit() # mutates requires_fit
    
    assert not foo.requires_fit
    reveal_type(foo.requires_fit)  # E: Literal[False], got Never (runtime: False)

The current behavior only seems valid assuming immutability (e.g. a @property without setter, Final, tuple member, frozen dataclass member, etc.). So, I believe in general type-checkers are incorrect here and should trust the assert.

I would like to hear what other people think before opening an issue with a spec proposal.

[hauntsaninja]

Narrowing is currently not specified at all. The focus of the spec has been on the semantics of annotations, since that is important for ecosystem compatibility across type checkers.

I would recommend working with a type checker to add (a mode for) sounder narrowing — in general it is hard to do that and still be usable, given aliasing and interior mutability

[carljm]

This issue is not limited to assert statements; it applies to all narrowing of attributes or subscripts on mutable types. E.g. if foo.requires_fit: also triggers narrowing in type checkers and is similarly unsound.

The problem here is that so many objects in Python are mutable by default, and so many things can potentially trigger code execution and possible mutation, that disallowing all such narrowing on that basis is too aggressive, rules out too many programs that are actually fine, and makes the type system very difficult to use in practice. (Pyre tried implementing sound-narrowing-only a number of years ago, and that was the result.) It seems like to do better here, we would need something like an effects system so that type checkers could actually track the possibility of mutation more precisely.