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

Andreas Abel abela at chalmers.se
Sat Nov 5 15:57:32 CET 2016


Well, instead of `it`, use `hid` ;)

data D : Set where
   instance
     c : D

wallop : {{_ : D}} → D
wallop {{x}} = x

inst : D
inst = wallop {{_}}  -- works since 2.5.2

-- Use hid if you want to turn an instance meta into a ordinary meta
hid : ∀{a}{A : Set a}{x : A} → A
hid {x = x} = x

unif : D
unif = wallop {{hid}} -- yellow


On 05.11.2016 13:31, Jesper Cockx wrote:
> 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
> <mailto: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
>     <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>
>         <mailto: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>
>
>         <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>
>         <mailto: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>
>         <mailto: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>
>                 <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>
>         <mailto: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>
>             <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>
>
>
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/ <http://www2.tcs.ifi.lmu.de/%7Eabel/>
>
>

-- 
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/


More information about the Agda mailing list