{"action":"opened","issue":{"url":"https://api.github.com/repos/agda/agda-stdlib/issues/539","repository_url":"https://api.github.com/repos/agda/agda-stdlib","labels_url":"https://api.github.com/repos/agda/agda-stdlib/issues/539/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda-stdlib/issues/539/comments","events_url":"https://api.github.com/repos/agda/agda-stdlib/issues/539/events","html_url":"https://github.com/agda/agda-stdlib/issues/539","id":383647562,"node_id":"MDU6SXNzdWUzODM2NDc1NjI=","number":539,"title":"program generated by ghc backend segfaults","user":{"login":"jmchapman","id":652332,"node_id":"MDQ6VXNlcjY1MjMzMg==","avatar_url":"https://avatars1.githubusercontent.com/u/652332?v=4","gravatar_id":"","url":"https://api.github.com/users/jmchapman","html_url":"https://github.com/jmchapman","followers_url":"https://api.github.com/users/jmchapman/followers","following_url":"https://api.github.com/users/jmchapman/following{/other_user}","gists_url":"https://api.github.com/users/jmchapman/gists{/gist_id}","starred_url":"https://api.github.com/users/jmchapman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jmchapman/subscriptions","organizations_url":"https://api.github.com/users/jmchapman/orgs","repos_url":"https://api.github.com/users/jmchapman/repos","events_url":"https://api.github.com/users/jmchapman/events{/privacy}","received_events_url":"https://api.github.com/users/jmchapman/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-11-22T20:10:17Z","updated_at":"2018-11-22T20:10:17Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"I have an evaluator for a language with well typed terms. If I compile the evaluator and test it on certain examples the generated haskell program segfaults at runtime. The language has bounded integers and bytestrings, the bounds are represented as extra proof arguments to the constructors of integers and bytestrings. If I make the bounds trivial (i.e. the unit type instead of i < j) then it works ok. It's from a large development spread over multiple files, I have boiled it down to a ~500 line single file which I attach. I will try to reduce it further but I thought this was a start.\r\n\r\nI have tested it with the latest versions of Agda+ std-lib from github.\r\n\r\n[Main.lagda.txt](https://github.com/agda/agda-stdlib/files/2609177/Main.lagda.txt)\r\n\r\n"}}
{"actor":{"display_login":"jmchapman"}}