{"action":"closed","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6715","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6715/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6715/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6715/events","html_url":"https://github.com/coq/coq/issues/6715","id":295319908,"number":6715,"title":"Program fixpoint: cannot instantiate \"?T\" because \"a\" is not in its scope","user":{"login":"nomeata","id":148037,"avatar_url":"https://avatars2.githubusercontent.com/u/148037?v=4","gravatar_id":"","url":"https://api.github.com/users/nomeata","html_url":"https://github.com/nomeata","followers_url":"https://api.github.com/users/nomeata/followers","following_url":"https://api.github.com/users/nomeata/following{/other_user}","gists_url":"https://api.github.com/users/nomeata/gists{/gist_id}","starred_url":"https://api.github.com/users/nomeata/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nomeata/subscriptions","organizations_url":"https://api.github.com/users/nomeata/orgs","repos_url":"https://api.github.com/users/nomeata/repos","events_url":"https://api.github.com/users/nomeata/events{/privacy}","received_events_url":"https://api.github.com/users/nomeata/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-02-07T22:40:53Z","updated_at":"2018-02-07T22:49:31Z","closed_at":"2018-02-07T22:49:31Z","author_association":"CONTRIBUTOR","body":"#### Version & OS\r\n\r\n```\r\n$ coqtop -v\r\nThe Coq Proof Assistant, version 8.6 (September 2017)\r\ncompiled on Sep 26 2017 9:14:9 with OCaml 4.05.0\r\n$ lsb_release -a\r\nNo LSB modules are available.\r\nDistributor ID:\tDebian\r\nDescription:\tDebian GNU/Linux unstable (sid)\r\nRelease:\tunstable\r\nCodename:\tsid\r\n```\r\n\r\n#### Description of the problem\r\n\r\nConsider this file:\r\n```\r\n(* Default settings (from HsToCoq.Coq.Preamble) *)\r\n\r\nRequire Coq.Program.Wf.\r\n\r\nInductive IntMap a : Type := Bin : bool -> a -> IntMap a -> IntMap a -> IntMap a\r\n                          |  Nil : IntMap a.\r\n\r\nFixpoint size_nat {a} (t : IntMap a) : nat :=\r\n  match t with\r\n  | Bin _ _ _ l r => S (size_nat l + size_nat r)%nat\r\n  | Nil _ => 0\r\n  end.\r\n\r\nRequire Omega.\r\nLtac termination_by_omega :=\r\n  Coq.Program.Tactics.program_simpl;\r\n  simpl;Omega.omega.\r\n\r\nProgram Fixpoint restrictKeys {a : Type} (t : IntMap a) {measure (size_nat t)} : IntMap a\r\n                   := match t  with\r\n                        | Bin _ p1 m1 l1 r1 =>\r\n                          let intersection1 := restrictKeys l1\r\n                          in\r\n                          intersection1\r\n                        | _  => Nil _\r\n                      end.\r\nSolve Obligations with (termination_by_omega).\r\n\r\nReset restrictKeys.\r\n\r\nProgram Fixpoint restrictKeys {a : Type} (t : IntMap a) {measure (size_nat t)} : IntMap a\r\n                   := match t  with\r\n                        | Bin _ p1 m1 l1 r1 =>\r\n                            match p1 with\r\n                              | true => Nil _\r\n                              | false => restrictKeys l1\r\n                            end\r\n                        | _  => Nil _\r\n                      end.\r\nSolve Obligations with (termination_by_omega).\r\n\r\nReset restrictKeys.\r\n\r\n\r\nProgram Fixpoint restrictKeys {a : Type} (t : IntMap a) {measure (size_nat t)} : IntMap a\r\n                   := match t  with\r\n                        | Bin _ p1 m1 l1 r1 =>\r\n                          let intersection1 :=\r\n                            match p1 with\r\n                              | true => Nil _\r\n                              | false => restrictKeys l1\r\n                            end\r\n                          in\r\n                          intersection1\r\n                        | _  => Nil _\r\n                      end.\r\nSolve Obligations with (termination_by_omega).\r\n```\r\n\r\nThe last `Program Fixpoint` fails with\r\n\r\n```\r\n\r\nError:\r\nIn environment\r\na : Type\r\nt : IntMap a\r\nrestrictKeys :\r\nforall (a0 : Type) (t0 : IntMap a0), size_nat t0 < size_nat t -> IntMap a0\r\np1 : bool\r\nm1 : a\r\nl1 : IntMap a\r\nr1 : IntMap a\r\nHeq_t : Bin a p1 m1 l1 r1 = t\r\nHeq_p1 : false = p1\r\nThe term \"restrictKeys a l1 ?recproof\" has type \"IntMap a\"\r\nwhile it is expected to have type\r\n \"IntMap\r\n    ?T@{a:=t; t:=restrictKeys; restrictKeys:=p1; p1:=m1; m1:=l1; l1:=r1;\r\n        r1:=Heq_t; Heq_t:=false}\" (cannot instantiate \"?T\" because \"a\" is not\r\nin its scope: available arguments are \"t\" \"restrictKeys\" \"p1\" \"m1\" \"l1\" \r\n\"r1\" \"Heq_t\" \"false\").\r\n```\r\n\r\nThe problem goes away if I  remove any of: \r\n * the enclosing `match … of` _or_\r\n * the enclosing `let`\r\nas shown by the first and second call to `Program Fixpoint`, which go through nicely.\r\n\r\n"}}
{"actor":{"display_login":"ejgallego"}}