fix: zetaDelta := false regression (#3459)

See new test. It is a mwe for an issue blocking Mathlib.

src/Lean/Elab/StructInst.lean

@@ -77,9 +77,27 @@ where
         go sources (sourcesNew.push source)
       else
         withFreshMacroScope do
-          let sourceNew ← `(src)
+          /-
+          Recall that local variables starting with `__` are treated as impl detail.
+          See `LocalContext.lean`.
+          Moreover, implementation detail let-vars are unfolded by `simp`
+          even when `zetaDelta := false`.
+          Motivation: the following failure when `zetaDelta := true`
+          ```
+          structure A where
+            a : Nat
+          structure B extends A where
+            b : Nat
+            w : a = b
+          def x : A where a := 37
+          @[simp] theorem x_a : x.a = 37 := rfl
+
+          def y : B := { x with b := 37, w := by simp }
+          ```
+          -/
+          let sourceNew ← `(__src)
           let r ← go sources (sourcesNew.push sourceNew)
-          `(let src := $source; $r)
+          `(let __src := $source; $r)
 
 structure ExplicitSourceInfo where
   stx        : Syntax

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -77,10 +77,10 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         reduceProjCont? (← unfoldDefinition? e)
 
 private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
-  if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! then
-    match (← getFVarLocalDecl e).value? with
-    | some v => return v
-    | none   => return e
+  let localDecl ← getFVarLocalDecl e
+  if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! || localDecl.isImplementationDetail then
+    let some v := localDecl.value? | return e
+    return v
   else
     return e
 

src/Lean/Meta/WHNF.lean

@@ -372,7 +372,9 @@ structure WhnfCoreConfig where
     match decl with
     | .cdecl .. => return e
     | .ldecl (value := v) .. =>
-      unless config.zetaDelta do return e
+      -- Let-declarations marked as implementation detail should always be unfolded
+      -- We initially added this feature for `simp`, and added it here for consistency.
+      unless config.zetaDelta || decl.isImplementationDetail do return e
       if (← getConfig).trackZetaDelta then
         modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
       whnfEasyCases v k config

tests/lean/run/zetaDeltaIssue.lean

@@ -0,0 +1,9 @@
+structure A where
+  a : Nat
+structure B extends A where
+  b : Nat
+  w : a = b
+def x : A where a := 37
+@[simp] theorem x_a : x.a = 37 := rfl
+
+def y : B := { x with b := 37, w := by simp }

tests/lean/structInstExtraEta.lean.expected.out

@@ -1,9 +1,9 @@
 def b : B :=
-let src := a;
-{ toA := src }
+let __src := a;
+{ toA := __src }
 def c : C :=
-let src := a;
-{ toB := { toA := src } }
+let __src := a;
+{ toB := { toA := __src } }
 def d : D :=
-let src := c;
-{ toB := src.toB }
+let __src := c;
+{ toB := __src.toB }