Type inconsistently and insufficiently refined

Bug Report

Through a if/elif (with multiple elif) construct using isinstance in conditional, I was expecting the type of the variable checked to be refined in the branches.

To Reproduce

from typing import Any, Union
class A: ...
class B: ...
class C: ...

def _binary_operation(left: C, right: Union[A, B]) -> Any: ...

ALL = Union[A, B, C]
def commutative_binary_operation(left: ALL, right: ALL) -> Any:
    # Handling of a corner case.
    if isinstance(left, C) and isinstance(right, C):
        ...
    elif isinstance(left, C):
        reveal_type(right)
        return _binary_operation(left, right)
    elif isinstance(right, C):
        reveal_type(left)
        return _binary_operation(right, left)

    # Treatment of other combination of types.
    ...

$ mypy test_issue.py

Expected Behavior

I was expecting mypy to raise no error, because I was expecting the type of right to be Union[test_issue.A, test_issue.B] at line 15 (and respectively, of left at line 18).

Actual Behavior

Here is the result of running mypy on the example above:

$ mypy test_issue.py
test_issue.py:15: note: Revealed type is 'Union[test_issue.A, test_issue.B, test_issue.C]'
test_issue.py:16: error: Argument 2 to "_binary_operation" has incompatible type "Union[A, B, C]"; expected "Union[A, B]"
test_issue.py:18: note: Revealed type is 'Union[test_issue.A, test_issue.B]'

Strangely, it seems that the second branch refines the type of left properly...

Your Environment

• Mypy version used: mypy 0.812
• Mypy command-line flags: None
• Mypy configuration options from mypy.ini (and other config files): None
• Python version used: Python 3.8.5
• Operating system and version: NixOS unstable

Führe zunächst das bereitgestellte Python-Snippet mit mypy 0.812 aus und vergleiche die in den beiden elif-Zweigen aufgedeckten Typen. Verfolge das für die inkonsistenten Ergebnisse verantwortliche Verhalten bei der Typ-Eingrenzung durch Bedingungen und überprüfe anschließend, dass die reproduzierten Aufrufe akzeptiert werden und die aufgedeckten Typen den erwarteten Vereinigungen entsprechen.