Skip to content

Old constraint solver always combines specializations using union #2799

@dcreager

Description

@dcreager

There are several open issues that all stem from the fact that the old constraint solver always combines specializations using union.

This is correct in some cases:

def f[T](t1: T, t2: T) -> T: ...

def _(x: int, y: str):
    reveal_type(x, y)  # revealed: int | str

The old solver does not have the ability to directly express range constraints or combinations of constraints. Instead, it only operates on "type mappings", which are partial/possible solutions. In this case, the old solver encounters "T = int" and "T = str" as partial solutions as we examine each argument. Since it only operates on type mappings, it needs a way to combine these two partial solutions into a single type mapping. This was the main use case that we were considering when writing the old solver, so we chose a heuristic that combines partial solutions using union.

The new constraint solver can express this example more directly. Function parameters are contravariant, so we end up with the constraint set int ≤ T ∧ str ≤ T, which is equivalent to int | str ≤ T. (This is why using a union as the heuristic is correct for these contravariant solutions, since those translate into lower bounds, which combine using meet.)

However, there are many cases where this is not the correct heuristic, especially now that we're inferring specializations for Callable types. A minimal repro of the reports we're seeing is:

class Base: ...
class Child(Base): ...

def f[T](t: T, c: Callable[[T], int]) -> T: ...
def cb(b: Base) -> int: ...

# currently: Base
# should be: Child
reveal_type(f(Child(), cb))

In this case, the old solver sees T = Child from the first argument, and T = Base from the second. It uses its simple heuristic to combine those into T = Base | Child, which simplifies to T = Base.

The old solver's heuristic is wrong here because T is not contravariant for both arguments. It is contravariant for the first argument, so the new solver infers Child ≤ T as the constraint set. For c, T is a "parameter inside a parameter", or "contravariant within contravariant", which simplifies to "covariant". So the constraint set that the new solver infers for the second parameter is T ≤ Base — it's an upper bound, not a lower bound. Combining those two constraint sets produces Child ≤ T ≤ Base. There aren't two lower bounds to combine, and so union never comes into play — and the old heuristic's simplification is incorrect.

(Note: this example also shows why it's important for the new solver to choose the smallest "interesting" solution.)

Metadata

Metadata

Assignees

No one assigned

    Labels

    genericsBugs or features relating to ty's generics implementation

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions