variable is treated as possibly being `None` when there's no code path that can set it to `None`

[Keymasterer44]

Describe the Bug

from typing import *

def test() -> list[str]:
    args: Optional[list[str]] = []
    return args
    

It seems that when a variable is declared as Optional, Pyrefly doesn't pay attention to whether the initial assignation is None or a value and just assumes on the return args statement that args might be None even though no code path exists under which it could reach the return statement with a None value.

Sandbox Link

https://pyrefly.org/sandbox/?project=N4IgZglgNgpgziAXKOBDAdgEwEYHsAeAdAA4CeS4ATrgLYAEALqcROgOZ0Q3G6UN0AqADroRmGGEbwGACgCUdALQA%2BOlAhwGAbU2UAuohF1jdVJTZxEdAPLEGEXOlRQt6zTob69dALx0tekYmlDAMAK6U6KbmcEHGIAA0IGQhYFCkhAy0UBQAxHQACqSp6XRoWHj4dADGjpBsEaj2joQi%2BQDKMDB0ABYMDMSWAPRDKRLphLxsQzDoQ5i41XBDtej1jc1zdGC8pgBuqNCo2LA1dRANlE0OUbh2N3Ct6GQMPY6KezCUcDe%2BdEIgADMhAAjAAmAEiLRfajfQLoMLoLg8PgwTCKTAQELVeyfP4Acgu6F4MHxImJDEUIQAjmEsWjFABrGCkRSoarVeBwAkAdzM6DJ6BAAF8kuzcTAAGLQGAUco4AgkcjCoA

(Only applicable for extension issues) IDE Information

No response

[yangdanny97]

This is working as intended, we respect the user's explicit type annotation over the inferred type of the RHS value.

for more discussion, see #2227

[Keymasterer44]

@yangdanny97 I may be missing some nuance here, apologies if yes, but one aspect which I'm not sure is considered by the discussion is that in the example I gave, realizing that the only possible value for the type at the return is list[str] wouldn't really be violating the annotation. The examples I saw when going through the discussion are all about a variable getting one type annotation but then being assigned a value of an entirely different type, meanwhile in my case any given list[str] is still a valid assignation to Optional[list[str]]. The inference, at least to me, seems less like a violation of the users specification and more an extension of it. It's not like the examples given in #2227 where the type of a variable is getting changed completely by an assignation that should be considered invalid, with those I fully agree that a user saying x: int should a taken over later code suddenly assigning ´Any´ to x and making that its type, since Any in that example is a lot broader than int while list[str] in my example is narrower than Optional[list[str]].

[yangdanny97]

Maybe we can consider this in cases when the RHS value's inferred type is a subtype of the annotation, but it gets complicated when we consider gradual types

Like, what happens if if the LHS is annotated list[Any] and the RHS infers to list[int]? Right now we would infer list[Any] because it's the user-specified type, and if we use list[int] then it can be overly specific and cause false positives - per the annotation, the list could be initialized with ints, but allow any contents.

Same goes the other way around. If LHS is list[int] the user wants to restrict the contents to int, but if the RHS is list[Any] and we use that then we lose type safety.

For simple examples where the types look about the same we can detect the presence of Any, but for more complex examples where the types on both sides look very different it could be tricky to resolve

Maybe the solution is to only do this if neither type contains Any? But that could lead to confusion if the behavior is inconsistent, esp since not every occurrence of Any is explicitly included part of the printed/written type form

[Keymasterer44]

Like, what happens if if the LHS is annotated list[Any] and the RHS infers to list[int]? Right now we would infer list[Any] because it's the user-specified type, and if we use list[int] then it can be overly specific and cause false positives - per the annotation, the list could be initialized with ints, but allow any contents.

By the idea as I described it some middle ground would exist where the type checker knows both to allow non int assignations but also to infer any reads to be int until an assignation happens that breaks the type checkers narrowing. With lists of course this gets complicated quickly anyways, even the current type checker implementation you're describing could break type safety if the RHS is a list[int] variable that is references someplace else. On the LHS variable non int values could be added to the list while the RHS variable still falsely thinks it's holding a reference to a list[int].

Same goes the other way around. If LHS is list[int] the user wants to restrict the contents to int, but if the RHS is list[Any] and we use that then we lose type safety.

I would say the LHS being list[int] and the RHS being list[Any] would have to be an error for type safety since Any is broader than int, in my head it falls under the kind of example discussed by #2227 where I agree that the LHS annotation should take precedent.

Maybe the solution is to only do this if neither type contains Any? But that could lead to confusion if the behavior is inconsistent, esp since not every occurrence of Any is explicitly included part of the printed/written type form

I wonder how feasible it is to implement the checker narrowing as follows:

• Anything where T is part of a return value can be narrowed beyond the LHS annotation based on assignations but not broadened beyond the minimum type specification required by the LHS type annotation.
• Anything that's a direct assignation or a method invocation where T is a parameter serves to either narrow or broaden what the checker knows T can be right now, with the restrictions I already mentioned above (especially the "you can't broaden to a type looser than the LHS annotation" part).

My logic I believe would look something like this:

some_list: list[Union[int, str, float]] = [n for n in range(3)]  # would be allowed since LHS annotation has int as an option
reveal_type(some_list)  # list[int]
some_list.append("a string")  # would be allowed since LHS annotation has str as an option
reveal_type(some_list)  # list[int | str]
any_value: Any = 0.1
some_list.append(any_value)  # two options on this assignation, either trying to put in Any causes a type checker error or the type checker assumes that the value must be compliant with list[Union[int, str, float]] and therefore broadens to that because it's the broadest type allowed by the LHR annotation, I'm not sure which approach would be the more sensible one to take
some_list.append([])  # would always cause an error no matter what since list isn't part of the LHS annotation

Generally with an Any RHS on a non Any LHS, as I go into a bit in the code comment, I see two approaches that to me seem like they could potentially provide sensible handling, though I'm not sure which would be preferable:

1. You don't allow Any on the RHS and treat it as an error.
2. You trust the user that the value is compliant with the LHS annotation and broaden to that exact annotation for further reads

In theory I think the approach of doing this read only narrowing based on writes should be sound, I of course am unsure how realistic it is to actually implement that level of complexity into the type inference, since you basically need a constant differentiation of what type T is depending on if it's being read or written.

[yangdanny97]

We can't ban Any by default, that would make type checking too restrictive to use. I think there's an opt-in error code either in this version or the next version for that though.

There's no way around losing type safety when Any gets used. If the user did that intentionally via an annotation, then that's fine since it's supposed to be a backdoor of sorts. The problem I have with my second example

If LHS is list[int] the user wants to restrict the contents to int, but if the RHS is list[Any] and we use that then we lose type safety.

Is that the user annotated list[int] so we shouldn't silently use Any against their actual annotation

[Keymasterer44]

We can't ban Any by default, that would make type checking too restrictive to use. I think there's an opt-in error code either in this version or the next version for that though.

That's fair enough.

Is that the user annotated list[int] so we shouldn't silently use Any against their actual annotation

If we go by a logic of saying that if Any is used we should just trust the user that they're making a valid assignation, where exactly would be the problem with then having the behaviour in the example I gave essentially be as follows:

some_list: list[Union[int, str, float]] = [n for n in range(3)]  # would be allowed since LHS annotation has int as an option
reveal_type(some_list)  # list[int]
some_list.append("a string")  # would be allowed since LHS annotation has str as an option
reveal_type(some_list)  # list[int | str]
any_value: Any = "a string but annotated as Any"
some_list.append(any_value)  # would be allowed since it's assumed that whatever Any the user is assigning is valid, causes the type checker to assume the broadest type allowed by the LHR annotation
reveal_type(some_list)  # list[int | str | float]
some_list.append([])  # would always cause an error no matter what since list isn't part of the LHS annotation

The main flaw I see is that the change to type could appear unintuitive to someone encountering it for the first time (especially if they didn't realize that they put a value of type Any into the list), but from a logical standpoint this approach seems to me like it would result in sound behaviour and properly respect both the initial annotation of some_list and the use of Any definitely making it unsafe to assume that the actual type at the moment is still list[int | str].

[yangdanny97]

The widening behavior in your example isn't safe because of aliasing

some_list: list[Union[int, str, float]] = [n for n in range(3)]  # would be allowed since LHS annotation has int as an option
reveal_type(some_list)  # list[int]
other_list = some_list # would other_list be `list[int]` at this point?
some_list.append("a string")  # would be allowed since LHS annotation has str as an option
reveal_type(some_list)  # list[int | str]

assert isinstance(other_list[-1], int) # runtime error