Merge PR coq#19775: Fixes coq#12417: check that the argument of "wf" …

…in funind is a well-typed relation

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <[email protected]>

doc/changelog/02-specification-language/19775-master+fix12417-check-typing-wf-relation.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  Anomaly in :cmd:`Function` when a well-founded relation had not the expected type
+  (`#19775 <https://github.com/coq/coq/pull/19775>`_,
+  fixes `#12417 <https://github.com/coq/coq/issues/12417>`_,
+  by Hugo Herbelin).

plugins/funind/recdef.ml

@@ -1615,6 +1615,16 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   ()
 
+let check_relation_type env evd relation =
+  let err () = CErrors.user_err (strbrk "a well-founded relation is expected to be of type A->A->Prop for some type A.") in
+  let evd, t = Typing.type_of env evd relation in
+  let open Reductionops in
+  match EConstr.kind evd (whd_all env evd t) with
+  | Prod (_, typ, _) ->
+    let rel = mkArrowR typ (mkArrowR (Vars.lift 1 typ) mkProp) in
+    if not (is_conv env evd rel t) then err ()
+  | _ -> err ()
+
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
 
 let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
@@ -1689,6 +1699,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
       env
   in
   let relation, evuctx = interp_constr env_with_pre_rec_args evd r in
+  let () = check_relation_type env_with_pre_rec_args evd relation in
   let evd = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in

test-suite/bugs/bug_12417.v

@@ -0,0 +1,41 @@
+Declare ML Module "rocq-runtime.plugins.funind".
+
+Inductive tm :=
+| E: nat -> tm
+| L: list tm -> tm.
+
+Definition T := list tm.
+
+Fixpoint max_list (p: nat) (l: list nat) : nat :=
+  match l with
+  | nil => p
+  | cons n l' => max_list (Init.Nat.max n p) l'
+  end.
+
+Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
+match l with
+| nil => nil
+| cons x l => cons (f x) (map f l)
+end.
+
+Fixpoint depth (t: tm) : nat :=
+  match t with
+  | E _ => 0
+  | L l => 1 + max_list 0 (map depth l)
+  end.
+
+Fixpoint sum_depth (l: T) : nat :=
+  match l with
+  | nil => 0
+  | cons n l' => (depth n) + sum_depth l'
+  end.
+
+Fail Function sum_total (l: T) {wf sum_depth l} : nat :=
+  match l with
+  | nil => 0
+  | cons t l' =>
+    (match t with
+      | E n => n
+      | L li => sum_total li
+      end) + sum_total l'
+  end.