[Agda] laziness damaged

[Serge D. Mechveliani]

People,

The issue 716 on the Bug Tracker includes an archive with an 
implementation for sorting functions  orderList-easy  and  orderList
for the `merge' method (O(n*log(n))
(see the comments on the Tracker).
The result of  orderList  is a record including a proof for orderedness
of the result list. 
The function `main' applies  orderList  to certain long list and prints  
out  [head ys, last ys]  for the result  ys
-- without using the proof part.
Still the cost of this computation is 6 times more than in the case of
orderList-easy
(for  Agda-2.3.0.1 + MAlonzo + lib-0.6).

Nils Anders writes there in `comments'

> This can certainly take extra time (and space) if the compiler isn't 
> smart enough to erase the proofs (and MAlonzo isn't).


Dear Agda developers,
please, pay attention to this point of laziness.

Agda is said _lazy_.
The developers even said "it is too lazy at the moment".
And now, it occurs  too strict at the moment.

For example, Haskell laziness would not allow this factor of 6 (in GHC) 
-- in many cases (though, it depends on the code details). 
Consider a function for division of naturals with remainder, returning 
a pair  (quot , rem),  where both parts are recursively accumulated in 
the program. And consider a client function
                            f n m = let (_, r) = quotRem n m in  r^2

For any reasonably programmed  quotRem,  f  will save the cost related
to accumulation of  quot.  This is by laziness.
One needs to use all the benefits of laziness.
This is very important for practice, mathematical methods are full with 
such examples.

May be, Agda has some profound reason for being strict in this particular
case and point?  What about the example of quotRem ? 
What is with other Agda compilers?

Thanks,
Sergei