{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2585","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2585/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2585/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2585/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2585","id":105087677,"number":2585,"title":"Idris is confused by implicit arguments that aren't named in the type signature.","user":{"login":"enolan","id":61517,"avatar_url":"https://avatars.githubusercontent.com/u/61517?v=3","gravatar_id":"","url":"https://api.github.com/users/enolan","html_url":"https://github.com/enolan","followers_url":"https://api.github.com/users/enolan/followers","following_url":"https://api.github.com/users/enolan/following{/other_user}","gists_url":"https://api.github.com/users/enolan/gists{/gist_id}","starred_url":"https://api.github.com/users/enolan/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/enolan/subscriptions","organizations_url":"https://api.github.com/users/enolan/orgs","repos_url":"https://api.github.com/users/enolan/repos","events_url":"https://api.github.com/users/enolan/events{/privacy}","received_events_url":"https://api.github.com/users/enolan/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/Expected%20behaviour","name":"Expected behaviour","color":"009800"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-09-06T11:19:51Z","updated_at":"2015-09-06T11:40:31Z","closed_at":null,"body":"```\r\ntakeEmptyIsEmpty : take n [] = []\r\ntakeEmptyIsEmpty {n =  Z   } = Refl\r\ntakeEmptyIsEmpty {n = (S k)} = Refl\r\n```\r\n\r\nIf you ask Idris what the type is, including implicit arguments:\r\n```\r\n*newbug> :set showimplicits \r\n*newbug> :t takeEmptyIsEmpty \r\nMain.takeEmptyIsEmpty : {a : Type} -> {n : Prelude.Nat.Nat} ->\r\n                        (=) {A = Prelude.List.List a}\r\n                            {B = Prelude.List.List a}\r\n                            (Prelude.List.take {a = a}\r\n                                               n\r\n                                               (Prelude.List.Nil {elem = a}))\r\n                            (Prelude.List.Nil {elem = a})\r\n```\r\n\r\nAnd yet:\r\n```\r\n*newbug> :t takeEmptyIsEmpty {a = Nat}\r\n(input):1:21:a is not an implicit argument of Main.takeEmptyIsEmpty\r\n```\r\nIt tells you a is not an implicit argument right after telling you it is and it has type Type. IIUC, a is generated because Nil, take and (=) all have implicit arguments specifying the type in question and it need to be propagated."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/138074578","html_url":"https://github.com/idris-lang/Idris-dev/issues/2585#issuecomment-138074578","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2585","id":138074578,"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":"2015-09-06T11:40:31Z","updated_at":"2015-09-06T11:40:31Z","body":"I think this is reasonable behaviour. Idris will only let you refer to implicit things which you have named explcitly in the type, so if you want to refer to 'a', you have to name it. Otherwise Idris will invent an internal name - there could be lots of such things which need to be propagated so inventing a name is tricky and inventing a user accessible name is likely to be fragile.\r\n\r\nSo then, the problem is in the display. Perhaps 'showimplicits' could be more clear about which names are internally generated and therefore inaccessible."}}