Improve pretty-printing

 * Dependent pairs are properly highlighted as either constructors or
   types
 * Names bound in dependent pair types show up as bound in their scope
 * Error messages use the included error context to properly highlight bound variables
 * Error contexts are shown with semantic colors

Fixes #855 and #862.