Dumb. Mangles Godel.

The premise is that for real world inputs some code may never be used, and so it's an advantage for late-checked types that you can have wrong code that will never cause any observed bug. I'd rather "waste" my time deleting nonsense code after it fails an early type-check. Less code = better reading/maintenance/extension.

Better to focus on the real advantages of single-type languages (usually, terser programs, although type inference can make some haskell/ML programs apparently type-less).