That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviously, but that's not an expressibility problem, and I wouldn't really equate what remains practical with triviality. With language extensions, you can just kind of do whatever as shown by Liquid Haskell.
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.
You are right, and the first version of my comment had exactly all this hedging (though less educated and sophisticated than your version).
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.
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.
https://hackage.haskell.org/package/type-settheory