Bug in sizeOf generation

Stream: lean4

[Parth Shastri]

The following inductive type yields a strange error.

inductive Bug
  | mk : (Unit → Nat → Bug) → Bug

error: application type mismatch
  a_ih✝ () ()
argument has type
  Unit
but function has type
  Nat → Nat

Using set_option genSizeOf false suppresses the error, suggesting it occurs in the code that generates the sizeOf definition.
I believe the bug lies in this function which determines if the field is to be skipped:

private partial def ignoreField (x : Expr) : MetaM Bool := do
  let type ← whnf (← inferType x)
  if type.isForall then
    -- TODO: add support for finite domains
    if type.isArrow && type.bindingDomain!.isConstOf ``Unit then
      ignoreField type.bindingBody!
    else
      return true
  else
    return false

Notice that the recursive call is made directly on the body of the forall type, rather than an expression of that type. Then, the inferType will yield an incorrect result.
A possible fix is to replace the function with the following

private partial def ignoreField (x : Expr) : MetaM Bool := do
  helper (← inferType x)
where
  helper type := do
    let type ← whnf type
    if type.isForall then
      -- TODO: add support for finite domains
      if type.isArrow && type.bindingDomain!.isConstOf ``Unit then
        helper type.bindingBody!
      else
        return true
    else
      return false