From 53146db6207ba41eccd122a1388ec7b84f665fe2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 22 Feb 2024 11:10:02 -0800
Subject: [PATCH] fix: `zetaDelta := false` regression (#3459)

See new test. It is a mwe for an issue blocking Mathlib.
---
 src/Lean/Elab/StructInst.lean                 | 22 +++++++++++++++++--
 src/Lean/Meta/Tactic/Simp/Main.lean           |  8 +++----
 src/Lean/Meta/WHNF.lean                       |  4 +++-
 tests/lean/run/zetaDeltaIssue.lean            |  9 ++++++++
 .../lean/structInstExtraEta.lean.expected.out | 12 +++++-----
 5 files changed, 42 insertions(+), 13 deletions(-)
 create mode 100644 tests/lean/run/zetaDeltaIssue.lean

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index b551d5cce4..ceb379a8c1 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 45a66b8c5c..a71442bb9d 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/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
 
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a08eb7c0a4..a8704f54ba 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/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
diff --git a/tests/lean/run/zetaDeltaIssue.lean b/tests/lean/run/zetaDeltaIssue.lean
new file mode 100644
index 0000000000..565c9a33dc
--- /dev/null
+++ b/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 }
diff --git a/tests/lean/structInstExtraEta.lean.expected.out b/tests/lean/structInstExtraEta.lean.expected.out
index 9e898fc193..91c2ef1ab7 100644
--- a/tests/lean/structInstExtraEta.lean.expected.out
+++ b/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 }