Refactoring elab exception handling

The Lean.Exception type used during elaboration comes in two flavors: errors and internal exceptions

/-- Exception type used in most Lean monads -/
inductive Exception where
  /-- Error messages that are displayed to users. `ref` is used to provide position information. -/
  | error (ref : Syntax) (msg : MessageData)
  /--
  Internal exceptions that are not meant to be seen by users.
  Examples: "postpone elaboration", "stuck at universe constraint", etc.
  -/
  | internal (id : InternalExceptionId) (extra : KVMap := {})

At the time of writing, the internal exceptions are

builtin_initialize postponeExceptionId : InternalExceptionId ← registerInternalExceptionId `postpone
builtin_initialize unsupportedSyntaxExceptionId : InternalExceptionId ← registerInternalExceptionId `unsupportedSyntax
builtin_initialize abortCommandExceptionId : InternalExceptionId ← registerInternalExceptionId `abortCommandElab
builtin_initialize abortTermExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTermElab
builtin_initialize abortTacticExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTactic
builtin_initialize autoBoundImplicitExceptionId : InternalExceptionId ← registerInternalExceptionId `autoBoundImplicit
builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
builtin_initialize checkAssignmentExceptionId : InternalExceptionId ← registerInternalExceptionId `checkAssignment
builtin_initialize outOfScopeExceptionId : InternalExceptionId ← registerInternalExceptionId `outOfScope
builtin_initialize congrHypothesisExceptionId : InternalExceptionId ← registerInternalExceptionId `congrHypothesisFailed
builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter
builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExceptionId `delabFailure
builtin_initialize analyzeFailureId : InternalExceptionId ← registerInternalExceptionId `analyzeFailure

As documented, internal exceptions are mainly about visibility. Note however that this usage is not enforced by the API: as try catch etc catch any Exception, it is very easy to accidentally catch internal exceptions as well and e.g. add them to the log (where they will be printed as "internal exception: ...").

While errors can/should generally only be handled generically such as by putting them into the log, internal exceptions give an easy and efficient way to be handled case by case via the exception ID. An interesting question is whether they in turn should never be handled in a generic way; some names like abort* certainly imply that they should never be caught except by the specific code handling them, but for others we should make sure there are no cases where e.g. generic backtracking logic is supposed to catch them (very quick review: Term.observing and Elab.App make sure not to backtrack on generic internal exceptions but Elab.Match does not). If this is indeed the expectation, it would be good to ensure this in the API by leaving internal exception catching to catchInternalId(s).

To complicate matters, there is one more kind of exception used in the code: "runtime exceptions", which currently consist of heartbeat and max rec depth exceptions (see Exception.isRuntime). They are encoded as errors but a comment mentions this is mostly because of module dependencies. On the one hand, they are handled individually in some cases so having an internal exception ID would make sense; on the other hand, they are clearly user-visible. So it might be the case that this is better handled by giving errors an ID as well which we will want at some point for purposes of an error index.

One special handling of runtime exceptions is that they in fact are not caught by CoreM try-catch by default (but are in CommandElabM, unclear to me whether that inconsistency should exist). This behavior can be turned off with a flag but it turns out that both uses of this flag follow the exact same pattern:

     withCatchingRuntimeEx
       try
         withoutCatchingRuntimeEx do
           tryBranch
       catch ex =>
         if ex.isRuntime then
           runtimeBranch
         else
           throw ex

So as a first refactoring, the flag could be replaced with a new combinator, changing the code to

tryCatchRuntimeEx
  tryBranch
  fun ex => runtimeBranch

For context, this all came up because in #3940, I fixed elab interruption (checkInterrupted) to never be caught inside the elaborator, which raised the questions above for the existing exceptions.

In summary, possible refactoring steps to be done here:

• replace with(out)CatchingRuntimeEx with new tryCatchRuntimeEx combinator
• (unclear) make try-catch ignore internal exceptions (and not just interrupt and runtime exceptions)
• (unclear) make runtime exceptions internal exceptions

Start with Lean.Exception, Exception.isRuntime, and the try-catch APIs, then inspect the mentioned CoreM and CommandElabM behavior plus Term.observing, Elab.App, and Elab.Match. Resolve whether internal and runtime exceptions should be caught generically, and make the resulting handling consistent across these entry points; the completed refactoring and documented exception policy define done.