{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/194","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/194/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/194/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/194/events","html_url":"https://github.com/FStarLang/FStar/issues/194","id":64847212,"number":194,"title":"\"Empty args\" for nested let rec","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},"labels":[{"url":"https://api.github.com/repos/FStarLang/FStar/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-03-27T20:42:21Z","updated_at":"2015-03-27T20:44:40Z","closed_at":null,"body":"As Franziska et al just noticed, the support for nested fixpoints is rather flaky in F*. For instance, the following code taken from their normalization proof:\r\n```\r\nval red_beta : t1:typ -> t2:typ -> x:var -> e:exp ->\r\n               typing (extend empty x t1) e t2 ->\r\n               (e' : exp -> red t1 e' -> Tot (red t2 (subst_beta_gen x e' e))) ->\r\n               e' : exp -> red t1 e' -> Tot (red t2 (EApp (ELam t1 e) e'))\r\nlet red_beta t1 t2 x e ty_t2 f e' red_e' =\r\n  let ExIntro v steps_ev = red_halts red_e' in\r\n  let rec induction (ter: steps e v) (* : Tot (red t2 (EApp (ELam t1 e) e'))*) =\r\n    (match ter with\r\n     | Multi_step same_e' e'' same_v step_e'e'' mult_e''v -> \r\n\tred_exp_closed (EApp (ELam t1 e) e') (TyApp (TyLam t1 ty_t2) (red_typable_empty red_e')) (fun e' (step_ee': step e e') -> magic())\r\n     | Multi_refl same_e' -> magic()\r\n    )\r\n  in\r\n  induction steps_ev\r\n```\r\ncauses the following `Empty args!` error:\r\n```\r\nUnexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.\r\nEmpty args!\r\n```\r\nLooking at the F* source this appears only 2 times in the code, and only once in the type-checker:\r\n```\r\n[hritcu@detained src]$ grep -R \"Empty args\"\r\nabsyn/syntax.fs:    n=(match args with [] -> failwith \"Empty args!\" | _ -> Exp_app(e1, args));\r\nocaml.ml:(failwith (\"Empty args!\"))\r\n```\r\nThe code in `absyn/syntax.fs` looks like this:\r\n```\r\nlet mk_Exp_app ((e1:exp),(args:args)) (t:option<typ>) p = {\r\n    n=(match args with [] -> failwith \"Empty args!\" | _ -> Exp_app(e1, args));\r\n    tk=get_typ_ref t;\r\n    pos=p;\r\n    uvs=mk_uvs(); fvs=mk_fvs();\r\n}\r\n```\r\nOn Franziska's machine uncommenting the type annotation on `induction` was causing the `Unexpected error` to change. I can't reproduce that part though.\r\n\r\nThis seems similar to #58, but manifests itself differently.\r\n"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/87084753","html_url":"https://github.com/FStarLang/FStar/issues/194#issuecomment-87084753","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/194","id":87084753,"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-03-27T20:44:40Z","updated_at":"2015-03-27T20:44:40Z","body":"The workaround is at the moment hoisting such fixpoints to the top level."}}