[Agda] about `abstract'

[Sergei Meshveliani]

On Mon, 2016-02-29 at 16:27 +0300, Sergei Meshveliani wrote:

> [..]
> 5. Currently I am trying to use _interactive highlighting_ for finding
> the above responsible call. I hope that it will highlight the place with
> "(f x)" in the text of  g  and stand there for a long time.
> If so, then this will reduce this messy procedure with setting/removing
> `anything' (or `postulate') in many places.


No, in this particular example highlighting does not help.
g x =  "let ... in foo",  
where  let-in  defines about 50 values inside it. And I know already
that a single value  v = f x  among them takes more than 99% of the type
check cost.  
And in the segment of  30 minutes < time < 120 minutes  of type
checking, it highlights all the first 2/3 part of this let-in, including
also 11 values after  "v = f x", and stays this way.

With this behavior, it occurs that it is easier to detect the
responsible place by seting `anything' to many values in this construct
and by removing them one by one with restarting `agda'.  

Is there possible some kind of profiling for detecting the place?

Anyway I am amazed by this effect with (f x) and "abstract f", and have
now a hope that the current project can be converted to a code that is
type-checked within may be, 10 Gb * 30 minutes. 

Regards,

------
Sergei