The canonical case of this is an empty list literal, but in everything that follows, we should assume it is generalized to all generic classes, not special-cased for builtin collection types.

We discussed these two code examples:

def a() -> list[int]:
    x = []
    y = x
    return y

def b() -> list[int | str]:
    x = []
    x.append(1)
    x.append("foo")
    return x

Today in both of these cases we infer list[Unknown] at the list construction, and don't emit any diagnostics on either of these examples. So we avoid false positives by using gradual types, but this is also quite unsound: if the return type of b were list[bytes], we still wouldn't emit any diagnostics!

(Similarly, for non-empty list literals without a declared type, we infer the union of Unknown with the elements present, which is compatible with the gradual guarantee and avoids false positives, but is similarly unsound with respect to later constraints on the type of the list.)

Pyright in non-strict mode effectively does the same thing we do today. In strict mode it adds some diagnostics warning that there's an Unknown type (for which the solution is "add an annotation.")

Mypy similarly just asks you to add an annotation in the first case, since it has nothing to go on, but in the second case it uses the (first, and only the first) append to infer a type for the list (promoting literal types), so it infers list[int] and then errors on the second append, and on the return (because list[int] is not assignable to list[int | str].)

Pyrefly does not include the "please add an annotation" or "there's an unknown type!" diagnostics that mypy and pyright-strict have on the first example. On the second example, it behaves the same as mypy. Its handling is not special-cased to builtin collection types or methods, but works for any generic class and its methods. It gives up if the list is aliased at all.

Some characteristics it seemed like we felt were desirable for our future handling of these cases (we didn't list these explicitly, I'm inferring from the direction of the conversation):

1. Errors are attributed to a reasonable location.
2. Hover shows a comprehensible type for the list that helps identify the problem when there is an error.
3. Gradual guarantee: if there is no annotation on the list creation, we shouldn't invent limitations on what you are allowed to put into the list, based on what you happen to put in first.
4. Our approach isn't broken by aliasing.

We focused on two primary potential strategies, which are ultimately two different implementation paths to a similar user experience:

Back-propagate type contexts

In this approach, we would track in semantic indexing, for each definition, all the later type contexts which may apply to it. So in a() we'd track that x = [] has a later type context from y = x, and that that definition of y in turn has a type context from return y (which is the return annotation). In b() we'd track that x = [] has multiple later type contexts from x.append(1), from x.append("foo"), and from return x.

So in a() we would follow the chain and arrive at the single type context list[int], and thus use that as the type of x right at x = [].

In b() we would unify all three type contexts and arrive at the solution list[int | str] which works for all three of them.

If the type contexts for a definition don't unify, we just have to make a best-effort choice (prefer the first context? prefer the "widest" context?), naturally resulting in some diagnostics later on.

One challenge of this approach is avoiding big increase in memory usage from the additional def -> context mappings we'd have to store in semantic indexing. Another challenge is finding the right level of "context" to store in that mapping for all cases. For example, in x.append(1) we need the entire statement, not just the x expression (we can't traverse up our AST). Similarly in foo(x) we'd need the entire call expression.

Synthesize type variables and build up constraint sets, solve them for the scope

In this approach we'd synthesize a typevar T at x = [] so the type of x is list[T], and then as we type-check the body of the function, collect constraints on the type of T. So x.append(1) would add a T :> Literal[1] constraint and return x would add a T == int | str constraint (due to invariance of list). At the end of inferring the scope, we'd solve this constraint set. If it doesn't unify, we'd have to then figure out where to place diagnostics (which would mean that we needed to also collect the range-source of each constraint, and there might be a challenge here with preserving that information when simplifying the constraint set). If it does unify we'd have to record our solution so that hover shows the solution rather than the synthesized typevar.