[Agda] Re: Does Agda2 have fast arrays?

[Permjacov Evgeniy]

 >OK, so we're agreeing on what the problem is -- it's coercions causing
problems for the ghc optimizer, where we're differing is >how much
impact it has in practice. Do you have an example in mind of a
(preferably simple!) program where ghc relies heavily >on type
information for optimzing?

Any tail recursive function can be 'unboxed' i.e. an accumulator
argument having one (and exactly one) data constructor can be broken
into pieces until only raw unboxed values left. The compiler needs
knowledge that folding function is strict in all accumulator fields for
this to happen. Any coerces will mess with strictness analisys, possibly
preventing optimization.

The inliner has some machinery, that relies on functions 'sizes',
coerces` role here is unknown.

Simplifier can work somehow with datatypes with one constructor,
throwing away unnesesary pattern matches.

You can also read 'performance haskell' entry in haskell wiki for other
examples.