Type checking fails to distribute across Tuple types

[bcmills]

Bug Report

Union types fail to distribute across Tuple types as they ought to when the set of concrete values of each type are identical.

To Reproduce

(https://mypy-play.net/?mypy=latest&python=3.12&gist=9d0052b0ed30856e5ad3985237f8754b)

from typing import Union, Tuple, Optional

def id(x: Tuple[float, Optional[float]]) -> Union[Tuple[float, float], Tuple[float, None]]:
    return x

Expected Behavior

Values of type Tuple[float, Optional[float]] and Union[Tuple[float, float], Tuple[float, None]] should be mutually compatible.

That is: Union ought to distribute across Tuple.

Actual Behavior

main.py:4: error: Incompatible return value type (got "tuple[float, float | None]", expected "tuple[float, float] | tuple[float, None]")  [return-value]

Your Environment

(See Playground link.)

• Python version used: 3.12

[VallinZ]

Is this a bug that need a fix? If so, can I work on this?

[A5rocks]

Yes this is a bug that needs a fix, but it probably touches some decently complicated subtyping rules so it's probably not the best first contribution :^)

Feel free to work on it though.

[A5rocks]

To follow up on this, this is actually in the typing spec! See https://typing.python.org/en/latest/spec/tuples.html#type-compatibility-rules

[VallinZ]

Thank you for proving more information!

[VallinZ]

Hi, I tried working on this bug and I think I successful catch the example mention in the bug report, but my implementation leads to a maximum recursive depth error for recursive data types. Can anyone take a look and see whether this implementation is on the correct idea or is totally off? I didn't want to PR to the mypy repo broken code, so I just provided a link to a PR in my fork repo with the current issue: VallinZ#4

[A5rocks]

I think eagerly expanding tuples of unions as you do is probably a bad idea. I haven't thought too much about it (and my first instinct was IMO wrong), but I think you could add a special case next to the current exhaustive enum/bool one which:

1. narrows the rhs union to just things with the same length as lhs
2. for every item + position in lhs, check that type is a subtype of the union of items at that position in each rhs tuple.

(I haven't really played through this in my head so I can't say whether that's totally correct logic or not. Hopefully it at least gives an idea!)

However, when I asked a few days ago people recommended that maybe normalizing (like you did) is a good idea, so... well, I don't know the specific reason you're running into issues with recursive types either.

[A5rocks]

Nevermind that approach is wrong. Sorry, I don't know if there's a better way to implement this than what you have.

(maybe avoiding creating all the tuples up front is possible? Left isn't in right and left is a tuple and right is a union, then you could split left on the first union element it has -- so that e.g. tuple[str, int | str, int | str] becomes tuple[str, int, int | str] | tuple[str, str, int | str], which you can then toss back into subtyping. I suspect there's something not good about being eager about things in face of recursive types.)

[VallinZ]

Got it, thank you for providing feedback! I'll look into the approach you suggested.

[jorenham]

If we assume that the Python union type is equivalent to the sum type (disjoint/tagged union type), and the tuple equivalent to the product type (which are both linear), then the distributive property indeed hold.

But I'm not sure if this is still the case if we consider the Python union as a "regular", non-disjoint union type 🤔.

See https://wikipedia.org/wiki/Type_system#Specialized_type_systems for their definitions.

Either way, the @overload spec seems to assume that Python's union type is distributive over overloads (an intersection type in disguise). So I see no reason not to also apply to tuples then 🤷🏻