Idris barely made it out of experimental status and was dog-slow. Not sure when you'd choose that over Haskell for production software.
I was thinking more along the lines of dependent types, because the kinds of problems where you'd really really need strong static types overlap with the need for dependent types, which Haskell has some support for (and Ocaml but less so).
But if I needed to prove something I'd probably do it in Coq since it interops with Ocaml fairly well.