Matrix transpose again

[Ignas Vyšniauskas]

Hi,

Dependent Type noob here.
I saw this solution suggested here to the matrix transpose problem:

-----
total
mtrans : Matrix a n m -> Matrix a m n
-- uncommenting changes nothing, read bellow
-- mtrans {m=k} (r :: []) = zipWith (::) r (repeat k [])
mtrans {m=k} [] = repeat k []
mtrans (r :: rs) = zipWith (::) r (mtrans rs)
-----

I didn't quite like it because transposing 0-sized matrices seemed
questionable (and indeed Idris will cry about incomplete terms if you
try to do `mtrans []` or `mtrans [[]]`).

So I'm trying to define a "proper" transpose by just starting from 1:

-----
ptrans : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
ptrans {m=k} (r :: []) = zipWith (::) r (repeat (S k) [])
ptrans (r :: rs) = zipWith (::) r (ptrans rs)
-----

[This is not how I wrote it orginally[1], but this the most obvious way
to see it is the same.]

However, this in idris-dev and 0.9.7 this fails with:

----
Can't unify Matrix a (S m) (S n) with Vect (Vect a n) (S m)

Specifically:
Can't unify n with S n
----

Even more interestingly, uncommenting the case in mtrans makes it
essentially the same as ptrans, but still passes type checking.

Is this a bug or am I doing something wrong? I also noticed an idris-dev
test, which I couldn't quite understand, but it might be related. The
function is pattern pattern-match on a list and on a vector, which I
don't understand:
https://github.com/edwinb/Idris-dev/blob/master/test/reg014/reg014.idr

Thanks,
Ignas

[1]: Here's an hpaste I originally pasted on #idris:
http://hpaste.org/89771

[Ignas Vyšniauskas]

Partly answering my own question so that other's don't have to.

I was told that the problem lies in

> ptrans (r :: rs) = zipWith (::) r (ptrans rs)

because the typecheker thinks that rs might be Nil (although it will not
due to the previous case), so I fixed it by instead doing:

ptrans (r :: (rest :: rs)) = zipWith (::) r (ptrans (rest :: rs))

--
Ignas