Coq: ltac-matching and reassembling applications is not identity

[andres-erbsen]

Description of the problem

Set Primitive Projections.
Record box {T} := Box { unbox : T }.
Set Printing All.
Goal True.
  let e := constr:(unbox (@Box nat 7)) in
  let E := lazymatch e with ?f ?x => constr:(f x) end in
  idtac e; idtac E;
  constr_eq E e.
(* Error: Tactic failure: Not equal. *)

It is especially confusing that doing the same with a record with no parameters does not fail.

cc @samuelgruetter

Coq Version

8.9.0

[SkySkimmer]

The surprising part is that ltac ?f ?x matches a projection IMO.

[JasonGross]

I think we need some way to manipulate projections in Ltac. I pushed for ?f ?x matching projections as part of the compatibility layer, but I'm open to other things. One use case of this is writing a cbn_head tactic:

Ltac head x :=
  match x with
  | ?f _ => head f
  | _ => x
  end.

Ltac cbn_head x :=
  let h := head x in eval cbn [h] in x.

I would also be able to write tactics that work for records of a given shape, and a parametric over the projections of the record.

[andres-erbsen]

Perhaps projections should be matched using _.(_)? #8829

[JasonGross]

If I can match a projection using ?v.(?p), and then pass p to a cbn argument list, and also can then write v.(p), and is_proj p passes, I would be satisfied with that (even though it might be a pain to track down all of the cases where the compatibility thing is happening; ideally there'd be an intermediate version of Coq where it emits a warning saying what line of original tactic code the failing match came from).

[andres-erbsen]

I mostly agree, except is_proj should probably not pass and there would need to be a new is_naked_proj or is_field something to avoid confusion.