[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Wed, Oct 03, 2012 at 01:47:08AM +0200, Andreas Abel wrote:
> When I try to load your example, I get a "stack overflow".  So it is not  
> a problem of the compiler, but already type checking fails.

Does type check constitute an essential part of compilation?

> I found the problem:
>
> > zs = merge xs ys
> >
> > hl : List Nat
> > hl   with zs
>
> If you "with" an expression, like "zs" here, it is normalized.  This  
> means that Agda has to compute the list of length 16000, with (in this  
> case possibly inefficient) call-by-name evaluation strategy.
>
> That can well blow the Agda type checker.
>
> It is advisable to avoid "with" in this case.
>
> -- this works
> bla : List ??? ??? List ???
> bla [] = []
> bla (z ??? zs') =  z ??? (last $ fromL z zs') ??? []
>
> hl = bla zs


But  bla zs =  bla (merge xs ys),

and  merge  and  bla  have explicit evaluation rules, and there are
explicit rules for constructing  xs and ys.
So,  bla zs  will be normalized at compilation time, as soon as the 
compiler sees all these rules (clauses).
Why there is a difference in normalization in `with' and in the two
patterns for  bla ?
Or may be, I do not know what is normalization in Agda.

Regards,

------
Sergei