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}