let elaboration more dependent than it should be

Consider this example

set_option pp.explicit true
/--
warning: declaration uses 'sorry'
---
info: P : Nat → Prop
m : Nat
⊢ @Eq Nat
    (let n := @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) m (@OfNat.ofNat Nat 2 (instOfNatNat 2));
    @ite Nat (@Eq Nat n (@OfNat.ofNat Nat 0 (instOfNatNat 0)))
      (instDecidableEqNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) m (@OfNat.ofNat Nat 2 (instOfNatNat 2)))
        (@OfNat.ofNat Nat 0 (instOfNatNat 0)))
      (@id Nat (@OfNat.ofNat Nat 0 (instOfNatNat 0))) (@OfNat.ofNat Nat 0 (instOfNatNat 0)))
    (@OfNat.ofNat Nat 0 (instOfNatNat 0))
-/
#guard_msgs in
example (P : Nat → Prop) m :
  (let n := m * 2
   if n = 0 then id 0 else 0) = 0 := by
  trace_state
  fail_if_success simp (config := Lean.Meta.Simp.neutralConfig) -dsimp only [id]
  simp (config := Lean.Meta.Simp.neutralConfig) +dsimp only [id]
  sorry

  #version

The let looks very non-dependent – it binds a Nat, and the body of the let doesn’t care about the concrete value.

Still, as can be seen in the goal state above, while n is abstract in the condition of the ite, it has been unfolded in the Decidable instance.

This can have unwanted consequences: The let is considered a depenent let by simp, and (with -zeta), the body will not be simplified by simp, but only by dsimp.

Maybe uses of simp -zeta are rare; it did show up in the wf processing (issue #7408).

It would be desirable if elaboration (type class inference) would not unfold n if it doesn’t need to, if possible.

Versions

Lean 4.18.0-rc1

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start with the reproducer in the issue and inspect elaboration, especially type class inference for the Decidable instance. Compare the behavior with simp -zeta and the wf processing mentioned in issue #7408. Done means elaboration avoids unfolding the let-bound n when its concrete value is unnecessary, while the reproducer shows the intended simplification behavior.