[Agda] Importing Infix Operation Inside a Record From Record Field

[Vag Vagoff]

module Bug where
id : ∀ {A} → A → A ; id a = a
infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a
infixr 90 _◦_ ; _◦_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) ; f 
◦ g = λ x → f (g x)

record Applicative (t : Set → Set) : Set₁ where
infixl 40 _⊛_
field
pure : ∀ {a} → a → t a
_⊛_ : ∀ {a b} → t (a → b) → t a → t b

record IsApplicative (t : Set → Set) : Set₁ where
field
applicative : Applicative t
pure : ∀ {a} → a → t a
pure = Applicative.pure applicative
infixl 40 _⊛_
_⊛_ : ∀ {a b} → t (a → b) → t a → t b
_⊛_ = Applicative._⊛_ applicative
field
identity : ∀ {a} {u : t a} → pure id ⊛ u ≡ u
------------------VVVVVVVVVVVVVVVV
composition : ∀ {a b c} {u : t (b → a)} {v : t (c → b)} {w : t c} → 
((pure _◦_ ⊛ u) ⊛ v) ⊛ w ≡ u ⊛ (v ⊛ w) -- [!] associativity does not 
works! i.e. unable to open parethesis: pure _◦_ ⊛ u ⊛ v ⊛ w ≡ u ⊛ (v ⊛ w)
------------------^^^^^^^^^^^^^^^^^^^^^^^^^
homomorphism : ∀ {a b} {x : a} {f : a → b} → pure f ⊛ pure x ≡ pure (f x)
interchange : ∀ {a b} {x : a} {u : t (a → b)} → u ⊛ pure x ≡ pure (λ f → 
f x) ⊛ u


Why associativity does not work for ⊛ in `composition' field? How to fix 
this record to do its job and leave readability high?