Bug report

I ran into this while creating an example for another report. When "merging" arrays using array_push and the splat operator, the resulting array shape is not complete.

Code snippet that reproduces the problem

https://phpstan.org/r/13388f61-19fe-4046-81c2-24f438783242

$a = [new HelloWorld()];
$b = [new HelloWorld(), new HelloWorld(), new HelloWorld()];

array_push($a, ...$b);

This produces the following as the type for $a:

array{HelloWorld, HelloWorld}

Expected output

array{HelloWorld, HelloWorld, HelloWorld, HelloWorld}

or

array<HelloWorld>