Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.
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.