Types can't check the correctness of everything, but they do prove that certain classes of errors don't exist in your program.
Tests, on the other hand, can test for many more types of bugs, but they can only look for errors, they can't prove correctness (except in very small, closed environments where you can literally test every possible combination of inputs and outputs).
That's particularly important when refactoring because you want to assert that you haven't introduced new bugs, and the type system will often let you prove that with almost zero effort on your part.
Static typing makes both of those trivial if your language (or linter) has enum-exhaustiveness checks for switch statements.
Tests are existentially quantified, types are universally quantified.
(Yeah, existential types, I know. Shut up. ;) )
