{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7595","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7595/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7595/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7595/events","html_url":"https://github.com/coq/coq/issues/7595","id":326079865,"number":7595,"title":"Universe coercion error, but only in coqtop [regression from 8.7]","user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars1.githubusercontent.com/u/330628?v=4","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":12,"created_at":"2018-05-24T11:31:15Z","updated_at":"2018-05-24T12:11:01Z","closed_at":null,"author_association":"CONTRIBUTOR","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\n8.8.0\r\n\r\n#### Operating system\r\nLinux\r\n\r\n#### Description of the problem\r\n\r\nThis needs two files to reproduce, the error goes away on inlining:\r\n\r\nFile `base2.v`:\r\n```\r\nFrom Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.\r\nSet Default Proof Using \"Type\".\r\nExport ListNotations.\r\nFrom Coq.Program Require Export Basics Syntax.\r\nGlobal Generalizable All Variables.\r\n\r\n(** * Type classes *)\r\n(** ** Decidable propositions *)\r\n(** This type class by (Spitters/van der Weegen, 2011) collects decidable\r\npropositions. *)\r\nClass Decision (P : Prop) := decide : {P} + {¬P}.\r\nHint Mode Decision ! : typeclass_instances.\r\nArguments decide _ {_} : simpl never, assert.\r\n\r\n(** ** Proof irrelevant types *)\r\n(** This type class collects types that are proof irrelevant. That means, all\r\nelements of the type are equal. We use this notion only used for propositions,\r\nbut by universe polymorphism we can generalize it. *)\r\nClass ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.\r\nHint Mode ProofIrrel ! : typeclass_instances.\r\n\r\nClass MGuard (M : Type → Type) :=\r\n  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.\r\nArguments mguard _ _ _ !_ _ _ / : assert.\r\nNotation \"'guard' P ; z\" := (mguard P (λ _, z))\r\n  (at level 20, z at level 200, only parsing, right associativity) .\r\nNotation \"'guard' P 'as' H ; z\" := (mguard P (λ H, z))\r\n  (at level 20, z at level 200, only parsing, right associativity) .\r\n```\r\n\r\nFile `option.v`:\r\n```\r\nRequire Import base2.\r\n\r\nLemma dec_stable `{Decision P} : ¬¬P → P.\r\nProof. firstorder. Qed.\r\n\r\n(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the\r\ncomponents is double negated, it will try to remove the double negation. *)\r\nTactic Notation \"destruct_decide\" constr(dec) \"as\" ident(H) :=\r\n  destruct dec as [H|H];\r\n  try match type of H with\r\n  | ¬¬_ => apply dec_stable in H\r\n  end.\r\nTactic Notation \"destruct_decide\" constr(dec) :=\r\n  let H := fresh in destruct_decide dec as H.\r\n\r\n\r\n(** * Monadic operations *)\r\nInstance option_guard: MGuard option := λ P dec A f,\r\n  match dec with left H => f H | _ => None end.\r\n\r\n(** * Tactics *)\r\nTactic Notation \"case_option_guard\" \"as\" ident(Hx) :=\r\n  match goal with\r\n  | H : context C [@mguard option _ ?P ?dec] |- _ =>\r\n    change (@mguard option _ P dec) with (λ A (f : P → option A),\r\n      match @decide P dec with left H' => f H' | _ => None end) in *;\r\n    destruct_decide (@decide P dec) as Hx\r\n  | |- context C [@mguard option _ ?P ?dec] =>\r\n    change (@mguard option _ P dec) with (λ A (f : P → option A),\r\n      match @decide P dec with left H' => f H' | _ => None end) in *;\r\n    destruct_decide (@decide P dec) as Hx\r\n  end.\r\nTactic Notation \"case_option_guard\" :=\r\n  let H := fresh in case_option_guard as H.\r\n\r\nLemma option_guard_True {A} P `{Decision P} (mx : option A) :\r\n  P → (guard P; mx) = mx.\r\nProof. intros. case_option_guard. reflexivity. contradiction. Qed.\r\n```\r\n\r\nBoth files compile fine when running `coqc`, but the last `Qed` fails when running `coqtop` or running interactively in emacs:\r\n```\r\nError: Illegal application: \r\nThe term \"option\" of type \"Type → Type\"\r\ncannot be applied to the term\r\n \"A\" : \"Type\"\r\nThis term has type \"Type@{Top.95}\" which should be coercible to\r\n \"Type@{Coq.Init.Datatypes.13}\".\r\n```"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/391691160","html_url":"https://github.com/coq/coq/issues/7595#issuecomment-391691160","issue_url":"https://api.github.com/repos/coq/coq/issues/7595","id":391691160,"user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars1.githubusercontent.com/u/330628?v=4","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"created_at":"2018-05-24T12:11:01Z","updated_at":"2018-05-24T12:11:01Z","author_association":"CONTRIBUTOR","body":"Oh, also, the same thing still worked with 8.7."}}
{"actor":{"display_login":"RalfJung"}}