Optional types not fully narrowed with multiple conditionals

Bug Report

Mypy does not fully narrow optional types when multiple conditionals are involved. I suspect this is because it is not able to make an inference step when performing type narrowing. e.g., below, you have facts ~ (x is None and y is None) and x is None on line 6, which allows you to narrow y: int | None to y: int. y: None can't happen, because y is None -> ~ x is None -> contradiction given the above facts.

To Reproduce

def f(x: int | None, y: int | None) -> int:
    if x is None and y is None:
        return 0
    if x is None:
        # y guaranteed non-null
        reveal_type(y) # int | None, but should be int
        return y + 1

Expected Behavior

mypy should narrow y to int.

Actual Behavior

mypy is not able to narrow y from int | None, and gives a false positive error:

sandbox.py:5: note: Revealed type is "Union[builtins.int, None]"
sandbox.py:6: error: Unsupported operand types for + ("None" and "int")  [operator]
sandbox.py:6: note: Left operand is of type "int | None"

Your Environment

• Mypy version used: 1.7.0
• Mypy command-line flags: none
• Mypy configuration options from mypy.ini (and other config files): none
• Python version used: 3.12.0

Reproduce the example in sandbox.py with mypy 1.7.0, Python 3.12, and no configuration flags, then trace the type-narrowing behavior for the multiple conditionals. The work is done when y is revealed as int and the return passes without the reported unsupported-operand error.