In a Turing complete dynamic language I believe that some properties of the runtime would be undecidable. The advantage of static typing is that many (most?) type systems are sufficiently constrained (i.e. not Turing complete) such that the typecheck procedure can be assured to terminate.

Of course, with sufficiently expressive type systems you end up with Haskell "UndecidableInstances" or Coq dependent types or C++ compile-time tetris, [0] and now you are back to the same problem as with analyzing the runtime. Otherwise you may find it difficult to encode the desired properties or invariants into your type system, for lack of expressive power... tradeoffs abound, and so on.

[0] https://news.ycombinator.com/item?id=9813800