{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2349","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2349/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2349/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2349/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2349","id":84960484,"number":2349,"title":"Associated types resolution in instance definition","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},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-06-04T07:28:20Z","updated_at":"2016-05-01T09:24:40Z","closed_at":null,"body":"Now that we've decided we should support associated types, I think the following should work:\r\n\r\n    class ListLike a where\r\n        Elem : Type\r\n        fromList : List Elem -> a\r\n  \r\n    data Silly = None | Cons Int Silly\r\n  \r\n    instance ListLike Silly where\r\n          Elem = Int\r\n          fromList [] = None\r\n          fromList (x :: xs) = Cons x (fromList xs)\r\n\r\nBut, alas, I get an error:\r\n\r\n        Type mismatch between\r\n                List Main.Silly instance of Main.ListLike, method Elem (Type of xs)\r\n        and\r\n                List Elem (Expected type)\r\n        \r\n        Specifically:\r\n                Type mismatch between\r\n                        Int\r\n                and\r\n                        Elem\r\n\r\nI suspect this is a type class resolution problem in the body of the instance - it can be worked around by defining a helper function of type `List Int -> Silly`."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/216030401","html_url":"https://github.com/idris-lang/Idris-dev/issues/2349#issuecomment-216030401","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2349","id":216030401,"user":{"login":"ahmadsalim","id":1647846,"avatar_url":"https://avatars.githubusercontent.com/u/1647846?v=3","gravatar_id":"","url":"https://api.github.com/users/ahmadsalim","html_url":"https://github.com/ahmadsalim","followers_url":"https://api.github.com/users/ahmadsalim/followers","following_url":"https://api.github.com/users/ahmadsalim/following{/other_user}","gists_url":"https://api.github.com/users/ahmadsalim/gists{/gist_id}","starred_url":"https://api.github.com/users/ahmadsalim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ahmadsalim/subscriptions","organizations_url":"https://api.github.com/users/ahmadsalim/orgs","repos_url":"https://api.github.com/users/ahmadsalim/repos","events_url":"https://api.github.com/users/ahmadsalim/events{/privacy}","received_events_url":"https://api.github.com/users/ahmadsalim/received_events","type":"User","site_admin":false},"created_at":"2016-05-01T09:24:40Z","updated_at":"2016-05-01T09:24:40Z","body":"I think this would be really nice if we got it working."}}