> every type checker in the world will reject this program due to the mere presence of the 'return 123' branch Just to expand on this a bit: It would be trivia

> every type checker in the world will reject this program due to the mere presence of the 'return 123' branch Just to expand on this a bit: It would be trivial to extend a type checker to cover this case. But a) It wouldn't be terribly useful because this is a rather stupid way to write code, and b) It would always be possible to contrive yet another example that the "extended type checker" would fail on, because static analysis can never completely replace running the program. That's basically Rice's Theorem.