Skip to content

Experiment with backtracking in the new solver #15908

Open
@ilevkivskyi

Description

@ilevkivskyi

Depend on #15906. This is a follow-up for series started by #15287

Currently when getting both upper and lower bounds for a type variable we randomly choose the lower one. This is not always the best choice and can lead to inference failures. A possible example is:

def dec(fn: Callable[[S, S, int], float]) -> Callable[[S], float]: ... 
def f(x: List[float], y: List[T], z: T) -> T: ...
dec(f)

this will infer constraints like

S <: List[float], S <: List[T], T <: float, T :> int

They split into two SCCs each containing one variable {T} and {S}, and the second depends on first one. So we would first solve T = int and then we will get updated constraints for S: S <: List[float], S <: List[int], with the only solution S = <nothing>. At the same time T = float, S = List[float] is a totally valid solution. We could get it by backtracking when we get <nothing> and trying different bound(s) in the previous SCC.

One possible problem I see is that this backtracking is exponential in worst case of inference failure (e.g. due to actual user error). Another problem is that backtracking can make implementation much less readable.

cc @JukkaL

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions