[Agda] Does Agda2 have fast arrays?

[Alan Jeffrey]

On 10/04/2010 10:15 PM, Brandon Moore wrote:
>
>    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.

Indeed, but there should still be lots of potential for this rule to 
fire, for example Agda generates:

   (d11 (Unsafe.Coerce.unsafeCoerce d2)) (Unsafe.Coerce.unsafeCoerce v0)

where:

   d11 :: (Int -> (Int -> (Data.Vector.Vector Int)))
   d11 = Data.Vector.enumFromN

   d2 :: Int
   d2 = 1

I don't see why coerce=id isn't firing in this case, and rewriting to:

   (d11 d2 (Unsafe.Coerce.unsafeCoerce v0)

Time to muck around with -ddump-simpl-iterations...

> {-# 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?

Aha, thanks!

A.