Bug in graph generation causes illegal application

[joscoh]

As discussed on Zulip, the following example with monadic binders and mutual well-founded recursion fails:

From ExtLib Require Export Monads MonadState StateMonad.
Require Import Coq.Lists.List.
From Equations Require Import Equations.
Require Import Lia.

Definition st A B := (state A B).
Definition st_bind {A B C: Type} (f: B -> st A C) (x: st A B) : st A C :=
  bind x f.
Definition st_ret {A B: Type} (x: B) : st A B := ret x.

Notation "x <- c1 ;; c2" := (@st_bind _ _ _ (fun x => c2) c1)
  (at level 61, c1 at next level, right associativity).

Inductive tm :=
  | mk_tm : tm_node -> unit -> tm
with tm_node :=
  | t_1 : tm_node
  | t_2: list tm -> tm_node.

Definition node_of (t: tm) : tm_node :=
  match t with
  | mk_tm n _ => n
  end.

(*Size metric for recursion*)
Fixpoint tm_size (t: tm) : nat :=
  match node_of t with
  | t_1 => 1
  | t_2 l => length l + S (list_sum (map tm_size l))
  end.

Definition tm_node_size (t: tm_node) : nat :=
  match t with
  | t_1 => 1
  | t_2 l => length l + S (list_sum (map tm_size l))
  end.

Section Foo.

Variable (St A: Type).
Variable (f1: tm -> tm_node -> st St A).

(*Encode mutual recursion with GADT*)
Variant foo_ty :=
  | N : tm_node -> foo_ty
  | L: list tm -> foo_ty.

(*dependent return type*)
Definition foo_ret (t: foo_ty) : Type :=
  match t with
  | N _ => st St A
  | L _ => st St (list A)
  end.

Definition foo_size (f: foo_ty) : nat :=
  match f with
  | N t => tm_node_size t
  | L t => length t + list_sum (map tm_size t)
  end.

(*Need for obligations*)
Definition foo_size_prop (t: tm) (x: foo_ty) : Prop :=
  match x with
  | N t1 => tm_node_size t1 = tm_size t
  | L l => Forall (fun x => tm_size x < tm_size t) l
  end.

Equations foo (x: tm) : st St A by wf (tm_size x) lt :=
  foo x := foo_node (N (node_of x)) _
where foo_node (y: foo_ty) (Hsize: foo_size_prop x y) : foo_ret y by wf (foo_size y) :=
  foo_node (N t) _ := f1 x t;
  foo_node (L nil) _ := st_ret nil;
  foo_node (L (t1 :: ts)) _ :=
    x1 <- foo t1 ;;
    x2 <- foo_node (L ts) _ ;;
    st_ret (x1 :: x2).
Next Obligation.
inversion Hsize; auto.
Defined.
Next Obligation. lia. Defined.
Next Obligation.
inversion Hsize; auto.
Defined.
Next Obligation.
destruct x; auto.
Defined.

It fails (on the last Defined) with the error:

Illegal application:
The term "foo_clause_1_foo_node_graph" of type
 "forall (x : tm) (y : foo_ty), foo_size_prop x y -> foo_ret y -> Type"
cannot be applied to the terms
 "x" : "tm"
 "fun (x0 : tm) (_ : tm_size x0 < tm_size x) => foo x0"
   : "forall x0 : tm, tm_size x0 < tm_size x -> st St A"
 "L ts" : "foo_ty"
 "foo_clause_1_foo_node x (fun (x0 : tm) (_ : tm_size x0 < tm_size x) => foo x0) (L ts)"
   : "foo_size_prop x (L ts) -> foo_ret (L ts)"
The 2nd term has type "forall x0 : tm, tm_size x0 < tm_size x -> st St A" which should be a subtype of
 "foo_ty".