So just because you can't devise a type system that accepts all correctly-typed programs doesn't mean that a statically-typed language can't create equivalents to any dynamically-typed program, assuming it's Turing complete. That's a misconception.
What falls under correctly-typed within most modern type systems is more than enough to write expressive programs. In fact, sometimes a static type system can be even more expressive than even the most expressive dynamic one (as is the case with Haskell, for example). As some evidence for this, I assert that one can re-create any dynamic type system within a Haskell program, using simple algebraic data types.
That's what I meant about dynamic typing not being needed. Yes, even languages like Haskell have runtime typing "escape hatches" but they're never necessary except for use with FFIs (ie, other languages) and are definitely a major code smell if you use them for normal coding. They're just not necessary.