[Agda] Inference difficulties

[Conal Elliott]

Thanks for the explanation, Jesper! Indeed, all of my failing examples can
be made to work if I explicitly insert enough implicit arguments at the
right places.

On Tue, Nov 10, 2020 at 12:50 AM Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/502f31e7/attachment.html>