[Agda] Dimension-safe matrix operations?

[Kenichi Asai]

If I want to use dimension-safe matrix operations (on a type of
matrices parameterized by numbers of rows and columns, similar to
Vec), what is the good way?  Are there comprehensive libraries for
them already, probably?  I appreciate any information.

Also, is the same (or similar) thing possible in Haskell (or even
OCaml)?  If so, information on Haskell (or OCaml) libraries is also
welcome.  Thank you in advance.

-- 
Kenichi Asai