{"action":"opened","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4237","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4237/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4237/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4237/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/4237","id":278694272,"number":4237,"title":"Clause errors always report right-hand side, even for left-hand-side errors","user":{"login":"eraserhd","id":147284,"avatar_url":"https://avatars0.githubusercontent.com/u/147284?v=4","gravatar_id":"","url":"https://api.github.com/users/eraserhd","html_url":"https://github.com/eraserhd","followers_url":"https://api.github.com/users/eraserhd/followers","following_url":"https://api.github.com/users/eraserhd/following{/other_user}","gists_url":"https://api.github.com/users/eraserhd/gists{/gist_id}","starred_url":"https://api.github.com/users/eraserhd/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/eraserhd/subscriptions","organizations_url":"https://api.github.com/users/eraserhd/orgs","repos_url":"https://api.github.com/users/eraserhd/repos","events_url":"https://api.github.com/users/eraserhd/events{/privacy}","received_events_url":"https://api.github.com/users/eraserhd/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-12-02T15:59:15Z","updated_at":"2017-12-02T15:59:15Z","closed_at":null,"author_association":"COLLABORATOR","body":"The span of clauses is actually the span of the right-hand side, and so this\r\nis reported when there is an error on the right-hand side _or the left-hand\r\nside_.\r\n\r\n# Steps to Reproduce\r\n\r\nFrom `test/error006/WithPatsNoWith.idr`:\r\n\r\n```idris\r\nmodule WithPatsNoWith\r\n\r\nfoo : Int -> Bool\r\nfoo 1 | 2 | 3 = True\r\nfoo _ = False\r\n```\r\n\r\nFrom `test/regression002/reg055a.idr`:\r\n\r\n```idris\r\napply : (a -> a -> b) -> a -> a\r\napply (\\x => \\y => x) a = a\r\napply f a = a \r\n```\r\n\r\n# Expected Behavior\r\n\r\n```\r\nWithPatsNoWith.idr:4:4-13:When checking left hand side of foo:\r\nunexpected patterns outside of \"with\" block\r\n```\r\n\r\nand\r\n\r\n```\r\nreg055a.idr:13:7-23:When checking left hand side of Foo.apply:\r\nCan't match on apply (\\x, y => x) a\r\n```\r\n\r\n# Observed Behavior\r\n\r\n```\r\nWithPatsNoWith.idr:4:15-20:When checking left hand side of foo:\r\nunexpected patterns outside of \"with\" block\r\n```\r\n\r\nand\r\n\r\n```\r\nreg055a.idr:13:25-27:When checking left hand side of Foo.apply:\r\nCan't match on apply (\\x, y => x) a\r\n```"}}
{"actor":{"display_login":"eraserhd"}}