(This PR is basically ready to review on top of #121, but I do want to write a bit more haddock and factor out some common patterns.)
The refactoring in #121, which makes it possible to catch a TypeError and cram the contained diagnostic into a TCWarning, makes it almost comically easy to recover from arbitrary type errors in checkExpr; see deferError. There's a bit of finagling to preserve the Call of the original error but the implementation is basically
deferErrors :: Type -> TCM Term -> TCM Term
deferErrors wanted check = check `catch` \err -> do
warning err
snd <$> newValueMeta wanted
The headline test case is MultipleErrors:
9e6aea7dbb/test/Fail/MultipleErrors.err (L1-L14)
The cost of this is that the "automatically jump to errors" thing in the interaction point was found dead in a ditch: the most common class of errors is no longer caught by the handleCommand handler which called tellEmacsToJumpToError. I would like to believe that this is probably a misfeature anyway and we can support a "go to the next error" explicit command instead.
(This PR is basically ready to review on top of #121, but I do want to write a bit more haddock and factor out some common patterns.)
The refactoring in #121, which makes it possible to catch a `TypeError` and cram the contained diagnostic into a `TCWarning`, makes it almost comically easy to recover from arbitrary type errors in `checkExpr`; see `deferError`. There's a bit of finagling to preserve the `Call` of the original error but the implementation is *basically*
```haskell
deferErrors :: Type -> TCM Term -> TCM Term
deferErrors wanted check = check `catch` \err -> do
warning err
snd <$> newValueMeta wanted
```
The headline test case is `MultipleErrors`:
https://codeberg.org/1lab/mikan/src/commit/9e6aea7dbb095a287875222057789e2cb347c9b2/test/Fail/MultipleErrors.err#L1-L14
The cost of this is that the "automatically jump to errors" thing in the interaction point was found dead in a ditch: the most common class of errors is no longer caught by the `handleCommand` handler which called `tellEmacsToJumpToError`. I would like to believe that this is probably a misfeature anyway and we can support a "go to the next error" explicit command instead.