Implementation of conversion checking errors which can reify part of the context leading to the actual failure as terms.

Conversion checking errors are initially thrown (by failConversion) in the floating state, which means they can accumulate information on where they happened as the call stack unwinds. This information will be presented to the user by wrapping the actual mismatched terms in a skeleton of the term where the mismatch happened. These terms had better not be nonsense! This requires that recursive calls within the conversion checker cooperate with the reconstruction process, using the functions in this module. Their use can be summarised as follows:

• A recursive call to compare a subterm of a normal form should be guarded by addConversionContext.
• A recursive call to a domain-specific conversion checking function which takes the input terms apart using a nontrivial view (e.g., equalLevel) should be guarded by nowConversionChecking.
• A recursive call under an application of a nontrivial substitution to the context and terms under consideration should be guarded by cutConversionErrors.
• Recursive calls that preserve the definitional identities of the terms under consideration do not need any special handling.

The goal of these rules is to allow for the user to pretend that conversion checking works by normalising then checking for syntactic equality: the reconstructed term should wrap the actual mismatch in "hereditary neutrals (to the left)", i.e. everything that compared equal on the way to the mismatched terms is normalised, but parts of the term that are beyond the mismatch are left as-is (and, in the future, will be presented "deemphasized").

How much of the context to reify is a design parameter that can be tuned. At the moment, we drop all ConvLam, ConvDom, ConvCod and visible ConvApply from the front of the zipper. Regardless, the conversion checker must be set up as if the entire context will be reified.

The ConversionZipper reflects recursive calls made to conversion checking of the immediate subterms of a normal form, and it can handle most cases of a recursive call happening in a weakening of the current context as well. However, some conversion-checking functions take the input values apart in nontrivial, type-specific ways before eventually calling into "ordinary" term conversion checking again.

If a floating ConversionError happens in one of these eventual calls, the reified call stack will not have anything corresponding to the value that got taken apart; this can result in the terms presented to the user being ill-typed (see testFailConvErrCtxLevels for an example). These calls can be handled in two ways, depending on whether or not preserving the surrounding context is likely to be useful in an error message. Here are examples of using each:

• Calls to equalLevel are likely to happen while checking hidden arguments to a defined symbol (e.g. a universe-polymorphic data type), which is a context worth preserving for error messages: telling the user l != l' is significantly less useful than telling them List {l} A != List {l'} B.

  Therefore, the call to equalLevel in equalTerm' is guarded by nowConversionChecking. If an error happens while conversion-checking some levels, the mismatched terms will be replaced by the (normalised forms of) the entire levels that were being compared.

• On the other hand, conversion checking of partial elements involves nontrivial modifications to the context, and, more importantly, generally happens to terms which display quite terribly before these substitutions are applied, often involving eta-expanded extended lambdas and the primitive primPOr. Subjectively, it's less useful to say that conversion checking failed for the hard-to-read system than it is to say that it failed for a particular face.

  For these reasons, compareTermOnFace (really, forallFaceMaps) uses cutConversionErrors to turn any floating errors from conversion-checking the faces into Finished errors, which no longer accumulate context. Whatever context was collected inside the face comparison will be preserved, but we will not remember that (or where) the partial elements were being compared.