Any better way to work around Higher order input? error in the SMT mode?

[zqy1018]

Hi! I recently started experimenting with lean-auto, primarily to explore its support for SMT solvers. However, I frequently encounter errors ending with Higher order input?, which are not always very informative and require manual debugging.

For instance, in the artificial example below, I initially could not locate the issue, but later realized that since f2 is a function, the entire term a could be considered higher-order.

set_option auto.smt true
set_option auto.smt.trust true

structure A where
  f1 : List Nat
  f2 : Nat → List Nat

example : ∀ (a : A) (n : Nat),
  a.f1.length < n → a.f1.length ≤ n :=
  by
    intros a n
    -- `auto` here reports `lamSort2STermAux :: Unexpected error. Higher order input?`
    -- tried on Lean 4.9.0 and 4.11.0
    sorry

On the other hand, it seems that some techniques, like term substitution using generalize, could potentially address this problem.

-- attempt again
example : ∀ (a : A) (n : Nat),
  a.f1.length < n → a.f1.length ≤ n :=
  by
    intros a n
    generalize a.f1 = ff
    auto  -- now it works!

However I am not entirely sure if this is a reliable solution. I would like to know if there is any plan to address these types of issues.