[Agda] Agda crash caused by excessive unfolding

[takeyama]

Hi Thomas,

(Sorry for the delay, as usual.)

  > But i#103 is defined by a simple "open P2 use i", so it doesn't look 
  > like it would be too hard to keep track of the fact that i#103 can be 
  > used refer to i#90. Any chance that Agda could be improved to do that?

Yes, but: I have tried the most naive slow way of comparing every
constants in scope with the constant about to be unfolded, as it
required no additional data to be kept.  Your particular example
prints out fine, but I know my current trial implementation is wrong
in certain respects and can't be committed.  I will try somemore
during TYPES Summer School.

Best Wishes,
Makoto
-- 
Makoto Takeyama
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052