{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/407","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/407/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/407/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/407/events","html_url":"https://github.com/FStarLang/FStar/issues/407","id":109420158,"number":407,"title":"Unexpected name clashes when using .fsi file.","user":{"login":"fmrl","id":630620,"avatar_url":"https://avatars.githubusercontent.com/u/630620?v=3","gravatar_id":"","url":"https://api.github.com/users/fmrl","html_url":"https://github.com/fmrl","followers_url":"https://api.github.com/users/fmrl/followers","following_url":"https://api.github.com/users/fmrl/following{/other_user}","gists_url":"https://api.github.com/users/fmrl/gists{/gist_id}","starred_url":"https://api.github.com/users/fmrl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fmrl/subscriptions","organizations_url":"https://api.github.com/users/fmrl/orgs","repos_url":"https://api.github.com/users/fmrl/repos","events_url":"https://api.github.com/users/fmrl/events{/privacy}","received_events_url":"https://api.github.com/users/fmrl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-10-02T02:35:42Z","updated_at":"2015-10-02T09:24:00Z","closed_at":null,"body":"Given a file named `ex1.fsi`:\r\n```\r\n(*--build-config\r\n--*)\r\n\r\nmodule Example1\r\n\r\n   // this example fails to verify if the type is defined here.\r\n   type YY 'aa = 'aa -> Tot 'aa\r\n```\r\n\r\nAnd the following file named `ex1.fst`:\r\n```\r\n(*--build-config\r\n   other-files:ex1.fsi\r\n--*)\r\n\r\nmodule Example1\r\n\r\n   // this example verifies if the type is defined here.\r\n   //type YY 'aa = 'aa -> Tot 'aa\r\n\r\n   type ZZ 'aa =\r\n      | MkZZ: yy:YY 'aa -> ZZ 'aa\r\n```\r\n\r\nI get the following error message:\r\n```\r\n<input>(11,17-11,19): Identifier not found: [YY] (Possible clash with related name at ex1.fsi(4,15-6,31))\r\n```\r\n\r\nIs this a mistake on my part or a bug in F*?\r\n\r\nThanks in advance.\r\n~mlr"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/144971844","html_url":"https://github.com/FStarLang/FStar/issues/407#issuecomment-144971844","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/407","id":144971844,"user":{"login":"markulf","id":9845640,"avatar_url":"https://avatars.githubusercontent.com/u/9845640?v=3","gravatar_id":"","url":"https://api.github.com/users/markulf","html_url":"https://github.com/markulf","followers_url":"https://api.github.com/users/markulf/followers","following_url":"https://api.github.com/users/markulf/following{/other_user}","gists_url":"https://api.github.com/users/markulf/gists{/gist_id}","starred_url":"https://api.github.com/users/markulf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/markulf/subscriptions","organizations_url":"https://api.github.com/users/markulf/orgs","repos_url":"https://api.github.com/users/markulf/repos","events_url":"https://api.github.com/users/markulf/events{/privacy}","received_events_url":"https://api.github.com/users/markulf/received_events","type":"User","site_admin":false},"created_at":"2015-10-02T09:24:00Z","updated_at":"2015-10-02T09:24:00Z","body":"The error message is confusing in this case. `(Possible clash with related name at ex1.fsi(4,15-6))` isn't really a clash, its more a hint that this is what should be implemented.\r\n\r\nI guess this is tough usability engineering, as one error messages may have to fit multiple situations depending on the context."}}