All this coq 'n agda stuff won't produce anything of practical value to software engineering before the singularity arrives. Haskell is already too much for practical work, ocaml's near the perfect typed language point.
Have you tried ocaml. Haskell keeps moving, takes much longer to get to grips with, and most users don't use all it's features (which keep growing). Meanwhile you can get your head around all of ocaml pretty easily and it gives you no surprises. Ocaml is for coders, haskell's for grad students.
this formal methods shit has been going for decades and will do so for decades more being hardly used by anyone, by which time the singularity will arrive and nobody will need to program