Have you used them? Switching to a language like Agda or Idris is entering the realm of formal verification because the types are so expressive. It's completely different to what most programmers are used to.

Essentially the types being used as so complex the type checker cannot automate the decision about two types being compatible so you have to write maths proofs to help. The types used in mainstream languages are simple enough that the type checker never needs help like that.

The cost of formal verification right now is immense but the benefit is close to bug free code. Mainstream strong statically languages require nowhere near the same amount of effort and give clear benefits over dynamic types.