Accumulate and report multiple errors when possible

[mikeshulman]

With this change, when one "branch" of a definition (e.g. component of a tuple, branch of a match or comatch, field of a record or codata type, or constructor of a datatype) fails to typecheck, instead of bailing out immediately with the error, we save it and continue typechecking the other branches. Any other branches that depend on a previous branch are ignored, as are those that typecheck correctly, but any errors produced by other branches that don't depend on a previous branch are accumulated and reported all together at the end. This way, for instance, if you're defining an ordered pair, you don't have to fix the first component before learning that there's also an error in the second component. For example:

axiom a : A
axiom b : B
def p : A × B ≔ (b, a)

 ￫ error[E0401]
 ￭ interactive input
 1 | def p : A × B ≔ (b, a)
   ^ term synthesized type B but is being checked against type A

 ￫ error[E0401]
 ￭ interactive input
 1 | def p : A × B ≔ (b, a)
   ^ term synthesized type A but is being checked against type B

(where b is underlined in the first error message and a in the second).

Current limitations include:

1. Parse errors and scoping errors can't be accumulated, as parsing and scope-checking happens at an earlier stage than typechecking.
2. Only branches that are syntactically evidently non-dependent on previous ones can have errors accumulated. In particular, a non-dependent sigma-type like Σ A (_ ↦ B) can't be used in the above example; even though the second component doesn't actually depend on the first, syntactically it might. This might be improvable with more laziness.
3. After one error is encountered, we skip all later branches that depend at all on any earlier branches, even if they only depend on branches whose typechecking succeeded. This includes all branches that make recursive calls (unless a different error occurs before encountering the recursive call during typechecking). Improving this would require a very different way of "dependency checking"; currently we just bind the variable/constant being defined to a flag that produces an error if it is ever used.

[favonia]

I want to mention that a similar request was made in RedPRL/asai#160 and I suggested some workaround there. However, given that more than one library user is thinking about the same thing, I am very motivated to come up with a better solution...