Error recovery in the type checker

[brendanzab]

We should be able to run programs that:

• are broken syntactically
• are partially type-incorrect

We should also be able to see more than one type error message.

At the moment we recover from syntactic errors, inserting concrete::Term::Error variants in the places that we fail to parse. But then we blow up if wen try to desugar these into RawTerms. Instead we should probably insert a static-error : {a : Type} -> String -> a function in those places instead...