(kernel) application type mismatch

[MikaelMayer]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following file has a kernel issue. Any comment with RB indicates that doing so will remove the bug, so it's pretty unstable. I was not able to reduce it further.

-- RB == removes bug
-- Removing IndentW RB
structure IW : Type 1 where
  I : Type

mutual

def aux (iw: IW) (e : Nat) (sm : List iw.I)
  : Nat :=
  e

-- I: Type instead of iw: IW RB
def aval (iw: IW) (n : Nat) (e : Nat) : Nat :=
  match n with
  | 0 => e
  | n' + 1 =>
      let e1 :=
        let input_map: List iw.I := [] --lifting RB
        let new_e := aux iw e input_map -- removing args RB
        avalCore iw n' new_e -- inlining RB
      avalCore iw n' e

-- Inlining RB
def avalCore (iw: IW) (n' : Nat) (e : Nat) : Nat :=
  aval iw n' e

end

Output

(kernel) application type mismatch
  aux (wfParam iw) (wfParam e) n'
argument has type
  Nat
but function has type
  List (IW.I (wfParam iw)) → Nat

Context

I minimize a lambda calculus rewriting and stumbled on this today.

Steps to Reproduce

1. Copy the code above
2. Paste it on https://live.lean-lang.org/#project=lean-nightly
3. Expand the info and observe the error message

Expected behavior: The file shouldn't fail

Actual behavior: The file fails

Versions

4.23.0-rc2
live.lean-lang.org and Windows

Additional Information

No configuration necessary

Impact

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

[nomeata]

Hmm, e1 looks unused. Intentional?

[MikaelMayer]

Intentional. It's used in the original source code. Actually in the original source code, the computation of e1 and the body of the let are two branches of a match statement, and the matchee does not matter. This nested let is the result of trying to remove the pattern marching while keeping the bug.

[nomeata]

Right, I just hope that an unused let won't lead debugging or fixing astray, if some step now just removes it.

[nomeata]

The issue is with proving the .eq_def thm:

-- RB == removes bug
-- Removing IndentW RB
structure IW : Type 1 where
  I : Type

set_option Elab.async false

def aux (iw: IW) (e : Nat) (sm : List iw.I)
  : Nat :=
  e

/--
error: Cannot derive unfold equation aval._mutual.eq_def
  (kernel) application type mismatch
    aux (wfParam iw) (wfParam e) n'
  argument has type
    Nat
  but function has type
    List (IW.I (wfParam iw)) → Nat
-/
#guard_msgs in
mutual
-- I: Type instead of iw: IW RB
def aval (iw: IW) (n : Nat) (e : Nat) : Nat :=
  match n with
  | 0 => e
  | n' + 1 =>
      let e1 :=
        let input_map: List iw.I := [] --lifting RB
        let new_e := aux iw e input_map -- removing args RB
        avalCore iw n' new_e -- inlining RB
      avalCore iw n' e
termination_by (n, 0)

-- Inlining RB
def avalCore (iw: IW) (n' : Nat) (e : Nat) : Nat :=
  aval iw n' e
termination_by (n', 1)

end

The problem also goes away if the second recursive call to avalCore uses e1 rather than e.

It also goes away when using e1 like this:

      if e1 == e1 then
      aval iw n' e else 0

But no further clues for now.

[joehendrix]

@nomeata Thanks, it looks like we can temporarily work around this through using partial then. It'd be good to have a fix (or at least insight into the cause) so we can remove the partial annotations for reasoning purposes.

[nomeata]

This is a regression from between v4.21.0 to v4.22.0.

And between nightly-2025-06-26 and nightly-2025-06-27, so
https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2025-06-27
so maybe #8968. @kmill, can you have a look?

[nomeata]

With set_option wf.preprocess false the bug disappears as well.

[nomeata]

without conclusive evidence (cannot use check here because of open terms) I suspect some bvar index calculation mistake in or near this code in simpHaveTelescope

        withExistingLocalDecls [hinfo.decl] <| withNewLemmas #[x] do
          let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
          let expr := mkApp (mkLambda n .default t rb.expr) v'
          let exprType := rb.exprType.lowerLooseBVars 1 1
          let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
          let exprResult := mkHave n t v' rb.exprResult
          match valModified, rb.modified with
          | false, false =>
            let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType expr
            return { expr, exprType, exprInit, exprResult, proof, modified := false }
          | true, false =>
            let proof := mkApp6 (mkConst ``have_val_congr' us) t exprType v v'
              (mkLambda n .default t rb.exprInit) vproof
            return { expr, exprType, exprInit, exprResult, proof, modified := true }
          | false, true =>
            let proof := mkApp6 (mkConst ``have_body_congr' us) t exprType v
              (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) (mkLambda n .default t rb.proof)
            return { expr, exprType, exprInit, exprResult, proof, modified := true }
          | true, true =>
            let proof := mkApp8 (mkConst ``have_congr' us) t exprType v v'
              (mkLambda n .default t rb.exprInit) (mkLambda n .default t rb.expr) vproof (mkLambda n .default t rb.proof)
            return { expr, exprType, exprInit, exprResult, proof, modified := true }

[nomeata]

More evidence is that this patch makes the problem go away:

--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -723,8 +723,9 @@ where
             let proof := mkApp2 (mkConst `Eq.refl [info.level]) exprType expr
             return { expr, exprType, exprInit, exprResult, proof, modified := false }
           | true, false =>
-            let proof := mkApp6 (mkConst ``have_val_congr' us) t exprType v v'
-              (mkLambda n .default t rb.exprInit) vproof
+            let proof ← mkSorry (← mkEq expr exprResult) true
             return { expr, exprType, exprInit, exprResult, proof, modified := true }
           | false, true =>
             let proof := mkApp6 (mkConst ``have_body_congr' us) t exprType v

and this

--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -673,7 +673,7 @@ where
           let proof := mkApp6 (mkConst ``have_unused' us) t exprType v expr expr
             (mkApp2 (mkConst ``Eq.refl [info.level]) exprType expr)
           return { expr, exprType, exprInit, exprResult, proof, modified := true }
-      else if fixed.contains i then
+      else if true then -- fixed.contains i then
         /-
         Fixed `have` (like `CongrArgKind.fixed`): dsimp the value and simp the body.
         The variable appears in the type of the body.

and this

--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -622,7 +622,7 @@ def simpHaveTelescope (e : Expr) : SimpM Result := do
       | .error ex => pure m!"{crossEmoji} {ex.toMessageData}") do
     let info ← getHaveTelescopeInfo e
     assert! !info.haveInfo.isEmpty
-    let (fixed, used) ← info.computeFixedUsed (keepUnused := !(← getConfig).zetaUnused)
+    let (fixed, used) ← info.computeFixedUsed (keepUnused := false) --  !(← getConfig).zetaUnused)
     let r ← simpHaveTelescopeAux info fixed used e 0 (Array.mkEmpty info.haveInfo.size)
     if r.modified && debug.simp.check.have.get (← getOptions) then
       check r.expr

and this

+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -715,7 +715,9 @@ where
         withExistingLocalDecls [hinfo.decl] <| withNewLemmas #[x] do
           let rb ← simpHaveTelescopeAux info fixed used b (i + 1) (xs.push x)
           let expr := mkApp (mkLambda n .default t rb.expr) v'
-          let exprType := rb.exprType.lowerLooseBVars 1 1
+          let exprType := mkApp (mkLambda n .default t rb.exprType) v'
           let exprInit := mkApp (mkLambda n .default t rb.exprInit) v
           let exprResult := mkHave n t v' rb.exprResult
           match valModified, rb.modified with

This is in branch

        Non-fixed `have` (like `CongrArgKind.eq`): simp both the value and the body.
        The variable does not appear in the type of the body.

which seems to be wrong.

But I’m somewhat out of my depth (and time) here. Will wait for input from @kmill.