[Haskell-cafe] Is it possible to do type-level arithmetic without UndeciableInstances?

[Paul Johnson]

This is a bit beyond my normal level of expertise, but if I understand 
it correctly the type checker is normally limited to type functions that 
are "primitive recursive" 
(http://en.wikipedia.org/wiki/Primitive_recursive_function).  This means 
that they are guaranteed to terminate, but on the other hand the 
resulting language is not Turing complete.

Setting UndecidableInstances lifts the Primitive Recursive restriction, 
making the type checker Turing Complete, but also creating the potential 
for endless loops.

So yes, you can do type arithmetic without UndecidableInstances, 
provided you limit yourself to the Primitive Recursive axioms.  The 
Wikipedia page lists them, and turning them into Haskell type classes 
shouldn't be more than a few milli-Olegs.

Paul.