[Agda] newbie instance resolution question: too many candidates?

[Andreas Abel]

On 05.11.2016 10:32, Jesper Cockx wrote:
> If you write ⦃ _ ⦄as an argument, then Agda won't use instance search
> for this argument but it will use the constraint solver instead.

I thought I changed that in 2.5.2, see
https://github.com/agda/agda/issues/2172

> You
> should just leave out the argument instead if you want to use the
> instance search. The following version works:
>
>       works2 : (e : E) (g : G) (e∈g : e ∈ g) →
>             _≡_ {A = V}
>                 (value e∈g)
>                 (value e∈g)
>       works2 e g e∈g = refl
>
> You do need to give {A = V} because the instance search doesn't work
> with unsolved metas in the type, because otherwise it may get stuck in a
> loop.
>
> Cheers,
> Jesper
>
> On Sat, Nov 5, 2016 at 8:23 AM, Ulf Norell <ulf.norell at gmail.com
> <mailto:ulf.norell at gmail.com>> wrote:
>
>     The problem isn't that there are too many candidates (the error
>     should be clearer about this) but that there are unsolved metas in
>     the target (_A_35).
>     See http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution
>     <http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution>
>     for the details.
>
>     / Ulf
>
>     On Sat, Nov 5, 2016 at 6:03 AM, Martin Stone Davis
>     <martin.stone.davis at gmail.com <mailto:martin.stone.davis at gmail.com>>
>     wrote:
>
>         I'm unclear why the below code fails to typecheck and confused
>         by the error message. First, the code:
>
>             open import Agda.Builtin.Equality
>
>             record Membership (E G : Set) : Set₁ where
>               field _∈_ : E → G → Set
>
>             open Membership ⦃ ... ⦄
>
>             record Valueable (A V : Set) : Set where
>               field value : A → V
>
>             open Valueable ⦃ ... ⦄
>
>             module _
>               (E G V : Set)
>               ⦃ E∈G : Membership E G ⦄
>               ⦃ e∈g→v : {e : E} {g : G} → Valueable (e ∈ g) V ⦄
>               where
>
>               works : (e : E) (g : G) (e∈g : e ∈ g) →
>                     _≡_ {A = V}
>                         (value ⦃ e∈g→v ⦄ e∈g)
>                         (value ⦃ e∈g→v ⦄ e∈g)
>               works e g e∈g = refl
>
>               fails : (e : E) (g : G) (e∈g : e ∈ g) →
>                     _≡_ {A = _}
>                         (value ⦃ _ ⦄ e∈g)
>                         (value ⦃ _ ⦄ e∈g)
>               fails e g e∈g = refl
>
>
>         Here are the relevant parts of the error message that have me
>         scratching my head:
>
>             _r_41 : Valueable ((E∈G Membership.∈ e) g) (_A_35 E G V e g e∈g)
>
>         (This is associated with yellow highlighting on the instance
>         argument to the first call to 'value' in 'fails'.)
>
>
>             Failed to solve the following constraints:
>               [0] Resolve instance argument
>                     _41 :
>                       (E₁ G₁ V₁ : Set) {{E∈G = E∈G₁ : Membership E₁ G₁}}
>                       {{e∈g→v = e∈g→v₁
>                         : {e = e₁ : E₁} {g = g₁ : G₁} →
>                           Valueable ((E∈G₁ Membership.∈ e₁) g₁) V₁}}
>                       (e₁ : E₁) (g₁ : G₁) (e∈g₁ : (E∈G₁ Membership.∈ e₁)
>             g₁) →
>                       Valueable ((E∈G₁ Membership.∈ e₁) g₁) (_A_35 E₁ G₁
>             V₁ e₁ g₁ e∈g₁)
>                   Candidates
>                     e∈g→v :
>                       {e = e₁ : E} {g = g₁ : G} → Valueable ((E∈G
>             Membership.∈ e₁) g₁) V
>                     E∈G : Membership E G
>
>         The above error message seems to indicate that both 'e∈g→v' and
>         'E∈G' are candidates for the instance argument to 'value'. But
>         'E∈G' doesn't have a 'Valueable' type! So, how can it be a
>         candidate?
>
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/