{"action":"closed","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2058","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2058/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2058/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2058/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2058","id":64031052,"number":2058,"title":"Namespaces leaking instance declarations: expected behaviour ?","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":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-03-24T15:48:29Z","updated_at":"2015-03-30T16:39:58Z","closed_at":"2015-03-30T16:39:58Z","body":"Namespaces are closed for variable declarations and\r\n````\r\n> namespace lala\r\n>   foo : Nat\r\n> namespace lula\r\n>   foo : Nat\r\n```\r\ntype checks fine. However, instance declarations seem to leak through namespaces and\r\n````\r\n> class Preorder t where\r\n>   total PO : t -> t -> Type \r\n>   total reflexive : (x : t) -> PO x x   \r\n>   total transitive : (x : t) -> (y : t) -> (z : t) -> PO x y -> PO y z -> PO x z\r\n\r\n> namespace lala\r\n>   instance Preorder t1 => Preorder (t1, t2) where\r\n>     PO x y = PO (fst x) (fst y)\r\n>     reflexive x = reflexive (fst x)\r\n>     transitive x y z xy yz = transitive (fst x) (fst y) (fst z) xy yz\r\n\r\n> namespace lula\r\n>   instance Preorder t2 => Preorder (t1, t2) where\r\n>     PO x y = PO (snd x) (snd y)\r\n>     reflexive x = reflexive (snd x)\r\n>     transitive x y z xy yz = transitive (snd x) (snd y) (snd z) xy yz\r\n```\r\ndoes not type check: \r\n````\r\n- + Errors (1)\r\n `-- namespace1.lidr line 13 col 11:\r\n     Overlapping instance: Preorder (t1, t2) already defined\r\n```\r\nIs this the expected behavior ? Thanks, Nicola\r\n"}}