{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2190","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2190/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2190/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2190/events","html_url":"https://github.com/agda/agda/issues/2190","id":177387147,"number":2190,"title":"with abstracts now also in arguments of parent function","user":{"login":"mechvel","id":1506057,"avatar_url":"https://avatars.githubusercontent.com/u/1506057?v=3","gravatar_id":"","url":"https://api.github.com/users/mechvel","html_url":"https://github.com/mechvel","followers_url":"https://api.github.com/users/mechvel/followers","following_url":"https://api.github.com/users/mechvel/following{/other_user}","gists_url":"https://api.github.com/users/mechvel/gists{/gist_id}","starred_url":"https://api.github.com/users/mechvel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mechvel/subscriptions","organizations_url":"https://api.github.com/users/mechvel/orgs","repos_url":"https://api.github.com/users/mechvel/repos","events_url":"https://api.github.com/users/mechvel/events{/privacy}","received_events_url":"https://api.github.com/users/mechvel/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/documentation","name":"documentation","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/parameter-refinement","name":"parameter-refinement","color":"f9d0c4"},{"url":"https://api.github.com/repos/agda/agda/labels/regression","name":"regression","color":"e11d21"},{"url":"https://api.github.com/repos/agda/agda/labels/with","name":"with","color":"ededed"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/16","html_url":"https://github.com/agda/agda/milestones/2.5.2","labels_url":"https://api.github.com/repos/agda/agda/milestones/16/labels","id":1713715,"number":16,"title":"2.5.2","description":null,"creator":{"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},"open_issues":34,"closed_issues":134,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-09-17T11:07:59Z","due_on":null,"closed_at":null},"comments":8,"created_at":"2016-09-16T10:01:06Z","updated_at":"2016-09-17T17:32:37Z","closed_at":null,"body":"This is on  Development Agda of September 16, 2016,  ghc-7.10.2,  \r\nDebian Linux.                                                    \r\nPlease, download \r\n\r\nhttp://www.botik.ru/pub/local/Mechveliani/agdaNotes/Bug-sep16-2016.agda \r\n\r\nIt is a small program.\r\nThere the argument   `sm<mty-p'ps `  \r\n has type \r\n`sm < mty (p' ∷ ps)`\r\n\r\nBut the type checker does not find this.\r\nAnd it improves when it is set    \r\n`debug =  sm<mty-p'ps`\r\ninstead of `sm<mty-p'ps`,\r\nwith setting for `debug`  the signature  \r\n`sm < mty (p' ∷ ps)`\r\n\r\n\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/247792013","html_url":"https://github.com/agda/agda/issues/2190#issuecomment-247792013","issue_url":"https://api.github.com/repos/agda/agda/issues/2190","id":247792013,"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},"created_at":"2016-09-17T17:32:37Z","updated_at":"2016-09-17T17:32:37Z","body":"> But at least, this my particular example needs to be type-checked. It will be unnatural if it is not type-checked. Will it?\r\n\r\nNot without modifications. With-abstraction now abstracts also over variables bound outside the function, like module parameters or parent function arguments. When that's not desirable you can do what you did and define an alias (`debug` in your case) to hide it from abstraction, or simply not use a 'with'."}}
{"actor":{"display_login":"UlfNorell"}}