Handle callable subtyping for generic callables

[grievejia]

Minimal repro:

from typing import Callable

def foo(x: Callable[[int], int]) -> None: ...
def bar[T](x: T) -> T: ...
foo(bar)

Expected: No error Actual: Argument Forall[T, (x: T) -> T] is not assignable to parameter x with type (int) -> int in function foo

[lolpack]

Sandbox link: https://pyrefly.org/sandbox/?code=GYJw9gtgBALgngBwJYDsDmUkQWEMoDCAhgDYlEBGJApgFC0Am1wUwYYAFAB4Bchp5KtQDaw1DAC6AGkwpJASigBaAHxQAcmBTU+AOn2NmUCkRDCAKhO59zi1VHN6DbTiZDygA

[rchen152]

I had the bright (not really) idea of calling solver.fresh_quantified() when we encounter a Forall in is_subset_eq. It handles the example here correctly but breaks down in cases like https://github.com/facebook/pyrefly/blob/11f833daf51e0e07bd55bf38da01f12d09aece4f/pyrefly/lib/test/paramspec.rs#L52-L59 because foo2, which should be the Forall, ends up as a Callable with variables that then get pinned on the next use :/

[grievejia]

Yeah we talked about this problem during PyCon discussion with Neil and Steven. I think Rebecca's intuition is right -- the only missing ingredient to make it work is to have a basic support for backtracking (aka make it possible to "restore" the solver state to certain "checkpoint", with some temporarily created vars discarded).

[github-actions[bot]]

This issue has someone assigned, but has not had recent activity for more than 2 weeks.

If you are still working on this issue, please add a comment so everyone knows. Otherwise, please unassign yourself and allow someone else to take over.

Thank you for your contributions!

[migeed-z]

The example above is no longer a type error. Is the issue resolved? cc @rchen152 and @grievejia

[rchen152]

Ah, this was fixed by https://github.com/facebook/pyrefly/commit/1dcab8bbc1065d63e7f87668896b4006cd8035d1 :)