ctype_digit($x) is true does not imply that $x is decimal-int-string #14792

Bug report

ctype_digit('02') is true (see https://3v4l.org/1UHhu), but '02' is not decimal-int-string

Code snippet that reproduces the problem

https://phpstan.org/r/548eea93-7a42-4ca8-92da-9dbb0773fd8e

Expected output

No error on line 6.

Did PHPStan help you today? Did it make you happy in any way?

No response