Here is a weird bug:

```
Declare ML Module "coq-core.plugins.ltac".
Global Set Default Proof Mode "Classic".
Notation "A -> B" := (forall (_ : A), B) (at level 99, right associativity, B at level 200).
Inductive eq (A : Type) (a : A) : A -> Type := refl : eq A a a.
Arguments refl {A a}.
(** This is needed *)
Global Set Primitive Projections.
(** Record with a single field. *)
Record A := { t : Type; }.
(** The idenity function on A. With primitive projections this should be
definitionally equal to x. *)
Definition idA (x : A) : A := {| t := t x |}.
(** Record extending first record with a coercion to it and an extra field. *)
Record B := { a :> A; extra : Type; }.
(** As expected, the identity function on A is the identity. *)
Succeed Definition test1 (x : A) : eq A x (idA (idA x)) := refl.
(** Weirdly however, the identity function can be appied to B. Coq appears to
discard idA entirely even though the argument has extra information and is not
just an A. Instead of failing this succeeds. *)
Definition test2 (x : B) : eq B x (idA (idA x)) := refl.
(** And no idA is left in the term. *)
Print test2.
```

Primitive projections appears to silently discard information when it thinks it can eta reduce, even though B terms contain more information than A so it appears to magically accept something completely different than the user intended. This example was minimized from a real practice example. Anybody seen something like this before?

Turning primitive projections off makes this fail as expected.

reversible coercions

Print test2 with Set Printing All shows

```
test2 =
fun x : B => @eq_refl B x
: forall x : B, @eq B x (@reverse_coercion B A x (idA (idA (a x))))
Arguments test2 x
```

(modified the test to use the prelude instead of being noinit)

Last updated: Oct 13 2024 at 01:02 UTC