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

[Jesper Cockx]

Wait, what?!? That seems really counterintuitive to me. But you're right,
the following also works on the current github Agda:

      works3 : (e : E) (g : G) (e∈g : e ∈ g) →
            _≡_ {A = V}
                (value ⦃ _ ⦄ e∈g)
                (value ⦃ _ ⦄ e∈g)
      works3 e g e∈g = refl

I would expect an underscore to be solved by the constraint solver, if I
wanted instance search I'd use 'it'. So now there's no easy way to turn an
instance implicit into a regular implicit, that seems like a loss of
expressivity to me.


Jesper

On Sat, Nov 5, 2016 at 11:26 AM, Andreas Abel <abela at chalmers.se> wrote:

> 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-argum
>> ents.html#instance-resolution
>>     <http://agda.readthedocs.io/en/latest/language/instance-argu
>> ments.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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161105/b49c8b9b/attachment.html