[Haskell-cafe] Undecidable Instances [Was: Is my code too complicated?]

[oleg at okmij.org]

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).