Unexpected failure of union type to unify with generic type with value restriction

[bwo]

gist link

code:

from typing import TypeVar


class A:
    pass


class B:
    pass


class C:
    pass


T = TypeVar("T", A, B, C)


def foo(o: T) -> None:
    assert False


def bar(o: A | B) -> None:
    return foo(o)

This fails: main.py:24: error: Value of type variable "T" of "foo" cannot be "A | B" [type-var]

In this case, where there is exactly one parameter with type T, I would expect it to succeed: in the call foo(o), with o: A | B, o must be either A (which is part of T's range), or B (likewise).

I understand that this would also fail and should fail:

def foo2(a: T, b: T) -> None:
    assert False

def bar2(a: A | B, b: A | B) -> None:
    return foo2(a, b)

Because a could be A and b could be B, which would violate the restriction in foo2 that they be the same type (whatever type they might be). But with foo as written, no such mischief can arise.

[A5rocks]

This is intentional; A | B is a super type of A and B, not necessarily one of them. I can't think of a counterexample with instances, so I think this is only matters because structural typing (?). With literals try A = Literal[1, 2] and B = Literal[3, 4], then passing x: Literal[1, 4] to bar.

[bwo]

tbh that doesn't make much sense to me either. Suppose you've got this (I realize the first is not the exact scenario you described):

S = TypeVar("S", Literal[1, 2], Literal[3, 4])

def baz(o: S) -> None:
    assert False
        
def quux(o: Literal[1, 2] | Literal[3, 4]) -> None:
    baz(o)

def spam(o: Literal[1, 4]) -> None:
    baz(o)

This fails with the error error: Value of type variable "S" of "baz" cannot be "Literal[1, 2, 3, 4]" [type-var] (and likewise for spam, with the error being that S cannot be Literal[1, 4]). But saying that s: S means that s can take on this range of values: 1, 2, 3, 4. This would again be significant with two arguments, because you might then meaningfully say that either they're both in (1, 2) or they're both in (3, 4) but you will never have one be 1 and the other be 4. But with one argument, then yes, Literal[1, 2, 3, 4] (or Literal[1, 4]) is not a subtype of either Literal[1, 2] or Literal[3, 4], but any value of those types is guaranteed to be within the range, as can be seen by the fact that this version typechecks fine:

        
S = TypeVar("S", Literal[1, 2], Literal[3, 4])

def baz(o: S) -> None:
    assert False
        
def quux(o: Literal[1, 2] | Literal[3, 4]) -> None:
    match o:
        case 1:
            return baz(o)
        case 2:
            return baz(o)
        case 3:
            return baz(o)
        case 4:
            return baz(o)
        case _:
            assert_never(o)
            
def spam(o: Literal[1, 4]) -> None:
    match o:
        case 1:
            return baz(o)
        case 4:
            return baz(o)
        case _:
            assert_never(o)

(likewise the original bar works with isinstance checks). This is just mechanically duplicating the code for the ranges of (types of) values it might take on. This even works with multiple arguments so long as both are properly derived from o, so that for instance this works:

T = TypeVar("T", A, B, C)


def foo(o: T, t: type[T]) -> None:
    assert False


def bar(o: A | B) -> None:
    if isinstance(o, A):
        return foo(o, type(o))
    elif isinstance(o, B):
        return foo(o, type(o))
    else:
        assert_never(o)
       

In fact it makes perfect sense that these would work out similarly, because when I have x: Literal[1, 4] as a value I wish to assign to a variable of type S, that's really no different from saying that I have an x: Literal[1] | Literal[4], and just as my o: A | B is either an A (hence it is one of the types a T can be, or a B (hence again one of the types a T can be), my x is either a 1 (hence one of the types an S can be), or a 4 (hence the other).

I certainly agree that Literal[1] | Literal[4] is not a subtype of either Literal[1,2] or of Literal[3,4]. But I think that it's not out of the question to ask mypy to do this analysis: each of the types it could be is a subtype of one or the other, and since there is only one value of the type in play no weird nonsense of the str + bytes stuff can happen.

[A5rocks]

OK I see I actually agree with you now, I didn't think through this enough. But:

1. there's no sense in special casing support for typevars which are used once. Literally don't use a typevar!
2. this would break how return types are done (which is another way in which using the typevar twice means this isn't valid):

from typing import Literal, Sequence, TypeVar

class A: ...
class B: ...
class C(A, B): ...

T = TypeVar("T", A, B)

def f(x: T) -> T:
    return x

def try_things(a: A, b: B, ab: A | B, c: C) -> None:
    reveal_type(f(a))  # N: Revealed type is "__main__.A"
    reveal_type(f(b))  # N: Revealed type is "__main__.B"
    reveal_type(f(ab))  # E: Value of type variable "T" of "f" cannot be "A | B"  \
                        # N: Revealed type is "Union[__main__.A, __main__.B]"
    reveal_type(f(c))  # N: Revealed type is "__main__.A"