Curriocity about weird type inference

[martinkozle]

Why does adding a tuple isinstance check, which I would guess should have no effect here, change the inferred type so much?

Code sample 1 in pyright playground

def f(a):
    if a == "str123":
        return a
    elif isinstance(a, int):
        return a
    return None


b = f(3)
reveal_type(b)

Output:

Type of "b" is "int | Literal['str123'] | None"

Code sample 2 in pyright playground

def f(a):
    if a == "str123":
        return a
    elif isinstance(a, int):
        return a
    elif isinstance(a, tuple):
        return a
    return None


b = f(3)
reveal_type(b)

Output:

Type of "b" is "Literal[3] | None"

[martinkozle]

To simplify the case a little bit:

Code sample 3 in pyright playground

def f(a):
    if isinstance(a, int):
        return a
    return None


b = f(3)
reveal_type(b)

Output:

Type of "b" is "int | None"

Code sample 4 in pyright playground

def f(a):
    if isinstance(a, int):
        return a
    elif isinstance(a, tuple):
        return a
    return None


b = f(3)
reveal_type(b)

Output:

Type of "b" is "Literal[3] | None"

Why does adding an isinstance tuple check narrow the type of the other branch?

[erictraut]

In your first example, pyright is able to infer the return type unambiguously. It's always int | None. In the second example, pyright first attempts to use its normal return type inference, which produces the answer int | tuple[Unknown, ...] | None. If the initial attempt produces a result with an Unknown, pyright then tries to use a more sophisticated technique called call-site return type inferences. This technique is limited to small and simple functions with unannotated parameters. It effectively re-analyzes the entire function using parameter types that are derived from the argument types. In your example, you're passing a value of 3, so it analyzes the function as though parameter a has type Literal[3]. This produces the result Literal[3] | None.

[martinkozle]

I didn't know that pyright first tries one algorithm and then falls back to another if the first inference isn't complete. Thank you for the explanation. The behavior makes sense now!
Although, now I have a follow up question of why the second method isn't always used if it narrows the type more accurately?