The question is not whether a type system will catch bugs. The question is whether a type system finds enough bugs that tests (sufficient to cover the things that the type system does not catch) would not also catch.
If you have to point to something like Idris I don't think you're making a real world argument yet.
If you have to point to something like Idris I don't think you're making a real world argument yet.