[Agda] Chapter "Traps"

[mechvel at scico.botik.ru]

Dear Agda developers,

I know that this is a known problem, but I recall of it because
probably it bites many people. The type checker reports of
the function

   f : (n : ℕ) → n ≢ 0 → ℕ
   f 0             0≢0 =  contradiction refl 0≢0
   f (suc 0)       _   =  1
   f (suc (suc n)) _   =  suc (f 1+n 1+n≢0) where
                                            1+n = suc n

as of not terminating.
The programmer has to guess to replace "1+n" with "suc n".


Probably Agda docs needs the chapter "Traps"
visible somewhere on the top.

There are many of them besides this one.
Here is fresh for me trap of of which I have been bitten:
In Haskell, I wrote

   f x =  let y = g x in h y y     (I)

instead of  f x = h (g x) (g x)
in order to make sure that (g x) is computed only once.
In lambda calculus, it is substituted as (h (g x) (g x)).
I do not know whether the Haskell language specifies sharing for (I),
but I expected that most Haskell compilers support sharing in (I):
they compile (I) so that  y  is shared and is computed only once.
Right?

And it occurs that Agda does not support sharing in (I).
As in my particular example the construct of the type (I) is recursive,
and deals with a large data, the evaluation "exploded".
Thanks to Ulf Norell who has pointed me to the effect of (I).

Another trap:  proofs for a function constructed with 'let', `where', 
`with', `case'.
Very often one needs to replace them with a new function which is moved 
to the top
of the scope.

Another trap:  there are many cases when it is not practically possible 
to separate
evaluation of a function  f  and proofs for its main properties.
In such a case one needs to mix "evaluation" and proof constructing in 
one loop,
and to take care of performance.

There are certain traps causing the type check cost explosion, and so 
on.

Regards,

------
Sergei