This is also an issue in Dependent Types. But the case is not as clear cut as you paint it as some argue that the expressibility lost and complexity gained in t

This is also an issue in Dependent Types. But the case is not as clear cut as you paint it as some argue that the expressibility lost and complexity gained in the system by forcing type checking to terminate is not worth it in practice. http://www.seas.upenn.edu/~liminjia/research/papers/lambda-eek.pdf http://www.seas.upenn.edu/~liminjia/research/papers/lambda-e...