Ertugrul Soeylemez wrote:
Essentially UndecidableInstances turns the type system into a Turing-complete programming language. One direct consequence is that type checking may not terminate
Actually, the type checking (specifically, instance resolution) always terminates, due to the recursion depth limit. When the type checker hit the limit, one can't generally say either it is because the program is ill-typed or the program is well-typed but needs a bigger limit. In practice, it is usually quite easy to tell the difference. The trace emitted by GHC helps. I'd like to emphasize however that UndecidableInstances is only a sufficient condition of a decidable type checking -- but by no means necessary. There are many good, type-decidable programs that are not accepted without UndecidableInstances. One of the simplest examples is shown in http://okmij.org/ftp/Haskell/types.html#undecidable-inst-defense The situation with UndecidableInstances seems similar to the primitive recursion criterion: all primitive recursion functions surely terminate; non-primitive recursion functions generally don't. That is not the reason to disregard the latter: There are many classes of non-primitive recursive functions that are total. To see that, one has to use more complex criteria. The added complexity is not worthwhile as far as GHC is concerned (The tradeoff is different in Agda, where the added complexity of more powerful termination checkers may be worthwhile).