[Agda] instance argument problems

[Andrew Pitts]

{-
I'm struggling to get instance arguments are they provided by the
latest versions of Agda (> v2.4.2) to work how I would like. For
example, taking the "simulate Haskell type class" example from the
documentation
-}
data Bool : Set where
  true : Bool
  false : Bool

record Eq (t : Set) : Set where
   field _==_ : t → t → Bool

open Eq {{...}}

-- Now package this into a record type for "sets with boolean equality":
record EqSet : Set₁ where
  field
    set : Set
    eq  : Eq set

open EqSet

{-
I'd hope that every time I had identifiers (A : EqSet)(x y set A) in
scope, I could use the expression x == y and have Agda figure out that
this was the eq A instance of _==_. However eq A is not a "candidate
expression" according to
<http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.InstanceArguments>.
For
example

bad-equality : (A : EqSet)(x y : set A) → Bool
bad-equality A x y =  x == y

fails to check, with the message

No variable of type Eq (set A) was found in scope.
when checking that x y are valid arguments to a function of type
{t : Set} {{r : Eq t}} → t → t → Bool

One can get round this by binding eq A to a variable, for example...
-}

good-equality : (A : EqSet)(x y : set A) → Bool
good-equality A x y = let _ = eq A in x == y

{-
...but that seems inelegant. Is there some way of redefining the
record type EqSet so that when we have a value A of type EqSet we
automatically get access to the eq A instance of _==_ ?

Andy
-}