More higher-order function type variable unification issues

[colehaus]

Thanks for addressing #5838!

In pyright 1.1.325, the following code:

from typing import Callable, Generic, TypeVar

A = TypeVar("A")
B = TypeVar("B")

class Gen(Generic[A]): ...

def id_(x: A) -> A:
    raise NotImplementedError()

def bstep(
    x: Gen[A],
    y: A,
) -> Gen[Gen[A]]:
    raise NotImplementedError()

def bfn(
    x: Gen[Gen[A]],
) -> Gen[A]:
    return bfn_generic(x, id_, bstep) # Errors here

def bfn_generic(
    x: Gen[A],
    id_: Callable[[B], B],
    step: Callable[[A, B], Gen[A]],
) -> A:
    raise NotImplementedError()

produces three type errors on the same line:

error: Argument of type "Gen[Gen[A@bfn]]" cannot be assigned to parameter "x" of type "Gen[A@bfn_generic]" in function "bfn_generic"
    "Gen[Gen[A@bfn]]" is incompatible with "Gen[A@bfn_generic]"
      Type parameter "A@Gen" is invariant, but "Gen[A@bfn]" is not the same as "A@bfn_generic" (reportGeneralTypeIssues)

error: Argument of type "(x: Gen[A@bstep], y: A@bstep) -> Gen[Gen[A@bstep]]" cannot be assigned to parameter "step" of type "(A@bfn_generic, B@bfn_generic) -> Gen[A@bfn_generic]" in function "bfn_generic"
    Type "(x: Gen[A@bstep], y: A@bstep) -> Gen[Gen[A@bstep]]" cannot be assigned to type "(A@bfn_generic, B@bfn_generic) -> Gen[A@bfn_generic]"
      Function return type "Gen[Gen[A@bfn | A@id_]]" is incompatible with type "Gen[A@bfn_generic]"
        "Gen[Gen[A@bfn | A@id_]]" is incompatible with "Gen[A@bfn_generic]"
          Type parameter "A@Gen" is invariant, but "Gen[A@bfn | A@id_]" is not the same as "A@bfn_generic" (reportGeneralTypeIssues)

error: Expression of type "Gen[A@bfn] | Gen[A@bfn | A@id_]" cannot be assigned to return type "Gen[A@bfn]"
    Type "Gen[A@bfn] | Gen[A@bfn | A@id_]" cannot be assigned to type "Gen[A@bfn]"
      "Gen[A@bfn | A@id_]" is incompatible with "Gen[A@bfn]"
        Type parameter "A@Gen" is invariant, but "A@bfn | A@id_" is not the same as "A@bfn" (reportGeneralTypeIssues)

I was having trouble simplifying this any further but was able to isolate this error:

def step(x: A, y: A) -> A:
    raise NotImplementedError()

def fn(x: A) -> A:
    return fn_generic(id_, step)

def fn_generic(id_: Callable[[B], B], step: Callable[[A, B], A]) -> A:
    raise NotImplementedError()

error: Expression of type "A@fn | A@id_" cannot be assigned to return type "A@fn"
    Type "A@fn | A@id_" cannot be assigned to type "A@fn" (reportGeneralTypeIssues)

I would have expected all these to type check and indeed they do in mypy (I also double-checked the equivalent Haskell against GHC to ensure this wasn't just mypy being too lax).

[erictraut]

Sorry for the slow response on this. I've made several unsuccessful attempts at fixing this. It's a very challenging case to handle.

Interestingly, the latest version of mypy (1.7.x) includes a new constraint solver algorithm that addresses many bugs and limitations found in its old constraint solver, but its new algorithm cannot handle the code sample above. It now generates a false positive error similar to the one pyright is generating. I've filed this bug in the mypy project.

I'll also note that pyright does work correctly if you swap the order of the arguments. Obviously, this shouldn't be necessary. It should work regardless of argument ordering.

def bfn(x: Gen[Gen[A]]) -> Gen[A]:
    return bfn_generic(x=x, step=bstep, id_=id_)