Termination checking of simple uncurried functions

Question

The following recursive binary function over naturals is obviously terminating:

open import Data.Nat

curried : ℕ → ℕ → ℕ
curried zero    k = k
curried (suc n) k = curried n (suc k)

and Agda accepts it as so.

However, the following uncurried version of the same function is also still obviously terminating, since the first coordinate of the pair is always peeling off a layer of suc, so the second coordinate shouldn't even matter:

open import Data.Product

uncurried : ℕ × ℕ → ℕ
uncurried (zero  , k) = k
uncurried (suc n , k) = uncurried (n , suc k)

Alas, the termination checker of Agda 2.6.2.2 rejects it:

Termination checking failed for the following functions:
  uncurried
Problematic calls:
  uncurried (n , suc k)

Is there a way (other than currying...) to push uncurried through the termination checker?