[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Sun, 2018-11-18 at 21:35 +0100, Ulf Norell wrote:

> [..]
>  To move this discussion forward I suggest that you give some of the
> following:
> 
> 
> - concrete examples of implicit coercions that you'd like to see
> - a rough sketch of how they are to be solved
> - references to the proof assistants that (in your opinion) have
> gotten implicit coercions right
> - some notes on why instance arguments are not a good replacement for
> implicit coercions


1. Examples are given in the book about a library for computer algebra
   "Axiom. 30 years horizon", 
   Chapter 2.7:  coercion, conversion ... There are given examples.
   It is on the Web.

2. Nicolas J. Doye. 
Automated coercion for axiom.  ACM journal, 1999.  
It is on the Web.

This paper looks like a foundation for an algorithm to find coercion.
I never tried to understand it.

3. May be, algebraic libraries in Coq develop coercion. 



> some notes on why instance arguments are not a good replacement for 
> implicit coercions


Suppose that Rational is represented as  n /' d,  n, d : Integer
(let us forget here of d /= 0).
Consider
            a :  Rational
            a =  2 + (1 /' 2)            -- (E)
 
To which types each part of (E) needs to be mapped, and how,
so that to obtain a valid expression of type Rational 
to be type-checked?

By implicit instances, _+_ can be resolved to _+r_ -- addition on
rational numbers.
But Agda will report an error, because 

   2  is not in Rational,  1 and 2 are not in Integer.

Some method needs to guess how to coerce (E) to the subsumed expression 
    
            ((+ 2) /' 1)  +  ((+ 1) /' (+ 2))

And the rest is by instance resolution for _+_.
Here 2 first transforms to  (+ 2),  and then to  (+ 2) /' (+ 1).

Mathematicians and engineers write (E) with subsuming this coercion.

The basic coercions are declared and defined in the user program.
For Agda, they can be set, say, as instances of the Coerce class,
why not?

In this example, basic coercions are
   n : Nat      ->  (+ n)       : Integer, 
   x : Integer  ->  x /' (+ 1)  : Rational.

The solver needs to find a chain of basic coercions that satisfy the
goal type and also is type-checked.

Can implicit instances for _+_ be set so that the current Agda to
type-check (E) ?
I think, they cannot. So that implicit instance arguments do not cover
coercion.
Am I missing something?
 
Regards,

------
Sergei