Indent terms printed in typechecking errors

This should make errors more readable, i.e. instead of printing:

    Can't unify <SOME_LONG_TYPE> with <SOME_OTHER_VERY_LONG_TYPE>

this change makes it print

    Can't unify
        <SOME_LONG_TYPE>
    with
        <SOME_OTHER_LONG_TYPE>

and similarly for other errors.
Fix bug in compilation of optimised Nats
Finished proof-reading implementation paper
Partially defined names should not reduce at compile-time

This has been the spec for a long time, but wasn't implemented fully since
the totality checker wasn't strong enough to find some obviously total
things. This is now switched on --- functions are checked for totality
after every mutual block, or every individual function (if not mutual).