[Agda] about `abstract'

[Sergei Meshveliani]

People,
consider the following example.

------------------------------------------------------- M.agda ----
module M where
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Nat using (ℕ; suc)

_+_ : ℕ → ℕ → ℕ
0     + n = n
suc m + n = suc (m + n)

------------------------------------------------------- M0.agda ---
module M0 where
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Nat using (suc)
open import M        using (_+_)

abstract
  +0 : ∀ n → n + 0 ≡ n
  +0 0       = PE.refl
  +0 (suc n) = PE.cong suc n+0≡n  where
                                  n+0≡n : n + 0 ≡ n
                                  n+0≡n = +0 n

------------------------------------------------------- M1.agda ---
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import M  using (_+_)
open import M0 using (+0)

two+0 :  2 + 0 ≡ 2
two+0 =  +0 2


========================================================
1. If I put  M._+_  under `abstract', then  M0.+0  would not type-check.
   Because this proof cannot be constructed only from the signature of 
_+_, it needs to operate with the implementation rules for _+_.

2. The given proof for  two+0  is constructed only from the signature of
   +0.  Hence  +0  can be placed under `abstract' (for this example).

Also I expect that the implementation part for  +0  will not be used
anywhere in type-checking any future client function, the type checker
will be satisfied with the signature of  +0.

Can you imagine the necessity of using the implementation rules for 0+ 
in type checking something?

3. I discover some functions in my application program which 
a) have implementation that would not be necessary for type-checking
   any reasonable future client function (similar as with the example of
   +0),
b) when placed under `abstract' reduce greatly the type check cost of 
   the application.

Am I missing something?

4. My current application consists (approximately) of the modules

   M1.agda ... M20.agda,  M21.agda, M22.agda.

M1 ... M20, M21  are already type-checked, and M22 presents a cost
problem.
Checking M22 takes more than 180 minutes  for  22Gb  heap 
(-M22G option) on a 32 Gb RAM machine 
(I have interrupted it).

M22.g  calls for  (f x),  where  f  is imported from a parametric module
defined in  M21,  f implements a certain equality proof.

If I put  f  (in M21)  under 'abstract', then it is sufficient  
(12 Gb) * (4 minutes)  for type checking M22. 

M22.g  uses many structures and functions imported from M1 ... M21,
and I cannot predict which call is the most expensive when type-checking
g. There are several calls that look as dangerous as  (f x).
So I set `anything' to almost each value defined under `let...in' in  g.
Then -- it is type-checked in 4 minutes. Then I start removing
`anything' one by one. Finally it occurs that only a single call for 
(f x)  is responsible for this enormous type check cost.

Then, I remove `anything', and put  M21.f  under `abstract'. 
(type-checking the calls of  f  it will need only to analyze the
signature of  f).
And this has reduced the type-check cost more than 100 times.

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.

What people would note concerning all this?

Thanks,

------
Sergei