str.split v. LiteralString false positive type error.

[rcls]

Describe the Bug

This appears to be a false-positive type error from pyrefly. Using str.split on a LiteralString ends up with confusion between list[str] and list[LiteralString]:

ERROR sandbox.py:6:5-6: Argument list[LiteralString] is not assignable to parameter x with type list[str] in function foo [bad-argument-type]

def foo(x: list[str]) -> None:
    pass

l = 'a b c d'.split()
foo(l)

Sandbox Link

https://pyrefly.org/sandbox/?project=N4IgZglgNgpgziAXKOBDAdgEwEYHsAeAdAA4CeSIAOljGAARi64AU%2BidUEcALgNo8AnALoBKOgFoAfHQByudDETU6KusVRw41alDoBeOgHJUdbHQDGdTIcJxinbsxHVGLKM-QgANCACu3aDgSckQQAGI6AFUAh1IGX3RzAPktdGpMWgZcAQBbVG4AfXRfHOwYAVZ2CHRuMSk6QSV0VToBGG5fAWawShAZErKBdmB8AF9e6m8QMjawKFJCblwcqAoIgAVSWfmGjBwCC3lIAHNO-Ih5QmoIgGUYGDoAC25uYjhEAHoPmdp5wmzjh8YOgPphcOY4B9zEcIKcBOd5B8sgI6KgAG6oaCobCwQ7oE5nZLNXDEIlBahkbiPeTiNHlOAXZoGXoAZkIAEYAEwTTyjHyoJIQOkAMWgMAoaCweCIZBAoyAA

(Only applicable for extension issues) IDE Information

No response

[grievejia]

In your example I think this Pyrefly error is legit -- it's not safe to pass a list[LiteralString] to a list[str] because your function may append extra non-literal strings to the list, invalidating the literal-ness. E.g.

y: str = read_from_internet()
def foo(x: list[str]) -> None:
    x.append(y)

l = 'a b c d'.split()
foo(l)
assert_type(l[-1], LiteralString)  # ERROR! `l[-1]` is no longer a string literal at runtime

Here is relevant discussion on typeshed with this issue.

However, I think there's an argument to not error if your example gets tweaked a little bit, e.g.

def foo(x: list[str]) -> None:
    pass

foo('a b c d'.split())  # In principle this should be safe. But Pyrefly can't differentiate this from the previous example

l: list[str] = 'a b c d'.split()  # In principle this should also be safe. But Pyrefly currently complains (maybe this is a contextual typing + overload related issue?). 
foo(l)  # OK

Right now the only tweak that "works" in Pyrefly is to explicitly "upcast" the string literal:

s: str = 'a b c d'  # OK
foo(s.split())  # OK

Though this workaround may not work in other type checkers -- not every checker interprets annotated assignments as an upcast as Pyrefly does.

[rcls]

As far as I understand, the code I gave is typeable in the type system that pyrefly uses:

• 'a b c d' has type Literal['a b c d'], which appears to implicitly converts to either LiteralString or str.
• str.split is overloaded, so that the type of 'a b c d'.split() can either be resolved to list[str] or it can be resolved to list[LiteralString]. In this case, nothing forces pyrefly to choose list[LiteralString].
• The call to foo takes type list[str], so we are left with that as the only possible choice.

But pyrefly considers only the one possibility for split here, leading it to miss a possible typing.

There is no need for covariant list types to type this code (and no need to allow passing of list[LiteralString] to list[str]).

[rcls]

Experimenting a bit, I note that pyrefly assigns different types to "a b c d".split() and ['a', 'b', 'c', 'd']. The first gets typed as list[LiteralString and the second gets typed as list[str]. Which seems rather ironic given that it is the second that has the array elements specified as lexical literals...

[yangdanny97]

The call to foo takes type list[str], so we are left with that as the only possible choice

The rules are specified in Python's typing spec, and state that if there are multiple matches we are to select the first one. Based on the spec, a contextual type doesn't have an effect on which overload is selected.

['a', 'b', 'c', 'd'] being typed as list[str] is because of different rules, where we promote all Literal types when resolving a generic type. This is intentional, but as you can see from #1138 it results in false-positives elsewhere.

So ultimately it's a combination of issues in the type system rules & the way the standard library types are written, and regardless of which way you infer things there will be false-positives in some cases. That's why the recommended workaround is to add a type annotation to prevent the type checker from guessing wrong.

This could be an area where we choose to deviate from the spec, if we come up with an approach that is better than "always infer list[str]" or "infer list[LiteralString] over list[str] whenever possible".

One idea I had off the top of my head is to infer a contained var constrained by str & LiteralString and let our first-use pinning pick the winner. This would result in the behavior you describe for the ['a', 'b', 'c', 'd'] case, but I'm not sure if it's legal to have one constraint be a subtype of another.

[rchen152]

Grabbing this because I'm tweaking Literal promotion. Not sure I can fix this, but the behavior here should at least be considered.

[rchen152]

The work I'm doing to mark literals as implicit or explicit doesn't fix this after all, so throwing it back in.

[randolf-scholz]

One idea I had off the top of my head is to infer a contained var constrained by str & LiteralString and let our first-use pinning pick the winner. This would result in the behavior you describe for the ['a', 'b', 'c', 'd'] case, but I'm not sure if it's legal to have one constraint be a subtype of another.

This is similar an idea I explored in mypy (python/mypy#20444) by modeling literals with a special "AnyOf" type (python/typing#566):

When a user types x = "foo", without annotation, we do not know apriori whether this is supposed to be Literal["foo"] or str.

So, infer the type of x as AnyOf[Literal["foo"], str]. This type behaves similarly to Union in some cases and similar to Intersection in others (python/typing#566 (comment)):

• X <: AnyOf[Y1, ..., Yn] if and only if X <: Yk for some k (union-like)
• AnyOf[Y1, ..., Yn] <: Z if and only if Yk <: Z for some k (intersection-like)

In OP's example, one could then check that this AnyOf type matches both the LiteralString -> LiteralString and str -> str overloads, and so the type of l should be AnyOf[list[LiteralString], list[str]].

Finally on the foo(l) call, the list[LiteralString] variant could be eliminated.