Conversion can fail to equate primitive projections with their compatibility constants

[Janno]

Description of the problem

This is an unforeseen consequence of #18373, I think. If I am right, it highlights a flaw in the attempt to decouple the concept and exact implementation of compatibility constants from the kernel. IIRC we convinced ourselves that the kernel would never need to check if a constant is a compatibility constant because compatibility constants would always be considered transparent and that would allow the kernel to reach the underlying projection. This is correct assuming that there is really no way to make the constants themselves opaque.

Unfortunately, even without the debug syntax I used in the example, it is very easy to make a compatibility constant opaque: any TransparentState.t value with tr_cst := Cpred.empty will do it. This happens for example when using a hint database's transparency state that has Hint Constants Opaque.

CC @rlepigre

Small Coq file to reproduce the bug

From Ltac2 Require Import Ltac2.
#[projections(primitive)]
Record r (u:unit) := { f : Prop -> Prop }.
Set Debug "unification".
Goal forall (x : r tt) (Q:Prop), False.
  intros x Q.
  #[local] Opaque ! f. (* Emulate a [TransparentState] value in which all constants, but not projections, are opaque *)
  Fail let lhs := Constr.Unsafe.make (Constr.Unsafe.App '@f [|'tt; 'x; 'Q|]) in
  Unification.unify (TransparentState.current ()) lhs '(@f tt x Q).

Version of Coq where this bug occurs

8.19.0

Last version of Coq where the bug did not occur

8.18

[Janno]

To elabrote in the issue a bit: of course the example code mentions the compatibility constant in "Opaque ! f" but the bug is that the effect of that command matters to the kernel. Unification does not fail when the term is open but otherwise equivalent because unification knows not to ask for the transparency of the compatibility constant. The kernel does not know and thus fails. As mentioned above, the same outcome can be achieved by getting the transparency from a hint db without ever mentioning "f". That last part is what convinced me that this is indeed a bug even if the reproducing example looks like it might be working as intended.

[SkySkimmer]

The status of Opaque ! is unclear but I guess the point is that using TransparentState.empty should also succeed

[Janno]

the point is that using TransparentState.empty should also succeed

I was hesitant when writing the report to use TransparentState.empty even though that was what I used for debugging. But I think you are right and even with all projections made opaque this should still work. In the end, the only thing that really matter is that CClosure.unfold_ref_with_args ends up using TransparentState.is_transparent_constant (through Table.value_of). The opacity of the projection probably does not matter at all.