It seems that
#[global] Bind Scope isn't superglobal, which is unfortunate in combination with namespacey-modules (here using
Include since it makes the problem more annoying):
Module Type N_alias. (* In fact, imagine a newtype wrapper*) Definition t := N. #[global] Bind Scope N_scope with t. End N_alias. Module virt_addr. Include N_alias. End virt_addr. #[global] Bind Scope N_scope with virt_addr.t. (* Seems I need this too, or the next line fails! *) Definition test (a b : virt_addr.t) : virt_addr.t := a + b.
More in general, I suspect real namespaces should not hide
#[export] effects https://github.com/coq/ceps/pull/25...
Is this an unexpected bug or an expected behavior?
Also mentioned in https://github.com/coq/ceps/pull/25#issuecomment-934444714 for future reference.
Yes, there is a perennial confusion between superglobal / export semantics for stuff that is attached to kernel definitions
both semantics make sense imo
(there is the same issue with Arguments / head constants, etc.)
Namespace virt_addr. we could get an even better semantics: declarations are visible iff containing _modules_ are imported, _not_ counting namespaces.
But for now, having both
#[export] work for everything uniformly would be great, even if I understand that’s sadly tons of work (due to unnecessary complexity?)
backwards compat more than complexity I think
although it's also kinda hard to find what's using global for what meaning, that could count as complexity
FWIW filed https://github.com/coq/coq/issues/14988 to refer to it.
Last updated: Feb 06 2023 at 12:04 UTC