(🎁) Support `TypeVar`s in the bounds of other `TypeVar`s

[KotlinIsland]

from typing import _T as T, TypeVar

L = TypeVar("L", bound=list[T])  # error: Type variable "typing._T" is unbound

def foo(l: L) -> L | T:  # error: A function returning TypeVar should receive at least one argument containing the same Typevar
    res = l[0]
    if res:
        return res
    return l

a: list[int] | list[str]

reveal_type(foo)  # "def [L <: list[T?], T] (l: L) -> L | T"
reveal_type(foo(a))  # list[int] | list[str]

Expected:

reveal_type(foo)  # "def [T, L <: list[T]] (l: L) -> L | T"
reveal_type(foo(a))  # list[int] | list[str] | int | str

Mypy should understand that T should be bound to foo from L

This is identical to generic TypeAliases:

L: TypeAlias = list[T]
a: L[int]

Here T is unbound, yet it's a valid and semantically sound expression.

Typescript example

The same idea could be represented in TypeScript as:

declare function foo<T, L extends T[]>(l: L): L | T

declare let a: number[] | string[]

let b = foo(a)

Although TS fails to infer the correct type here. (it infers as unknown)

basedmypy

This is partially supported in basedmypy

[erictraut]

This concept doesn't make sense. A TypeVar used within the bound of a TypeVar would have no defined scope. It should therefore be considered an error to use a TypeVar within a bound or constraint expression. PEP 484 isn't as clear as it could be on this point. I've attempted to remedy that omission in draft PEP 695.

[DetachHead]

how so? typescript supports it:

declare function foo<T, L extends T[]>(l: L, t: T): T

declare const a: number[]
declare const b: number

const c = foo(a, b) //inferred as foo<number, number[]>

[KotlinIsland]

@erictraut In my opinion this is identical to generic TypeAliases:

L: TypeAlias = list[T]
a: L[int]

Here T is unbound, yet it's a valid and semantically sound expression.

I've attempted to remedy that omission in draft PEP 695.

class ClassC[T: dict[str, V]]: ...  # Type checker error: generic type
# But
class ClassC[V, T: dict[str, V]]: ...  # LGTM

The second example is how I understand the example in the OP.

[AlexWaygood]

Things like this should be discussed in the python/typing issue tracker or on the typing-sig mailing list, not the mypy issue tracker. We'd need agreement on the spec before individual type checkers could start supporting this.

[KotlinIsland]

@AlexWaygood Could you transfer the issue to python/typing?

[smheidrich]

As this is basically a subset of the functionality offered by higher-kinded types/TypeVars (HKTs) requested in #548, I'm wondering if it might make sense to have this as a first step before full HKT support?

The example from the beginning

L = TypeVar("L", bound=list[T])

def foo(l: L) -> L | T: ...

would, in the suggested HKT syntax, be written as

L = TypeVar("L", bound=list[T], args=1)

def foo(l: L[T]) -> L[T] | T: ...

I think it might be confusing if both of these possibilities coexisted, so maybe the syntax for this feature could adopt the one from HKTs but put restrictions on it to limit it to non-full-HKT cases, i.e. making it forbidden to use L parametrized with anything other than T? But then again, if the entire PEP for this were to only make sense in anticipation of the subsequent HKT PEP, it might be better to skip it and go with full HKTs immediately? 🤔