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 打印与倒数第二行有关的错误“Unsolved metas at the following locations”：

    assoc⊕ = assoc+

并特别指向 assoc+。

如何提供提示或以其他方式更改代码以便在没有此警告的情况下编译？

我当然可以通过取消隐藏参数来摆脱它，但这意味着我必须在任何地方指定显式参数，即使在不需要它的地方......

Answer 1

You can exploit the fact that Agda allows you to specify implicit arguments even inside a lambda abstraction. More specifically, you can write this:

λ {r s t} → assoc+ {r} {s} {t}
-- with a type {r s t : ℕ} → ((r + s) + t) == (r + (s + t))

And indeed, replacing assoc+ with the expression above makes the compiler happy. It would seem that the unification has a problem with the last argument (t), so we can even ignore r and s and only fill in t explicitly:

assoc⊕ = λ {_ _ t} → assoc+ {k = t}