Not trying to convince you, although I disagree completely. I only want to share how I think about it in case it resonates. I am over simplifying but bear with me.

It is impossible how to know if a program will halt without running it, in general terms (Halting problem).

One way to think about the type system is as a less expressive language that is guaranteed to halt. So, it has the pro that we can check properties of the system without running it (IMHO, that is amazing), but it also has the con that it is less expressive (I know, or think I know sometimes, some property holds but you need to express it using the the system) which can be frustrating.