[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