Cannot resolve overloaded projection _≈_

[Akshobhya1234]

When defining direct product of quasigroup as

quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
quasigroup M N = record
{ Carrier = M.Carrier × N.Carrier
; ≈ = Pointwise {! M.≈ !} {! !}
; ∙ = zip M.∙ N.∙
; \ = zip M.\ N.\
; // = zip M.// N.//
; isQuasigroup = record
{ isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
; ∙-cong = zip M.∙-cong N.∙-cong
; \-cong = zip M.\-cong N.\-cong
; //-cong = zip M.//-cong N.//-cong
; leftDivides = (λ x y → M.leftDividesˡ , N.leftDividesˡ <> x <> y) , (λ x y → M.leftDividesʳ , N.leftDividesʳ <> x <> y)
; rightDivides = (λ x y → M.rightDividesˡ , N.rightDividesˡ <> x <> y) , (λ x y → M.rightDividesʳ , N.rightDividesʳ <> x <> y)
}
} where module M = Quasigroup M; module N = Quasigroup N

It says "Cannot resolve overloaded projection ≈ because it is not applied to a visible argument when inferring the type of M.≈"

@JacquesCarette Can you have a look at it.

[Akshobhya1234]

I think I found the issue. It depends on how the quasigroup is defined in stdlib. I will create an issue in stdlib to change the definition.

[JacquesCarette]

Have you tried M._≈_ instead? That's the real name of the function.

[Akshobhya1234]

Have you tried M._≈_ instead? That's the real name of the function.

That is exactly the issue. We cannot use M._≈_.

[JacquesCarette]

But that makes no sense - that names comes from a module, and it shouldn't be overloaded at all. Can you provide a bigger explanation?

[JacquesCarette]

What I don't understand is how/where two version of ≈ as in-scope in M. I can understand that that's the problem.

[Akshobhya1234]

What I don't understand is how/where two version of ≈ as in-scope in M. I can understand that that's the problem.

Got your question. To be honest even I am confused. The agda error will not make it clear as to where two version of ≈ is in-scope in M. (Could it be from Magma that is defined in same file?) But I think we will face similar issue when we try to define direct product for Lattice.

[Akshobhya1234]

But for now this issue is resolved with the current changes proposed to quasigroup in stdlib.

[JacquesCarette]

One way to find out is to put ≈ in a hole, and do C-c C-w (for 'where', I think), and it will tell you where the definition(s) come from. (I think the documentation says "hy in scope")

[Akshobhya1234]

@JacquesCarette I got the issue. We had 2 instances of _≈_ one from Quasigroup and other from RawQuasigroup when we say

open RawQuasigroup rawQuasigroup public
using (_≈_; //-rawMagma; \\-rawMagma; ∙-rawMagma)

in Quasigroup

To overcome this with we could remove _≈_ like
open RawQuasigroup rawQuasigroup public
using (//-rawMagma; \\-rawMagma; ∙-rawMagma)

[JacquesCarette]

Yes, that's probably a good idea.