proof - Agda でレコードを定義するときの未解決のメタ

Question

次のコードを検討してください。

module UnresolvedMeta where

  record Test (M : Set) : Set1 where
    field
      _≈_ : M -> M -> Set
      _⊕_ : M -> M -> M
      assoc⊕ : ∀ {r s t} -> ((r ⊕ s) ⊕ t) ≈ (r ⊕ (s ⊕ t))

  data ℕ : Set where
    n0 : ℕ
    suc : ℕ -> ℕ

  data _==_ : ℕ -> ℕ -> Set where
    refl== : ∀ {k} -> k == k

  _+_ : ℕ -> ℕ -> ℕ
  k + n0 = k
  k + suc m = suc (k + m)

  lem-suc== : ∀ {k m} -> k == m -> suc k == suc m
  lem-suc== refl== = refl==

  assoc+ : ∀ {i j k} -> ((i + j) + k) == (i + (j + k))
  assoc+ {i} {j} {n0} = refl== {i + j}
  assoc+ {i} {j} {suc k} = lem-suc== (assoc+ {i} {j} {k})

  thm-ℕ-is-a-test : Test ℕ
  thm-ℕ-is-a-test = record {
    _⊕_ = _+_;
    _≈_ = _==_;
    assoc⊕ = assoc+
    }

Agda (バージョン 2.3.2.2) をロードすると、Agda は最後から 2 番目の行に関連するエラー「次の場所にある未解決のメタ」を出力します。

    assoc⊕ = assoc+

特にassoc +を指しています。

この警告なしでコンパイルされるように、ヒントを提供するか、コードを変更するにはどうすればよいですか?

もちろん、引数を非表示にすることでそれを取り除くことができますが、それは、必要のない場所であっても、どこでも明示的な引数を指定する必要があることを意味します...