[Agda] Does Agda2 have fast arrays?

[Brandon Moore]

  I tried adding rule:

{-# RULES "coerce=id" forall (x :: a) . unsafeCoerce x = x #-}

but (as you can see) it only fired once, sigh.  It maybe that unsafeCoerce is being inlined before optimized, unfortunately trying to optimize the primitive:
Core is a typed language and rules can only apply if they preserve types. For example there are a bunch of rules which try to replace calls to fromIntegral with assorted specialized conversions. I think you can take this as evidence that trying to generate Haskell cleaner Haskell code simply by leaving out unnecessary coercions wouldn't be very effective on this example. 
{-# RULES "coerce#=id" forall (x :: a) . unsafeCoerce# x = x #-}

is a syntax error!  (Apparently rules don't like identifiers with #s in their names.)  Somewhat annoying, since (AFAICT) most of the occurrences of unsafeCoerce are actually statically of type a->a, so should be removeable by the rule coerce=id.
are you compiling with the MagicHash option?