[Agda] "Cannot resolve" vs "Multiple definition"

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sat Jun 20 13:37:02 CEST 2020


Dear Agda developers,

When the same item  foo  is brought to the scope from different places,
Agda-2.6.1 reports something like
"Multiple definition of  foo  ...".

But sometimes it reports
"Cannot resolve overloaded projection  foo  because principal
argument is not of record type ...
".
The source of the error looks the same, but the reports are very 
different.
The former looks more helpful.

Example:

record Semiring :  Set _ where
   ...
   open Monoid *-monoid public using () renaming (assoc to *-assoc; ...)

module OfRing (R : Ring)
   where
   open Ring R using (*-assoc; ...)
   ...
   -x*y x y = begin⟨ setoid ⟩
                   (- x) * y        ≈⟨ *-congʳ (sym (-1* x)) ⟩
                   (-1# * x) * y    ≈⟨ *-assoc -1# x y ⟩
                   -1# * (x * y)    ≈⟨ -1* _ ⟩
                   - (x * y)
              ∎
"Cannot resolve overloaded projection *-assoc because principal
argument is not of record type
when checking that the expression *-assoc -1# x y has type
-1# * x * y ≈ -1# * (x * y)
"

Needs this to be fixed?
Thanks,

------
Sergei


More information about the Agda mailing list