Unexpected Occurrence of recursive function

Stream: new members

[Alex Reynaldi]

I'm trying to define a map function over the fin n -> U type so that I can use them as if they were vectors. When attempting to map a function recursively I get an error but simply inlining the map works. Why does this happen?

def finvec (U : Type) (n : ℕ) : Type := fin n → U

def finvec.map {U V: Type} {n : ℕ} (f : U → V) (v : finvec U n) : finvec V n :=
λi, f (v i)

-- short example case of error
inductive tree (U : Type) : Type
| leaf : U → tree
| node : ∀{n}, finvec tree n → tree

-- Causes "unexpected occurence of recursive function" error
def replaceInTreeBad {U V : Type} (f : U → V) : tree U → tree V
| (tree.leaf u) := tree.leaf (f u)
| (tree.node subtrees) := tree.node (finvec.map replaceInTreeBad subtrees)

-- Works fine
def replaceInTreeGood {U V : Type} (f : U → V) : tree U → tree V
| (tree.leaf u) := tree.leaf (f u)
| (tree.node subtrees) := tree.node (λi, replaceInTreeGood (subtrees i))

[Eric Wieser]

If you replace finvec.map replaceInTreeBad with finvec.map (λ i, replaceInTreeBad i) then you get a different error