[choeger]

Of course there is a room for pragmatism when it comes to type system. Just lookup the computational complexity of HM inference. But to be useful, the restrictions need to be understood very well. Otherwise your implementation very probably ends up unsound.