[Agda] many ways to import the same thing from record

[mechvel at scico.botik.ru]

Can anybody, please, explain something concerning the _attached code_?
(it is small).

The effect is that the same setoid can be imported in many ways from
Semiring, and by even more ways from CommutativeRing, and so on.
And in some programs the type checker is satisfied only with one of
such ways.

This relates both to Agda programming in general and to standard 
library.

The example implements a part of a proof for the statement:
for a  Semiring  having the property
``nz*nz : ∀ {x y} → x ≉ 0# → y ≉ 0# → (x * y) ≉ 0#``
(call it  FooSemiring)
it holds that the  subset of nonzero elements  is a Magma, if the `_∙_`
operation is put the restriction of `_*_` to Nonzero.

The code defines the notions of Subset and Submagma,
and tries to form a Submagma for Nonzero in any FooSemiring.
But Agda-2.6.1 reports

   Algebra.IsSemiringWithoutAnnihilatingZero.*-isMonoid /=
   Algebra.IsSemiringWithoutAnnihilatingZero.+-isCommutativeMonoid
   when checking that the expression nzSubsetoid has type
   Subsetoid α α= α= (Magma.setoid *-magma)

It is about the last two lines
```
  nzSubmagma : Submagma α α= α= *-magma
  nzSubmagma = submagmaᶜ nzSubsetoid closed*
```
I have an impression that it happens the following.
nzSubsetoid  is formed for the base `setoid` imported form FooSemiring,
and this setoid is extracted from `Semiring.+-monoid`
- probably this is put so in lib-1.3, by occasion.
But it could as well extract it from `Semiring.*-monoid`.

Further, the Submagma record has `magma` as argument, and in the
definition of Submagma, `setoid` is exracted from this `magma`.
And the argument in the type of  nzSubmagma  is set `Semiring.*-magma`,
because it aims at the multiplicative magma of a Semiring.

Mathematically, `+-magma` and `*-magma` of (Semiring R) have the same 
setoid
inside.
Does Agda refer to these setoids somehow with the same reference?

Probably, in my program, the type checker does not identify these 
setoids.
To check this, I split this setoid import to the two steps:
```
  open FooSemiring R using (Carrier; ...; *-magma)
  open Magma *-magma using (setoid)
```
instead of importing is directly from FooSemiring.
Now Agda is satisfied.

Something is suspicious here.
As there are many levels in the record hierarchy for algebra in
standard library, it occurs that the same thing can be imported
from the top domain by hundreds of ways. And for almost all of these
ways, the type checker will report an error - for some programs.
This presents a problem.
Because it is easier to import everything needed by a single `open` 
declaration
for the top record rather than to search for a lucky chain of imports.
May be, this is due to a bug in Agda?
I do not know how standard library can help here.

Am I missing something?

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.agda.zip
Type: application/zip
Size: 1100 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200606/88653a67/attachment.zip>