Obtaining eta expansion of constructor without typeclasses

A while back, @JasonGross pointed out that you can obtain an eta expansion of a record's constructor without relying on user-provided typeclass instances like

(* all you need to do is provide something like this, listing out the fields of your record: *)
Instance etaX : Settable _ := settable! mkX <A; B; C>.

and his solution looks as follows:

Record X := mkX { A : nat ; B : nat ; C : bool ; }.

Ltac make_eta X :=
  let s
      := constr:(ltac:(
                   let x := fresh "x" in
                   intro x; unshelve eexists;
                   [ econstructor; destruct x | destruct x; reflexivity ])
                 : forall x : X, { x' : X | x' = x }) in
  lazymatch s with
  | fun x => exist _ (@?s x) _ => s
  end.

Check ltac:(let s := make_eta X in exact s).

It creates an eta-expanded version of the constructor mkX:

fun x : X =>
{|
  A := match x with
       | {| A := A; B := B; C := C |} => (fun (A0 _ : nat) (_ : bool) => A0) A B C
       end;
  B := match x with
       | {| A := A; B := B; C := C |} => (fun (_ B0 : nat) (_ : bool) => B0) A B C
       end;
  C := match x with
       | {| A := A; B := B; C := C |} => (fun (_ _ : nat) (C0 : bool) => C0) A B C
       end
|}
     : X -> X

However, @tchajed (and myself, too) did not like that solution because it does not reuse the existing getters, but creates new ones.

Now, for those who like Ltac2 hacks, here's a way to obtain an eta-expanded constructor that does reuse the existing getters:

Require Import Ltac2.Ltac2.
Require Ltac2.Option.

Module Import ModA.
  Record foo(A: Type)(n: nat) := {
    fieldA: unit;
    fieldB: n = n;
    fieldC: bool;
  }.
End ModA.

(* to show that the code below is robust against this kind of shadowing *)
Definition fieldA := @id.

Ltac2 rec strip_foralls(t: constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Prod b u => let (bs, body) := strip_foralls u in (b :: bs, body)
  | _ => ([], t)
  end.

Ltac2 app_arg_count(t: constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.App f args => Array.length args
  | _ => 0
  end.

Ltac2 binder_to_field(qualification: ident list)(b: binder) :=
   Option.get (Env.get (List.append qualification [Option.get (Constr.Binder.name b)])).

Ltac2 field_names(ctor_ref: Std.reference) :=
  let ctor_type := Constr.type (Env.instantiate ctor_ref) in
  let (binders, result) := strip_foralls ctor_type in
  let n_type_args := app_arg_count result in
  let field_name_binders := List.skipn n_type_args binders in
  List.map (binder_to_field (List.removelast (Env.path ctor_ref))) field_name_binders.

Ltac2 constructor_of_record(t: constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Ind ind inst =>
    Std.ConstructRef (Constr.Unsafe.constructor ind 0)
  | _ => Control.throw (Invalid_argument (Some (Message.of_constr t)))
  end.

Ltac2 Eval constructor_of_record constr:(foo).

Ltac2 mkApp(f: constr)(args: constr array) :=
  Constr.Unsafe.make (Constr.Unsafe.App f args).

Ltac2 eta(t: constr) :=
  let (h, args) := match Constr.Unsafe.kind t with
                   | Constr.Unsafe.App h args => (h, args)
                   | _ => (t, Array.empty ())
                   end in
  let ctor := constructor_of_record h in
  let getters := List.map (fun getterRef => mkApp (Env.instantiate getterRef) args)
                          (field_names ctor) in
  constr:(fun x: $t => ltac2:(
    let projections := List.map (fun getter => constr:($getter &x)) getters in
    let res := mkApp (mkApp (Env.instantiate ctor) args) (Array.of_list projections) in
    exact $res)).

Definition foo_eta(T: Type)(n: nat): foo T n -> foo T n :=
  ltac2:(let res := eta constr:(foo T n) in exact $res).

Print foo_eta.
(*
foo_eta =
fun (T : Type) (n : nat) (x : foo T n) =>
{| ModA.fieldA := ModA.fieldA T n x; fieldB := fieldB T n x; fieldC := fieldC T n x |}
     : forall (T : Type) (n : nat), foo T n -> foo T n
*)

Definition X_eta: X -> X :=
  ltac2:(let res := eta constr:(X) in exact $res).

Print X_eta.
(* creates an eta-expanded version of the constructor mkX, reusing the existing getters A, B, C:
X_eta = fun x : X => {| A := A x; B := B x; C := C x |}
     : X -> X
*)

I haven't tried yet whether it could replace the current typeclass-based approach, nor spent any thought on whether such code is morally acceptable, but just wanted to paste it here for whoever might find it entertaining :wink:

tchajed / coq-record-update

Obtaining eta expansion of constructor without typeclasses #19