{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3234","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3234/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3234/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3234/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3234","id":161180039,"number":3234,"title":"What am I doing wrong? Are interfaces broken? Is this a regression?","user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/F-Question","name":"F-Question","color":"bebe00"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/I-Expected%20Behaviour","name":"I-Expected Behaviour","color":"AAAAAA"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/U-Language%20Design","name":"U-Language Design","color":"d4c5f9"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":10,"created_at":"2016-06-20T12:06:14Z","updated_at":"2016-07-06T20:46:50Z","closed_at":null,"body":"The program\r\n```\r\n> import Syntax.PreorderReasoning\r\n\r\n> %default total\r\n> %access public export\r\n> %auto_implicits on\r\n\r\n> interface (Num t) => NumMultZeroOne t where\r\n>   multZeroRightZero   : (x : t) -> x * 0 = 0\r\n>   multZeroLeftZero    : (x : t) -> 0 * x = 0\r\n>   multOneRightNeutral : (x : t) -> x * 1 = x\r\n>   multOneLeftNeutral  : (x : t) -> 1 * x = x\r\n\r\n> cross : (a -> c) -> (b -> d) -> (a, b) -> (c, d)\r\n> cross f g (x, y) = (f x, g y)\r\n\r\n> sumMapSnd : {A, B : Type} -> (Num B) => List (A, B) -> B\r\n> sumMapSnd abs = sum (map snd abs) \r\n\r\n> mapIdRightMult : {A, B : Type} -> (Num B) => (List (A, B), B) -> List (A, B)\r\n> mapIdRightMult (abs, b) = map (cross id (* b)) abs\r\n\r\n> mapIdRightMultLemma : {A, B : Type} -> (NumMultZeroOne B) => \r\n>                       (absb : (List (A, B), B)) -> \r\n>                       sumMapSnd (mapIdRightMult absb)\r\n>                       =\r\n>                       (sumMapSnd (fst absb)) * (snd absb)\r\n> mapIdRightMultLemma (Nil, b) = \r\n>     ( sumMapSnd (mapIdRightMult (Nil, b)) )\r\n>   ={ Refl }=\r\n>     ( sumMapSnd (map (cross id (* b)) Nil) )\r\n>   ={ Refl }=\r\n>     ( sumMapSnd Nil )\r\n>   ={ Refl }=\r\n>     ( 0 )\r\n>   ={ ?kuku }= \r\n>   -- ={ sym (multZeroLeftZero b) }=\r\n>     ( 0 * b )\r\n>   ={ Refl }=     \r\n>     ( (sumMapSnd Nil) * b )\r\n>   ={ Refl }=     \r\n>     ( (sumMapSnd (fst (Nil, b))) * (snd (Nil, b)) )   \r\n>   QED\r\n> mapIdRightMultLemma ((ab :: abs), b) = ?lala\r\n```\r\ntype checks fine. But replacing lines 35-36\r\n```\r\n>   ={ ?kuku }= \r\n>   -- ={ sym (multZeroLeftZero b) }=\r\n```\r\nwith\r\n```\r\n>   -- ={ ?kuku }= \r\n>   ={ sym (multZeroLeftZero b) }=\r\n```\r\nyields\r\n```\r\n- + Errors (1)\r\n `-- 3223_cant_infer.lidr line 27 col 20:\r\n     Can't infer argument A to sumMapSnd, \r\n     Can't infer argument A to mapIdRightMult, \r\n     Can't infer argument A to Pair, \r\n     Can't infer argument A to sumMapSnd, \r\n     Can't infer argument A to Pair, \r\n     Can't infer argument A to cross, \r\n     Can't infer argument A to id, \r\n     Can't infer argument A to sumMapSnd, \r\n     Can't infer argument A to Pair, \r\n     Can't infer argument A to sumMapSnd, \r\n     Can't infer argument A to Pair, \r\n     Can't infer argument A to sumMapSnd, \r\n     Can't infer argument A to Pair, \r\n     Can't infer argument elem to List, \r\n     Can't infer argument elem to []\r\n```\r\nWhat is going on here? Is there something broken with interfaces? Is this a regression? Am I doing something wrong?\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/230901141","html_url":"https://github.com/idris-lang/Idris-dev/issues/3234#issuecomment-230901141","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3234","id":230901141,"user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"created_at":"2016-07-06T20:46:50Z","updated_at":"2016-07-06T20:46:50Z","body":"> It can only be lists of elements of type (A, B) I agree, but Idris doesn't have enough to work that out by unification.\r\n\r\nWas it always like that? I was under the impression that the type of the arguments of a function is determined by the function's signature. And `(Nil, b)` in\r\n```\r\n>     ( sumMapSnd (mapIdRightMult (Nil, b)) )\r\n```\r\nhas to be the explicit argument of `mapIdRightMultLemma`, I believe."}}
{"actor":{"display_login":"nicolabotta"}}