Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Inconsistent treatment of redeclarations of names #5976

Open
nad opened this issue Jun 25, 2022 · 1 comment
Open

Inconsistent treatment of redeclarations of names #5976

nad opened this issue Jun 25, 2022 · 1 comment
Labels
modules Issues relating to the module system scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
Milestone
icebox

Comments

@nad
Copy link
Contributor

nad commented Jun 25, 2022

Currently the following code is allowed:

module _ where

module M where

import Agda.Primitive   as M
import Agda.Builtin.Nat as M

However, the following code is rejected:

module _ where

import Agda.Primitive   as M
import Agda.Builtin.Nat as M

module M where
Duplicate definition of module M. Previous definition of module M
at
[…]/Agda/Primitive.agda:5,13-22
when scope checking the declaration
  module M where

I suspect that this is by accident rather than design, and I think we should treat these two cases in the same way.

Here is another example. The following code is accepted:

module _ where

module M where

  postulate Nat : Set

open import Agda.Builtin.Nat

open M public

However, the following code is not accepted:

module _ where

module M where

  postulate Nat : Set

open import Agda.Builtin.Nat

Nat : Set
Nat = M.Nat
Multiple definitions of Nat. Previous definition at
[…]/Agda/Builtin/Nat.agda:8,6-9
when scope checking the declaration
  Nat : Set
@nad nad added type: bug Issues and pull requests about actual bugs modules Issues relating to the module system labels Jun 25, 2022
@nad nad added this to the icebox milestone Jun 25, 2022
@andreasabel andreasabel added the scope Issues relating to scope checking label Jun 27, 2022
@andreasabel
Copy link
Member

See also https://github.com/andreasabel/agda-scope#rfc-agda-shadowing-rules.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
modules Issues relating to the module system scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
2 participants
@nad @andreasabel