Program Fixpoint with wf fixannot and function return types

[allioux]

There seems to be a problem in the proof term generated by Program Fixpoint when the wf fixannot is set and when the return type is a function type.

The problem occurs in the recursive call to foo in the following example:

Require Import Coq.Program.Wf.

Inductive Nat : Type :=
| O : Nat
| S : Nat -> Nat.

Inductive wfn : Nat -> Nat -> Prop :=
| wfn_suc : forall n, wfn n (S n)
| wfn_trans : forall x y z, wfn x y -> wfn y z -> wfn x z
.

Definition wfn_Sn (n : Nat) : Acc wfn (S n).
Admitted.

Lemma wfn_wf : well_founded wfn.
Admitted.

Program Fixpoint foo (n : Nat) {wf wfn n }: Nat -> Nat := fun x =>
  match n with
    O => x
  | S n => foo n _
  end.
Obligation 1. apply wfn_suc. Qed.
Obligation 3. unfold MR. apply wfn_wf. Qed.

foo n _ should be of type Nat -> Nat and the program shouldn't typecheck as a term of type Nat is expected.
Instead, it seems the argument is treated as implicit and the program is accepted.
When inspecting the produced proof obligation, one can see that the term x is passed to foo.
This problem does not occur when no fixannot is set.

My coq version is 8.13.

[herbelin]

There seems indeed to be a problem with wf here. Informing @coq/funind-maintainers.

[Matafou]

This concerns Program, not Function. Informing @mattam82.

[herbelin]

Oups, sorry.

[herbelin]

Fixed by #18834. Thanks!