[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

On 2020-11-28 16:12, Sandro Stucki wrote:
>> 
> 
>>> The workaround is to wrap the direct definition in a data-type or
>>> record. That requires some extra constructors/projections to
>> convert
>>> between direct proofs of equality and the wrapped ones, but the
>>> problem with implicit arguments seems to disappear.
>>> 
>> 
>> In my example with Fraction and Prefraction (in my last letter)
>> everything looks wrapped enough, I do not know what kind of wrapping
>> do you mean.
> 
> Your definition of _=fr_ is not a data type or record. It's exactly
> the sort of definition I was referring to, where one relation is
> defined in terms of another, via computation.
> 
>    _=fr_ :  Rel Fraction α=
>    f =fr g =  (num f * denom g) ≈ (num g * denom f)
> 
> Have a look at the example I linked to to see what I mean by wrapping:
> 
> record _≃_ (i j : A ≅ B) : Set e where
>   constructor ⌞_⌟
>   open _≅_ using (from)
>   field from-≈ : from i ≈ from j
> 
> The record has a single field from-≈ with the type that corresponds
> exactly to to the derived notion of equation we want. In your case
> that field would have type
> 
>   (num f * denom g) ≈ (num g * denom f)
> 
> You can then provide a proof of the equality using ⌞ p ⌟ instead
> of p. The point of the record is for Agda to remember the two
> parameters f and g, which it 'forgets' when you provide a value of the
> defined equality type directly.
> 

May be you mean that

  data _=fr'_ : Rel Fraction _
    where
    eqFr : {f g : Fraction} →
           (num f) * (denom g) ≈ (num g) * (denom f) → f =fr' g

will do in my case?
Also James Wood writes that the definition of =fr (and thus =fr' too) 
ignore certain
parts of the Fraction record (the two remaining fields), and so the 
unification will
not work in  =fr
(if so, then probably for =fr' too).
?

And still the definition

   _=fr_ :  Rel Fraction _
   f =fr g =  (num f * denom g) ≈ (num g * denom f)

looks as the most natural.
I doubt greatly of whether it worth to twist/complicate it for the 
purpose to
make a certain unification work more widely.

--
SM