[Agda] Inference difficulties

[Conal Elliott]

I’ve been encountering inference difficulties working with agda-categories.
I’ve whittled down the problem to a simplified example that doesn’t use
agda-categories (source also attached as T8.agda):

open import Levelopen import Algebra.Bundles using (Magma)open import
Relation.Binary using (Rel)open import Function.Equality using (_⟶_)
renaming (id to ⟶-id)record Cat (o ℓ : Level) : Set (suc (o ⊔ ℓ))
where  infix  4 _⇒_  field    Obj : Set o    _⇒_ : Rel Obj ℓ    id  :
∀ {A} → A ⇒ A    -- ... elidedM : Cat _ _M = record { Obj = Magma 0ℓ
0ℓ           ; _⇒_ = λ A B → Magma.setoid A ⟶ Magma.setoid B
; id  = ⟶-id           -- ...           } open Cat M_ : ∀ {A : Magma
0ℓ 0ℓ} → A ⇒ A_ = id

The error message (referring to the use of id in the last line):

__∙__27 : Algebra.Core.Op₂ (Magma.Carrier A)  [ at
/Users/conal/Agda/cat-linear/src/T8.agda:24,5-7 ]_∙-cong_30  :
Algebra.Definitions.Congruent₂ (λ z z₁ → (A Magma.≈ z) z₁)    __∙__27
[ at /Users/conal/Agda/cat-linear/src/T8.agda:24,5-7 ]

If I replace Magma by a structure with more operations, such as Ring, I see
more such errors, failing to infer each operation and associated property.

I’m stumped and would appreciate any insights about causes and cures for
this inference failure.

– Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201109/a30d9a79/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: T8.agda
Type: application/octet-stream
Size: 850 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201109/a30d9a79/attachment.obj>