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

[Martin Stone Davis]

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?