{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/3071","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/3071/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/3071/comments","events_url":"https://api.github.com/repos/agda/agda/issues/3071/events","html_url":"https://github.com/agda/agda/pull/3071","id":325375226,"number":3071,"title":"generalize (second version)","user":{"login":"divipp","id":1005160,"avatar_url":"https://avatars2.githubusercontent.com/u/1005160?v=4","gravatar_id":"","url":"https://api.github.com/users/divipp","html_url":"https://github.com/divipp","followers_url":"https://api.github.com/users/divipp/followers","following_url":"https://api.github.com/users/divipp/following{/other_user}","gists_url":"https://api.github.com/users/divipp/gists{/gist_id}","starred_url":"https://api.github.com/users/divipp/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/divipp/subscriptions","organizations_url":"https://api.github.com/users/divipp/orgs","repos_url":"https://api.github.com/users/divipp/repos","events_url":"https://api.github.com/users/divipp/events{/privacy}","received_events_url":"https://api.github.com/users/divipp/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-05-22T16:38:08Z","updated_at":"2018-05-23T13:06:49Z","closed_at":null,"author_association":"NONE","pull_request":{"url":"https://api.github.com/repos/agda/agda/pulls/3071","html_url":"https://github.com/agda/agda/pull/3071","diff_url":"https://github.com/agda/agda/pull/3071.diff","patch_url":"https://github.com/agda/agda/pull/3071.patch"},"body":"Second version of 'generalize'\r\n\r\nTODO:\r\n\r\n- documentation in `doc/release-notes`\r\n- more tests\r\n\r\nKnown bugs & limitations:\r\n\r\n- bug: generalizable variables escape their scope\r\n- more robust implementation: Currently the metavariables in the types of generalizable variables are solved during type inference, and later these metavariables are reset to unsolved state. Better would be to add fresh metavariables each time.\r\n- The generalized type should be build up from outside to inside, adding outer bindings first. Currently it is done in the other way around, so metavariables are solved before the generalization begins, but not solved during the generalization. See <https://lists.chalmers.se/pipermail/agda/2018/010188.html>\r\n- feature request: support generalize in the rhs <https://github.com/divipp/agda/issues/4>\r\n- feature request: export generalizable variables\r\n- other bugs: <https://github.com/divipp/agda/issues>\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/391339593","html_url":"https://github.com/agda/agda/pull/3071#issuecomment-391339593","issue_url":"https://api.github.com/repos/agda/agda/issues/3071","id":391339593,"user":{"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},"created_at":"2018-05-23T13:06:49Z","updated_at":"2018-05-23T13:06:49Z","author_association":"MEMBER","body":"Looks good to me.\r\n\r\n@asr Should we wait to merge until after the `2.5.4` release to avoid conflicts with potential last-minute bug fixes?"}}
{"actor":{"display_login":"UlfNorell"}}