<div dir="ltr">Hi all,<div><br></div>I&#39;d like to initiate the discussion about anonymous modules (modules with names &#39;_&#39;) under the keyword &#39;private&#39;. Currently, such a module will be opened publicly, effectively ignoring the private keyword. I wonder how people feel about alternatives like having anonymous modules under &#39;private&#39; stay private, changing the semantics of &#39;open public&#39; under &#39;private&#39;, or even banning public opening under &#39;private&#39; but giving anonymous modules special treatments. Personally I am in favor of the last option.<div><br></div><div>I opened an issue on GitHub this morning <a href="https://github.com/agda/agda/issues/2199" target="_blank">https://github.com/agda/agda/issues/2199</a> and Andreas Abel quickly patched Agda to at least give you an error message. There is a small discussion on GitHub among Andreas, Ulf and me but Andreas (and me too) thinks we should discuss this in a larger forum.<br><div><br></div><div>Best,</div></div><div>Favonia</div></div>