[Agda] Importing Infix Operation Inside a Record From Record Field (Indentation fixed)

[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 parenthesis: 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?