{"action":"closed","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1771","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1771/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1771/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1771/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/1771","id":51197777,"number":1771,"title":"Out of memory typechecking list literals","user":{"login":"projedi","id":399115,"avatar_url":"https://avatars.githubusercontent.com/u/399115?v=3","gravatar_id":"","url":"https://api.github.com/users/projedi","html_url":"https://github.com/projedi","followers_url":"https://api.github.com/users/projedi/followers","following_url":"https://api.github.com/users/projedi/following{/other_user}","gists_url":"https://api.github.com/users/projedi/gists{/gist_id}","starred_url":"https://api.github.com/users/projedi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/projedi/subscriptions","organizations_url":"https://api.github.com/users/projedi/orgs","repos_url":"https://api.github.com/users/projedi/repos","events_url":"https://api.github.com/users/projedi/events{/privacy}","received_events_url":"https://api.github.com/users/projedi/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/A-Confirmed","name":"A-Confirmed","color":"fbca04"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2014-12-06T22:01:24Z","updated_at":"2016-04-11T16:53:17Z","closed_at":"2016-04-11T16:53:17Z","body":"When trying to typecheck this:\r\n```idris\r\nmodule Main\r\n\r\ntest : List () -> IO ()\r\n\r\nmain : IO ()\r\nmain = do\r\n  test\r\n    [ ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    ]\r\n  test\r\n    [ ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    , ()\r\n    ]\r\n```\r\nidris eats too much memory.\r\n\r\nProfiling shows that all the allocations are coming from `Idris.AbsSyntax.mkUniqueNames`. `traceM`-powered debugging shows that allocation happens while evaluating `Idris.ElabTerm.build` in `Idris.Elab.Clause.elabClause`. And all the memory is used to store the AST which for a list of length\r\n`n` is of size `3^n` because of overloaded `::` and `Nil` constructors.\r\n\r\nI tried to understand who and why evaluates the entire AST before pruning the alternatives but got lost."}}