{"action":"closed","issue":{"url":"https://api.github.com/repos/agda/agda/issues/3175","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/3175/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/3175/comments","events_url":"https://api.github.com/repos/agda/agda/issues/3175/events","html_url":"https://github.com/agda/agda/issues/3175","id":349485445,"node_id":"MDU6SXNzdWUzNDk0ODU0NDU=","number":3175,"title":"Instance resolution fails with defined method","user":{"login":"andreasabel","id":1155218,"node_id":"MDQ6VXNlcjExNTUyMTg=","avatar_url":"https://avatars3.githubusercontent.com/u/1155218?v=4","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},"labels":[{"id":245649400,"node_id":"MDU6TGFiZWwyNDU2NDk0MDA=","url":"https://api.github.com/repos/agda/agda/labels/instance","name":"instance","color":"ededed","default":false}],"state":"closed","locked":false,"assignee":{"login":"jespercockx","id":2910371,"node_id":"MDQ6VXNlcjI5MTAzNzE=","avatar_url":"https://avatars2.githubusercontent.com/u/2910371?v=4","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false},"assignees":[{"login":"jespercockx","id":2910371,"node_id":"MDQ6VXNlcjI5MTAzNzE=","avatar_url":"https://avatars2.githubusercontent.com/u/2910371?v=4","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/22","html_url":"https://github.com/agda/agda/milestone/22","labels_url":"https://api.github.com/repos/agda/agda/milestones/22/labels","id":2988930,"node_id":"MDk6TWlsZXN0b25lMjk4ODkzMA==","number":22,"title":"2.6.0","description":"","creator":{"login":"asr","id":635804,"node_id":"MDQ6VXNlcjYzNTgwNA==","avatar_url":"https://avatars2.githubusercontent.com/u/635804?v=4","gravatar_id":"","url":"https://api.github.com/users/asr","html_url":"https://github.com/asr","followers_url":"https://api.github.com/users/asr/followers","following_url":"https://api.github.com/users/asr/following{/other_user}","gists_url":"https://api.github.com/users/asr/gists{/gist_id}","starred_url":"https://api.github.com/users/asr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/asr/subscriptions","organizations_url":"https://api.github.com/users/asr/orgs","repos_url":"https://api.github.com/users/asr/repos","events_url":"https://api.github.com/users/asr/events{/privacy}","received_events_url":"https://api.github.com/users/asr/received_events","type":"User","site_admin":false},"open_issues":114,"closed_issues":147,"state":"open","created_at":"2017-12-19T15:00:28Z","updated_at":"2018-12-04T15:38:09Z","due_on":"2018-12-23T08:00:00Z","closed_at":null},"comments":2,"created_at":"2018-08-10T11:47:53Z","updated_at":"2018-12-04T15:38:09Z","closed_at":"2018-12-04T15:38:09Z","author_association":"CONTRIBUTOR","body":"```agda\r\nopen import Data.List using (List; []; _∷_; map; foldr; _++_)\r\n\r\ndata Rose (A : Set) : Set where\r\n  leaf : (a : A) → Rose A\r\n  node : (rs : List (Rose A)) → Rose A\r\n\r\nrecord IsSeq (A S : Set) : Set where\r\n  field\r\n    nil : S\r\n    sg  : (a : A) → S\r\n    _∙_ : (s t : S) → S\r\n\r\n  concat : (ss : List S) → S\r\n  concat = foldr _∙_ nil\r\n\r\nopen IsSeq {{...}}\r\n\r\n{-# TERMINATING #-}\r\nflatten : ∀{A S} {{_ : IsSeq A S}} → Rose A → S\r\nflatten (leaf a) = sg a\r\nflatten (node rs) = concat (map flatten rs)\r\n```\r\n`concat` is yellow.\r\n```\r\nFailed to solve the following constraints:\r\n  Resolve instance argument\r\n    _r_30\r\n      : {A S : Set} ⦃ z : IsSeq A S ⦄ (rs₁ : List (Rose A)) →\r\n        IsSeq (_A_28 (rs = rs₁)) S\r\n  Candidates _ : IsSeq ;A ;S\r\n```"}}
{"actor":{"display_login":"jespercockx"}}