[Agda] Cost of ``open ... public using (...)''?

[Wolfram Kahl]

On

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.CodeSprints

I read:

 |     Nisse, Andreas, Peter II: Optimizing Agda (positivity graph) 
 | 
 | [...]
 | We: Trying to make "open M x using (y)" not create useless things.
 | Fr: Gave up on this for now.

I have observed significant cost of

    open M x public using (y)

, and I am working around this regularly (at some cost to
the niceness of my code), but I don't think that I have ever seen
this performance impact without ``public''.
(I just did a quick test: ``using'' in a pure import context (i.e., no ``public'')
 actually saved a tiny bit on allocation and MUT time.)


My main question is: Does the problem with ``using public'' only affect ``using'',
or also ``hiding''?
(``hiding'' is much more of a hassle to work around, especially with large modules...)


Apart from that, I am also curious: What is behind this effect anyways?
Is there an issue on the issue tracker associated with it?
(I could not identify anything from what I found for ``using'' or ``open using''.)


Wolfram


P.S.: This page seems to be strangely disconnected from the AIM it belonged to...