From 4a317ae3f8d743e54e7bfbc0f030d3e4529f6572 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 31 Mar 2024 19:36:35 -0700
Subject: [PATCH] fix: `.yesWithDeltaI` behavior (#3816)

It should not increase the transparency level from `reducible` to
`instances`. See new test.
---
 src/Lean/Meta/Basic.lean                      |  6 ++++++
 src/Lean/Meta/ExprDefEq.lean                  |  2 +-
 src/Lean/Meta/WHNF.lean                       |  7 ++++---
 .../run/simp_proj_transparency_issue.lean     | 19 +++++++++++++++++++
 4 files changed, 30 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/simp_proj_transparency_issue.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index eb016a815f18..de87b256c102 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1444,6 +1444,12 @@ def whnfD (e : Expr) : MetaM Expr :=
 def whnfI (e : Expr) : MetaM Expr :=
   withTransparency TransparencyMode.instances <| whnf e
 
+/-- `whnf` with at most instances transparency. -/
+def whnfAtMostI (e : Expr) : MetaM Expr := do
+  match (← getTransparency) with
+  | .all | .default => withTransparency TransparencyMode.instances <| whnf e
+  | _ => whnf e
+
 /--
   Mark declaration `declName` with the attribute `[inline]`.
   This method does not check whether the given declaration is a definition.
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index dde3b7d3b215..42ad9500ff40 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1872,7 +1872,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfI` is used to reduce the projection structure.
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
     We added this refinement to address a performance issue in code such as
     ```
     let val : Test := bar c1 key
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a5b08970b734..9b6b06f2c165 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -343,8 +343,8 @@ inductive ProjReductionKind where
   -/
   | yesWithDelta
   /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfI` is used at `s` during the process.
-  Recall that `whnfI` is like `whnf` but uses transparency `instances`.
+  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
+  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -625,7 +625,8 @@ where
         | .no => return e
         | .yes => k (← go c)
         | .yesWithDelta => k (← whnf c)
-        | .yesWithDeltaI => k (← whnfI c)
+        -- Remark: If the current transparency setting is `reducible`, we should not increase it to `instances`
+        | .yesWithDeltaI => k (← whnfAtMostI c)
       | _ => unreachable!
 
 /--
diff --git a/tests/lean/run/simp_proj_transparency_issue.lean b/tests/lean/run/simp_proj_transparency_issue.lean
new file mode 100644
index 000000000000..0cdbb4f66dc8
--- /dev/null
+++ b/tests/lean/run/simp_proj_transparency_issue.lean
@@ -0,0 +1,19 @@
+structure Foo where
+  x : Nat
+  y : Nat := 10
+
+@[instance]
+def f (x : Nat) : Foo :=
+  { x := x + x }
+
+@[instance]
+def g (x : Nat) : Foo :=
+  { x := x + x }
+
+opaque q : Nat → Prop
+
+example (h : q (f x).1) : q (g x).1 := by
+  -- Projections must not bump transparency setting from `reducible` to `instances`
+  -- Thus, the following tactic must fail
+  fail_if_success simp [h]
+  assumption