[Agda] yet another grinding reload

[Conor McBride]

Hi Ulf

On 26 Mar 2010, at 04:29, Ulf Norell wrote:

> I just had a quick look and it's termination checking that takes most
> of the time when reloading. We don't do termination checking after a
> refinement (maybe we should),

Well, it surely means refinement can loop.

> so that's why refining the goal works
> and not reloading. It seems that the reason for it taking so long is  
> that
> the term you give is massive after all the implicit arguments are in
> place.

That's quite funny, because there's no recursion in that file.
How expensive would it be to prefix the termination check with a
dumb dependency analysis? Or is that as expensive as grabbing the
call graph?

A bit scary that the blowup is so much. I wonder if there's a way
to notice that these inferred terms can't have recursive references
in them.

How peculiar.

Thanks

Conor

(Hope you're having a good time at AIM XI!)