stuck resolving metavariables in agda proof

Question

I'm trying to prove a result for the following bizarre datatype in Agda. Here's the data type in question and its constructors (see SpLoc below):

-- supplemental data type for nats >= 2
data ℕ² : Set where
    two  : ℕ²
    succ : ℕ² -> ℕ²

toℕ² : ∀ n {_ : Positive n} -> ℕ²
toℕ²  0 {()}
toℕ²  1 {()}
toℕ² (suc (suc zero))       = two
toℕ² (suc (suc (suc n)))    = succ (toℕ² (suc (suc n))) 

to-nat : ℕ² -> ℕ
to-nat two = 2
to-nat (succ k) = 1 + to-nat k

-- spiral locations (sploc)
data SpLoc (A : Set) : ℕ² -> Set where
    cen : (k : ℕ²) -> (SpLoc A k)               -- center loc
    ss  : (k : ℕ²) -> (SpLoc A k) -> SpLoc A k  -- spiral successor
    rs  : (k : ℕ²) -> (SpLoc A k) -> SpLoc A k  -- radial successor

Certain properties are asserted involving iterated application of the spiral successor fn, so I also have an iterate function:

iterated : ∀ {A : Set}  -> (f : A -> A) -> ℕ -> A -> A
iterated f zero x = x
iterated f (suc n) x = f (iterated f n x)

This operator produces the 'distance' (number of hops) a given spiral location is from the center:

-- spiral center dist.
scd : ∀ {A : Set} -> ∀ (k : ℕ²) -> (SpLoc A k) -> ℕ
scd {A} k (cen k)   = 0
scd {A} k (ss k p)  = (scd k p) + 1
scd {A} k (rs k p)  = (to-nat k) * (scd k p) + 1  

The lemma/corollary I'm trying to prove about the above operator--followed by the steps I have made so far is below:

scd-03 : ∀ {A : Set} -> ∀ (k : ℕ²) -> ∀ (n : ℕ) -> scd k ( iterated (ss k) n (cen k) ) ≡ n 
scd-03 {A} k 0 = {- omitted, seems to go through -}
scd-03 {A} k (suc n) = 
    begin
        scd k (iterated (ss k) (suc n) (cen k))
    ≡⟨⟩ 
        scd k ( (ss k) (iterated (ss k) n (cen k)) )
    ≡⟨⟩ 
        (scd k (iterated (ss k) n (cen k))) + 1
    ≡⟨ +-comm (scd k (iterated (ss k) n (cen k))) 1 ⟩ 
        1 + scd k (iterated (ss k) n (cen k)) 
    ≡⟨⟩ 
        suc ( scd k (iterated (ss k) n (cen k)) ) 
    ≡⟨ cong (suc) (scd-03 {A} k n)  ⟩
        suc n 
    ∎ 

It seems that the steps match with the goal, although when running check once the above chain of rewrites is in place, I get the following error regarding unsolved metas (metavariables):

Failed to solve the following constraints:
  _A_38 (k = k) (n = (suc n)) = _A_38 (k = k) (n = n) : Set
    (blocked on _A_38)
_A_38 : Set
_A_47 : Set
_A_53 : Set

The +-comm specifically is in red (using VSCode extension here). Doing some reading, it seems like the issue might have to with implicit parameters, so I made the k explicit (was originally implicit) though it hasn't resolved the issue.

Any advice or tips on how to proceed or resolve this? Or dealing with metavariable errors in general?

Answer 1

The scd in scd-03's type signature is highlighted in yellow, which means that it's missing implicit arguments. Writing scd {A} instead solves it.