Graceful error handling of erroneous terms.

1. Additional info for type-checking. During type-checking of a term we pass a path to the term. So if a term is not well-typed, we produce an error with the path to this sub-term. Next, on the REPL top level we know which meta-term was checked, and we are able to extract corresponding meta sub-term. Next, since meta-terms have positional information, we are able to locate erroneous term directly in the user input (REPL or file).
2. Different display of errors depending on a console. If console is ASCII console, we highlight erroneous terms. Otherwise, we put a special mark (▶) at the beginning of the erroneous term.
3. Downside: type-checking becomes slower.