{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/237","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/237/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/237/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/237/events","html_url":"https://github.com/FStarLang/FStar/issues/237","id":75342533,"number":237,"title":"Problems in k_foralle","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":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-05-11T20:12:48Z","updated_at":"2015-05-11T21:59:03Z","closed_at":null,"body":"This problem appears in `tinyfstar-new.fst` in the `k_foralle` proof. After a bit of local simplification the code looks like this:\r\n```\r\n(* This takes forever to typecheck and fails without the assert;\r\n   plus this fails without the explicit type annotation on k' in KTApp\r\n   (Unresolved implicit argument). *)\r\nval k_foralle : #g:env -> #t1:typ -> #t2:typ ->\r\n                =hk1:kinding g t1 KType ->\r\n                =hk2:kinding (eextend t1 g) t2 KType ->\r\n                Tot (kinding g (TTApp (TConst TcForallE) t1)\r\n                               (KKArr (KTArr t1 KType) KType))\r\nlet k_foralle g t1 t2 hk1 hk2 =\r\n  let gwf = kinding_ewf hk1 in\r\n  (* assert(KKArr (KTArr t1 KType) KType =  *)\r\n  (*        ktsubst_beta t1 (KKArr (KTArr (TVar 0) KType) KType)); *)\r\n  KTApp (KKArr (KTArr (TVar 0) KType) KType) (KConst TcForallE gwf) hk1 (magic())\r\n```\r\nI've put a lot of effort into reproducing this in a smaller setting, but so far without any success. Basically the same code in `bug237.fst` works just fine."},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/101060619","html_url":"https://github.com/FStarLang/FStar/issues/237#issuecomment-101060619","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/237","id":101060619,"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-05-11T21:59:03Z","updated_at":"2015-05-11T21:59:03Z","body":"The minimal counterexample for this looks like this:\r\n```\r\ntype knd =\r\n  | KType : knd\r\n  | KKArr : knd -> knd\r\n\r\nval ktsubst_beta : knd -> Tot knd\r\nlet ktsubst_beta k = k\r\n\r\nval tconsts : unit -> Tot knd\r\nlet tconsts () = KKArr KType\r\n\r\ntype kinding : k:knd -> Type =\r\n| KConst : kinding (tconsts())\r\n| KTApp : #k':knd -> hk1:kinding (KKArr k') -> kinding (ktsubst_beta k')\r\n\r\nval k_foralle : u:unit -> Tot (kinding KType)\r\nlet k_foralle () =  KTApp (* KType *) KConst\r\n(* Problem: without the annotation and the explicit k' in KTApp\r\n   this causes \"Unresolved implicit argument\" *)\r\n```"}}