{"action":"opened","issue":{"url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/5599","repository_url":"https://api.github.com/repos/Zimmi48/bugzilla-test","labels_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/5599/labels{/name}","comments_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/5599/comments","events_url":"https://api.github.com/repos/Zimmi48/bugzilla-test/issues/5599/events","html_url":"https://github.com/Zimmi48/bugzilla-test/issues/5599","id":253151964,"number":5599,"title":"Type errors involving constraints are sometimes wrong","user":{"login":"Zimmi48","id":1108325,"avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-08-27T09:20:32Z","updated_at":"2017-08-27T09:20:32Z","closed_at":null,"body":"Note: the issue was created automatically with bugzilla2github tool\n\n# Bugzilla Bug ID: 5599\nDate: 2017-06-14 03:24:51 +0200\nFrom: @_JasonGross\nTo:   \nCC:   coq-bugs-redist@lists.gforge.inria.fr\n\nLast updated: 2017-06-14 04:38:21 +0200\n\n\n## Bugzilla Comment ID: 16812\nDate: 2017-06-14 03:24:51 +0200\nFrom: @_JasonGross\n\nThis is a suspicious error message:\n\nThe term \"and\" has type \"Prop -> Prop -> Prop\" while it is expected to have \ntype \"Prop -> Prop -> Prop\" (cannot satisfy constraint\n\"True\" == \"(fun _ : flat_type ?base_type_code => Prop) ()%ctype\").\n\nThe invalid constraint is an accurate rendition of what's wrong, but the type \nerror is wrong.  Example code coming soon.\n\n\n## Bugzilla Comment ID: 16813\nDate: 2017-06-14 04:38:21 +0200\nFrom: @_JasonGross\n\nExample:\n(* -*- mode: coq; coq-prog-args: (\"-emacs\" \"-R\" \"src\" \"Crypto\" \"-R\" \"Bedrock\" \n\"Bedrock\" \"-R\" \"coqprime/Coqprime\" \"Coqprime\" \"-top\" \"ArithmeticSimplifierWf\") \n-*- *)\n(* File reduced by coq-bug-finder from original input, then from 425 lines to \n28 lines, then from 581 lines to 38 lines, then from 218 lines to 65 lines, \nthen from 222 lines to 86 lines, then from 202 lines to 87 lines, then from 447 \nlines to 107 lines, then from 221 lines to 142 lines, then from 335 lines to \n195 lines, then from 350 lines to 195 lines, then from 217 lines to 196 lines, \nthen from 144 lines to 60 lines, then from 76 lines to 60 lines, then from 53 \nlines to 36 lines, then from 52 lines to 37 lines *)\n(* coqc version 8.6 (June 2017) compiled on Jun 12 2017 14:31:24 with OCaml \n4.02.3\n   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,(HEAD \ndetached from 7e992fa) (ce1e1dba837ad6e2c79ff7e531b5e3adea3cd327) *)\n\nContext (base_type_code : Type).\nInductive flat_type := Tbase (T : base_type_code) | Unit | Prod (A B : \nflat_type).\nSection flat_type.\n  Context (interp_base_type : base_type_code -> Type).\n  Fixpoint interp_flat_type (t : flat_type) :=\n    match t with\n    | Tbase t => interp_base_type t\n    | Unit => unit\n    | Prod x y => prod (interp_flat_type x) (interp_flat_type y)\n    end.\nEnd flat_type.\nFixpoint smart_interp_flat_map2 {f1 f2 g}\n         (h : forall x, f1 x -> f2 x -> g (Tbase x))\n         (tt : g Unit)\n         (pair : forall A B, g A -> g B -> g (Prod A B))\n         {t}\n  : interp_flat_type f1 t -> interp_flat_type f2 t -> g t\n  := match t return interp_flat_type f1 t -> interp_flat_type f2 t -> g t with\n     | Tbase _ => h _\n     | Unit => fun _ _ => tt\n     | Prod A B => fun (v1 : interp_flat_type _ A * interp_flat_type _ B)\n                       (v2 : interp_flat_type _ A * interp_flat_type _ B)\n                   => pair _ _\n                           (@smart_interp_flat_map2 f1 f2 g h tt pair A (fst \nv1) (fst v2))\n                           (@smart_interp_flat_map2 f1 f2 g h tt pair B (snd \nv1) (snd v2))\n     end.\nDefinition wff_as_expr_or_const {t}\n  : interp_flat_type (fun _ => nat) t\n    -> interp_flat_type (fun _ => nat) t\n    -> Prop\n  := smart_interp_flat_map2\n       (fun t z1 z2 => False)\n       I\n       (fun _ _ => and).\n(* Error:\nIn environment\nt : flat_type\nf : flat_type\nf0 : flat_type\nThe term \"and\" has type \"Prop -> Prop -> Prop\" while it is expected to have \ntype \"Prop -> Prop -> Prop\" (cannot satisfy constraint\n\"True\" == \"(fun _ : flat_type => Prop) Unit\"). *)\n\n"}}
{"actor":{"display_login":"Zimmi48"}}