module _ where
import Agda.Builtin.Nat as NAT
module M where
abstract
open import Agda.Builtin.Nat public -- no warning
z : Nat
z = zero
A : Set
A = M.Nat -- fails if 'public' is removed
module O where
abstract
open NAT public -- Warning OpenPublicAbstract
z : Nat
z = zero
B : Set
B = O.Nat -- fails if 'public' is removed
The OpenPublicAbstract warning is not issued in the first case (open import), probably that is unintended.
It is issued in the second case (open), but the warning is wrong.
public does not have any effect in an abstract block.
when scope checking the declaration
module O where
If that were true, I could remove public where it is marked as dead code, but then O.Nat is no longer in scope.
The warning was introduced by @gallais in PR #3984 when fixing #760 to clarify the situation on how private and abstract act on imports (open).
True is that abstract has no effect on open public, however here we already have the UselessAbstract warning.
However public does have some effect even in abstract blocks, so the current warning OpenPublicAbstract is misleading.
I guess the intention was that abstract does not have an effect on open and import and these declarations should not be put in abstract blocks because this can confuse the reader. Yet it is not about the public, really.
The warning OpenPublicPrivate has similar problems.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4