All true, but there is more. SPJ and S Marlow [1] list the following additional advantages of using a typed intermediate representation, which would/could apply to MIR too.

1. Running a type-checker on the IR "is a very powerful consistency check on the compiler itself. Imagine that you write an 'optimisation; that accidentally generates code that treats an integer value as a function, and tries to call it. The chances are that the program will segmentation fault, or fail at runtime in a bizarre way. Tracing a seg-fault back to the particular optimisation pass that broke the program is a long road. Now imagine instead that we run [the type-checker on the IR] after every optimisation pass: it will report a precisely located error immediately after the offending optimisation. What a blessing [...] in practice we have found that it is surprisingly hard to accidentally write optimisations that are type-correct but not semantically correct."

2. Running a type-checker after translation to IR serves as a "100% independent check on the type inference engine".

3. A high-level typed IR is a "[s]anity check on the design of the source language."

All quotes from [1].

[1] S. Marlow, S. Peyton-Jones, The Glasgow Haskell Compiler. http://www.aosabook.org/en/ghc.html