Comment by ux266478

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.

https://hackage.haskell.org/package/type-settheory