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

[Nils Anders Danielsson]

On 2013-01-29 04:59, Wolfram Kahl wrote:
> My main question is: Does the problem with ``using public'' only affect ``using'',
> or also ``hiding''?

I documented the problem in a patch comment:

   Failed attempt to exclude private things when applying modules.
   + When the user writes
   
       open M e <import directive>
   
     or
   
       module X = M e <import directive>
   
     there is little point in including private things in the generated
     modules, with some exceptions. However, the exceptions are quite
     important. For instance, consider
   
       module X = M A using (c),
   
     where c is a constructor of the datatype D. If we do not include
     "D A" as a private member of X, then we cannot (in general, with the
     current setup) fill in all the "Defn" fields for X.c. This could
     perhaps be fixed, but there may be other exceptions which I have not
     thought of, so I will roll back (most of) this patch.

-- 
/NAD