Inference question: empty list and .append() call

[jrheard-seesaw]

Code sample in pyright playground

# pyright: strict

def hello_world(x: int) -> list[str]:
    result = []
    
    if x % 2 == 0:
        result.append("hello")

    return result

# Type of "append" is partially unknown
#  Type of "append" is "(object: Unknown, /) -> None"  (reportUnknownMemberType)
# Return type, "list[Unknown]", is partially unknown  (reportUnknownVariableType)

Hi! In the code snippet above, as a human reader, I can tell that result "should be" (in my opinion) of type list[str]; but Pyright says that the list is of type list[Unknown].

When I try the same thing in the mypy playground and add a couple of reveal_type() calls, I see that one line after result is defined, mypy says main.py:5: note: Revealed type is "builtins.list[Any]"; but right before the return call, mypy says main.py:10: note: Revealed type is "builtins.list[builtins.str]".

As a new Pyright user, I've gotten the impression that Pyright's inference is in general stronger / more aggressive (please correct me if I'm mischaracterizing it) than mypy's, and so I would have expected that Pyright would infer that result is of type list[str]. I'm a bit fuzzy on the details of why I expected this, though, because I don't know much about how type inference works under the hood.

Sorry for the long-winded question. The short version is: why does Pyright say that result is of type list[Unknown] and not list[str]? Thank you!

[erictraut]

Pyright's type inference philosophy is based on the principle that the type of an object is established at the time it is constructed. You can't, for example, say that a list object starts its life as a list[str] and later change your mind and decide that you want it to be a list[str | int]. All subsequent operations are validated based on the type of an object that it had when it was created. The methods that can be safely called on that object are based on its type. Its type is not influenced by the methods that are called on it; that would be backward.

The same principle applies here. At the time the list is constructed, its type is list[Unknown] because there is no additional context available to provide a more specific type. When an object is constructed, its type is fixed. It can't change to some other type based on the methods that you invoke on it or the arguments you pass to those methods.

[jrheard-seesaw]

Got it, that makes sense. Thanks for the explanation!