{"action":"closed","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2890","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2890/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2890/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2890/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2890","id":126231787,"number":2890,"title":"Problem with the \"using\" notation chapter of the tutorial","user":{"login":"luxbock","id":2667851,"avatar_url":"https://avatars.githubusercontent.com/u/2667851?v=3","gravatar_id":"","url":"https://api.github.com/users/luxbock","html_url":"https://github.com/luxbock","followers_url":"https://api.github.com/users/luxbock/followers","following_url":"https://api.github.com/users/luxbock/following{/other_user}","gists_url":"https://api.github.com/users/luxbock/gists{/gist_id}","starred_url":"https://api.github.com/users/luxbock/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/luxbock/subscriptions","organizations_url":"https://api.github.com/users/luxbock/orgs","repos_url":"https://api.github.com/users/luxbock/repos","events_url":"https://api.github.com/users/luxbock/events{/privacy}","received_events_url":"https://api.github.com/users/luxbock/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/Documentation","name":"Documentation","color":"fad8c7"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-01-12T17:37:40Z","updated_at":"2016-03-18T14:41:43Z","closed_at":"2016-03-18T14:41:43Z","body":"Following along the tutorial, with this in my file\r\n\r\n```idris\r\nmodule Main\r\n\r\ndata Vect : Nat -> Type -> Type where\r\n  Nil  : Vect Z a\r\n  (::) : a -> Vect k a -> Vect (S k) a\r\n\r\nusing (x:a, y:a, xs:Vect n a)\r\n  data Elem : a -> Vect n a -> Type where\r\n    Here  : Elem x (x :: xs)\r\n    There : Elem x xs -> Elem x (y :: xs)\r\n\r\ntestVec : Vect 4 Integer\r\ntestVec = 3 :: 4 :: 5 :: 6 :: Nil\r\n\r\ninVect : Elem 5 testVec\r\ninVect = There (There Here)\r\n```\r\n\r\nI get the following error:\r\n\r\n```\r\n `-- hello.idr line 16 col 7:\r\n     When checking right hand side of inVect with expected type\r\n             Elem 5 testVec\r\n     \r\n     Type mismatch between\r\n             Elem 5 (y2 :: y :: 5 :: xs) (Type of There (There Here))\r\n     and\r\n             Elem 5 testVec (Expected type)\r\n     \r\n     Specifically:\r\n             Type mismatch between\r\n                     y1 :: y :: 5 :: xs\r\n             and\r\n                     testVec\r\n```\r\n\r\n@david-christiansen said the problem is with a recent changes to name resolution of lowercase identifiers, and changing the last `testVec` to `Main.testVec` indeed works as expected."}}