{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4386","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4386/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4386/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4386/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/4386","id":306303509,"number":4386,"title":"Incorrect type mismatch when using type synonym","user":{"login":"JadenGeller","id":4544152,"avatar_url":"https://avatars0.githubusercontent.com/u/4544152?v=4","gravatar_id":"","url":"https://api.github.com/users/JadenGeller","html_url":"https://github.com/JadenGeller","followers_url":"https://api.github.com/users/JadenGeller/followers","following_url":"https://api.github.com/users/JadenGeller/following{/other_user}","gists_url":"https://api.github.com/users/JadenGeller/gists{/gist_id}","starred_url":"https://api.github.com/users/JadenGeller/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JadenGeller/subscriptions","organizations_url":"https://api.github.com/users/JadenGeller/orgs","repos_url":"https://api.github.com/users/JadenGeller/repos","events_url":"https://api.github.com/users/JadenGeller/events{/privacy}","received_events_url":"https://api.github.com/users/JadenGeller/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-03-19T00:56:08Z","updated_at":"2018-03-20T18:14:34Z","closed_at":null,"author_association":"NONE","body":"# Steps to Reproduce\r\nTypecheck the following snippet:\r\n```idris\r\ndata Tree : (Type -> Type) -> Type -> Type where\r\n    Leaf : Tree f a\r\n    Branch : (f a) -> a -> (f a) -> Tree f a\r\n    \r\nTreeList : Type -> Type\r\nTreeList = Tree TreeList\r\n\r\nquicktree : Ord a => List a -> TreeList a\r\nquicktree [] = Leaf\r\nquicktree (x :: xs) = let (ls, rs) = partition (< x) xs\r\n                      in Branch (quicktree ls) x (quicktree rs)\r\n```\r\n# Expected Behavior\r\nTypechecks without error.\r\n\r\n# Observed Behavior\r\n```\r\nWhen checking right hand side of quicktree with expected type\r\n        TreeList a\r\n\r\nType mismatch between\r\n        Tree f a1 (Type of Leaf)\r\nand\r\n        TreeList a (Expected type)\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/374702745","html_url":"https://github.com/idris-lang/Idris-dev/issues/4386#issuecomment-374702745","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/4386","id":374702745,"user":{"login":"joom","id":1611120,"avatar_url":"https://avatars2.githubusercontent.com/u/1611120?v=4","gravatar_id":"","url":"https://api.github.com/users/joom","html_url":"https://github.com/joom","followers_url":"https://api.github.com/users/joom/followers","following_url":"https://api.github.com/users/joom/following{/other_user}","gists_url":"https://api.github.com/users/joom/gists{/gist_id}","starred_url":"https://api.github.com/users/joom/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/joom/subscriptions","organizations_url":"https://api.github.com/users/joom/orgs","repos_url":"https://api.github.com/users/joom/repos","events_url":"https://api.github.com/users/joom/events{/privacy}","received_events_url":"https://api.github.com/users/joom/received_events","type":"User","site_admin":false},"created_at":"2018-03-20T18:14:34Z","updated_at":"2018-03-20T18:14:34Z","author_association":"CONTRIBUTOR","body":"I feel like an example that doesn't involve an infinite loop would make things clearer. If you didn't get that type error, would type checking terminate for this program? When Idris tries to normalize `TreeList a` during type checking, it would get an infinite loop, I think. Can someone confirm that?"}}
{"actor":{"display_login":"joom"}}