Error "(kernel) application type mismatch" in theorem on inductive type

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

I'm getting the error above in strange circumstances. My reproducer has two almost-identical recursive theorems, the error occurs when the second theorem use the first theorem instead of recursing.

Update: This appears to be related to cases and the wf termination checker, see https://github.com/leanprover/lean4/issues/8839#issuecomment-2980413352.

This might be related to #6544, however that uses induction while my main reproducer doesn't.

It might also be related to #8488, I can't tell if they are caused by the same issue.

Steps to Reproduce

abbrev Ctx := List String

/-- Uncurried lambda expressions. -/
inductive Expr1 where
  | abs : List String → Expr1 → Expr1
--| var : String → Expr1
--| app : ...

/-- Curried lambda expressions. -/
inductive Expr2 where
  | abs : String → Expr2 → Expr2

/-- Conversion from Expr1 to Expr2. -/
def conv : Expr1 → Expr2
  | .abs xs b => xs.foldr .abs (conv b)

-- In the real program Prop1 is interesting, but in this minimal version it's almost trivial.
inductive Prop1 : Ctx → Expr1 → Prop
  | abs_rule (Γ : Ctx) (xs : List String) (b : Expr1) :
      Prop1 (xs.reverse ++ Γ) b →
      Prop1 Γ (.abs xs b)

-- Likewise for Prop2.
inductive Prop2 : Ctx → Expr2 → Prop where
  | abs_rule (Γ : Ctx) (x : String) (b : Expr2) :
      Prop2 (x :: Γ) b →
      Prop2 Γ (.abs x b)

-- Theorem: `conv` preserves the property.
-- No errors.
theorem conv_prop_v1 (Γ : Ctx) (e : Expr1) : Prop1 Γ e → Prop2 Γ (conv e) := by
  intro h; cases h with
  | abs_rule Γ xs b hb =>
    simp only [conv]
    match _ : xs with
    | .nil =>
      simp_all
      apply conv_prop_v1
      exact hb
    | .cons x xs' =>
      simp_all
      apply Prop2.abs_rule
      rw [←conv]
      apply conv_prop_v1
      apply Prop1.abs_rule
      exact hb

-- Same theorem with almost the same proof, except it uses `conv_prop_v1` instead of recursion in one place.
/-
ERROR:
(kernel) application type mismatch
  @x✝.1 (@id (Prop1 Γ✝ b) hb)
argument has type
  Prop1 Γ✝ b
but function has type
  Prop1 Γ b → Prop2 Γ (conv b)
-/
theorem conv_prop_v2 (Γ : Ctx) (e : Expr1) : Prop1 Γ e → Prop2 Γ (conv e) := by
  intro h; cases h with
  | abs_rule Γ xs b hb =>
    simp only [conv]
    match _ : xs with
    | .nil =>
      simp_all
      apply conv_prop_v2 -- normal recursion
      exact hb
    | .cons x xs' =>
      simp_all
      apply Prop2.abs_rule
      rw [←conv]
      apply conv_prop_v1 -- NOTE: this uses `conv_prop_v1` instead of recursion
      apply Prop1.abs_rule
      exact hb

-- Note:
-- Changing the recursive application `apply conv_prop_v2` to also use
-- `conv_prop_v1` makes the error disappear (!).

Expected behavior: No error.

Actual behavior: Error.

Versions

4.20.0, 4.21.0-rc3, 4.22.0-nightly-2025-06-16

Additional Information

I'm not sure how the variables of the constructors are determined. If I change (xs.reverse ++ Γ) to Γ in Prop1, then Γ is no longer a variable of Prop1.abs_rule (the line | abs_rule Γ xs b hb => becomes an error: "too many variable names provided at alternative"). I'm not sure if this is relevant.

I have another reproducer that uses a single theorem and induction:

-- Hacks to make the proof to work.
-- In the real program Γ is important, but in this minimal version it's basically unused.
theorem Prop1_ignores_Γ (Γ Γ' : Ctx) (e : Expr1) : Prop1 Γ e → Prop1 Γ' e := by
  intro h; cases h with
  | abs_rule Γ xs b hb => exact Prop1.abs_rule _ _ _ (Prop1_ignores_Γ _ _ _ hb)
theorem Prop2_ignores_Γ (Γ Γ' : Ctx) (e : Expr2) : Prop2 Γ e → Prop2 Γ' e := by
  intro h; cases h with
  | abs_rule Γ x b hb => exact Prop2.abs_rule _ _ _ (Prop2_ignores_Γ _ _ _ hb)

-- Theorem: `conv` preserves the property.
/-
ERROR:
(kernel) application type mismatch
  @x✝.1 (@id (Prop1 Γ✝ b) hb)
argument has type
  Prop1 Γ✝ b
but function has type
  Prop1 Γ b → Prop2 Γ (conv b)
-/
theorem conv_prop_v3 (Γ : Ctx) (e : Expr1) : Prop1 Γ e → Prop2 Γ (conv e) := by
  intro h; cases h with
  | abs_rule Γ xs b hb =>
    simp only [conv]
    induction xs with
    | nil =>
      simp_all
      trace_state -- hb : Prop1 Γ b  ⊢  Prop2 Γ (conv b)
      apply conv_prop_v3
      exact hb
    | cons x xs' ih =>
      simp_all
      apply Prop2.abs_rule
      apply Prop2_ignores_Γ
      apply ih
      apply Prop1_ignores_Γ
      exact hb

Impact

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

Start by running the minimal reproducer from the issue against the listed Lean versions and inspect the interaction between cases, induction, and the well-founded termination checker. Compare conv_prop_v1, conv_prop_v2, and conv_prop_v3, using the reported kernel type mismatch as the failure condition. Done means the reproducer elaborates without the error and the expected theorem is accepted.