#127 Z/EVES typechecker loops with recursive typechecking

[Andrius Velykis]

If the "check recursive types" option is selected, Z/EVES typechecker loops when typechecking proofs with undefined/domainCheck names. If the proof references another lemma, the typechecker does not complete and CZT hangs.

A simple example to reproduce:

\begin{schema}{NAME}
  x : \nat
\end{schema}

\begin[disabled]{theorem}{rule lemmaTest}
  \forall x: \nat @ true
\end{theorem}

\begin{zproof}[NAME\$domainCheck]
  with enabled (lemmaTest) rewrite;
\end{zproof}

The issue appears with domainCheck proofs. It also manifests for proofs without theorems, e.g.:

\begin[disabled]{theorem}{rule lemmaTest}
  \forall x: \nat @ true
\end{theorem}

\begin{zproof}[unknownProof]
  with enabled (lemmaTest) rewrite;
\end{zproof}

[Andrius Velykis]

Added a workaround in b7e7664d3e0649dfa3c08efc45105fc642c90be6. Now direct loops (ID to itself) are ignored when calculating order of recursive types.

The issue should also be fixed to avoid such UndeclaredAnns being generated altogether..