Extensionality Tactic does not seem to be running the `Obligation Tactic` as implied by error message

[Durbatuluk1701]

This is not quite a self-contained example but hopefully is enough to justify the issue. Essentially, when trying Unset Equation With Funext and defining a Local Obligation Tactic that is sufficient to solve the extensionality proof automatically, Equations will still throw a warning with "Solve Obligations tactic return error: Tactic failure: Could not prove extensionality automatically".

Here is an example:

  (* Local Obligation Tactic := ... *)
  Equations? dfs_aux (g : t) (stack : list K.t) (visited : KSet.t)
      : KSet.t
      by wf (KSet.cardinal (KSet.diff (vertices g) visited), length stack)
          (lexprod _ _ lt lt) :=

    dfs_aux g []        visited := visited;

    dfs_aux g (v :: vs) visited :=
      match KSet.mem visited v as Hvis return KSet.mem visited v = Hvis -> _ with
      | true => fun _ =>
        dfs_aux g vs visited
      | false =>
        fun Hviseq =>
        match has_vertex g v as HV return has_vertex g v = HV -> _ with
        | true => fun _ =>
          let visited' := KSet.add visited v in
          let neighbors := KSet.to_list (nodes_out g v) in
          dfs_aux g (neighbors ++ vs) visited'
        | false =>
          fun _ =>
          dfs_aux g vs (KSet.add visited v)
        end eq_refl
      end eq_refl.
  + left.
    apply KSet.cardinal_diff_add_lt.
    - rewrite <- has_vertex_vertices. assumption.
    - assumption.
  + assert (Hnotin: KSet.mem (vertices g) v = false).
    { rewrite <- has_vertex_vertices. assumption. }
    rewrite (KSet.cardinal_diff_add_notin _ _ _ Hnotin).
    right. simpl. lia.
  Qed.
  (*
  Solve Obligations tactic returned error: Tactic failure: Could not prove extensionality automatically.
    This will become an error in the future
    [solve_obligation_error,tactics,default]
    1 obligation remaining
    Obligation 1 of dfs_aux_unfold_eq:
    (forall (g : t) (stack : list K.t) (visited : KSet.t),
    dfs_aux g stack visited = dfs_aux_unfold g stack visited).
  *)
  Obligations.
  (*
  1 obligation(s) remaining: 
  Obligation 1 of dfs_aux_unfold_eq:
  (forall (g : t) (stack : list K.t) (visited : KSet.t),
  dfs_aux g stack visited = dfs_aux_unfold g stack visited).
  *)
  (* You could just use "Solve All Obligations." now or *)
  Next Obligation.
  (*
    dfs_aux_unfold_eq (remaining: 1/1)
      dfs_aux_unfold_eq_obligation: (solved: pending) (loc : )
  *)
  Defined.

Note how Solve All Obligations (or just opening and immediately closing the Obligation) is sufficient to solve it (thus my belief that the Solve Obligations tactic can in fact solve the extensionality proof), but it still throws this warning.

It is not necessarily critical because ultimately it still works, but it is sort of an ugly warning during compilation I would like to try to avoid.

---

Another interesting thing: if a From Equations.Prop Require Import Tactics. is removed from the file, then the warning changes to Solve Obligations tactic returned error: Tactic failure: Equations.Init.unfold_recursor has not been bound yet., but basically nothing else changes AFAICT

[Durbatuluk1701]

Okay here is closer to a self-contained example, although sorry it includes a lot of likely unimportant tactic stuff, but it at least compiles (with rocq-core 9.0.1 and rocq-equations 1.3.1+9.0):

From Equations Require Import Equations Init. 
From Equations.Prop Require Import Equations.
From Ltac2 Require Export Ltac2 Printf Pstring Notations.
From Ltac2 Require Export Bool Lazy Array Lazy FMap Fresh Control Ltac1 Constr.
From Stdlib Require Import Lia.

(**
 * [fresh_names_in_goal n basename] generates a list of [n] fresh identifiers
 * that do not conflict with names currently in the goal or with each other.
 * All generated names will have [basename] as their prefix.
 *)
Ltac2 rec fresh_names_in_goal (n : int) (basename : ident) (avoid : Fresh.Free.t) (acc : ident list) : ident list :=
  if Int.le n 0 then
    List.rev acc
  else
    let h := Fresh.fresh avoid basename in
    fresh_names_in_goal (Int.sub n 1) basename 
      (Free.union (Free.of_ids [h]) avoid) (h :: acc).

(**
 * A convenient wrapper to generate a list of [n] fresh hypothesis names.
 *)
Ltac2 fresh_hyps (n : int) (basename : string) : ident list :=
  match Ident.of_string basename with
  | None => throw_invalid_argument "fresh_hyps" "basename must be a valid identifier"
  | Some name =>
    (* Generate fresh names in the goal, avoiding conflicts with existing names *)
    fresh_names_in_goal n name (Fresh.Free.of_goal ()) []
  end.

(**
 * A variant of [fresh_hyp] that always generates a single fresh name.
 *)
Ltac2 fresh_hyp (basename : string) : ident :=
  let avoid := Fresh.Free.of_goal () in
  match Ident.of_string basename with
  | None => throw_invalid_argument "fresh_hyp" "basename must be a valid identifier"
  | Some basename_ident =>
    (* Generate a single fresh name, avoiding conflicts with existing names *)
    Fresh.fresh avoid basename_ident
  end.

Ltac contains_ltac sub c :=
  match c with
  | context [ sub ] => idtac
  end.

Ltac2 contains (sub : constr) (c : constr) : bool :=
  Control.once (fun () =>
    Control.plus
      (fun () =>
         ltac1:(sub c |- contains_ltac sub c) (Ltac1.of_constr sub) (Ltac1.of_constr c);
         true
      )
      (fun _ => false)
  ).

Ltac2 is_closed (c : constr) : bool :=
  Control.once (fun () =>
    Control.plus (fun () => let _ := type c in true) (fun _ => false)
  ).

Ltac2 rec check_prefixes (f : constr) (args : constr array) (t : constr) (idx : int) :=
  if Int.gt idx (Array.length args) then Control.zero (Tactic_failure None)
  else
    let prefix := 
      if Int.equal idx 0 then f
      else Constr.Unsafe.make (Constr.Unsafe.App f (Array.sub args 0 idx))
    in
    
    if is_closed prefix then
      let ty := type prefix in
      if contains t ty then
        if contains t prefix then check_prefixes f args t (Int.add idx 1)
        else ltac1:(p |- generalize p) (Ltac1.of_constr prefix)
      else check_prefixes f args t (Int.add idx 1)
    else check_prefixes f args t (Int.add idx 1).

(* Extracts a single subterm and routes it to the prefix slicer *)
Ltac2 check_term_and_generalize (u : constr) (t : constr) : unit :=
  match Constr.Unsafe.kind u with
  | Constr.Unsafe.App f args => check_prefixes f args t 0
  | _ => Control.zero (Tactic_failure None)
  end.

Ltac2 generalize_one_dep t :=
  match! goal with
  | [ |- context [ ?u ] ] => check_term_and_generalize u t
  end.

Ltac2 ddest (t : constr) :=
  repeat (generalize_one_dep t); destruct $t.

Ltac2 Notation "ddest" t(constr) := ddest t.

Inductive tree A :=
| Leaf : A -> tree A
| Node : tree A -> tree A -> tree A.
Arguments Leaf {A} _.
Arguments Node {A} _ _.

Fixpoint height {A} (t : tree A) : nat :=
  match t with
  | Leaf _ => 0
  | Node l r => S (Nat.max (height l) (height r))
  end.

Unset Equations With Funext.
Set Default Proof Mode "Classic".
Local Obligation Tactic :=
  simpl in *; Tactics.program_simplify;
  CoreTactics.equations_simpl;
  try Tactics.program_solve_wf;
  ltac2:(try (
    match! goal with
    | [ |- ?orig _ _ _ = ?unf _ _ _ ] =>
      match Constr.Unsafe.kind orig, Constr.Unsafe.kind unf with
      | Constr.Unsafe.Constant origr _, Constr.Unsafe.Constant unfr _ =>
        let orig_ref := Std.ConstRef origr in
        let unf_ref := Std.ConstRef unfr in
        Std.unfold [(orig_ref, Std.AllOccurrences)] 
          { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences };
        match! goal with
        | [ |- context [ @FixWf ?a ?r ?wf ?p ?f ?x ] ] =>
          let step := fresh_hyp "step" in
          set($step := fun y (_ : $r y $x) => @FixWf $a $r $wf $p $f y) in *;
          let stepv := Control.hyp step in
          Control.unshelve (fun () => 
            erewrite (@FixWf_unfold_step $a $r $wf $p $f $x _ $stepv)) >
          [
            clear step; red; intros; ltac1:( simp_sigmas )
            | subst step; 
              Std.unfold [(unf_ref, Std.AllOccurrences)] 
                { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }; 
                repeat (
                  match! goal with
                  | [ |- context [match ?e with _ => _ end] ] =>
                    destruct $e; eauto; try reflexivity; try (congruence)
                  end
                )
            | solve [ reflexivity ]
          ]
        end;
        match! goal with
        | [ |- ?f _ _ _ _ = ?f _ _ _ _ ] => 
          match Constr.Unsafe.kind f with
          | Constr.Unsafe.Constant fref _ =>
            let f_ref := Std.ConstRef fref in
            Std.unfold [(f_ref, Std.AllOccurrences)] 
              { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }
          | _ => fail
          end
        end;
        repeat (match! goal with
        | [ |- context [ match ?e with _ => _ end ] ] =>
            ddest $e; eauto; try reflexivity; try (congruence)
        end)
      | _, _ => fail
      end
    end
  )).

Equations tree_lt {A} (n1 n2 : tree A) : bool by wf ((height n1) + (height n2)) :=
  tree_lt Leaf Leaf := false;
  tree_lt Leaf (Node _ _) := true;
  tree_lt (Node _ _) Leaf := false;
  tree_lt (Node l1 r1) (Node l2 r2) := 
    match Nat.ltb (height l1) (height l2) as Hlt return (Nat.ltb (height l1) (height l2) = Hlt -> bool) with
    | false => fun _ => false
    | true => fun Hlt => orb (tree_lt l1 l2) (
      match Nat.ltb (height l2) (height l1) as Hrt return (Nat.ltb (height l2) (height l1) = Hrt -> bool) with
      | false => fun _ => false
      | true => fun Hlt_bad => tree_lt (Node l1 r2) (Node l2 r1)
      end eq_refl
    )
    end eq_refl.
Next Obligation.
  try (erewrite PeanoNat.Nat.ltb_lt in *; lia).
Qed.
Next Obligation.
  try (erewrite PeanoNat.Nat.ltb_lt in *; lia).
Qed.
(*
Solve Obligations tactic returned error: Tactic failure: Could not prove extensionality automatically.
This will become an error in the future
[solve_obligation_error,tactics,default]
1 obligation remaining
Obligation 1 of tree_lt_unfold_eq:
(forall (A : Type) (n1 n2 : tree A), tree_lt n1 n2 = tree_lt_unfold n1 n2).
*)
Next Obligation.
Defined.