Question about length-based tuple type narrowing

[evfinkn]

I encountered this surprising behavior:

def example1(nums: tuple[int, ...]):
    if len(nums) == 0 or len(nums) > 1:
        return
    reveal_type(nums)  # Type of "nums" is "tuple[()] | tuple[int]"

def example2(nums: tuple[int, ...]):
    if len(nums) <= 0 or len(nums) > 1:
        return
    reveal_type(nums)  # Type of "nums" is "tuple[int]"

Tuples can't have negative length, so I would expect len(nums) == 0 and lens(nums) <= 0 to be equivalent, making tuple[int] the revealed type in example1 like in example2. At first, I thought that maybe Pyright doesn't make any assumptions about the range of values len returns, but it correctly identifies that the if len(nums) < 0 branch is unreachable:

def example3(nums: tuple[int, ...]):
    if len(nums) < 0:
        return  # Type analysis indicates code is unreachable
    elif len(nums) == 0 or len(nums) > 1:
        return
    reveal_type(nums)  # Type of "nums" is "tuple[()] | tuple[int]"

Is this intended?

[evfinkn]

As an aside, I would also expect example3 to narrow nums to tuple[int] like in example2 since they have the same length checks. The same goes for the following:

def example4(nums: tuple[int, ...]):
    if len(nums) < 0 or len(nums) == 0 or len(nums) > 1:
        return
    reveal_type(nums)  # Type of "nums" is "tuple[()] | tuple[int]"

But that might be a separate issue.

[erictraut]

Is this intended?

No, this looks like a bug. Thanks for reporting it. I'll create a bug report from this discussion.

[erictraut]

Here's a link to the issue: #9031