> it's coarse-grained and errs on the side of caution

That's what type systems in general do. There is no type system for a turing-complete language that is both sound and complete. (Trivial proof: if (undecidable) halt; unsound.)