{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1716","labels_url":"https://api.github.com/repos/agda/agda/issues/1716/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1716/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1716/events","html_url":"https://github.com/agda/agda/issues/1716","id":116069672,"number":1716,"title":"Discussion: instance argument candidates from the context","user":{"login":"UlfNorell","id":447950,"avatar_url":"https://avatars.githubusercontent.com/u/447950?v=3","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},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/enhancement","name":"enhancement","color":"84b6eb"},{"url":"https://api.github.com/repos/agda/agda/labels/Instance","name":"Instance","color":"ededed"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-11-10T09:33:21Z","updated_at":"2015-11-10T16:55:54Z","closed_at":null,"body":"Currently any variable in the context is available for instance search, so you can define things like\r\n\r\n    foo : {A : Set} (eqA : Eq A) → A → A → Bool\r\n    foo eqA x y = isYes (x == y)\r\n\r\nMy question is this: are there cases where you need this, or could we restrict instance search to only consider variables from the context that are themselves instance arguments?\r\n\r\nThere are two reasons why I think this would be desirable\r\n- it mirrors the treatment of top-level instances (only things declared `instance` are considered)\r\n- there can be very many things in the context, making instance search slow"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/155485283","html_url":"https://github.com/agda/agda/issues/1716#issuecomment-155485283","issue_url":"https://api.github.com/repos/agda/agda/issues/1716","id":155485283,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"created_at":"2015-11-10T16:55:54Z","updated_at":"2015-11-10T16:55:54Z","body":"I cannot judge the consequences of this, but a cautious agreement to your proposal from me."}}