{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/434","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/434/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/434/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/434/events","html_url":"https://github.com/FStarLang/FStar/issues/434","id":116186076,"number":434,"title":"Revising the semantics of assumed type constants","user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars.githubusercontent.com/u/6163359?v=3","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-11-10T19:41:06Z","updated_at":"2015-11-10T20:37:50Z","closed_at":null,"body":"Currently, if you write \r\n\r\n```\r\ntype t\r\n```\r\n i.e., a type without a definition, F* treats this as a **new** type constant, distinct from all other constants. \r\n\r\nThis has led to some confusion in many developments, where the intended usage was just to assume some type variable. The confusion has been bad enough that some developments inadvertently end up proving false. \r\n\r\nTo make this behavior less surprising, we should:\r\n\r\n1. Forbid the constructor above. \r\n\r\n2. If you want a new type constant without any constructors (occasionally we do, e.g., in Prims, where we introduce new primitive types), then you must write\r\n\r\n```\r\nnew type t\r\n```\r\n\r\n3. If you want to assume a type variable, then you must write\r\n\r\n```\r\nassume type t\r\n```\r\n\r\nAll of this applies equally to types that have parameters.\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/155558695","html_url":"https://github.com/FStarLang/FStar/issues/434#issuecomment-155558695","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/434","id":155558695,"user":{"login":"catalin-hritcu","id":5850655,"avatar_url":"https://avatars.githubusercontent.com/u/5850655?v=3","gravatar_id":"","url":"https://api.github.com/users/catalin-hritcu","html_url":"https://github.com/catalin-hritcu","followers_url":"https://api.github.com/users/catalin-hritcu/followers","following_url":"https://api.github.com/users/catalin-hritcu/following{/other_user}","gists_url":"https://api.github.com/users/catalin-hritcu/gists{/gist_id}","starred_url":"https://api.github.com/users/catalin-hritcu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/catalin-hritcu/subscriptions","organizations_url":"https://api.github.com/users/catalin-hritcu/orgs","repos_url":"https://api.github.com/users/catalin-hritcu/repos","events_url":"https://api.github.com/users/catalin-hritcu/events{/privacy}","received_events_url":"https://api.github.com/users/catalin-hritcu/received_events","type":"User","site_admin":false},"created_at":"2015-11-10T20:37:50Z","updated_at":"2015-11-10T20:37:50Z","body":"How about calling it \"fresh\" instead of \"new\"?\n"}}