[Agda] instance argument problems

[Andrew Pitts]

On 30 May 2015 at 16:14, effectfully <effectfully at gmail.com> wrote:
> There was a similar question:
> http://comments.gmane.org/gmane.comp.lang.agda/7546

Glad to see I was not the first to ask this. But the only answer in
that thread was not helpful, since there is every reason to want to
package structures up into large record types.

In fact, in my previous post I forget to give the sort of example that
really has me stumped. For example, in the context of the previous
message, suppose I try to declare a function

bad-fun :  (A : EqSet)(x y : set A) → (x == y) ≡ (x == y)
bad-fun A x y = refl

Then the two occurrences of x == y get highlighted in dreaded yellow
and I can't see how to get round that. I know the example is
contrived, but I want to use the eq A instance of _==_ on the left
hand side of declarations as well as the right hand side. How to do
that??

Andy