I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.
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
It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.
I can see the real pain point more being the fact that it's not like a typical proof assistant, and utilizing it as one is going to be unintuitive and strange.
When I said 'Haskell', I really meant 'vanilla Haskell a sane person might want to write'. Similar to how C++'s type system is fully Turing complete, but you shouldn't use it that way.