Incorrect tuple type narrowing with len (not an else case)

[evtn]

Note: I've seen #9031, this is very similar, but also very different

Describe the bug
len() on tuple[T, ...] triggers some weird typeguard-like narrowing even outside the condition, where narrowing shouldn't happen at all

Code or Screenshots

def test(*b):
    if len(b) > 1:
        pass # notice that this is not a return, so next line is not an else case
    
    b[0] # error: Index 0 is out of range for type tuple[()]


def other_test(*b):
    b[0] # no error

VS Code extension or command-line
CLI, 1.1.391

[erictraut]

Pyright is working as intended here. The len(b) > 1 narrows the type of tuple[Unknown, ...] to tuple[Unknown, *tuple[Unknown, ...]] in the positive case and tuple[()] in the negative case. The merge is the union of these two types, and b[0] is not allowed for tuple[()].

[evtn]

But there's no negative case here, the line with an error is always hit

So there shouldn't be any narrowing

[erictraut]

There's always a positive and negative case. Here the negative case (the "not taken") is implied rather than explicit.

You can see this must be the case if you were to replace the pass statement with a return statement. The negative ("implied else") narrowing is the only type that survives in that case. Since your example uses a pass statement, both the positive ("if") and negative ("implied else") narrowed types are merged at the end of the if block.

[evtn]

This sounds more like a technical detail rather than one coming from reasoning.

The fact is, the if statement here has no effect on the code after, so I think pyright should either just revert its narrowing to a more wide one when leaving 'if' statement, or merge types back without losing information

I guess the merging that is done now is technically correct, but it results in a type that is not special-cased for indices as tuple[[Unknown], ...] is

I also see that adding a if len(b) == 0: return does help with the issue, but a less verbose and widely used if not b: return does not.