Of course, if a compiler and its type system are sound, then the fact that certain errors are eliminated follows trivially, but, in practice, this does not prev

Of course, if a compiler and its type system are sound, then the fact that certain errors are eliminated follows trivially, but, in practice, this does not prevent types (and especially those of the rich type systems you are advocating) having bugs in their implementation. Take, for example, floating-point numbers in Excel. Even something as fundamental as floating point types need documentation, which is why we have IEEE 754.