[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Mon, 2018-11-19 at 21:44 +0300, Sergei Meshveliani wrote:
> 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
> 

> [..]
> 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?
> [..]


Here is a more interesting example.
Let 
   Pol (R : CommutativeRing) (x : String) 

be a type of polynomials in a variable  x  with coefficients in 
C = Carrier R.

Put the basic coercions as
 
 cToPol :  C -> Pol R x   for any R : CommutativeRing
 cToPol c =  c*x^0 

 polZ->polQ :  Pol Integer x -> Pol Rational x  
 polZ->polQ =  
            map each coefficient as  \c -> c /' 1

For  x : String,  1, 2 : Integer, what does it mean

                  1 * x^3  +  1 /' 2     -- (E) 
?
In this case the goal type is not declared.

The first  summand belongs to  Pol Integer x,
the second summand belongs to  Rational.
Both summands need to be lifted to some `minimal' type where some
instance of _+_ is defined. 

The coercer method finds that 
* the first  summand is coerced by  polZ->polQ  to  Pol Rational x,
* the second summand is coerced by  cToPol      to  Pol Rational x,
* the composition of these two coercions converts (E) to a valid   
  expression
             (1 /' 2) * x^3  +  (1 /' 2) * x^0     -- (E') 

In real programs it can be written

                    x  +  1 /' 2,

and it will be first converted to  (+ 1) * x^0  +  (+ 1) /' (+ 2).


Regards,

------
Sergei