[Agda] unclear import report
Serge D. Mechveliani
mechvel at botik.ru
Wed Mar 13 12:53:29 CET 2013
Dear all,
I have a code of kind
---------------------------------------------------------------
...
open Monoid Mon using (invMb; e; ...)
renaming (setoid to baseSetoid ...)
...
open Monoid subMon renaming (invMb to invMb-sub)
...
BaseInverse = Inverse {M = Mg} e -- Line 631
---------------------------------------------------------------
,
where
this module imports from AlgClasses1.agda,
the record Monoid is defined in AlgClasses1.agda,
and it has a field `e' -- at the Line 271 of this file.
Agda-2.3.2 MAlonzo reports
------------------------------------------------------------------
home/mechvel/doconA/0.01/reports/1/AlgClasses2.agda:631,37-38
Ambiguous name e. It could refer to any one of
.AlgClasses2._._.e
bound at
/home/mechvel/doconA/0.01/reports/1/AlgClasses1.agda:271,3-4
.AlgClasses2._._.e
bound at
/home/mechvel/doconA/0.01/reports/1/AlgClasses1.agda:271,3-4
when scope checking e
------------------------------------------------------------------
I think, this is because `e' is imported by the two paths from the same
root of AlgClasses1.agda:271 :
via "open Monoid Mon" and via "open Monoid subMon".
1. The report does not show where the import diverges.
The user needs to search through a lengthy code in a hope to find a
pair of responsible places.
Can this report be fixed in Agda ?
2. After I have found the place, I fix the error by inserting
" using () " after "open Monoid subMon".
I thought that
open Monoid subMon renaming (invMb to invMb-sub)
means to open only invMb -- with renaming.
But, probably, it also opens all other items. Does it?
Thanks,
------
Sergei
More information about the Agda
mailing list