Entangle types from tuple unions

[Cutipus]

I've noticed that Pyright doesn't narrow the type of a value based on the type of values "connected" to it.
In the following examples, Pyright could theoretically narrow the types further by noticing the types of the tuple elements are correlated/entangled.
I would love to see this added!

Examples rely on the following function

def example(x: bool) -> tuple[str, int] | tuple[int, None]:
    if x:
        return 'hello', 2
    else:
        return 0, None

Example 1

Pyright doesn't infer that b's type can only be int, despite a being narrowed to str which implies b must be type int.

def main():
    a, b = example(True)
    if isinstance(a, int):
        return
    #assert isinstance(b, int)  # redundant, but solves the issue
    reveal_type(b)  # Type of "b" is "int | None"

Example 2

Pyright says foo's type can be tuple[int, None] despite the previous check proving the first element can't be int.

def main():
    foo = example(True)
    if isinstance(foo[0], int):
        return
    reveal_type(foo)  # Type of "foo" is "tuple[str, int] | tuple[int, None]"

Example 3

Interestingly this works.

def main():
    match example(True):
        case int(a), b:
            reveal_type(b)  # Type of "b" is "None"
        case str(a), b:
            reveal_type(b)  # Type of "b" is "int"

[erictraut]

Pyright does a limited form of this in match statements, as you see above. To my knowledge, no other type checker does even that.

In general, entanglements between variables is problematic for performance reasons. It creates dependencies (often false dependencies) that greatly increase the time it takes for type evaluations to converge. This can cause analysis times for a function (especially one that has a loop) to increase a hundredfold. I was able to mitigate this performance impact in the case of a match statement, but I don't see a way to mitigate it in the general type guard case. For that reason, example 1 is something we'd be unlikely to implement. It wouldn't be a good tradeoff for pyright and pylance users.

I think example 2 would be possible to implement without a significant performance hit, but it would be quite a bit of work to implement. It's something I'd consider adding in the future — but only if there's a strong signal from pyright users that it's a common pattern.

[Cutipus]

I see! Thank you for the consideration.
For the sake of completeness, I checked other typecheckers and it seems like they don't implement it at all. I also checked how typescript handles it, and they properly handle analogue for example 2, but not for example 1. Without a reference for any other successful implementations, it seems like a tall ask.

Guess it's my hint to use match/case more often.