search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.77k stars 639 forks source link

Evarconv does not handle opaque primitive projections correctly #17774

Closed Janno closed 1 year ago

Janno commented 1 year ago

Description of the problem

Evarconv considers opaque primitive projections not unifiable with themselves. The code below reproduces the problem in a roundabout way. (There is only one code path in Coq that calls Evarconv with transparency states that are not TransparentState.full!)

#[projections(primitive)]
Record r := { w : Prop -> Prop -> Prop }.

Set Typeclasses Filtered Unification. (* Only used to trigger evarconv code path *)
Class C (P : Prop) := {}.
Definition wand_apply (v : r) (P Q : Prop) : C (w v P Q) := Build_C _.
#[local] Hint Resolve wand_apply : typeclass_instances.

Goal forall (v : r) (Q P : Prop), C (w v P Q).
Proof.
  intros.
  Succeed typeclasses eauto.
  #[local] Hint Opaque w : typeclass_instances.
  Set Debug "unification,ho-unification".
  Fail typeclasses eauto.
Abort.

The example does not work on master because Typeclasses Filtered Unification has been removed. Our (closed source) OCaml plugin that first exhibited this problem only compiles with 8.17 right now so we do not know if the problem exists on master.

Coq Version

8.17

rlepigre commented 1 year ago

This can also be reproduced on master now, thanks to https://github.com/coq/coq/pull/17777 (see the new test case in https://github.com/coq/coq/pull/17788).