{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1624","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1624/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1624/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1624/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/1624","id":45579983,"number":1624,"title":"error in record's generated getter/setter using type-class constraint","user":{"login":"zraffer","id":8678430,"avatar_url":"https://avatars.githubusercontent.com/u/8678430?v=3","gravatar_id":"","url":"https://api.github.com/users/zraffer","html_url":"https://github.com/zraffer","followers_url":"https://api.github.com/users/zraffer/followers","following_url":"https://api.github.com/users/zraffer/following{/other_user}","gists_url":"https://api.github.com/users/zraffer/gists{/gist_id}","starred_url":"https://api.github.com/users/zraffer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zraffer/subscriptions","organizations_url":"https://api.github.com/users/zraffer/orgs","repos_url":"https://api.github.com/users/zraffer/repos","events_url":"https://api.github.com/users/zraffer/events{/privacy}","received_events_url":"https://api.github.com/users/zraffer/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2014-10-12T13:38:49Z","updated_at":"2015-05-17T21:56:06Z","closed_at":"2015-05-17T21:56:06Z","body":"The following code emits a type error when I declare `MySum` as a record. If I change it to `data` the code will be compilable. Checked with 0.9.14.3 from Hackage and 0.9.14.2-git:bc8fa59 from git master.\r\n\r\n```Idris\r\nclass Dependent (base: Type) where\r\n  fiber : base -> Type\r\n\r\nrecord MyRec : Type where\r\n  MkRec : \r\n    (recBase: Type) ->\r\n    (recFiber: Dependent recBase) ->\r\n    MyRec\r\n\r\nrecord MySum : MyRec -> Type where\r\n  MkSum : \r\n    (Dependent base) =>\r\n    (sumBase: base) ->\r\n    (sumFiber: fiber sumBase) ->\r\n    MySum (MkRec base %instance) \r\n```\r\n\r\nThe error message is:\r\n\r\n```\r\n(val):0:0:When elaborating type of Main.MySum.constrarg:\r\nWhen elaborating argument recBase to Main.MkRec:\r\n        Can't unify\r\n                MySum (MkRec implicit_base constrarg) -> Type\r\n        with\r\n                Type\r\n        \r\n        Specifically:\r\n                Can't unify\r\n                        MySum (MkRec implicit_base constrarg) -> Type\r\n                with\r\n                        Type\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/102863337","html_url":"https://github.com/idris-lang/Idris-dev/issues/1624#issuecomment-102863337","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1624","id":102863337,"user":{"login":"david-christiansen","id":115330,"avatar_url":"https://avatars.githubusercontent.com/u/115330?v=3","gravatar_id":"","url":"https://api.github.com/users/david-christiansen","html_url":"https://github.com/david-christiansen","followers_url":"https://api.github.com/users/david-christiansen/followers","following_url":"https://api.github.com/users/david-christiansen/following{/other_user}","gists_url":"https://api.github.com/users/david-christiansen/gists{/gist_id}","starred_url":"https://api.github.com/users/david-christiansen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/david-christiansen/subscriptions","organizations_url":"https://api.github.com/users/david-christiansen/orgs","repos_url":"https://api.github.com/users/david-christiansen/repos","events_url":"https://api.github.com/users/david-christiansen/events{/privacy}","received_events_url":"https://api.github.com/users/david-christiansen/received_events","type":"User","site_admin":false},"created_at":"2015-05-17T21:56:06Z","updated_at":"2015-05-17T21:56:06Z","body":"Corresponding code in the new record syntax works:\r\n```\r\n\r\nclass Dependent (base: Type) where\r\n  fiber : base -> Type\r\n\r\nrecord MyRec where\r\n  constructor MkRec\r\n  recBase: Type\r\n  recFiber: Dependent recBase\r\n\r\n\r\nrecord MySum (r : MyRec) where\r\n  constructor MkSum\r\n  dict : Dependent (recBase r)\r\n  sumBase: recBase r\r\n  sumFiber: fiber @{dict} sumBase\r\n\r\n```"}}