Skip to content

Consolidate multi-inference architecture #3001

@ibraheemdev

Description

@ibraheemdev

There are a number of places in ty where it is necessary to infer a given expression multiple times. Our handling of this is currently inconsistent, but there are two broad categories where "multi-inference" is necessary.

Union expansion

When assigning to a member (attribute or subscript) on a union target, the union is expanded, and the RHS expression must be assignable to the corresponding member on each of its elements:

class A:
    x: list[int | str]

class B:
    x: list[int | None]

def _(target: A | B):
    target.x = [1] # list[int | str] & list[int | None]

    # if isinstance(target, A):
    #     target.x = [1]  # list[int | str]
    # elsif isinstance(target, B):
    #     target.x = [1]  # list[int | None]

def f(target: dict[str, list[int | str]] | dict[str, list[int | None]]):
    target["x"] = [1] # list[int | str] & list[int | None]

    # if isinstance(x, dict[str, list[int | str]]):
    #     target["x"] = [1]  # list[int | str]
    # elsif isinstance(x, dict[str, list[int | None]]):
    #     target["x"] = [1]  # list[int | None]

In this case, the RHS expression does not exactly have a single inferred type, and so we should infer the intersection of all inferred types, i.e.,list[int | str] | list[int | None] in the above example. Note that such an intersection type is generally unsound, but it is valid here because the inferred type itself does not leak outside the assignment statement, and is only visible through an IDE hover or similar.

One problem with this approach is that diagnostics may be duplicated across multi-inference attempts. The current solution to this is to perform the first inference attempt without type context, and silence diagnostics for later attempts. However, this can lead to odd behavior with reveal_type calls, as the intersection type has not yet been inferred when reveal_type diagnostics are processed during the first inference attempt. A possible solution to this is to instead perform the final inference attempt without type context, for more complete diagnostics.

Union narrowing

On the other hand, when assigning to a union target directly, the RHS expression must only be assignable to a single element of the union. This is the case for annotated assignments:

x: list[int | str] | list[str | None] = [1]  # list[int | None]

In the above case, narrowing to the correct type context may require inferring the same expression multiple times, but the result of multi-inference should be a single type for each nested expression, not an intersection. Note that there may also be multiple valid inferred types for a given expression, in which case we may choose the first assignable type, or the union of all assignable types:

x: list[int | str] | list[int | None] = [1] # list[int | str] | list[int | None]

Note that nested type context can lead to a combinatorial number of inference attempts, and so collecting the tree of all possible inferred types is not feasible:

x: list[list[int | str] | list[int | None]] | list[list[int | str] | list[str | None]] = [
    [1]
]

We currently perform multiple inference correctly for generic calls, speculatively attempting inference, and narrowing to the first element of the type context that leads to valid call binding. We should do the same for collection literal expressions, as they are special cases of generic calls.

Another place where narrowing is required is during overload resolution. We currently infer the arguments multiple times for each overload, storing the intersection of all inferred types. However, this is currently unsound, as intersection types may leak to the caller during generic call inference:

@overload
def f[T](x: T, y: int) -> T: ...
@overload
def f(x: list[int | str], y: str) -> Any: ...
def f(x: Any, y: int | str) -> Any: ...

x = f([1], 1)
reveal_type(x) # list[int | str] & list[int]

We should perform inference only speculatively until overload resolution complete, after which a unique type context is chosen for each expression.

Note that unlike the union expansion case, diagnostics are not a problem when narrowing, as they are simply disabled until a target type context is chosen.


Note that the inverse cases also apply, i.e., generic call inference with an intersection type as type context should perform intersection expansion, and member assignment on an intersection target should perform intersection narrowing.

Metadata

Metadata

Assignees

Labels

bidirectional inferenceInference of types that takes into account the context of a declared type or expected type

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions