You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and

You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and dynamic typing. But it's ultimately a minimal argument instead of an interesting one. A dynamically typed fragment of code can be interpreted as a program in a statically typed world. From here we can attempt to use inference to partially recover real static information and use it during compilation. This is as old as dynamic languages---typed specialization! It's also a genuinely sophisticated static type system imposed on a genuinely dynamic language. That's an interesting POV from the compiler's perspective, and it should not be ignored. The other interesting perspective, though, and the one of more modern excitement, is that it's less about whether or not a program technically has a particular type but whether or not failure to be expressible at "good" types should be brought to the programmers attention immediately! You can see a statically typed language as a gradually typed language which refuses to compile whenever `any` gets inferred, for instance.