{"action":"closed","issue":{"url":"https://api.github.com/repos/coq/coq/issues/9186","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/9186/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/9186/comments","events_url":"https://api.github.com/repos/coq/coq/issues/9186/events","html_url":"https://github.com/coq/coq/issues/9186","id":389611491,"node_id":"MDU6SXNzdWUzODk2MTE0OTE=","number":9186,"title":"Conversion test raised an anomaly: \"conversion was given ill-typed terms (FProd).\"","user":{"login":"akr","id":10538,"node_id":"MDQ6VXNlcjEwNTM4","avatar_url":"https://avatars1.githubusercontent.com/u/10538?v=4","gravatar_id":"","url":"https://api.github.com/users/akr","html_url":"https://github.com/akr","followers_url":"https://api.github.com/users/akr/followers","following_url":"https://api.github.com/users/akr/following{/other_user}","gists_url":"https://api.github.com/users/akr/gists{/gist_id}","starred_url":"https://api.github.com/users/akr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/akr/subscriptions","organizations_url":"https://api.github.com/users/akr/orgs","repos_url":"https://api.github.com/users/akr/repos","events_url":"https://api.github.com/users/akr/events{/privacy}","received_events_url":"https://api.github.com/users/akr/received_events","type":"User","site_admin":false},"labels":[{"id":723816203,"node_id":"MDU6TGFiZWw3MjM4MTYyMDM=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20anomaly","name":"kind: anomaly","color":"e00403","default":false}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-12-11T06:13:59Z","updated_at":"2018-12-11T19:00:00Z","closed_at":"2018-12-11T19:00:00Z","author_association":"NONE","body":"<!-- Thank you for your contribution.\r\n     Please complete the following information when reporting a bug. -->\r\n\r\n#### Version\r\n\r\n<!-- You can get this information by running `coqtop -v`. -->\r\n\r\n```\r\n% coqtop -v\r\nThe Coq Proof Assistant, version 8.8.2 (October 2018)\r\ncompiled on Oct 7 2018 20:17:55 with OCaml 4.07.0\r\n```\r\n\r\n#### Operating system\r\n\r\n```\r\n% lsb_release -a\r\nNo LSB modules are available.\r\nDistributor ID:\tDebian\r\nDescription:\tDebian GNU/Linux 9.6 (stretch)\r\nRelease:\t9.6\r\nCodename:\tstretch\r\n% uname -mrsv\r\nLinux 4.9.0-8-amd64 #1 SMP Debian 4.9.130-2 (2018-10-27) x86_64\r\n```\r\n\r\n#### Description of the problem\r\n\r\n<!-- It is helpful to provide enough information so that we can reproduce the bug.\r\n     In particular, please include a code example which produces it.\r\n     If the example is small, you can include it here between ``` ```.\r\n     Otherwise, please provide a link to a repository, a gist (https://gist.github.com)\r\n     or drag-and-drop a `.zip` archive. -->\r\n\r\nI found an anomaly as follows.\r\n\r\n```\r\nFixpoint arrow_type (Ts : list Set) (Tr : Set) :=\r\n  match Ts with\r\n  | nil => Tr\r\n  | cons T Ts' => T -> arrow_type Ts' Tr\r\n  end.\r\n\r\nFixpoint forall_type (Ts : list Set)\r\n    (f : unit -> Set) : Set :=\r\n  match Ts as Ts return (unit -> Set) -> Set with\r\n  | nil => fun f => f tt\r\n  | cons T Ts' => fun f => T -> forall_type Ts' f\r\n  end f.\r\n\r\nDefinition test_func (Ts : list Set) (Tv : Set)\r\n    (f : arrow_type Ts Tv) := tt.\r\n\r\nDefinition test_type (Ts : list Set) (Tr : Set) : Set :=\r\n  forall_type Ts (fun (dummy : unit) => True -> Tr).\r\n\r\nDefinition test (Ts : list Set) (Tr : Set)\r\n    (f : test_type Ts Tr) :=\r\n    test_func Ts (True -> Tr) f.\r\n(*\r\nConversion test raised an anomaly:\r\nAnomaly \"conversion was given ill-typed terms (FProd).\"\r\nPlease report at http://coq.inria.fr/bugs/.\r\n*)\r\n```\r\n\r\n\r\n"}}
{"actor":{"display_login":"ppedrot"}}