Intuition: unpacking a 'tuple[int, int] | tuple[str, str]' into a new tuple should not result in 'tuple[int | str, int | str]'

[MajorDallas]

Let me preface this by saying I don't believe this behavior to be incorrect. I do think some extra precision could be had for the following situation:

    fields = (...)  # : tuple[*tuple[tuple[int, int], ...], tuple[str, str]]
    for c, a in fields:
        reveal_type(c)  # : int | str
        reveal_type(a)  # : int | str
        reveal_type((c, a))  # : tuple[int | str, int | str]
    # without unpacking
    for f in fields:
        reveal_type(f)  #  tuple[int, int] | tuple[str, str]
        reveal_type(f[0])  # : int | str
        reveal_type(f[1])  # : int | str
        reveal_type((f[0], f[1])  # : tuple[int | str, int | str]

The last reveal_type in both blocks is correct: a tuple of two unions is the tuple of those two unions--of course!

The 2nd version actually surprised me at first, though. I had expected that if the type checker knows that f is tuple[int, int] | tuple[str, str], then it should know that (f[0], f[1]) (or (c, a)) is also tuple[int, int] | tuple[str, str]. The hindsight was "how could it if both elements are int | str? Duh!"

If it could be proven that (f[0], f[1]) has the same type as f while iterating fields, then the following shouldn't be rejected:

    for c, a in fields:
        if c < a:  
        # Operator "<" not supported for types "int | str" and "int | str"
        #  Operator "<" not supported for types "int" and "str"
        #  Operator "<" not supported for types "str" and "int"
            return -1
        elif c > a:
        # Operator ">" not supported for types "int | str" and "int | str"
        #  Operator ">" not supported for types "int" and "str"
        #  Operator ">" not supported for types "str" and "int"
            return 1

It feels like the type checker has enough information to come to the same conclusion as my first intuition that c < a would be type-safe as long as each (c, a)'s type is known. But I dunno 🤷

[erictraut]

Within a type checker, the types of expressions are evaluated from inside out. That is, a subexpression's type is evaluated first, and then this type information is used to inform the containing type's expression. This mirrors the order of execution at runtime. That means the type of f[0] and f[1] are evaluated first, then the resulting types are used to evaluate the type of (f[0], f[1]). In your example above, the type of f[0] is int | str, and the type of f[1] is int | str, so it follows that the type of (f[0], f[1]) is tuple[int | str, int | str].

Static type checkers do not track conditional types between two or more expressions. For example, pyright doesn't track that the narrowed type of c is int if the type of a is also int but is str if a is str. This form of "entanglement" would be theoretically possible to track, but in practice it would explode in complexity and runtime cost for all but the simplest of examples. The type checker would also need to prove that the conditions involved in the entanglement still hold between the point where the condition is generated and the expression is subsequently used, which adds even more complexity. I'm not aware of any static type checker or compiler (in any language) that attempts to do this. It would completely destroy the performance of pyright, so it's unlikely we'd ever add such support.

[MajorDallas]

That's about what I figured, tbh. It seems like an easy thing to recognize, but proving it....

There's always # type: ignore, at least.

(Aside: I wonder if a type system supporting dependent types could represent this situation? Dependent types haven't yet made their way much passed the realm of proof assistants, unless you count Idris... Not really relevant for Python, just musing.)