A polymorphic version of ` withCollectingNewGoalsFrom`

Stream: lean4

[Leni Aniva]

Is there a polymorphic version of this function? I want to elaborate an expression and simultaneously return extra information, but this function restricts the return type to Expr.

e.g. something like

def withCollectingNewGoalsFrom { a } (k : TacticM a) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (a × List MVarId) :=