Not really, a language in which some type errors are impossible (rather than merely very unlikely) makes it drastically easier to prove something useful about programs (e.g. to optimize away runtime checks that would otherwise be needed as a safety net and impossible cases).