A conversion fast path using normalisation by evaluation. Evaluation keeps neutral spines with lazy unfoldings and compares them with one-step η for functions and pairs. Convertible accepts the comparison; DontKnow leaves it to ordinary unification.

Constructs whose reduction depends on the tope context or modalities, and holes, abort this fast path. Extension types and recBOT are compared structurally. See the conversion, soundness and attribution notes below.

nbeConvertible evaluates both sides into a value domain with closures (sharing by construction: a definition's value is evaluated once per occurrence, not once per copy, and Haskell's laziness makes the evaluation call-by-need) and compares the values structurally, with one-step η for lambdas and pairs mirroring etaMatch. Evaluation is emph{glued}: a spine over a definition keeps the spine as well as its unfolding, and the unfolding is lazy. Two spines over the same definition are then compared argument by argument, without unfolding it. Only where the spines disagree is an unfolding forced.

It answers only Convertible or DontKnow, never a definite inequality, so a caller falls back to the ordinary unification on DontKnow. The two cases are not opposites, which is why the answer is not a Bool. NbE can accept comparisons that ordinary unification rejects: pairwise application decomposition can create subgoals that βδ-equal applications need not meet (see unifyViaDecompose).

The evaluator is a pure function of the Context: valueOfVar is a plain reader-only lookup, and fresh variables for comparing closures are de Bruijn levels (HFresh), so the foil scope machinery is never extended and no quote function is needed.

Soundness is a subset argument: Convertible is answered only for terms that are βδ-convertible up to α and the one-step η above, with every construct whose reduction consults the context — recOR guard selection, holes, the modal constructs — evaluating to an opaque VAbort that poisons the comparison into DontKnow. Extension types and recBOT are compared structurally (see the note at their eval case): a structurally identical pair of restricted types is also accepted by the ordinary unification, through reflexive coverage and the cross-face coherences already proved at formation. The soundness claim concerns definitional equality, rather than the comparisons accepted by the previous unification algorithm.

None of the underlying techniques are ours. Semantic conversion checking — evaluate both sides into a value domain with closures and compare the values, applying functions to fresh generic values — is the algorithm of Coquand, An algorithm for type-checking dependent types (Science of Computer Programming 26, 1996), the implementation-level core of normalisation by evaluation (Berger and Schwichtenberg, LICS 1991).

Comparing two stuck terms by their spines, head first and arguments pairwise, rather than by normalising them, is the algorithmic equality of Abel and Coquand, /Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs/ (Fundamenta Informaticae 77(4):345–395, 2007; TLCA 2005), see https://www2.tcs.ifi.lmu.de/~abel/lfsigma.pdf.

The representation we use for it is the emph{glued evaluation} of András Kovács' smalltt. Its README states the tension as "in basic conversion checking, we want to evaluate as efficiently as possible; in quoting, we want to output terms which are as small as possible". It resolves the tension by evaluating a top-level variable to "values which represent lazy ('non-deterministic') choice between unfolding the definition, and not unfolding it". Following smalltt, conv also speculates: "whenever we have the same top-level head symbol on both sides, we try to unify the spines", and unfolds only when that fails. smalltt separates its modes and uses gluing for quoting small terms as well. This module has no quote function, so it needs neither. The general implementation shape, environment machines with closures and de Bruijn levels for fresh variables, follows the same author's elaboration-zoo.

For the fragment this module deliberately aborts on (tope-indexed reduction such as recOR), the template is cubical: Sterling and Angiuli, Normalization for Cubical Type Theory (LICS 2021), and its implementation lineage in cooltt.

What is specific to rzk is only the packaging: the all-or-nothing gating (Convertible or DontKnow, never refute), and VAbort poisoning of the context-sensitive fragment so that the fast path stays sound by a subset argument.