{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1998","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/1998/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1998/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1998/events","html_url":"https://github.com/agda/agda/issues/1998","id":157711220,"number":1998,"title":"A postulate, a parameterised record, and an instance argument walk into a non-linear slowdown","user":{"login":"mietek","id":166207,"avatar_url":"https://avatars.githubusercontent.com/u/166207?v=3","gravatar_id":"","url":"https://api.github.com/users/mietek","html_url":"https://github.com/mietek","followers_url":"https://api.github.com/users/mietek/followers","following_url":"https://api.github.com/users/mietek/following{/other_user}","gists_url":"https://api.github.com/users/mietek/gists{/gist_id}","starred_url":"https://api.github.com/users/mietek/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mietek/subscriptions","organizations_url":"https://api.github.com/users/mietek/orgs","repos_url":"https://api.github.com/users/mietek/repos","events_url":"https://api.github.com/users/mietek/events{/privacy}","received_events_url":"https://api.github.com/users/mietek/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/instance","name":"instance","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/performance","name":"performance","color":"ededed"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-05-31T16:12:59Z","updated_at":"2016-06-06T16:48:13Z","closed_at":null,"body":"This code takes an unreasonable amount of time to typecheck.  The amount of time can be increased or decreased by adding or removing constructors of the `Baz` datatype, or adjusting the complexity of these constructors.  When the code does finally typecheck, unsolved metavariables remain.\r\n\r\nThe issue can be avoided by removing the `p` record parameter, *or* the `asBaseT` instance declaration.\r\n```agda\r\npostulate\r\n  Foo : Set\r\n\r\nrecord BaseT : Set₁ where\r\n  field f : Foo\r\n\r\nrecord ParamT (p : Foo) : Set₁ where\r\n  field f : Foo\r\n  instance\r\n    asBaseT : BaseT\r\n    asBaseT = record { f = f }\r\n\r\ndata Bar : Set where\r\n  o : Bar\r\n\r\ndata Baz {{_ : BaseT}} : Bar → Set where\r\n  t1 : Baz o\r\n  t2 : Baz o → Baz o\r\n  t3 : Baz o → Baz o → Baz o\r\n  t4 : Baz o → Baz o → Baz o → Baz o\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/224017158","html_url":"https://github.com/agda/agda/issues/1998#issuecomment-224017158","issue_url":"https://api.github.com/repos/agda/agda/issues/1998","id":224017158,"user":{"login":"mietek","id":166207,"avatar_url":"https://avatars.githubusercontent.com/u/166207?v=3","gravatar_id":"","url":"https://api.github.com/users/mietek","html_url":"https://github.com/mietek","followers_url":"https://api.github.com/users/mietek/followers","following_url":"https://api.github.com/users/mietek/following{/other_user}","gists_url":"https://api.github.com/users/mietek/gists{/gist_id}","starred_url":"https://api.github.com/users/mietek/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mietek/subscriptions","organizations_url":"https://api.github.com/users/mietek/orgs","repos_url":"https://api.github.com/users/mietek/repos","events_url":"https://api.github.com/users/mietek/events{/privacy}","received_events_url":"https://api.github.com/users/mietek/received_events","type":"User","site_admin":false},"created_at":"2016-06-06T16:48:13Z","updated_at":"2016-06-06T16:48:13Z","body":"This may be related to https://github.com/agda/agda/issues/1952."}}
{"actor":{"display_login":"mietek"}}