Idris - equality assertion fails

Question

Please consider the following function, even if the implementation is not that relevant:

vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n))
vectTranspose {n = Z} [] = [[],[],[]]
vectTranspose {n = (S len)} (x :: xs) with (natToFin len (S len))
    | Just l = let
        previous = map (map weaken) (vectTranspose xs)
    in updateAt x (l ::) previous

if I try to compute vectTranspose in the REPL, I get [[],[],[]] as expected.

Still, if I add an equality assertion like the following in my code

emptyTest : vectTranspose [] = [[],[],[]]
emptyTest = Refl

then I get a compile error:

When checking right hand side of emptyTest with expected type
        vectTranspose [] = [[], [], []]

Type mismatch between
        [[], [], []] = [[], [], []] (Type of Refl)
and
        vectTranspose [] = [[], [], []] (Expected type)

Specifically:
        Type mismatch between
                [[], [], []]
        and
                vectTranspose []

Am I missing something? Should I specify somehow the type of [[],[],[]] in the assertion?

Answer 1

The fact that idris complains about the type of

Specifically:
    Type mismatch between
            [[], [], []]
    and
            vectTranspose []

indicates that vectTranspose is still in the type and has not been resolved. That is the case if vectTranspose is not total and indeed it is not:

VecTest.vectTranspose is possibly not total due to:
with block in VecTest.vectTranspose, which is not total as there are missing cases

which happens because you have not covered all the Maybe cases.

A simple solution could be to create a small helper function:

total
natToFin': (n: Nat) -> Fin (S n)
natToFin' Z = FZ
natToFin' (S k) = FS (natToFin' k)

total
vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n))
vectTranspose {n = Z} [] = [[], [], []]
vectTranspose {n = (S len)} (x :: xs) with (natToFin' len)
    vectTranspose {n = (S len)} (x :: xs) | l = let
           previous = map (map weaken) (vectTranspose xs)
           in updateAt x (l ::) previous