[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Sun, 2018-11-18 at 21:35 +0100, Ulf Norell wrote:
> On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo
> <m.escardo at cs.bham.ac.uk> wrote:
>         
>         You will not solve the shortcomings of my mathematical style
>         by refusing 
>         to implement implicit coercion in Agda.
> 
> 
> I feel that the discussion has derailed a little at this point. The
> issue isn't that some people
> are stubbornly refusing to implement this one simple thing that would
> make life easier for
> the practising mathematician. The problem is that implicit coercions
> are very difficult to get
> right. 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
> 

See my example with `record Coerce ...' in my last letter.
May be the first step can be
 
  "record Coerce ..." 
  + 
  allow overlapping instances with choosing among the overlaps the 
  instance most special by substitution.
  +
  may be, trying to implement things in Agda as a library
  (can Reflexion be used?).


About implicit instances:
I use

-------------------------------------------------------
 open Group {{...}}
 instance _ = G
          _ = G'

 preservesInversion :
   (mHomo : MonoidHomomorphism)
   (let f = MonoidHomomorphism.carrierMap mHomo) (x : Carrier) →
                                                 f (x ⁻¹) ≈ (f x) ⁻¹

 preservesInversion (monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) 
                                                                  x =
   begin
    f x'                     ≈⟨ sym (∙ε fx') ⟩
    fx' ∙ ε                  ≈⟨ ∙cong2 (sym (x∙x⁻¹ fx)) ⟩
    fx' ∙ (fx ∙ fx ⁻¹)       ≈⟨ sym (assoc fx' fx (fx ⁻¹)) ⟩
    (fx' ∙ fx) ∙ (fx ⁻¹)     ≈⟨ ∙cong1 (sym (f∙homo x' x)) ⟩
    (f (x' ∙ x)) ∙ (fx ⁻¹)   ≈⟨ ∙cong1 (f-cong (x⁻¹∙x x)) ⟩    -- 119
                                                      -- 
    f ε ∙ (fx ⁻¹)            ≈⟨ ∙cong1 f-preserves-ε ⟩
    ε ∙ (fx ⁻¹)              ≈⟨ ε∙ (fx ⁻¹) ⟩
    (f x) ⁻¹
  ∎
  where
  x' = x ⁻¹;   fx = f x;   fx' = f x'
---------------------------------------------------------

The example uses only Standard library for algebra.
Many operation occurrences here are overloaded, 
and this removes a lot of garbage in denotation.

Currently I have a report
"(Group.Carrier G) !=< (Group.Carrier G') of type (Set α)
when checking that the expression x has type Group.Carrier G'
"
and hope to find the thing and to fix the program.

Regards,

------
Sergei