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.