Incorrect type narrowing via isinstance after temporary type narrowing on initial object

[DerBiasto]

Describe the Bug

I have a function in which I pass some object with an attribute x of class A. A.x has type int | None. A has a subclass B which narrows the type of B.x to just int.

I can use an isinstance(o, B) check to narrow o.x to int.

However after checking if o.x where o is not narrowed to B, the instance check fails to apply any further narrowing, regardless of what was done with the if o.x check.

Checking if o.x while o is narrowed to B has no such effect.

This snippet illustrates the problem:

from typing import reveal_type
import dataclasses


@dataclasses.dataclass(frozen=True)
class A:
    x: int | None
    y: int


@dataclasses.dataclass(frozen=True)
class B(A):
    x: int
    y: int | None


def foo(o: A):
    reveal_type(o.x)  # int | None <- correct
    bar(o.x)  # error <- correct
    if isinstance(o, B):
        reveal_type(o.x)  # int <- correct
        bar(o.x)  # no error <- correct

        if o.x: pass

        reveal_type(o.x)  # int <- correct
        bar(o.x)  # no error <- correct
    
    if o.x: pass

    reveal_type(o.x)  # int | None <- correct
    bar(o.x)  # error <- correct

    if isinstance(o, B):
        reveal_type(o.x)  # int | None <- incorrect. correct: int
        bar(o.x)  # error <- incorrect
    
    if o.x: return

    reveal_type(o.x)  # Literal[0] | None <- correct.
    bar(o.x)  # error <- correct

    if isinstance(o, B):
        reveal_type(o.x)  # Literal[0] | None <- incorrect. correct: int
        bar(o.x)  # error <- incorrect


def bar(x: int):
    pass

The same thing happens for less narrow types in a subclass (which yields a bad-override error on definition, but still shouldn't behave like this).

def foo2(o: A):
    reveal_type(o.y)  # int <- correct
    bar(o.y)  # no error <- correct
    if isinstance(o, B):
        reveal_type(o.y)  # int | None <- correct
        bar(o.y)  # error <- correct

        if o.y: pass
        
        reveal_type(o.y)  # int | None <- correct
        bar(o.y)  # error <- correct
    
    if o.y: pass

    if isinstance(o, B):
        reveal_type(o.y)  # int <- incorrect. correct: int | None
        bar(o.y)  # no error <- incorrect
    
    if o.y: return

    reveal_type(o.y)  # Literal[0] <- correct.
    bar(o.y)  # no error <- correct

    if isinstance(o, B):
        reveal_type(o.y)  # Literal[0] <- incorrect. correct: Literal[0] | None
        bar(o.y)  # no error <- incorrect

I first encountered this bug with pyrefly 1.2.0, but I confirmed that is still occurs with 1.3.1.

Sandbox Link

https://pyrefly.org/sandbox/?project=v2.tVZNT8MwDP0rlnpokaBBcKvgsP0C7ohDBdXYpUHtQBu_HidO0nyzruttyhy_2H7PfTNWprNn_C3QSYXaGu3G2vyuMN1v1z-LceBsSIcb1cxjg4PU_KajkzyanXFbbTSBKamdzQAYnXFe8QbMFau-itfHG4DCugdPd7jIBjExxad2MGFyukGEKzJ-C1tXXnE4P4uP1fMI3BSKoBjZKHavBCeCTI0B3FUbuaSVE-C-VwlrndniR_IR5lasYlqPuZqVTXi9fwtLr9esPQq8uAVaNyKO5KXfoYdvKeshI61Tknz0BPo_Sbw5_ZigEuTzUf-VFi4TKlefrgjtkc5AL-lDmgnOBs5NIy0LfGFOFpTKYmdCDxkCXFq6CxrrQCCaWY0I3UABL3QA6sOKUGgjdt_ottEeYMEFGu0OPg-Hr7FhTF_nw451Pfvg7yNzbjDU1QDtT7uXHt5NB1y6lxHTxm3I41k2pCQXUuZMSCk8CEZkfcUf

(Only applicable for extension issues) IDE Information

No response

[randolf-scholz]

    if o.x: return

    reveal_type(o.x)  # Literal[0] | None <- correct.

This seems incorrect as well. For example, o.x could be a subtype of int, but Literal[0] must be the integer 0 itself, and not a subtype of int.