{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1777","labels_url":"https://api.github.com/repos/agda/agda/issues/1777/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1777/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1777/events","html_url":"https://github.com/agda/agda/issues/1777","id":126580154,"number":1777,"title":"with-abstraction should be allowed when a case includes record syntax","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":[{"url":"https://api.github.com/repos/agda/agda/labels/info-needed","name":"info-needed","color":"159818"},{"url":"https://api.github.com/repos/agda/agda/labels/records","name":"records","color":"ededed"}],"state":"open","locked":false,"assignee":{"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},"milestone":null,"comments":2,"created_at":"2016-01-14T05:25:57Z","updated_at":"2016-01-14T18:50:07Z","closed_at":null,"body":"Agda is not allowing the use of a with-abstraction when a case includes record syntax. In ```qux```, below, Agda complains that ```With clause pattern record { unMaybeRecord = just x } is not an instance of its parent pattern```. However, ```bar``` and ```baz``` type-check.\r\n\r\n```\r\nmodule WithCaseSplitRecord (A : Set) where\r\n  case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B\r\n  case x of f = f x\r\n\r\n  data MaybeData : Set where\r\n    nothing : MaybeData\r\n    just : A → MaybeData\r\n\r\n  record MaybeRecord : Set where\r\n    field\r\n      unMaybeRecord : MaybeData\r\n\r\n  postulate\r\n    foo : A → MaybeData\r\n\r\n  bar : MaybeData → Set\r\n  bar nothing = {!!}\r\n  bar (just x) with foo x\r\n  ... | nothing = {!!}\r\n  ... | just y = {!!}\r\n\r\n  baz : MaybeRecord → Set\r\n  baz record { unMaybeRecord = nothing } = {!!}\r\n  baz record { unMaybeRecord = just x } =\r\n    case foo x of\r\n    λ { nothing → {!!}\r\n      ; (just y) → {!!}\r\n      }\r\n\r\n  qux : MaybeRecord → Set\r\n  qux record { unMaybeRecord = nothing } = {!!}\r\n  qux record { unMaybeRecord = just x } with foo x\r\n  ... | foox = {!!}\r\n```\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/171736704","html_url":"https://github.com/agda/agda/issues/1777#issuecomment-171736704","issue_url":"https://api.github.com/repos/agda/agda/issues/1777","id":171736704,"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-01-14T18:50:07Z","updated_at":"2016-01-14T18:50:07Z","body":"Much better. However, there is a problem with case-splittng. If I try to C-c C-c on ```foox``` in the last hole of ```qux```, I get the following, which does not type-check:\r\n```\r\n  qux : MaybeRecord → Set\r\n  qux record { unMaybeRecord = nothing } = {!!}\r\n  qux record { unMaybeRecord = just x } with foo x\r\n  qux (.Sandbox.WithCaseSplitRecord.recCon-NOT-PRINTED (just x)) | nothing = ?\r\n  qux (.Sandbox.WithCaseSplitRecord.recCon-NOT-PRINTED (just x₁)) | just x = ?\r\n```"}}