Widening generic types when calling methods in context.

[randolf-scholz]

I am wondering if there is a general recipe to annotate methods that return a new instance, so that it allows widening the type based on the outer context.

Question: Is it possible, in the current type system as of python 3.14, to annotate this method:

def join(dict_a, dict_b):
     return dict_a | dict_b

such that the following test passes without type errors

from typing import assert_type, reveal_type

def test(left: dict[int, int], right: dict[str, int]) -> None:
    # without outer context, the type is precise
    reveal_type(join(left, right))  # dict[int | str, int]
    assert_type(join(left, right), dict[int | str, int])
    # outer context allows widening
    x: dict[str | int, int] = join(left, right)
    y: dict[str | int | list, int] = join(left, right)
    z: dict[object, int] = join(left, right)

Context

Consider the following example:

x: dict[int, int] = {0:0, 1:0}
y: dict[str, int] = {"a":0, "b":0}
                                   # mypy | pyright | ty | pyrefly | zuban
a: dict[object, int] = x | y       # ❌️   | ❌️      | ❌️ | ❌️      | ❌️
b: dict[object, int] = {**x, **y}  # ❌️   | ✅️      | ✅️ | ✅️      | ✅️️

According to PEP 584 – Add Union Operators To dict, x | y is essentially equivalent to {**x, **y}, so the first surprise here is that the type checkers except for mypy accept one but not the other. This can be due to special casing of the literal constructor.

However, it raises the question of how to communicate to the type checker when a method returns a new instance, and widening the type is OK.

My Attempt

The best I could come up with was adding a "slack-variable" to the output, but it doesn't work. I hoped that a type checker would infer K :> object if necessary, and so allow y: dict[object, int] = join(left, right), but none of the type checkers I tested allows this. Only ty seems to partially accept this, but requires getting rid of the default K=Never and consequently emits dict[Unknown | int | str, Unknown | int on the reveal_type

from typing import Never, assert_type, reveal_type

def join[K1, V1, K2, V2, K=Never, V=Never](
    left: dict[K1, V1],
    right: dict[K2, V2],
) -> dict[K | K1 | K2, V | V1 | V2]:
    return dict(left | right)

def test(left: dict[int, int], right: dict[str, int]) -> None:
    # without outer context, the type is precise
    reveal_type(join(left, right))  # dict[int | str, int]
    assert_type(join(left, right), dict[int | str, int])
    # outer context allows widening
    x: dict[str | int, int] = join(left, right)
    y: dict[str | int | list, int] = join(left, right)
    z: dict[object, int] = join(left, right)

My current thinking is that this possibly requires HKT (#548), or more specifically lower bounding a TypeVar by another TypeVar, so that for example the join method could be typed as:

def join[K1, V1, K2, V2, K :> K1|K2, V :> V1|V2](
    left: dict[K1, V1],
    right: dict[K2, V2]
) -> dict[K, V]: ...