These strong types will always be somewhat cumbersome, because they are the proof that your program is correct in certain respects, and non-trivial proofs are not free. When you hear someone use the phrase "correct by construction," you should ask you do when you accidentally construct the wrong thing. I'm afraid the answer is that you "correct by reconstruction."
