`Unknown` inferred when solving generic overloaded calls involving invariant generics specialized with `Any`

[AlexWaygood]

Summary

Observe: the first reveal_type shows us solving the type variables correctly, but for the second reveal_type, not only do we fail to solve the type variables, we fallback to Unknown for the whole type!

from typing import Any, overload, reveal_type

class Invariant[KT, VT]:
    attr2: VT

    @overload
    def foo(self, other: Invariant[KT, VT]) -> Invariant[KT, VT]: ...
    @overload
    def foo[T1, T2](self, other: Invariant[T1, T2]) -> Invariant[KT | T1, VT | T2]: ...
    def foo(self, other):
        raise NotImplementedError

def g(x: Invariant[int, int], y: Invariant[int, str], z: Invariant[int, Any]):
    reveal_type(x.foo(y))  # Invariant[int, int | str]
    
    reveal_type(x.foo(z))  # ty: Unknown
                           # pycroscope: Any[multiple_overload_matches]
                           # mypy, zuban: Invariant[Any, Any]
                           # pyrefly, pyright: Invariant[int, int]

This comes up in the real world with dict.__or__ in typeshed:

https://github.com/astral-sh/ruff/blob/546d3b2b1ad214976c5238174efcb061df548207/crates/ty_vendored/vendor/typeshed/stdlib/builtins.pyi#L3056-L3061

Meaning:

reveal_type({"foo": "bar"} | {})  # Unknown

Multiplay gist comparing our inference with other type checkers: 0685f09832604c2cb53928d004881454.

Version

No response

[AlexWaygood]

Claude reckons we determine that both the first and second overload match here for the x.foo(z) call. That then causes us to fallback to Unknown since the return types of the first and second overloads are not equivalent (step 5 of the overload evaluation algorithm in the spec).

[AlexWaygood]

While this result feels deeply unintuitive and it does still feel to me like overload 2 is a "better" fit here, it does seem like we're following the spec here for how overloaded generics solving is supposed to work. So the best fix here might be to remove the first overload from typeshed upstream -- strictly speaking, it should be unnecessary.

It does seem like no current type checker does what I'd expect/hope here (which would be to infer Invariant[int, int | Any]).

[AlexWaygood]

The first overload for dict.__or__ is redundant, so the immediate issue with dict.__or__ will be solved if python/typeshed#14284 is merged. (Edit: it has now been merged.) But the issue also exists for defaultdict.__or__, ChainMap.__or__ and UserDict.__or__, and in those cases the first overload serves a purpose, expressing that __or__ will return a subclass of that class if called on a subclass:

https://github.com/astral-sh/ruff/blob/546d3b2b1ad214976c5238174efcb061df548207/crates/ty_vendored/vendor/typeshed/stdlib/collections/__init__.pyi#L709-L714

from collections import defaultdict

x = defaultdict(str, {"foo": "bar"})
reveal_type(x | {})  # Unknown

It seems like we're following the spec here, but I worry that this result will be unintuitive for our users -- inferring Unknown looks like a bug, even if it strictly-speaking isn't. I suppose our options are:

1. Amend the spec so that the algorithm arrives at an answer closer to mypy/zuban here?
2. Attempt something a bit more like pycroscope, where rather than having a binary Any/Unknown division we have fine-grained tracking for where dynamic types originated from. Sort-of similar to what we already do for Todo types -- but we'd want to keep the information around in release builds, unlike what we do for Todo types.

[carljm]

Those options are mostly orthogonal -- it may make sense to do both!

Regarding (1), it would probably be worth a bit of looking into what heuristic exactly is actually used by pyright/mypy/zuban.