type mismatch occurs while the evaluated values are equal

Question

I'm a beginner in Idris and trying to make a code valid.

Could you let me know the better place for noob questions on Idris?

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = filter {len=l} p xs
   in if p x then
        ((FS a) ** x::tail)
      else
        ((weaken a) ** tail)

I wrote another filter which can't pass the type check yet.

This new filter's type implies that the filtered vector cannot be longer than the original one.

However, Idris saids

...
Specifically:
                Type mismatch between
                        finToNat a
                and
                        finToNat (weaken a)

We know those two terms always have the same value.

How can I describe the fact and let Idris say ok?

Answer 1

You have to show that finToNat a = finToNat (weaken a). tail has type Vect (finToNat a) elem, but you need Vect (finToNat (weaken a)) elem for the second component in the last line, because you wrote weaken a in the first pair component.

lemma : {n : _} -> (a : Fin n) -> finToNat (weaken a) = finToNat a
lemma FZ     = Refl
lemma (FS x) = rewrite lemma x in Refl

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = Main.filter {len=l} p xs
  in if p x then
       ((FS a) ** x::tail)
     else
       (weaken a ** (rewrite lemma a in tail))