Represent typechecking errors as annotated terms

[robrix]

Annotating terms with typechecking errors in the failure case yields a tree describing the failure with precise reference to the nodes in error.

This can also be driven interactively as a means of refining ill-typed into well-typed terms.

[robrix]

We could represent this with AnnotatedTerm<Either<Error, Term>> or something more like Free<Expression<Free>, Error> (PartialTerm might be a better name than Free, by analogy with AnnotatedTerm vs. Cofree).

[robrix]

PartialTerm would best represent cases where some subtree is ill-typed. That might preclude the discovery of well-typed sub-subtrees.

AnnotatedTerm would allow us to express this better, at the expense of having to traverse the entire thing to discover the errors.