{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2372","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2372/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2372/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2372/events","html_url":"https://github.com/agda/agda/issues/2372","id":198225795,"number":2372,"title":"error message given in a confusing location (\"Terms marked as eligible for instance search should end with a name\")","user":{"login":"m0davis","id":203587,"avatar_url":"https://avatars.githubusercontent.com/u/203587?v=3","gravatar_id":"","url":"https://api.github.com/users/m0davis","html_url":"https://github.com/m0davis","followers_url":"https://api.github.com/users/m0davis/followers","following_url":"https://api.github.com/users/m0davis/following{/other_user}","gists_url":"https://api.github.com/users/m0davis/gists{/gist_id}","starred_url":"https://api.github.com/users/m0davis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/m0davis/subscriptions","organizations_url":"https://api.github.com/users/m0davis/orgs","repos_url":"https://api.github.com/users/m0davis/repos","events_url":"https://api.github.com/users/m0davis/events{/privacy}","received_events_url":"https://api.github.com/users/m0davis/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-12-31T09:33:11Z","updated_at":"2016-12-31T09:52:28Z","closed_at":null,"body":"Agda properly complains that `Terms marked as eligible for instance search should end with a name`, but the error message can come come too late, confusing the user. This happens when the invalid instance declaration's type is inferred.\r\n```\r\npostulate D : Set\r\n\r\ninstance i = D --If the type of `i` were given explicitly, Agda would display the error here\r\n\r\nrecord R : Set₁ where\r\n  field\r\n    r : Set\r\n\r\nopen R {{ ... }} public\r\n\r\nf : r → Set₁ -- Here, confusingly, is where Agda registers its complaint\r\nf = {!!}\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/269857982","html_url":"https://github.com/agda/agda/issues/2372#issuecomment-269857982","issue_url":"https://api.github.com/repos/agda/agda/issues/2372","id":269857982,"user":{"login":"m0davis","id":203587,"avatar_url":"https://avatars.githubusercontent.com/u/203587?v=3","gravatar_id":"","url":"https://api.github.com/users/m0davis","html_url":"https://github.com/m0davis","followers_url":"https://api.github.com/users/m0davis/followers","following_url":"https://api.github.com/users/m0davis/following{/other_user}","gists_url":"https://api.github.com/users/m0davis/gists{/gist_id}","starred_url":"https://api.github.com/users/m0davis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/m0davis/subscriptions","organizations_url":"https://api.github.com/users/m0davis/orgs","repos_url":"https://api.github.com/users/m0davis/repos","events_url":"https://api.github.com/users/m0davis/events{/privacy}","received_events_url":"https://api.github.com/users/m0davis/received_events","type":"User","site_admin":false},"created_at":"2016-12-31T09:52:28Z","updated_at":"2016-12-31T09:52:28Z","body":"Probably related: Agda doesn't find the instance when it's declared in a separate file.\r\n\r\nM1.agda\r\n```\r\npostulate D : Set\r\n\r\nrecord R : Set₁ where\r\n  field\r\n    r : Set\r\n\r\nopen R {{ ... }} public\r\n\r\ninstance iR = record { r = D }\r\n```\r\nM2.agda\r\n```\r\nopen import M1\r\n\r\nf : r → Set₁ -- No instance of type R was found in scope.\r\nf = {!!}\r\n```"}}
{"actor":{"display_login":"m0davis"}}