{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2649","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2649/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2649/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2649/events","html_url":"https://github.com/agda/agda/issues/2649","id":243234540,"number":2649,"title":"Empty list of \"previous definition\" in duplicate definition error","user":{"login":"gallais","id":1094905,"avatar_url":"https://avatars1.githubusercontent.com/u/1094905?v=4","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false},"labels":[{"id":245647635,"url":"https://api.github.com/repos/agda/agda/labels/error-reporting","name":"error-reporting","color":"ededed","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/18","html_url":"https://github.com/agda/agda/milestone/18","labels_url":"https://api.github.com/repos/agda/agda/milestones/18/labels","id":2003446,"number":18,"title":"2.5.3","description":null,"creator":{"login":"UlfNorell","id":447950,"avatar_url":"https://avatars0.githubusercontent.com/u/447950?v=4","gravatar_id":"","url":"https://api.github.com/users/UlfNorell","html_url":"https://github.com/UlfNorell","followers_url":"https://api.github.com/users/UlfNorell/followers","following_url":"https://api.github.com/users/UlfNorell/following{/other_user}","gists_url":"https://api.github.com/users/UlfNorell/gists{/gist_id}","starred_url":"https://api.github.com/users/UlfNorell/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/UlfNorell/subscriptions","organizations_url":"https://api.github.com/users/UlfNorell/orgs","repos_url":"https://api.github.com/users/UlfNorell/repos","events_url":"https://api.github.com/users/UlfNorell/events{/privacy}","received_events_url":"https://api.github.com/users/UlfNorell/received_events","type":"User","site_admin":false},"open_issues":59,"closed_issues":134,"state":"open","created_at":"2016-09-14T08:32:52Z","updated_at":"2017-07-24T12:09:14Z","due_on":null,"closed_at":null},"comments":0,"created_at":"2017-07-16T11:51:45Z","updated_at":"2017-07-24T12:24:57Z","closed_at":null,"body":"While working on #2648, I've come across a weird error message:\r\n\r\n```\r\n/home/gallais/projects/agda/test/LibSucceed/Issue854/Run.lagda:65,10-11\r\nDuplicate definition of module M. Previous definition of module M\r\nat\r\nwhen scope checking the declaration\r\n  module M = RawMonad rawMonad\r\n```\r\n\r\nThe problem arises in [this file](https://github.com/agda/agda/blob/master/test/LibSucceed/Issue854/Run.lagda#L65) from [this `module M` definition](https://github.com/agda/agda-stdlib/blob/78d9beb9c951f63471a5196fe9cdfcc5c0e22d43/src/Data/List/Any/Membership/Propositional.agda#L25) which is simply used as an anonymous \"module level\" lambda (and, arguably, should be a `private` definition)."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/317405981","html_url":"https://github.com/agda/agda/issues/2649#issuecomment-317405981","issue_url":"https://api.github.com/repos/agda/agda/issues/2649","id":317405981,"user":{"login":"gallais","id":1094905,"avatar_url":"https://avatars1.githubusercontent.com/u/1094905?v=4","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false},"created_at":"2017-07-24T12:24:57Z","updated_at":"2017-07-24T12:24:57Z","body":"Shrunk test case:\r\n\r\nIssue2649-3.agda:\r\n```\r\nmodule Issue2649-3 where\r\n\r\nmodule MyModule (A : Set) (a : A) where\r\n\r\n  dft : A\r\n  dft = a\r\n```\r\nIssue2649-2.agda:\r\n```\r\nmodule Issue2649-2 where\r\n\r\nopen import Issue2649-3\r\n\r\nopen module M {A : Set} {a : A} = MyModule A a public\r\n```\r\nIssue2649.agda:\r\n```\r\nmodule Issue2649 where\r\n\r\nopen import Issue2649-3\r\nopen import Issue2649-2\r\n\r\nid : {A : Set} → A → A\r\nid x = M.dft where module M = MyModule _ x\r\n```\r\n\r\nError message:\r\n\r\n```\r\n/home/gallais/languages/agda/Issue2649.agda:7,27-28\r\nDuplicate definition of module M. Previous definition of module M\r\nat\r\nwhen scope checking the declaration\r\n  module M = MyModule _ x\r\n```"}}
{"actor":{"display_login":"gallais"}}