clarify meta variables in error messages

[gelisam]

A type error like

Expected
  ((META(MetaPtr 8524) → Bool) → (META(MetaPtr 8512) → META(MetaPtr 8403)))
but got
  ((META(MetaPtr 8524) → Bool) →
   ((List META(MetaPtr 8524)) → (Maybe META(MetaPtr 8524))))
Specifically, Syntax doesn't match (List META(MetaPtr 8524))

Is pretty hard to read. Let's do like GHC and pick short names for those meta variables, like this:

Expected
  ((a → Bool) → (b → c))
but got
  ((a → Bool) → ((List a) → (Maybe a)))
Specifically, Syntax doesn't match (List a)

Now that the error is readable, we can actually see a more important problem: we didn't even replace the meta variable b with its value Syntax, thus resulting in a seemingly-inconsistent error message!

[david-christiansen]

The current structure of the type checker is that it stops when it encounters a single unification failure, which is why there are unsubstituted metas (that would have been solved by subsequent unifications that would succeed).

It would be very good to make as much progress as possible, instead of stopping, and to show multiple errors at once. There are some features of Klister that make this more challenging than in something like ML or Haskell, however - the structure of the type checking computation depends more on prior data. In particular, a type error in a macro means that we should not attempt to execute the macro, which may mask some later errors.

So there's two problems here. The easy one is to assign a more readable notation for underdetermined metas. I don't want to do "a b c", just because we may end up with clashes with user-assigned type variable names, but some other notation to distinguish them would be nice (maybe with \langle and \rangle around them, like we did in the TyDe slides). The hard one is to figure out the right way to deal with errors - I think replacing the macro's value with a special value that indicates the macro can't run should be enough, but we have to be careful because it's really type errors in the transitive dependencies of the macro that make the problem.

[david-christiansen]

See also #49 for a partial attempt at this stuff.