[Agda] record field as Instance Argument

[Guillermo Calderon - INCO]

Hi,

I am working with Instance Arguments to simulate Haskell classes
as explained here:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments

So, I have:

  record Eq (t : Set) : Set where
    field _==_ : t → t → Bool
    _/=_ : t → t → Bool
    a /= b = not $ a == b

and the following record definition:

record A2 : Set₁ where
   field
     A : Set
     EqA : Eq A
     a b : A
   a≠b : Bool
   a≠b =  a /= b

Agda gives an error at the last /= :
"No variable of type Eq A was found in scope".
But EqA is in the scope.  Why Agda does not consider it?

I can fix it defining an alias of EqA as an instance Eq.
The keyword instance is required.
I do not find the way to apply "instance" directly over the field EqA.

record A2 : Set₁ where
   field
     A : Set
     EqA : Eq A
     a b : A
   instance foo = EqA
   a≠b : Bool
   a≠b =  a /= b

Is there a better  way to solve this?
Thanks,
Guillermo