Type errors that mention the part of the rule declaration being offended?

[Mallku2]

I have trouble trying to understand type error messages that do not mention explicitly which part of the rule declaration is being offended (either its premises, arguments, parameter, assumptions, etc). For example, I cannot quite grasp the meaning of the following error message:

Type checking application failed:
Children: [subproof, (p a), ((forall ((@varlist x1) @varlist.nil)) (p x1))]
Message: Unexpected argument type 0 of subproof
  LHS (Proof G), from (Proof G)
  RHS Bool
  Context []

produced by the step:

(step-pop t1 (@cl (not (forall ( ( x1 U ) ) (p x1))) (p a)) :rule subproof :premises ( (p a) ))

where subproof is defined as:

(declare-rule subproof ((F Bool) (G Bool :list))
  :assumption F
  :premises (G)
  :requires (...) ; Not showing it, for simplicity
  :conclusion-given
)

(the previous definitions belong to https://github.com/cvc5/AletheInEunoia/tree/main/signature; let me know if it would be useful to provide more info about the error!)