Functionality testing will tell you when you've failed to encode an invariant in your type, and there's a good chance that the reason you failed to is just that it's more effort than it's worth. Else we'd all be writing proofs for every program in Coq.
In practice, as I alluded to in my previous post, you really want types combined with broad functionality testing across a range of scenarios. You really don't want to be relying on "it compiles, I assume it works" unless you're able to back out of a deployment in seconds when it doesn't.
Some things are probably not worth typing, but if they're not worth typing they're not worth testing either. Whatever your target defect rate, the most efficient way to hit that target is using types.
Sure there is. Stop testing random bits of internal functionality, start testing huge modules with well-known (semi-public) APIs, or your entire program, and combine that with a ~reasonable~ type system. You want full-system testing. You don't need a whole lot of tests to be sure "it's basically working", and it's a lot easier to turn repeatable bug reports into tests.
When you inevitably break a piece of functionality despite your types, you might not know precisely how it broke, but at least you know it's broken without a customer calling you up. And every time a customer does call you up, you can add a full-functionality test - "this is what the user did, and this is what I expect from that".
Every other engineering branch backs up good practices and solid math with lots of testing. So should we, types or no types.
Types are awesome. Languages like Rust give them to me without having to learn a ton of theory. However, eventually, I realise that my types have boxed me into a certain design - and I need to refactor heavily, which involves rewriting a large chunk of my types which I was relying on to show me that my code was correct.