Kernel error for `inferInstanceAs` with let declarations

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 the expected type contains a let variable that needs to be unfolded to unify with the provided type, inferInstanceAs fails with a kernel type mismatch.

Context

#general > backward.isDefEq.respectTransparency

Steps to Reproduce

/--
error: (kernel) declaration type mismatch, '_example._aux_1' has type
  Type → Nat
but it is expected to have type
  (E : Type) → E
---
warning: declaration uses `sorry`
-/
#guard_msgs in
example : True := by
  let E : Type := id Nat
  let hE : Inhabited E := inferInstanceAs (Inhabited Nat)
  sorry

Versions

Lean 4.31.0-nightly-2026-04-14

Impact

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

Start with the minimal reproduction for inferInstanceAs and the linked backward.isDefEq.respectTransparency discussion, then test it against the latest nightly release. The work is done when the example no longer produces the kernel declaration type mismatch while preserving the expected type-checking behavior.