[Agda] How to set up fixities for record parameters?

[Vag]

And the workaround that Nils recommended in September works for all cases:

module Tst where

infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ·≡· : a ≡ a

Op : Set → Set {- An operation on A -}
Op A = A → A → A

record Plus {A : Set} (plus : Op A) : Set where
     infixl 40 _+_
     _+_ = plus

record Cross {A : Set} (cross : Op A) : Set where
     infixl 40 _×_
     _×_ = cross

record Concatenative (A : Set) (cross : Op A) (g : A) (plus : Op A)  (e : A) : Set where
     cr : Cross cross ; cr = record { } ; open Cross cr ; pl : Plus plus ; pl = record { } ; open Plus pl
     field
         move : ∀ {X Y a} → X + Y × a ≡ X × a + Y

module Grp (A : Set) (cross : Op A) (g : A) (plus : Op A)  (e : A) where
     cr : Cross cross ; cr = record { } ; open Cross cr ; pl : Plus plus ; pl = record { } ; open Plus pl
     postulate move : ∀ {X Y a} → X + (Y × a) ≡ (X × a) + Y

data Test {A : Set} (plus cross : Op A) : Set where
     tst : ∀ {a b c d} → let pl : Plus plus ; pl = record { } ; open Plus pl ; cr : Cross cross ; cr = record { } ; open Cross cr in a + b × c ≡ d → Test plus cross -- *OK*