{"action":"opened","issue":{"url":"https://api.github.com/repos/rlepigre/subml/issues/1","repository_url":"https://api.github.com/repos/rlepigre/subml","labels_url":"https://api.github.com/repos/rlepigre/subml/issues/1/labels{/name}","comments_url":"https://api.github.com/repos/rlepigre/subml/issues/1/comments","events_url":"https://api.github.com/repos/rlepigre/subml/issues/1/events","html_url":"https://github.com/rlepigre/subml/issues/1","id":301764607,"number":1,"title":"Parse error may show as a type error...","user":{"login":"rlepigre","id":1555539,"avatar_url":"https://avatars0.githubusercontent.com/u/1555539?v=4","gravatar_id":"","url":"https://api.github.com/users/rlepigre","html_url":"https://github.com/rlepigre","followers_url":"https://api.github.com/users/rlepigre/followers","following_url":"https://api.github.com/users/rlepigre/following{/other_user}","gists_url":"https://api.github.com/users/rlepigre/gists{/gist_id}","starred_url":"https://api.github.com/users/rlepigre/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rlepigre/subscriptions","organizations_url":"https://api.github.com/users/rlepigre/orgs","repos_url":"https://api.github.com/users/rlepigre/repos","events_url":"https://api.github.com/users/rlepigre/events{/privacy}","received_events_url":"https://api.github.com/users/rlepigre/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-03-02T13:23:32Z","updated_at":"2018-03-02T13:23:32Z","closed_at":null,"author_association":"OWNER","body":"In the following, the missing dot leads to the second case of the pattern matching begin left out by the parser (for the next value). But without this second case the typing is not right, and since we type-check before parsing the following value we get a type error.\r\n\r\n```\r\ntype Bool = [Tru | Fls]\r\ntype SList(α,A) = μα X.[Nil | Cons of {hd : A; tl : X}]\r\ntype F(A,X) = [Nil | Cons of {hd : A; tl : X}]\r\n\r\nval rec partition : ∀A.∀α.(A → Bool) → SList(α,A) → (SList(α,A) × SList(α,A)) =\r\n  fun test l →\r\n    case l of\r\n    | []   → ([], [])\r\n    | x::l → let α,A such that l : SList(α,A) in\r\n             let c : (μα X F(A,X)) × (μα X.F(A,X)) = partition test l in (* <-- HERE *)\r\n             if test x then ((x::c.1) , c.2) else (c.2,(x::c.1))\r\n```"}}
{"actor":{"display_login":"rlepigre"}}