fix: Use whnf for mutual recursion with types hiding → (#2926)

the code stumbled over recursive functions whose type doesn’t have
enough manifest foralls, like:

```
def FunType := Nat → Nat

mutual
def foo : FunType
  | .zero => 0
  | .succ n => bar n
def bar : FunType
  | .zero => 0
  | .succ n => foo n
end
termination_by foo n => n; bar n => n
```

This can be fixed by using `whnf` in appropriate places, to expose the
`.forall` constructor.

Fixes #2925, comes with test case.

src/Lean/Elab/PreDefinition/WF/PackDomain.lean

@@ -124,7 +124,8 @@ where
       let args := e.getAppArgs
       let fNew := mkConst preDefsNew[funIdx]!.declName f.constLevels!
       let fNew := mkAppN fNew args[:fixedPrefix]
-      let Expr.forallE _ d .. ← inferType fNew | unreachable!
+      let Expr.forallE _ d .. ← whnf (← inferType fNew) | unreachable!
+      -- NB: Use whnf in case the type is not a manifest forall, but a definition around it
       let argNew ← mkUnaryArg d args[fixedPrefix:]
       return mkApp fNew argNew
     let rec

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -51,13 +51,13 @@ private partial def mkNewCoDomain (preDefsOriginal : Array PreDefinition) (preDe
       let casesOn := mkAppN casesOn xTypeArgs -- parameters
       let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive
       let casesOn := mkApp casesOn x -- major
-      let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x =>
-        mkLambdaFVars #[x] (preDefTypes[i]!.bindingBody!.instantiate1 x)
+      let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x => do
+        mkLambdaFVars #[x] ((← whnf preDefTypes[i]!).bindingBody!.instantiate1 x)
       let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1]! fun x => do
         mkLambdaFVars #[x] (← go x (i+1))
       return mkApp2 casesOn minor1 minor2
     else
-      return preDefTypes[i]!.bindingBody!.instantiate1 x
+      return (← whnf preDefTypes[i]!).bindingBody!.instantiate1 x
   go x 0
 
 /--
@@ -176,7 +176,7 @@ where
 def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
   if preDefs.size == 1 then return preDefs[0]!
   withFixedPrefix fixedPrefix preDefs fun ys types vals => do
-    let domains := types.map fun type => type.bindingDomain!
+    let domains ← types.mapM fun type => do pure (← whnf type).bindingDomain!
     let domain ← mkNewDomain domains
     withLocalDeclD (← mkFreshUserName `_x) domain fun x => do
       let codomain ← mkNewCoDomain preDefsOriginal types x

tests/lean/run/issue2925.lean

@@ -0,0 +1,15 @@
+def FunType := Nat → Nat
+def Fun2Type := Nat → Nat → Nat
+
+mutual
+def foo : FunType
+  | .zero => 0
+  | .succ n => bar n
+def bar : Nat → Nat
+  | .zero => 0
+  | .succ n => baz n 0
+def baz : Fun2Type
+  | .zero, m => 0
+  | .succ n, m => foo n
+end
+termination_by foo n => n; bar n => n; baz n _ => n