dependent type Matrix with implicit conversion from Vect m (Vect n a)

Matrix

module Matrix

data Matrix : Nat -> Nat -> Type -> Type where
  Matr : Vect m (Vect n a) -> Matrix n m a

(+) : Matrix n m a -> Vect n a -> Matrix n (m + 1) a
(+) (Matr rows) row = Matr (rows ++ [row])

implicit vectVectToMatr : Vect m (Vect n a) -> Matrix n m a
vectVectToMatr = Matr

example usage:

[[1,2], [3,4]] + [5,6]
-- Matr [[1, 2], [3, 4], [5, 6]] : Matrix 2 3 Integer

and of course you can't add mismatching rows

[[1,2], [3,4]] + [5,6,7]
--         Can't unify
--                Vect (S n) a
--        with
--                Vect 0 a
--
--        Specifically:
--                Can't unify
--                        S n
--                with
--                        0