Coq-Equations Illegal application : the Xth term has type "T"

Following from the issue 211, I tried rewriting my code to simplify it but I keep getting the

Error: Illegal application: 
The Xth term has type
 "A" which should be coercible to "B".

I either get this immediately after my definition or once I finished proving every obligation and I Qed.

I tried coming up with a simple example with the error, hopefully it's simple enough (and I hope it is similar to what I have haha). If I remove the map_In everything works ok but... I'm guessing that's still a bug or something I'm doing wrong :p.

PS. I took Ssromega from here.

Require Import List.
From mathcomp Require Import all_ssreflect.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Asymmetric Patterns.

From Equations Require Import Equations.

Require Import Ssromega.

Section list_size.
    Context {A : Type} (f : A -> nat).
    Equations list_size (l : list A) : nat :=
      {
        list_size nil := 0;
        list_size (cons x xs) := S (f x + list_size xs)
      }.
End list_size.

Section Map.
  Variables (A : eqType) (B : Type).
  
  Equations map_In {A B : Type}
     (l : list A) (f : forall (x : A), In x l -> B) : list B :=
  map_In nil _ := nil;
  map_In (cons x xs) f := cons (f x _) (map_In xs (fun x H => f x _)).
  
End Map.


Section Test.

  Variables (L U R : Type).

  Inductive Foo : Type :=
  | C1 : L -> Foo
  | C3 : L -> seq Foo -> Foo.

  Inductive Result : Type :=
  | ULeaf : U -> Result
  | UNode : list Result -> Result.
  (* Derive NoConfusion for Result. *)

  Fixpoint rsize (r : Result) :=
    match r with
    | ULeaf a => 0
    | UNode l => S (list_size rsize l)
    end.

  Lemma In_result_rsize_leq r res :
    In r res ->
    rsize r < (list_size rsize res).
  Proof.
    funelim (list_size rsize res) => //=.
    case=> [-> | Hin]; [| have Hleq := (H r Hin)]; ssromega.
  Qed.



  
  Variables (Null : R) (resolve : U -> Result).


  Equations? execute (initial_value : U) (foos : seq Foo) : seq R  :=
    {
      execute _ [::] := [::];
      
      execute initial_value (_ :: qs) := (complete_value (resolve initial_value)) ++ execute initial_value qs
            
          where complete_value (res : Result) : seq R by wf (rsize res) :=
                  {
                    complete_value (UNode res) := flatten (map_In res (fun r Hin => complete_value r)); 
      
                    complete_value (ULeaf res) := [::]
                  }
            
    }.
  all: do ?[by have Hleq := (In_result_rsize_leq r res Hin); ssromega].
  Qed.
  
End Test.