{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1916","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/1916/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1916/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1916/events","html_url":"https://github.com/agda/agda/issues/1916","id":143334903,"number":1916,"title":"Lack of documentation of breaking change","user":{"login":"nad","id":293222,"avatar_url":"https://avatars.githubusercontent.com/u/293222?v=3","gravatar_id":"","url":"https://api.github.com/users/nad","html_url":"https://github.com/nad","followers_url":"https://api.github.com/users/nad/followers","following_url":"https://api.github.com/users/nad/following{/other_user}","gists_url":"https://api.github.com/users/nad/gists{/gist_id}","starred_url":"https://api.github.com/users/nad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nad/subscriptions","organizations_url":"https://api.github.com/users/nad/orgs","repos_url":"https://api.github.com/users/nad/repos","events_url":"https://api.github.com/users/nad/events{/privacy}","received_events_url":"https://api.github.com/users/nad/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/documentation","name":"documentation","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/instance","name":"instance","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/priority-high","name":"priority-high","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/regression","name":"regression","color":"e11d21"}],"state":"open","locked":false,"assignee":null,"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/2","html_url":"https://github.com/agda/agda/milestones/2.5.1","labels_url":"https://api.github.com/repos/agda/agda/milestones/2/labels","id":1247354,"number":2,"title":"2.5.1","description":"","creator":{"login":"asr","id":635804,"avatar_url":"https://avatars.githubusercontent.com/u/635804?v=3","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":11,"closed_issues":163,"state":"open","created_at":"2015-08-09T23:15:42Z","updated_at":"2016-03-24T19:13:36Z","due_on":null,"closed_at":null},"comments":1,"created_at":"2016-03-24T19:13:36Z","updated_at":"2016-03-24T19:27:55Z","closed_at":null,"body":"Consider the following code, which is accepted by Agda 2.4.2.5:\r\n```\r\npostulate\r\n  A B : Set\r\n  a   : A\r\n\r\nrecord R (X Y : Set) : Set where\r\n  field\r\n    r : X → Y\r\n\r\nopen R ⦃ ... ⦄\r\n\r\ninstance\r\n  postulate\r\n    aa : R A A\r\n    bb : R B B\r\n\r\nx : A\r\nx = r (r a)\r\n```\r\nThe current development version of Agda rejects this code, because instance resolution gives too many candidates:\r\n```\r\nResolve instance argument _r_8 : R _X_6 A.\r\n  Candidates:\r\n    [ bb : R B B\r\n    , aa : R A A ]\r\nResolve instance argument _r_11 : R A _X_6.\r\n  Candidates:\r\n    [ bb : R B B\r\n    , aa : R A A ]\r\n```\r\n\r\nI find it annoying that `bb` can be a candidate, because the types don't match. I guess this is related to the following comment due to @guillaumebrunerie (c84e4a3a2d861db7260e0fb05dc7c18d3cbd36b0) that I found in `Agda.TypeChecking.InstanceArguments`:\r\n> If one of the arguments of the typeclass is a meta which is not rigidly constrained, then don’t do anything because it may loop.\r\n\r\nI'm not sure if Agda's rejection of the code above is appropriate, but this breaking change should at least be documented (and perhaps also explained) in the manual and in the changelog."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/200983433","html_url":"https://github.com/agda/agda/issues/1916#issuecomment-200983433","issue_url":"https://api.github.com/repos/agda/agda/issues/1916","id":200983433,"user":{"login":"nad","id":293222,"avatar_url":"https://avatars.githubusercontent.com/u/293222?v=3","gravatar_id":"","url":"https://api.github.com/users/nad","html_url":"https://github.com/nad","followers_url":"https://api.github.com/users/nad/followers","following_url":"https://api.github.com/users/nad/following{/other_user}","gists_url":"https://api.github.com/users/nad/gists{/gist_id}","starred_url":"https://api.github.com/users/nad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nad/subscriptions","organizations_url":"https://api.github.com/users/nad/orgs","repos_url":"https://api.github.com/users/nad/repos","events_url":"https://api.github.com/users/nad/events{/privacy}","received_events_url":"https://api.github.com/users/nad/received_events","type":"User","site_admin":false},"created_at":"2016-03-24T19:27:55Z","updated_at":"2016-03-24T19:27:55Z","body":"> The current development version of Agda rejects this code, because instance resolution gives too many candidates:\r\n\r\nIn fact, if `bb` is removed, then Agda still refuses to attempt to use `aa`:\r\n```\r\nResolve instance argument _r_7 : R _X_5 A.\r\n  Candidates:\r\n    [ aa : R A A ]\r\nResolve instance argument _r_10 : R A _X_5.\r\n  Candidates:\r\n    [ aa : R A A ]\r\n```\r\n\r\nThe documentation states, incorrectly, that \"If there is a single solution we use it to solve the goal\"."}}