[Agda] Agda mysteriously hangs

[Josh Ko]

Hi,

We have been working on encoding concurrent processes with simple
session types in Agda, and come up with a datatype for coinductive
process terms, which is heavily indexed with typing contexts. We
have followed the locally nameless approach [1], which means there
are both free and bound channels, represented by strings and (safe)
de Bruijn indices respectively. One key operation is abstracting
a free channel to a bound channel, whose implementation requires
a lot of typecasts (rewrites) all through the code and is hard to
be put into a form of guarded recursion (our process terms are
coinductive). We decided to turn off the termination checker at
least for the moment, so we can carry on to some other proofs.
The strange thing is: if we do not add

  {-# OPTIONS --no-termination-check #-}

at the top of the file, then the typechecker stops and the function
is highlighted as non-terminating, which is expected. If the option
is turned on, however, the typechecker just hangs. Now if one leaves
any hole in the file (with the option still turned on), say appending

  dummy : ℕ
  dummy = {!!}

at the end, then the typechecker stops again. Is there an explanation
for this phenomenon? I have put the relevant files at

  http://w.csie.org/~b94087/EvenMoreHeavilyIndexedSyntaxRevisited/

and the problematic function is called abs in the file DTerm.agda,
which can take a long time to load even if the --no-termination-check
option is off or a hole is left. The version of Agda is the most
recent development version pulled from the darcs repository.

Thanks!

-- JK


[1] Aydemir et al. Engineering Formal Metatheory. POPL '08.
    http://doi.acm.org/10.1145/1328438.1328443