{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3683","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3683/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3683/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3683/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3683","id":213089559,"number":3683,"title":"Interface parameter with implicits in type","user":{"login":"erisco","id":963181,"avatar_url":"https://avatars2.githubusercontent.com/u/963181?v=3","gravatar_id":"","url":"https://api.github.com/users/erisco","html_url":"https://github.com/erisco","followers_url":"https://api.github.com/users/erisco/followers","following_url":"https://api.github.com/users/erisco/following{/other_user}","gists_url":"https://api.github.com/users/erisco/gists{/gist_id}","starred_url":"https://api.github.com/users/erisco/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/erisco/subscriptions","organizations_url":"https://api.github.com/users/erisco/orgs","repos_url":"https://api.github.com/users/erisco/repos","events_url":"https://api.github.com/users/erisco/events{/privacy}","received_events_url":"https://api.github.com/users/erisco/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2017-03-09T16:23:48Z","updated_at":"2017-03-10T07:20:18Z","closed_at":null,"body":"Test case:\r\n```\r\n    interface X (r : {a:Type} -> a -> Type) where\r\n```\r\n\r\nOutput:\r\n```\r\ntest.idr:1:11:When checking type of constructor of Main.X:\r\nWhen checking argument r to Main.X:\r\n        Type mismatch between\r\n                a -> Type (Type of r)\r\n        and\r\n                a1 -> Type (Expected type)\r\n\r\n        Specifically:\r\n                Type mismatch between\r\n                        v0 -> Type\r\n                and\r\n                        Type\r\n```\r\n\r\nIdris version 0.99.\r\n\r\nI do not know if this is a missing feature, bug, or purposefully does not work. If this did work I could abbreviate more code, as implicits do."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/285596615","html_url":"https://github.com/idris-lang/Idris-dev/issues/3683#issuecomment-285596615","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3683","id":285596615,"user":{"login":"erisco","id":963181,"avatar_url":"https://avatars2.githubusercontent.com/u/963181?v=3","gravatar_id":"","url":"https://api.github.com/users/erisco","html_url":"https://github.com/erisco","followers_url":"https://api.github.com/users/erisco/followers","following_url":"https://api.github.com/users/erisco/following{/other_user}","gists_url":"https://api.github.com/users/erisco/gists{/gist_id}","starred_url":"https://api.github.com/users/erisco/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/erisco/subscriptions","organizations_url":"https://api.github.com/users/erisco/orgs","repos_url":"https://api.github.com/users/erisco/repos","events_url":"https://api.github.com/users/erisco/events{/privacy}","received_events_url":"https://api.github.com/users/erisco/received_events","type":"User","site_admin":false},"created_at":"2017-03-10T07:20:18Z","updated_at":"2017-03-10T07:20:18Z","body":"@ahmadsalim as in `interface X (r : (a:Type) -> a -> Type) where`? Yes, that works. The issue is that Idris will not infer `a` for me and this causes unwanted verbosity."}}
{"actor":{"display_login":"erisco"}}