unresolved metas when defining a record in Agda

Question

Consider the following code:

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+
    }

When loaded with Agda (version 2.3.2.2), Agda prints an error "Unsolved metas at the following locations" pertaining to the line penultimate line:

    assoc⊕ = assoc+

and specifically pointing to assoc+.

How do I provide a hint or otherwise change the code so it compiles without this warning?

I can of course get rid of it by unhiding the arguments, but that means I would have to specify explicit arguments everywhere, even in places where it is not needed...

Vitus Vitus · Accepted Answer · 2014-01-16T18:42:26

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}

unresolved metas when defining a record in Agda

1 Answers