Variance bug on TypeVar with value restriction

[JelleZijlstra]

from typing import TypeVar, Union, Generic

T1 = TypeVar("T1", int, str, covariant=True)
T2 = TypeVar("T2", int, str)

class X1(Generic[T1]):
    def f(self) -> T1: ...
class X2(Generic[T2]):
    def f(self) -> T2: ...

def f1(x: X1[int]) -> None: ...
def f2(x: X2[int]) -> None: ...

f1(X1[int]())
f1(X1[bool]())

f2(X2[int]())
f2(X2[bool]())

https://mypy-play.net/?mypy=latest&python=3.10&gist=5a4f16dd13bd4b18a7c2323ba464f627

Mypy allows this without errors, but pyright shows an error on the last line and I think it's right: T2 is invariant, so we shouldn't allow bool there:

Argument of type "X2[bool]" cannot be assigned to parameter "x" of type "X2[int]" in function "f2"
  TypeVar "T2@X2" is invariant
    "bool" is incompatible with "int"

[sobolevn]

Thanks, @JelleZijlstra! I will take a look 🙂

Related #11378

[sobolevn]

I think the problem is in this line: T1 = TypeVar("T1", int, str, covariant=True)

When defining a type variable with exact values, we want to match these values by type exactly. So, covariant=True should be not allowed in this variable.

Related typing-sig discussion: https://mail.python.org/archives/list/[email protected]/thread/BQYZOF3DSCO3V5HHTWVSPK2PRUQPDIVL/

[erictraut]

A constrained TypeVar doesn't require an exact match. The following is perfectly legit:

T = TypeVar("T", int, str)

def func(a: T) -> T:
    return a

func(True)

The variance of a TypeVar applies only when it is used as a type parameter in a generic class, such as X1 and X2 in Jelle's example above. In that case, it must be an exact match if it's invariant but can be a subtype (such as bool) if it's covariant. In other words, there are legitimate uses for a covariant constrained TypeVar.

[erictraut]

I think mypy is doing the right thing here. It shouldn't emit an error. Jelle references an error emitted by pyright, but that was due to a bug that I have since fixed. Pyright now generates no errors for the above code, so it's in sync with mypy. I think this can be closed.