unexpected `tuple[]` behavior

[jorenham]

from typing import Any, Literal, Never, overload, reveal_type

@overload
def ndim(shape: tuple[Never, ...]) -> int: ...
@overload
def ndim(shape: tuple[int]) -> Literal[1]: ...
@overload
def ndim(shape: tuple[int, int]) -> Literal[2]: ...
@overload
def ndim(shape: tuple[int, ...]) -> int: ...
def ndim(shape: tuple[int, ...]) -> int:
    return len(shape)


def demo_gradual(s: tuple[Any, ...]):
    reveal_type(ndim(s))  # Unknown     (expected: int)

def demo_one(s: tuple[int]):
    reveal_type(ndim(s))  # Literal[1]  (OK)

def demo_two(s: tuple[int, int]):
    reveal_type(ndim(s))  # Literal[2]  (OK)

def demo_variadic(s: tuple[int, ...]):
    reveal_type(ndim(s))  # int         (OK)

https://pyrefly.org/sandbox/?project=N4IgZglgNgpgziAXKOBDAdgEwEYHsAeAdAA4CeS4ATrgLYAEALqcROgOZ0Q3G6UN0BBdKQA0dADIQGMSqihiAcjABuMsblWUouVJjGUVMOQH0mxGAB10VgAIaZ23VcwwwdLFwAUcABapziIwArsSwANpKmmIAVAwh4ZFqdIQpALqpAJR0ALQAfJzoDIEphLb2WjqYzq7umF6%2B-jCBcaEwYawMmTn5ktKyUGEAjKnFKWWajlVYNR403n4Bwa3thWIdXXkSUjJyYQBMI8lj6HYTldVus-ONzfFtHWIlG-kdo6XTl3VzDYst4Q9HQjPApFKx0cF0AxxSjoOiwdDXcwZKwoj50Fw0XDGNiyTBBOTeW7LISiQGZRBgiEGVQmMwwTxXOAZLJ0ADEdAAqugANboXAAd1hELonhg%2BHMAGNpJhAh1kdY0Risbh0PS4ET-oVyZTwdSjFBTMx6YzmeD2b0dgNhuDPAB5ADS8ou6JgmNM-NwhKWmoYay1GQpQt1hlpRoZX28prZWz6uwONodTsVrqxylQlAguggEq9f3uqzJAZ1kJDBrp4fqUfZHWFtbtjqsIBEICCDGgcBI5EQIHZHLbUCkpDoYCC6ClEBVcFRLjcYF4NFQDGM6CCNGwMk8%2BFlhSymzgDEogeFUKCMOHFhAClX68PdGA%2BAAvhfG82yAYwFBSIQGLQoBR2QACqQ76fnQaBYHg%2BB0BKKqQGwp6LhO6DvOyADKMAwHQPgMAwxDqgA9Phb6uJ%2BhC8Gw%2BEwOg%2BGYLgEpwPhMHoHBCFtiq%2BHDrwdCoGm0CoNgsDQbBEDwbIbGwrgxDiR2VhkAwPgqtkmhwEhdAALx0BeADMhCDHsz7oCAD7Nqg46qAAYtAMAUOBOAEJ2RlAA

In demo_gradual I would have expected it to either

• match the first tuple[Never, ...] overload, since tuple[Any, ...] (and only tuple[Any, ...]) is assignable to tuple[Never, ...] (this matches pyright), or
• match all overloads and return the intersection of the results, which would be int in this case. This would be more in line with the typing spec.

Either way, I expected tuple[Any, ...] to result in an int.

But instead, it returns Unknown, which makes me thing that none of the overloads match.

The other three overloads are behaving correctly.

[migeed-z]

I will take a look!

[migeed-z]

I took a look. As far as the spec, it seems to me that pyrefly is right? the reason is that the spec says:

For all arguments, determine whether all possible materializations of the argument’s type are assignable to the corresponding parameter type for each of the remaining overloads. If so, eliminate all of the subsequent remaining overloads.

So we have that:

• not all materializations of tuple[Any, ...] are assignable to tuple[Never, ...]
• not all materializations of tuple[Any, ...] are assignable to tuple[int]

and so on for all 4 overloads. So we don't eliminate any of them.

Then it says that:

If the return types are not equivalent, overload matching is ambiguous. In this case, assume a return type of Any and stop.

and we have that Literal[1] is not equivalent to Literal[2], so we get any?

[jorenham]

Well, I guess I completely disagree with the spec then, because that's not at all how gradual typing is meant to be used 😅.

In this case, tuple[Any, ...] is assignable to the parameters of all 4 overloads (through materialization). Thus tuple[Any, ...] is assignable to tuple[Never, ...] | tuple[int] | tuple[int, int] | tuple[int, ...] ¹. The overloading operator distributes over the union type operator (not according to the spec _grumble, but according to type theory). So on the rhs we obtain int | Literal[1] | Literal[2] | int as return type, or equivalently, int.

The spec dictating that it should return Any in this case is not only type-unsafe (because that's what Any fundamentally is), it is unnecessary, and at odds with type theory.

Also, Any is meant to represent a type that cannot be known statically. But clearly, that's not the case here. At runtime it is clear that any of the 4 overloads could apply, and that, therefore, the any of the 4 return types could be returned. The only correct and type-safe outcome is to therefore return a union of these 4 return types ².

Anyway, since this is the upteenth time I've ranted about this, I should probably address this in the discourse. Hopefully the spec can still be saved (currently both mypy and pyright don't conform to it on this point, so I currently don't see why not, but you never know I guess).

Usually I'm all for sticking to the typing spec. But in this case it directly hurts type-safety for no good reason. And just like you shouldn't listen to a cop if they tell you do something unsafe without a good reason, I also don't think you should listen to the typing spec here.

Footnotes

1. It's a union because tuple[Any, ...] is strictly gradual. For fully static types, this would have been an intersection. ↩

2. If we would have a "gradual union" (often called the AnyOf type, see https://github.com/python/typing/issues/566), that might also have been an acceptable option here, seeing as the input is gradual. ↩

[migeed-z]

A conformance test for this exists. This is the pyright result. Definitely possible that the spec is wrong, but I would be keen to understand the implications of taking the union (why not greatest upper bound?) on the rest of the type system. That could mean further community discussion.

[jorenham]

why not greatest upper bound?

That would also be valid, but not as narrow as it could be. In this case it wouldn't matter though.

[github-actions]

This issue has someone assigned, but has not had recent activity for more than 2 weeks.

If you are still working on this issue, please add a comment so everyone knows. Otherwise, please unassign yourself and allow someone else to take over.

Thank you for your contributions!