[Agda] Does Agda2 have fast arrays?

[Don Stewart]

nad:
> On 2010-10-02 18:17, Don Stewart wrote:
>> Could Agda target one of the high performance array libraries in
>> Haskell?  E.g. repa or vector?
>
> Agda has a Haskell FFI, so that should be easy, assuming that the
> library APIs don't use too exotic types. However, Agda code is compiled
> into Haskell by inserting unsafeCoerce almost everywhere, so I would not
> expect good performance, especially if REWRITE pragmas are involved.
>

What can we do about the coercions? I suspect they make GHC sad.