Strange error message with function variables

[codyroux]

The following inductive gives a strange error when generating

inductive Im (f : Nat → Nat) : Nat → Nat → Prop where
| mk (x : Nat) : Im f x (f x)


/-- error: exprToConstructorExpr: We do not support higher order application of f in Expr f x
-/
#guard_msgs(error) in
derive_generator fun f y => ∃ x, Im f x y

This message is confusing: what is a "higher order application"?

A better message is: "variables in application position are not allowed in Im".

A much better thing would be to allow this.