[Agda] Inference difficulties

[Jesper Cockx]

Hi Conal,

I believe you're being bitten by the automatic insertion of implicit lambda
abstractions. When Agda tries to check an expression at an implicit pi type
like ∀ `{A : Magma 0ℓ 0ℓ} → A ⇒ A`, it will automatically insert an
abstraction `λ {A} → ...` Likewise, when checking `id` it will
automatically insert an implicit argument `{_}`. So the expression Agda
actually tries to check is not `id` but `λ {A} →id {_}`. But now there's
many possible solutions for the `_`, and Agda doesn't know which one to
pick!

To work around the automatic insertion, you need to pass the `A`
explicitly, for example like this:

```
id' : ∀ {A : Magma 0ℓ 0ℓ} → A ⇒ A
id' {A} = id {A}
```

There were two papers at ICFP this year that propose more intelligent
strategies for the insertion of implicits (
https://dl.acm.org/doi/10.1145/3408971 and
https://dl.acm.org/doi/10.1145/3408983), but neither of them has been
implemented for Agda so far.

-- Jesper

On Tue, Nov 10, 2020 at 5:40 AM Conal Elliott <conal at conal.net> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201110/2c707610/attachment.html>