Limited support when the decreasing argument is a Prop while the return type is in Type

[HuStmpHrrr]

It seems that somehow Equations is not able to handle a particular application where the decreasing argument is a Prop but the result is meaningful. A reproduction is the following code:

Require Import Coq.Program.Equality.
From Equations Require Import Equations.

Generalizable All Variables.

Inductive exp : Set :=
(* Natural numbers *)
| a_fn : exp -> exp -> exp
| a_app : exp -> exp -> exp.

Reserved Notation "'env'".

Inductive domain : Set :=
| d_fn : env -> exp -> domain
where "'env'" := (nat -> domain).

Definition extend_env (p : env) (d : domain) : env :=
  fun n =>
    match n with
    | 0 => d
    | S n' => p n'
    end.

Inductive eval_exp : exp -> env -> domain -> Prop :=
| eval_exp_fn : `( eval_exp (a_fn A m) p (d_fn p m) )
| eval_exp_app :
  `( eval_exp M p m ->
     eval_exp N p n ->
     eval_app m n r ->
     eval_exp (a_app M N) p r )
with eval_app : domain -> domain -> domain -> Prop :=
| eval_app_fn :
  `( eval_exp M (extend p n) m ->
     eval_app (d_fn p M) n m ).

Inductive eval_exp_order : exp -> env -> Prop :=
| eeo_fn :
  `( eval_exp_order (a_fn A M) p )
| eeo_app :
  `( eval_exp_order M p ->
     eval_exp_order N p ->
     (forall m n, eval_exp M p m -> eval_exp N p n -> eval_app_order m n) ->
     eval_exp_order (a_app M N) p )

with eval_app_order : domain -> domain -> Prop :=
| eao_fn :
  `( eval_exp_order M (extend_env p n) ->
     eval_app_order (d_fn p M) n ).

#[local]
  Ltac impl_obl_tac1 :=
  match goal with
  | H : eval_exp_order _ _ |- _ => dependent destruction H
  | H : eval_app_order _ _ |- _ => dependent destruction H
  end.

#[local]
  Ltac impl_obl_tac :=
  try impl_obl_tac1; try econstructor; eauto.

#[tactic="impl_obl_tac"]
Equations eval_exp_impl m p (H : eval_exp_order m p) : { d | eval_exp m p d } by struct H :=
| a_fn A m, p, H => exist _ (d_fn p m) (eval_exp_fn _ _ _)
| a_app M N, p, H =>
    let (m , Hm) := eval_exp_impl M p _ in
    let (n , Hn) := eval_exp_impl N p _ in
    let (a, Ha) := eval_app_impl m n _ in
    exist _ a _

  with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H :=
| (d_fn p M), n, H =>
    let (m, Hm) := eval_exp_impl M (extend_env p n) _ in
    exist _ m _.

(* This will become an error in the future [solve_obligation_error,tactics] *)

Obligations.

(* 1 obligation(s) remaining: *)
(* Obligation 1 of eval_app_impl_equation_1: *)
(* (forall (p : env) (M : exp) (n : domain) (H : eval_app_order (d_fn p M) n), *)
(*  eval_app_impl (d_fn p M) n H = *)
(*  (let (m, Hm) := eval_exp_impl M (extend_env p n) (eval_exp_impl_obligations_obligation_5 p M n H) in *)
(*   exist (fun d : domain => eval_app (d_fn p M) n d) m (eval_exp_impl_obligations_obligation_6 p M n H m Hm))). *)
(* 1 obligation(s) remaining: *)
(* Obligation 1 of eval_exp_impl_equation_1: *)
(* (forall (A m : exp) (p : env) (H : eval_exp_order (a_fn A m) p), *)
(*  eval_exp_impl (a_fn A m) p H = exist (fun d : domain => eval_exp (a_fn A m) p d) (d_fn p m) (eval_exp_fn A m p)). *)
(* 1 obligation(s) remaining: *)
(* Obligation 1 of eval_exp_impl_equation_2: *)
(* (forall (M N : exp) (p : env) (H : eval_exp_order (a_app M N) p), *)
(*  eval_exp_impl (a_app M N) p H = *)
(*  (let (m, Hm) := eval_exp_impl M p (eval_exp_impl_obligations_obligation_1 M N p H) in *)
(*   let (n, Hn) := eval_exp_impl N p (eval_exp_impl_obligations_obligation_2 M N p H m Hm) in *)
(*   let (a, Ha) := eval_app_impl m n (eval_exp_impl_obligations_obligation_3 M N p H m Hm n Hn) in *)
(*   exist (fun d : domain => eval_exp (a_app M N) p d) a (eval_exp_impl_obligations_obligation_4 M N p H m Hm n Hn a Ha))). *)

Next Obligation.
  dependent destruction H. reflexivity.

  Restart.

  (* or the original tactic suffices *)
  impl_obl_tac.
Defined.
Next Obligation. impl_obl_tac. Defined.
Next Obligation. impl_obl_tac. Defined.

(* it seems the elimination principle is not generated as well. *)

There are a few problems:

1. Equations fails to prove _equation_* obligations automatically. I suppose this is because Equations does not expect a decreasing argument in Prop like this. It spits out the following message and leaves obligations behind:

This will become an error in the future [solve_obligation_error,tactics]

However, the actual proof is quite easy. A dependent destruction will conclude the obligation. 2. Even if it is fine for Equations to leave some obligations behind, I would still expect that the specified tactic impl_obl_tac to be used to solve these obligations, but it is not quite the case right now. 3. ~~Also it seems the elimination principle for the Equations is not generated at all.~~ It is generated.

This issue is observed in a more complex application here: https://github.com/Beluga-lang/McLTT/pull/80.