{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2962","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2962/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2962/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2962/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2962","id":132629289,"number":2962,"title":"Coverage of interface implementation is not checked for totality","user":{"login":"colin-adams","id":123895,"avatar_url":"https://avatars.githubusercontent.com/u/123895?v=3","gravatar_id":"","url":"https://api.github.com/users/colin-adams","html_url":"https://github.com/colin-adams","followers_url":"https://api.github.com/users/colin-adams/followers","following_url":"https://api.github.com/users/colin-adams/following{/other_user}","gists_url":"https://api.github.com/users/colin-adams/gists{/gist_id}","starred_url":"https://api.github.com/users/colin-adams/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/colin-adams/subscriptions","organizations_url":"https://api.github.com/users/colin-adams/orgs","repos_url":"https://api.github.com/users/colin-adams/repos","events_url":"https://api.github.com/users/colin-adams/events{/privacy}","received_events_url":"https://api.github.com/users/colin-adams/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-02-10T07:50:11Z","updated_at":"2016-02-14T12:34:32Z","closed_at":null,"body":"E.g.:\r\n\r\nmodule Test_show\r\n\r\n%default total\r\n\r\ndata Te = C1 | C2 | C3\r\n\r\nShow Te where\r\n  show C1 = \"C1\"\r\n  \r\n\r\nThis checks (Idris 0.10) without complaining, both in Emacs and with:\r\n\r\nidris --check test_show.idr\r\n"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/183882153","html_url":"https://github.com/idris-lang/Idris-dev/issues/2962#issuecomment-183882153","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2962","id":183882153,"user":{"login":"edwinb","id":255926,"avatar_url":"https://avatars.githubusercontent.com/u/255926?v=3","gravatar_id":"","url":"https://api.github.com/users/edwinb","html_url":"https://github.com/edwinb","followers_url":"https://api.github.com/users/edwinb/followers","following_url":"https://api.github.com/users/edwinb/following{/other_user}","gists_url":"https://api.github.com/users/edwinb/gists{/gist_id}","starred_url":"https://api.github.com/users/edwinb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/edwinb/subscriptions","organizations_url":"https://api.github.com/users/edwinb/orgs","repos_url":"https://api.github.com/users/edwinb/repos","events_url":"https://api.github.com/users/edwinb/events{/privacy}","received_events_url":"https://api.github.com/users/edwinb/received_events","type":"User","site_admin":false},"created_at":"2016-02-14T12:34:32Z","updated_at":"2016-02-14T12:34:32Z","body":"It turns out this is getting checked but not reported - everything gets checked for totality whether you have the 'total' default or not, but this isn't being reported because 'show' in the prelude is explicitly marked as okay to be 'partial'. This explains why you don't see a similar problem for Eq.\r\n\r\nYour '%default total' should override this for your instance, but doesn't. \r\n\r\nI have a fix for this, but I want to make it a slightly better fix before I push it..."}}