in extraction optimization, a eta-reduction leads to a not generalizable '_a

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2570
From: Frédéric Tuong <frederictuong@gmail.com>
Reported version: 8.5

[coqbot]

Comment author: Frédéric Tuong <frederictuong@gmail.com>

====================
The problem

Starting from this well-typed program in Coq trunk 14161 :

Require Import Vector.
Require Import List.

Definition to_list0 : forall A n,
Vector.t A n -> { _ : list A | True } :=
fun A _ v => @ exist (list A) (fun _ => True)
match v with
| Vector.cons x _ _ => List.cons x List.nil
| Vector.nil => List.nil
end I.

Definition u1 : forall M N L n
(to_list1 : forall A n,
Vector.t A n -> { _ : list A | True })
(sep : Vector.t M n)
(xs : list L)
(surr : Vector.t N n),
M -> M.
intros until 4;
pose (v_to_list A v := let (l, _) := to_list0 A n v in l);
pose (c := fun B n s l => @ List.combine _ B (v_to_list n s) l);
refine (List.fold_left _ (c _ _ sep (c _ _ surr xs)));
auto with *.
Defined.

we get in OCaml 3.12 a ML file which does not match its extracted MLI, because the extracted [u1] has a too general type.
This can be resolved by manually replacing [let v_to_list = to_list0 n] by [let v_to_list v = to_list0 n v].

====================
Other possible solutions

a) Note that in the original Coq code, if we replace, [to_list0] by [to_list1] in [u1], the extracted implementation matches correctly its interface.
b) Instead of doing a manual eta-expansion, we can disable the optimization responsible of this error in Coq with [Set Extraction Flag 494.]. Then, we have a well-accepted code (which moreover does not use [Obj.magic]).

====================
Localization in the source

In coq_svn_14161[...]mlutil.ml, the eta-reduction performed in the function [kill_dummy] does not perform an eta-reduction test to avoid a not generalizable ['_a]. At the time of writing, the author has not searched further if this test may or not be done in a similar way as coq_svn_14161[...]extraction.ml.
Remark also, even if it has not been tested, that we may factorize the part under the case [MLletin] in [kill_dummy] with the [MLletin] part in [kill_dummy_hd] by abstracting what is necessary.

====================
Note

We have presented a simplified case where the ML is well-typed alone. In a more complete project, it may happen that the obtained ML is not well-typed before the need to see if it matches its MLI.

[coqbot]

Comment author: @letouzey

Thanks for this bug report. This issue should now be fixed in trunk
since commit 14782. I'll also backport this fix in the 8.3 branch soon.

Best,
Pierre Letouzey