Unsoundness involving Literals and bounded type vars

[hauntsaninja]

Describe the bug

Inferring literals when TypeVars have bounds may not be sound.

To Reproduce

from typing import Any, Iterable, List, Literal, Protocol, TypeVar

_T = TypeVar("_T")
_T_co = TypeVar("_T_co", covariant=True)
_T_contra = TypeVar("_T_contra", contravariant=True)

class SupportsAdd(Protocol[_T_contra, _T_co]):
    def __add__(self, __x: _T_contra) -> _T_co: ...

_SupportsSumSimple = TypeVar("_SupportsSumSimple", bound=SupportsAdd[Any, Any])

def my_sum(__iterable: Iterable[_SupportsSumSimple]) -> _SupportsSumSimple:
    vs = list(__iterable)
    assert vs
    r = vs[0]
    for v in vs[1:]:
        r += v
    return r

class SupportsRAdd(Protocol[_T_contra, _T_co]):
    def __radd__(self, __x: _T_contra) -> _T_co: ...

class _SupportsSumWithNoDefaultGiven(SupportsAdd[Any, Any], SupportsRAdd[int, Any], Protocol): ...

_SupportsSumNoDefaultT = TypeVar("_SupportsSumNoDefaultT", bound=_SupportsSumWithNoDefaultGiven)

def life_like_sum(__iterable: Iterable[_SupportsSumNoDefaultT]) -> _SupportsSumNoDefaultT | Literal[0]: ...

Z2 = Literal[0, 1]

def f() -> None:
    l: List[Z2] = [0, 1, 1]
    reveal_type(my_sum(l))
    reveal_type(life_like_sum(l))

pyright gives me:

pyright 1.1.277
/Users/shantanu/dev/mypy/lit.py
  /Users/shantanu/dev/mypy/lit.py:33:17 - information: Type of "my_sum(l)" is "Literal[0, 1]"
  /Users/shantanu/dev/mypy/lit.py:34:17 - information: Type of "life_like_sum(l)" is "Literal[0, 1]"

When obviously the value is 2.
Note that mypy matches pyright's (unsound) behaviour.

This was originally filed on typeshed, but only came to my attention recently:
python/typeshed#8230
This was worked around for builtins.sum in python/typeshed#8231 , but there's clearly a more general problem here.

[erictraut]

This is an ambiguity in the type system. Both pyright and mypy use heuristics to determine whether to preserve literals within the constraint solver. I've spent a lot of time tuning these heuristics so they produce the right results the vast majority of the time, but there will inevitably be cases where the heuristic fails. This is one of those cases.

I don't see a way fix this case without breaking many more common cases.

If you feel strongly about this case or think that it's potentially more common than I'm assuming, we could discuss the issue in python/typing to see if someone has a general solution.