[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

[eru]

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.