[Agda] using `abstract'

[Sergei Meshveliani]

People,

I am trying to understand of whether the `abstract' construct can be
sensibly used in application.

1. Last 2 years I complained several times on that `abstract' is allowed
almost nowhere in my program.
But today the situation is changed! 
I have tried to put `abstract' to many proofs, and it is type-checked.
I am not sure, but the impression is that mainly it is allowed now
(in Agda 2.4.2.4).

2. I have reported an example of ``abstract case ...'' which probably
presents a bug.

3. I wrote earlier that many proofs can be put under `abstract', and
that this will hopefully reduce the type check cost. 

May be this will reduce the cost.
But I need to understand: what possibilities will be lost?

Consider an example:

  abstract
    lemma : ∀ {m n : ℕ} → m ∸ n ≡ 0 → m ≤ n
    lemma {0}     {_}     _     =  z≤n
    lemma {suc m} {0}     ()
    lemma {suc m} {suc n} m∸n≡0 =  s≤s $ lemma {m} {n} m∸n≡0

What important possibilities are lost by putting it under `abstract' ?

For example: let  
                  2∸4=0 : 2 ∸ 4 ≡ 0.
Then, 
      p = (lemma 2∸4=0)  : 2 ≤ 4,

and this is achieved by using `lemma' as abstract.
Here  p  occurs an _unknown value_ of type  2 ≤ 4.
Right?

If `lemma' is not under `abstract', then the program can analyze what
precisely the construction of  p  is,  for example, how many  s≤s  has
it in its value.
Right?

In what scopes/modules `abstract' will has its effect in applying this
`lemma' ?

Can it really happen that a client function will not be satisfied with
this particular abstracted `lemma' ?

If such clients have sense, then consider the following suggestion.


4. Suppose that the Language allows ``applying as abstract''
   and also ``applying as concrete''
   -- instead of declaring a function being `abstract'.

For example:

    p =  lemma 2∸4=0
    <do something with  p>

    p' = (abstract lemma) 2∸4=0
    <do something with  p'>

The word `abstract' is not in the declaration of `lemma', but it is set
at the place where `lemma' is applied.
The first call of `lemma' applies the concrete version, and the second
call applies the abstract version.

This is on the user program decision: where the abstract version is
sufficient and where is not. It depends on the situation, on the meaning
of the program fragment.

Is it true that `abstract' needs to be a way of applying a function
and not a way if declaring it?

Can somebody, please, explain the subject?
  
Thanks,

------
Sergei