(kernel) unknown constant in mutually recursive definition

[nomeata]

Description

In some (possibly not-well-founded) mutually recursive definitions, we get (kernel) unknown constant.

Context

I stumbled over this while trying to help someone on Zulip.

Steps to Reproduce

MWE:

mutual
  inductive Thing : Type
    | Bag : Object → Thing
  inductive Object : Type
    | Bike : Object
    | Box : Thing -> Object
end

mutual
  def sizeOfThing : Thing → Nat
    | .Bag o => 1 + sizeOfObject o
  def sizeOfObject : Object → Nat
    | .Bike => 42
    | .Box t => 1 + sizeOfThing t
end

axiom Nat.add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n

mutual
theorem aboutThings : ∀ t, sizeOfThing t % 2 = 1
  | .Bag o => by
    unfold sizeOfThing
    rw [Nat.add_mod, aboutObjects /- o-/]
    rfl

theorem aboutObjects : ∀ o, sizeOfObject o % 2 = 0
  | .Bike => rfl
  | .Box t => by
    unfold sizeOfObject
    rw [Nat.add_mod, aboutThings t]
    rfl
end
decreasing_by sorry

This prints

(kernel) unknown constant 'aboutObjects'
declaration uses 'sorry'

The kernel error goes away if I use aboutObjects o in the call to rw, i.e. with an explicit argument.

Expected behavior: No kernel errors.

Actual behavior: The kernel prints an error

Versions

~/build/lean/mathlib4 $ lean --version
Lean (version 4.2.0-rc1, commit a62d2fd49796, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Smaller reproducer:

opaque myId : (Nat → Nat) → (Nat → Nat) := id

mutual
def foo : Nat → Nat
  | .zero => 0
  | .succ n => (myId bar) n
def bar : Nat → Nat
  | .zero => 0
  | .succ n => foo n
end
termination_by foo n => n; bar n => n

The recursive call seems to be missing an argument. Maybe packDomain, or a pass before packDomain needs to eta-expand.

[nomeata]

<internal monologe>
This code seems to be related:

    let isBad (e : Expr) : Bool :=
      match isAppOfPreDef? e with
      | none   => false
      | some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i]!.declName != preDefs[i]!.declName
    if let some bad := valueNew.find? isBad then
      if let some i := isAppOfPreDef? bad then
        throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i]!.declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]!}"

but I am not sure I follow: Why should it be bad if a call has more arguments? As #2892 shows that can be perfectly fine if the result type happens to be a function type. Will dive a bit deeper here, and cook up a few test cases.

NB: replaceRecApps does eta-expand as needed. So other passes should do so as well.
</internal monologe>