alt Hacker NewsCorrect. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).
That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.
1. https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf
I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.