{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3480","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3480/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3480/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3480/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3480","id":181763906,"number":3480,"title":"+ operator used in type signature not commutative in unification","user":{"login":"owickstrom","id":1464328,"avatar_url":"https://avatars.githubusercontent.com/u/1464328?v=3","gravatar_id":"","url":"https://api.github.com/users/owickstrom","html_url":"https://github.com/owickstrom","followers_url":"https://api.github.com/users/owickstrom/followers","following_url":"https://api.github.com/users/owickstrom/following{/other_user}","gists_url":"https://api.github.com/users/owickstrom/gists{/gist_id}","starred_url":"https://api.github.com/users/owickstrom/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/owickstrom/subscriptions","organizations_url":"https://api.github.com/users/owickstrom/orgs","repos_url":"https://api.github.com/users/owickstrom/repos","events_url":"https://api.github.com/users/owickstrom/events{/privacy}","received_events_url":"https://api.github.com/users/owickstrom/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/I-Expected%20Behaviour","name":"I-Expected Behaviour","color":"AAAAAA"}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2016-10-07T20:45:36Z","updated_at":"2016-10-08T06:09:48Z","closed_at":"2016-10-07T23:55:10Z","body":"So, I've reduced a program based on `Vect` to this example where using `(l + 1)` in the type signature does not unify with the type of the body expression, where I thought it would. It seems the `+` operator on `Nat` is not commutative in unification.\r\n\r\n**A small warning:** I started hacking with Idris just this week. I have tried to find a similar report among the other issues, with no luck, so I'll give this a shot.\r\n\r\nThe program looks like this:\r\n\r\n```\r\nmodule Main\r\n\r\nimport Data.Vect\r\n\r\nprepend : (elem : t) -> Vect l t -> Vect (l + 1) t\r\nprepend x xs = [x] ++ xs\r\n```\r\n\r\nWhen loading this in the REPL, I get:\r\n\r\n```\r\n     When checking right hand side of prepend with expected type\r\n             Vect (l + 1) t\r\n     \r\n     Type mismatch between\r\n             Vect (1 + l) t (Type of [x] ++ xs)\r\n     and\r\n             Vect (plus l 1) t (Expected type)\r\n     \r\n     Specifically:\r\n             Type mismatch between\r\n                     plus 1 l\r\n             and\r\n                     plus l 1\r\n```\r\n\r\nIf I flip `(l + 1)` in the type signature to `(1 + l)` it type checks properly. I expect `plus 1 l` and `plus l 1` to unify as well."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/252405774","html_url":"https://github.com/idris-lang/Idris-dev/issues/3480#issuecomment-252405774","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3480","id":252405774,"user":{"login":"owickstrom","id":1464328,"avatar_url":"https://avatars.githubusercontent.com/u/1464328?v=3","gravatar_id":"","url":"https://api.github.com/users/owickstrom","html_url":"https://github.com/owickstrom","followers_url":"https://api.github.com/users/owickstrom/followers","following_url":"https://api.github.com/users/owickstrom/following{/other_user}","gists_url":"https://api.github.com/users/owickstrom/gists{/gist_id}","starred_url":"https://api.github.com/users/owickstrom/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/owickstrom/subscriptions","organizations_url":"https://api.github.com/users/owickstrom/orgs","repos_url":"https://api.github.com/users/owickstrom/repos","events_url":"https://api.github.com/users/owickstrom/events{/privacy}","received_events_url":"https://api.github.com/users/owickstrom/received_events","type":"User","site_admin":false},"created_at":"2016-10-08T06:09:48Z","updated_at":"2016-10-08T06:09:48Z","body":"I see. Thank you both for explaining it so well, and sorry for posting this as a bug. I should have probably gone through the mailing list or IRC first."}}
{"actor":{"display_login":"owickstrom"}}