`sizeOf` generation failure on higher-order nested types

[arthur-adjedj]

Prerequisites

• 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

When defining certain kinds of nested inductive types, lean may throw a kernel error related to auxiliary theorems produced when generating the SizeOf instance.

Steps to Reproduce

inductive Higher (f : Type → Type) (A : Type) where
  | c_higher : f A → Higher f A

inductive Bar where
  | bar : Higher List Bar → Bar

Expected behavior: No error

Actual behavior:

(kernel) application type mismatch
  Eq.trans (congrArg (Nat.add 1) (Bar._sizeOf_3_eq a✝))
    (Eq.symm (Higher.c_higher.sizeOf_spec List Bar (fun a => List._sizeOf_inst a) Bar._sizeOf_inst a✝))
argument has type
  1 + sizeOf a✝ = sizeOf (Higher.c_higher List Bar a✝)
but function has type
  Nat.add 1 (sizeOf a✝) = sizeOf (Higher.c_higher List Bar a✝) →
    Nat.add 1 (Bar._sizeOf_3 a✝) = sizeOf (Higher.c_higher List Bar a✝)

Versions

Lean 4.28.0-nightly-2025-12-28
Target: x86_64-unknown-linux-gnu

Impact

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