[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