[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