[Agda] Termination checking: valid or invalid

[Wojciech Jedynak]

Hello everybody,

I'm attaching a small example function on rose trees implemented using
a function instead of a list of subtrees. The 'mirror' function is
written in two flavors and only the first one passes termination
checking. Should the second version be accepted as well?
I'm using the Darcs Agda from a few days ago.

Greetings,
Wojciech

\begin{code}

module Question where

open import Data.Nat
open import Data.Fin
open import Function
open import Data.Vec

postulate
  A : Set

data Tree : Set where
  leaf : Tree
  node : A → {n : ℕ} → (Fin n → Tree) → Tree

-- find the "complement" of the given i
reverse-fin : ∀ {n} → Fin n → Fin n
reverse-fin i = lookup i (reverse (allFin _))

-- passes termination checking
mirror : Tree → Tree
mirror leaf = leaf
mirror (node a fts) = node a (λ i → mirror (fts (reverse-fin i)))

-- fails termination checking
mirror2 : Tree → Tree
mirror2 leaf = leaf
mirror2 (node a fts) = node a (λ i → mirror2 $ fts (reverse-fin i))

\end{code}