join constraints with Any when constraints are in same shape

[oraluben]

Fix #6463, #2164 by join Union with same shape with Any, for example, Union[List[int], List[str]] -> List[Any], I use Any because List[Union[str, int]] is obviously wrong.

according to this,

• Infer Union[List[int], List[str]] for the type of []. This might be tricky to implement -- basically we'd need to support multiple possible answers from type inference, whereas currently we assume there's just one.

another way to fix that issue is to adjust any_constraints and solve_constraints to solve Union on any position of a type, currently it seems to work only on the 'leaf node'.

I'm not sure if this is a proper way to fix that, please have a look at your convenience.

[oraluben]

this do not fix this, so I think a good way is to treat List[<nothing>] as subset of List[<whatever>], which currently is not.

[ilevkivskyi]

I think this is not a good solution TBH. It just masks the problem instead of solving it. For example, IIUC in the original example in the issue you propose to solve List[T] <: Union[List[str], List[int]] with just T being Any. This is unsafe.

The option of making List[<nothing>] a subtype of List[int] appeared couple times recently, but it may be risky because we rely on <nothing> being a real bottom type at least in some places (e.g. protocol variance checks). It is not clear what we should do with these.

I am leaning towards the tricky option @JukkaL mentions. Essentially we would need to avoid pushing unions on the type context stack (when type-checking r.h.s. of an assignment, and when type-checking arguments in a call). Instead we would need to push every item of a union, type-check the expression in this context, and then union the results. We already do something similar for type-checking overload calls with union arguments.

This latter approach looks potentially promising from the point of view of quality of inference results, however it might be tricky. Also performance implications are not clear.

[oraluben]

Yes you'r right, this does not actually solve the problem.

And I have also test if just treat every <nothing> as subtype of anything, and it do break when inferring Protocols, so I have a version that do this only in dict, list, set, and tuple, which will have <nothing> when initialed empty.
I don't think this is a good solution neither, for it breaks the consistency when handling <nothing>. Just push this to have a reference.

I will see what can be done to infer Union, thanks for your reply!

[JukkaL]

Note that making List[<nothing>] a subtype of List[int] would not be safe, since lists are mutable. Assume we have instance of List[<nothing>]. We could pass that to a function expecting List[int], which could append an integer. We could also pass this List[<nothing>] object to a function expecting List[str], and it could read an integer from a supposed List[str].

[ilevkivskyi]

@JukkaL Argument of Pyre people (who actually consider it a subtype) is that if we prohibit this type to appear as a type of variable (btw mypy partially prohibits this), then the unsafety is practically negligible. On one hand this sounds reasonable, but on other hand, I don't like this kind of special-casing. Plus it will break protocol checks.

[oraluben]

Personally, I think List should not have <nothing> as its variable, it's more intuitive that empty List should have a List[Any] type.

[gvanrossum]

@oraluben Do you understand how mypy generally handles empty lists? There are two special cases.

Case 1: Type inferred from context:

def foo(a: List[T]) -> List[T]:
    ...
x: List[int] = foo([])

Mypy does some constraint solving here, where the expected return type of the call to foo() is used to infer the right value for T (in this example int).

A simpler case is:

def foo(a: List[int]):
    ...
foo([])

Again, the type of [] is inferred from the context, which is fixed here (List[int]).

You can even check this by writing foo(reveal_type([])) -- the constraint solving "passes through" reveal_type().

Case 2: Type inferred from peeking at later assignment:

a = []
a.append(1)

Here the type of a is inferred to be List[int]. This is done in a very different way -- mypy literally looks ahead in the function for the next use of a, and checks whether it is a simple operation like a.append().

Otherwise: If neither of these cases holds, the type of [] is List[<nothing>], and this is always supposed to give an error:

a = []  # E: Need type annotation for 'a'
if a:
    a.append(1)

Here a is used before the type is determined, and the "peek" operation doesn't work.

You get the same error (though for a different reason) if you try to split the example from case 1 in two:

def foo(a: List[T]) -> List[T]:
    ...
a = []  # E:  Need type annotation for 'a'
x: List[int] = foo(a)

Here the type of a cannot be affected by its use in the context of foo(a).