[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Mon, 2018-11-19 at 20:18 +0100, Guillaume Brunerie wrote:
> It seems like there are non-trivial interactions between implicit
> coercions and instance arguments.
> For instance if you have an implicit coercion inj : N -> Q, and n m :
> N, then what is n + m : Q supposed to mean?
> Is it inj (n +_N m) or is it (inj n) +_Q (inj m) ?
                                                                    (I)

> Of course in that case they are both (propositionally) equal, that’s
> why a mathematician is happy with it, but which one should Agda
> choose?
> 

Different sequences of basic coercions having the same result.
This also means different evaluation _algorithms_ for run-time.
And these algorithms may have a very different _cost_.

For example, for  n : Bin 
             
    (n * n) modulo 2  =mod_2=  (n modulo 2) *m (n modulo 2),      (II)

but the left-hand side method can be many times more expensive than the
right-hand side.

In classical mathematical books, authors do not care of the evaluation
cost.
But the programmer must care.
The programmer must understand the danger in each particular case, and
when there is a risk, one needs to set _explicit_ coercion in-place.

Thus, for (I), I would write      n + m : Q  

carelessly (is Q = Rational ?), and let it coerce as it can. 
And for (II), I would write
                      noCoercion ((n mod 2) * (n mod 2))

(there can be a default agreement, or some small sign for denotation).

Also imagine that the interactive type checker could list the found
sequences of basic coercions, with suggesting to choose by pointing to
No. 

Many years ago I programmed in Axiom interpreter and in the Spad
language of Axiom (it is a compiled language).
I was giving to Axiom expressions, and they where coerced. I do not
recall how precisely it was, studying coercion (there is also
"conversion") was not my subject. But my impression there was that 
a) coercion helps, b) I always can avoid unneeded coercion. 

I am not sure, probably coercion/conversion is not a part of the Spad
compiler. May be this is a part of the interactive shell of the Axiom
system.

I suspect that for Agda, it could be implemented as a part of a library
(I may mistake) written in Agda and being used in the interactive mode
and also in automatic type checking.

Regards,

------
Sergei