Bugs in the typechecker are rare (it's widely exercised if the language is at all popular) and generally fixed quickly. If you have an expression of type A you can be pretty confident you're getting a value that's passed through a constructor for type A.

Can a human encode something different by that than what they intended to encode? Certainly. But it's got the highest cost-benefit of any approach to double-checking your code I've found.

That's not what I mean. It's trivial to encode your types in such a way that it incorrectly implements domain logic and there is no meta-meta language enforcing correctness there.

How so? To the extent that you use your types with your code, getting your types wrong will lead to either type errors in correct code (in which case you notice and fix them) or overly loose types that will allow incorrect code to pass (in which case you don't get an actual bug unless you make a corresponding mistake in your code).