{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4438","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4438/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4438/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4438/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/4438","id":321999984,"number":4438,"title":"Question: Type checker bug?","user":{"login":"SamuraiJack","id":72431,"avatar_url":"https://avatars3.githubusercontent.com/u/72431?v=4","gravatar_id":"","url":"https://api.github.com/users/SamuraiJack","html_url":"https://github.com/SamuraiJack","followers_url":"https://api.github.com/users/SamuraiJack/followers","following_url":"https://api.github.com/users/SamuraiJack/following{/other_user}","gists_url":"https://api.github.com/users/SamuraiJack/gists{/gist_id}","starred_url":"https://api.github.com/users/SamuraiJack/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SamuraiJack/subscriptions","organizations_url":"https://api.github.com/users/SamuraiJack/orgs","repos_url":"https://api.github.com/users/SamuraiJack/repos","events_url":"https://api.github.com/users/SamuraiJack/events{/privacy}","received_events_url":"https://api.github.com/users/SamuraiJack/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2018-05-10T16:42:52Z","updated_at":"2018-05-28T12:37:42Z","closed_at":null,"author_association":"NONE","body":"The definition of \"my\" in this gits does not type check: https://gist.github.com/SamuraiJack/f42dd2204fe87054b831cabee810b3c3 because of the Functor constraint on `f`. When removing the constraint all typechecks.\r\n\r\nIs this a bug, or I am missing some theory?"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/392516109","html_url":"https://github.com/idris-lang/Idris-dev/issues/4438#issuecomment-392516109","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4438","id":392516109,"user":{"login":"howtonotwin","id":15616055,"avatar_url":"https://avatars1.githubusercontent.com/u/15616055?v=4","gravatar_id":"","url":"https://api.github.com/users/howtonotwin","html_url":"https://github.com/howtonotwin","followers_url":"https://api.github.com/users/howtonotwin/followers","following_url":"https://api.github.com/users/howtonotwin/following{/other_user}","gists_url":"https://api.github.com/users/howtonotwin/gists{/gist_id}","starred_url":"https://api.github.com/users/howtonotwin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/howtonotwin/subscriptions","organizations_url":"https://api.github.com/users/howtonotwin/orgs","repos_url":"https://api.github.com/users/howtonotwin/repos","events_url":"https://api.github.com/users/howtonotwin/events{/privacy}","received_events_url":"https://api.github.com/users/howtonotwin/received_events","type":"User","site_admin":false},"created_at":"2018-05-28T12:37:42Z","updated_at":"2018-05-28T12:37:42Z","author_association":"NONE","body":"Well, yes, that typechecks fine. In `zz`, you have an unbound implicit parameter `f0 : Type -> Type`, an instance `Functor f0`, an explicit argument `f : Type -> Type`, which doesn't have a `Functor` instance, and `z : Nat`. The declaration typechecks perfectly fine and in the same way for both `Algebra` and `some` (and good thing, or else there must be dark magicks at work). But the type declarations are still wrong, and it's just coincidence that the actual definition doesn't trigger the error itself.\r\n\r\nThe *usage* of `Algebra` or `some` triggers the error. *Not* their *definition*. That's my point: maybe we should emit a warning when we see type declarations that look like this, because they are probably wrong."}}
{"actor":{"display_login":"howtonotwin"}}