I mean you are kinda right but kinda wrong. To get a proof checker you take a typed lambda calculus and extend it with Pi, Sigma, and Indexed Inductive types while maintaining soundness.

Yes haskell's `bottom` breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.