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

Nils Anders Danielsson nad at chalmers.se
Tue Jan 29 11:27:46 CET 2013

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>
       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.


More information about the Agda mailing list