{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1734","labels_url":"https://api.github.com/repos/agda/agda/issues/1734/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1734/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1734/events","html_url":"https://github.com/agda/agda/issues/1734","id":120501225,"number":1734,"title":"Clause compiler skrews up with catch-alls","user":{"login":"pigworker","id":3717047,"avatar_url":"https://avatars.githubusercontent.com/u/3717047?v=3","gravatar_id":"","url":"https://api.github.com/users/pigworker","html_url":"https://github.com/pigworker","followers_url":"https://api.github.com/users/pigworker/followers","following_url":"https://api.github.com/users/pigworker/following{/other_user}","gists_url":"https://api.github.com/users/pigworker/gists{/gist_id}","starred_url":"https://api.github.com/users/pigworker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pigworker/subscriptions","organizations_url":"https://api.github.com/users/pigworker/orgs","repos_url":"https://api.github.com/users/pigworker/repos","events_url":"https://api.github.com/users/pigworker/events{/privacy}","received_events_url":"https://api.github.com/users/pigworker/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/bug","name":"bug","color":"fc2929"},{"url":"https://api.github.com/repos/agda/agda/labels/PatternMatching","name":"PatternMatching","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/Priority-High","name":"Priority-High","color":"ededed"}],"state":"closed","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":3,"created_at":"2015-12-04T22:40:57Z","updated_at":"2015-12-05T20:26:00Z","closed_at":"2015-12-05T20:22:03Z","body":"Here's some trouble, distilled down from an exercise I was preparing for my class. I'm using version 2.4.2.4 (so that I can compile programs which use copatterns).\r\n\r\nI need a few basics: \r\n\r\n    record One : Set where constructor <>\r\n\r\n    data Two : Set where tt ff : Two\r\n\r\n    record Sg (S : Set)(T : S -> Set) : Set where\r\n      constructor _,_\r\n      field\r\n        fst : S\r\n        snd : T fst\r\n    open Sg public\r\n\r\n    _+_ : Set -> Set -> Set\r\n    S + T = Sg Two \\ { tt -> S ; ff -> T }\r\n\r\nNow, I define the singletons over `Two`.\r\n\r\n    data Twoey : Two -> Set where\r\n      ffey  : Twoey ff\r\n      ttey  : Twoey tt\r\n\r\nI'll be pattern matching on a later `Twoey` to learn about an earlier `Two`.\r\n\r\nNext, I need some actual payload. Doesn't matter what.\r\n\r\n    postulate Thingy : Set\r\n\r\nSometimes we have payload and sometimes not. A Boolean value tells whether we have some.\r\n\r\n    ThingyIf : Two -> Set\r\n    ThingyIf tt = Thingy\r\n    ThingyIf ff = One\r\n\r\nI should be able to extract payload, but not necessarily all the time.\r\n\r\n    thingy? : (b : Two) -> ThingyIf b -> Twoey b + One -> Thingy + One\r\n    thingy? .ff <> (tt , ffey) = ff , <>\r\n    thingy? .tt x  (tt , ttey) = tt , x\r\n    thingy? _ _ _ = ff , <>\r\n\r\n    oops = \\ x -> thingy? tt x (tt , ttey)\r\n\r\nThe trouble is that, normalizing,\r\n\r\n    oops = \\ x -> tt , <>  -- the <> should be the payload x\r\n\r\nIt's weird. I couldn't make it happen with `Twoey b` alone: I needed `Twoey b + One`.\r\n\r\nI also checked that reordering the arguments made it go away. This...\r\n\r\n    thygni? : (b : Two) -> Twoey b + One -> ThingyIf b -> Thingy + One\r\n    thygni? .ff (tt , ffey) <> = ff , <>\r\n    thygni? .tt (tt , ttey) x  = tt , x\r\n    thygni? _ _ _ = ff , <>\r\n\r\n    spoo = \\ x -> thygni? tt (tt , ttey) x\r\n\r\n...gives\r\n\r\n    spoo = \\ x -> tt , x\r\n\r\nMoreover, replacing the gratuitous `<>` pattern by a variable...\r\n\r\n    hingy? : (b : Two) -> ThingyIf b -> Twoey b + One -> Thingy + One\r\n    hingy? .ff x  (tt , ffey) = ff , <>\r\n    hingy? .tt x  (tt , ttey) = tt , x\r\n    hingy? _ _ _ = ff , <>\r\n\r\n...gives...\r\n\r\n    ops = \\ x -> hingy? tt x (tt , ttey)\r\n\r\n...and it has to be a variable: an `_` gives the same outcome as `<>`.\r\n\r\nSadly, I discovered this problem as part of a larger system, where a `Thingy` was a file handle. The compiled code segfaulted gloriously. But it looks like the problem starts before compilation.\r\n\r\nI have a workaround, which is to use a postulated unit type in `ThingyIf`, preventing the excessive pattern matching. So I've stopped panicking. I'm afraid I can't really change the order of the arguments so easily, as it arises by instantiating a more general definition. I'd post the broader context, but it's a specimen solution to a \"live\" homework problem."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/162243394","html_url":"https://github.com/agda/agda/issues/1734#issuecomment-162243394","issue_url":"https://api.github.com/repos/agda/agda/issues/1734","id":162243394,"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-12-05T20:26:00Z","updated_at":"2015-12-05T20:26:00Z","body":"The fix was not hard: just be more corageous and follow the split tree even when there are catch-alls and literals.  Seems to work.  I guess originally I just did not know what to do in these cases.\r\n\r\nI speculate this test case never worked properly with the clause compiler."}}