[Agda] Does Agda2 have fast arrays?

[Permjacov Evgeniy]

 Hello. I'm currently implementing some linear algebra in haskell. The
problem is, that polymorphic arrays in Haskell are slow and their sizes
are not encoded in types (there are some tricks, though. But code looks
quite ugly for arrays with dinamic size). Agda has dependent types, so
it is possible to encode array sizes directly in array type. But
language for performance calculations need compact arrays with O(0) fast
indexing. So, is there any simple way to build 'unboxed arrays' for
Agda? Maybe there are some useful modules or built-ins ?