Transpor matriz vetorial em Idris2 com tipos dependentes

Tenho dificuldade em descobrir o que é meu erro de tipo ou compilação do Idris2, então pensei que poderia pedir a alguns veteranos ou entusiastas do Idris2 para me darem alguma explicação sobre como posso fazer minha abordagem funcionar ou por que ela não pode funcionar assim. Qualquer informação adicional e conselho aprofundado são sempre muito apreciados, pois quero usar o conhecimento para converter coisas de Haskell para Idris2 para estruturas prováveis, etc.

A solução geral que já conheço é esta (com todas as funções auxiliares):

data Vect : (len : Nat) -> (a : Type) -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f []        []         = []
zipWith f (x :: xs) (y :: ys)  = f x y :: zipWith f xs ys


replicate : (n : Nat) -> a -> Vect n a
replicate 0     _  = []
replicate (S k) va = va :: replicate k va

replicate' : {n : _} -> a -> Vect n a
replicate' = replicate n


transpose : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = replicate' []
transpose (xs::xss) = zipWith (::) xs (transpose xss)

Essa foi a solução do guia do GitHub com o qual eu estava aprendendo.

Agora minha abordagem:

transLines : Vect n (Vect (S m) a) -> Vect n a
transLines [] = []
transLines ((x :: _) :: xss) = x :: transLines xss

dropLines : Vect n (Vect (S m) a) -> Vect n (Vect m a)
dropLines [] = []
dropLines ((_ :: xs) :: xss) = xs :: dropLines xss


transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} [] = []
transpose' ([]:: _) = []
transpose' ma = (transLines ma) :: transpose' (dropLines ma)

Eu sei o que especificamente não funciona, os tipos de "Vect n (Vect ma)" e "Vect ?n (Vect (S ?m) a)" não podem corresponder quando eu chamo "droplines ma" na função de transposição, mas é aí que estou preso, não sei se é possível alterar algumas definições para que funcione, ou se a abordagem como um todo simplesmente não é viável com tipos dependentes.

Obrigado antecipadamente e Felicidades