[Agda] A question on records

[David Leduc]

Hi,

I would like to introduce some notation with imolicit arguments as can
be done in Coq.
Unfortunately wen I type check the code below the underscore becomes
yellow (I guess it's because something is wrong).
If I replace the underscore by A then it does not typecheck at all.
How to solve this problem?

module test where

record T (A : Set) : Set1 where
  field r : A -> A -> A

_$_ : {A : Set} -> {t : T A} -> A -> A -> A
x $ y = T.r _ x y