Type narrowing with `if None not in Sequence[Any | None]` not working as expected

[sebdivinity]

Bug Report

I expected that I could easily narrow multiple variables at once by using None not in Sequence[Any | None]. However mypy does not infer that. Nevertheless, after this condition it's impossible that variables have type None.

To Reproduce

def test(a: int|None, b: int|None) -> int:
    if None not in [a, b]:
        reveal_type(a)
        reveal_type(b)
        return a+b
    elif b is None:
        return a
    elif a is None:
        return b
    else:
        return 0

https://mypy-play.net/?mypy=latest&python=3.11&gist=40a2a733aa93c342e4ce013382949229

Expected Behavior

main.py:3: note: Revealed type is "builtins.int"
main.py:4: note: Revealed type is "builtins.int"

Actual Behavior

main.py:3: note: Revealed type is "Union[builtins.int, None]"
main.py:4: note: Revealed type is "Union[builtins.int, None]"
main.py:5: error: Unsupported operand types for + ("int" and "None") [operator]
main.py:5: error: Unsupported operand types for + ("None" and "int") [operator]
main.py:5: error: Unsupported left operand type for + ("None") [operator]
main.py:5: note: Both left and right operands are unions
main.py:7: error: Incompatible return value type (got "Optional[int]", expected "int") [return-value]

• Mypy version used: 1.1.1
• Mypy command-line flags: None
• Mypy configuration options from mypy.ini (and other config files): None
• Python version used: 3.11

[ikonst]

Generally a in b doesn't narrow a nor b (except in a special case where b is a union of TypedDicts). Is it a dup of #10977?

[sebdivinity]

Yep seems like a duplicate.

The cleanest way I've found to overcome this issue without changing the condition is with something like that.

def test(a: int|None, b: int|None) -> int:
    if None not in [a, b]:
        a = cast(int, a)
        b = cast(int, b)
        reveal_type(a)
        reveal_type(b)
        return a+b
    elif b is None:
        return a
    elif a is None:
        return b
    else:
        return 0

However, I'm not sure if this would be considered good practice. Would love to get a feedback before closing this issue.

Also, I did not quite understood why the following code in #10977 was unsafe because of invariance. Would love to get some explainations on it if possible :). There is no generic type involved so I don't get the issue here.

a: set[Optional[str]]
if None in a:
    return
reveal_type(a)

[ikonst]

set is mutable so https://mypy.readthedocs.io/en/stable/common_issues.html#invariance-vs-covariance applies.

For example:

a: set[Optional[str]]
b = a
if None in a:
    return
reveal_type(a)  # set[str]
b.add(None)
reveal_type(a)  # set[str] — but now it's a lie

[erictraut]

I did not quite understood why the code in #10977 was unsafe

When a type checker applies type narrowing, it transforms a wider type to a narrower type. By definition, the narrower type must be a subtype of the wider type. Since set[str] is not a subtype of set[str | None] (because of invariance), that means set[str | None] cannot be narrowed to set[str].

[erictraut]

It might be feasible to support type narrowing for both expressions a and b in the statement if None not in [a, b] in the positive ("if") case, but the types of both a and b in the negative ("else") case cannot be narrowed. Their types would both continue to be int | None in the negative case. So even if mypy were to implement type narrowing for this expression form, the OP's code would still produce type errors.

I recommend avoiding this coding pattern and using something like this instead. It's behaviorally the same, slightly more performant at runtime, and type checks without a problem.

def test(a: int | None, b: int | None) -> int:
    if a is None:
        if b is None:
            return 0
        return b
    if b is None:
        return a
    return a + b

[AlexWaygood]

Thanks @ikonst and @erictraut for your explanations! As has been previously stated, this seems like a duplicate of #10977, and I think all questions have been answered here, so I'm closing this now.

[sebdivinity]

Yep thanks for all the explaination ! Very instructive