[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