Computing the type of the matrix diagonal using min

MatrixDiagonal2.idr

module Main

import Data.Vect

-- the regular min uses (<) and is not suitable here,
-- we need mymin and diagonal to follow the same recursion pattern
mymin : Nat -> Nat -> Nat
mymin Z y = Z
mymin x Z = Z
mymin (S x) (S y) = S (mymin x y)

diagonal : Vect m (Vect n a) -> Vect (mymin m n) a
diagonal Nil = Nil
diagonal (Nil :: xss) = Nil
diagonal ((x :: xs) :: xss) = x :: diagonal (map tail xss)

example1 : diagonal [[1, 2]
                    ,[3, 4]
                    ]
         = [1, 4]
example1 = Refl

example2 : diagonal [[1, 2, 3]
                    ,[4, 5, 6]
                    ]
         = [1, 5]
example2 = Refl

example3 : diagonal [[1, 2]
                    ,[3, 4]
                    ,[5, 6]
                    ]
         = [1, 4]
example3 = Refl


main : IO ()
main = do
  putStrLn "typechecks."