Pyright hangs when a unification variable occurs inside itself

[qexat]

Description

When a unification variable occurs inside itself (for example, in the context of a recursive type), Pyright hangs.

Code or Screenshots

import typing

def hummingbird[A, B, C](a: typing.Callable[[B, C, B], A]) -> typing.Callable[[B, C], A]:
    return lambda b, c: a(b, c, b)


def vireo[A, B, C](a: A, b: B, c: typing.Callable[[A, B], C]) -> C:
    return c(a, b)


typing.reveal_type(hummingbird(vireo))

I am running pyright from the command line.

$ pyright --verbose repro.py
Auto-excluding **/node_modules
Auto-excluding **/__pycache__
Auto-excluding **/.*
Assuming Python version 3.13.2.final.0
Execution environment: python
  Extra paths:
    (none)
  Python version: 3.13.2.final.0
  Python platform: Linux
  Search paths:
    /usr/lib/node_modules/pyright/dist/typeshed-fallback/stdlib
    /tmp/pyright-crash-repro
    /tmp/pyright-crash-repro/typings
    /usr/lib/node_modules/pyright/dist/typeshed-fallback/stubs/...
    /usr/lib/python3.13
    /usr/lib/python3.13/lib-dynload
    /home/clarisse/.local/lib/python3.13/site-packages
    /usr/lib/python3.13/site-packages
Found 1 source file

Happens with Pyright v1.1.398.

Interestingly, mypy seems to have an escape by giving up and filling with Nevers.

$ mypy repro.py
repro.py:11:20: note: Revealed type is "def (Never, Never) -> Never"
Success: no issues found in 1 source file

In pure theory, x should have the type ((((?0, ?1) -> ?2) as ?0), ?1) -> ?2, which is impossible to express in the current type system as far as I am aware.

[erictraut]

Thanks for the bug report and the clear code sample. I'm able to repro the problem, and I'll investigate further.

[erictraut]

Here's a repro that is further simplified:

from typing import Callable

def func1[A](a: Callable[[A, A], None]) -> None: ...
def func2[B](a: B, c: Callable[[B], None]) -> None: ...

func1(func2)

[qexat]

I can't test it more throughly right now but using the web playground (1.1.400), it seems that the hanging still occurs