From bb92b53bcf2999eb65d4a25fbbc4459dc081e08e Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 6 Sep 2024 12:04:13 -0700
Subject: [PATCH 1/6] fix: prevent `addPPExplicitToExposeDiff` from assigning
 metavariables
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Type mismatch errors have a nice feature where expressions are annotated with `pp.explicit` to expose differences via `isDefEq` checking. However, this procedure has side effects since `isDefEq` may assign metavariables. This PR wraps the procedure with `withNewMCtxDepth` to prevent such assignments.

Assignments can lead to confusing behavior. For example, in the following a higher-order unification fails, but the difference-finding procedure unifies metavariables in a naive way, producing a baffling error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
    f (g n) = n := hfg n

example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
  with_reducible refine test n2 ?_
  /-
  type mismatch
    test n2 ?m.648
  has type
    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
  but is expected to have type
    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
  -/
```
With the change, the reported type is now `?m.153 (?m.154 n2) = n2`.
---
 src/Lean/Meta/Check.lean          | 3 ++-
 tests/lean/1870.lean.expected.out | 6 +++---
 tests/lean/run/4405.lean          | 4 ++--
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index b1e78d375fce..fd2e5bfa3684 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -74,7 +74,8 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
   if (← getOptions).getBool `pp.all false || (← getOptions).getBool `pp.explicit false then
     return (a, b)
   else
-    visit (← instantiateMVars a) (← instantiateMVars b)
+    -- Use a new metacontext depth to prevent isDefEq from unifying any metavariables.
+    withNewMCtxDepth do visit (← instantiateMVars a) (← instantiateMVars b)
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index a6f2f8e7561c..b55e432900e8 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,7 +1,7 @@
-1870.lean:12:2-12:35: error: type mismatch
-  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
+1870.lean:21:2-21:35: error: type mismatch
+  congrArg ?_ (congrArg ?_ ?_)
 has type
-  OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
+  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
 1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index 65e4a429de5a..e3ace5cd4fe8 100644
--- a/tests/lean/run/4405.lean
+++ b/tests/lean/run/4405.lean
@@ -15,9 +15,9 @@ def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
 
 /--
 error: type mismatch
-  Fin.is_lt ?m.185
+  Fin.is_lt ?m.181
 has type
-  ↑?m.185 < ?m.184 : Prop
+  ↑?m.181 < ?m.180 : Prop
 but is expected to have type
   ?a < ?a : Prop
 ---

From d018246eb8f0ab2cf498f44c17d92dbe0e8de9a9 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 26 Oct 2024 16:53:26 -0700
Subject: [PATCH 2/6] new strategy: just avoid faking higher-order unification;
 also adds support for over-applied functions

---
 src/Lean/Meta/Check.lean                      | 71 +++++++++++--------
 .../1018unknowMVarIssue.lean.expected.out     |  8 +--
 tests/lean/1870.lean.expected.out             |  6 +-
 tests/lean/run/addPPExplicitToExposeDiff.lean | 50 +++++++++++++
 4 files changed, 99 insertions(+), 36 deletions(-)
 create mode 100644 tests/lean/run/addPPExplicitToExposeDiff.lean

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index fd2e5bfa3684..aa6c86734b5c 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -69,50 +69,63 @@ but is expected to have type
 ```
 Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
 error messages.
+
+This function has side effects. It will make sensible metavariable assignments to represent partial completion of `isDefEq`,
+since that can give better error messages.
 -/
 partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
   if (← getOptions).getBool `pp.all false || (← getOptions).getBool `pp.explicit false then
     return (a, b)
   else
-    -- Use a new metacontext depth to prevent isDefEq from unifying any metavariables.
-    withNewMCtxDepth do visit (← instantiateMVars a) (← instantiateMVars b)
+    visit (← instantiateMVars a) (← instantiateMVars b)
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
-      if !a.isApp || !b.isApp then
+      if !a.isApp || !b.isApp || a.getAppNumArgs != b.getAppNumArgs then
         return (a, b)
-      else if a.getAppNumArgs != b.getAppNumArgs then
+      else if a.getAppFn'.isMVar || b.getAppFn'.isMVar then
+        -- This is a failed higher-order unification. Do not proceed to `isDefEq`.
         return (a, b)
       else if !(← isDefEq a.getAppFn b.getAppFn) then
-        return (a, b)
+        let (fa, fb) ← visit a.getAppFn b.getAppFn
+        return (mkAppN fa a.getAppArgs, mkAppN fb b.getAppArgs)
       else
-        let fType ← inferType a.getAppFn
-        forallBoundedTelescope fType a.getAppNumArgs fun xs _ => do
-          let mut as := a.getAppArgs
-          let mut bs := b.getAppArgs
-          if let some (as', bs') ← hasExplicitDiff? xs as bs then
-            return (mkAppN a.getAppFn as', mkAppN b.getAppFn bs')
-          else
-            for i in [:as.size] do
-              unless (← isDefEq as[i]! bs[i]!) do
-                let (ai, bi) ← visit as[i]! bs[i]!
-                as := as.set! i ai
-                bs := bs.set! i bi
-            let a := mkAppN a.getAppFn as
-            let b := mkAppN b.getAppFn bs
-            return (a.setAppPPExplicit, b.setAppPPExplicit)
+        -- The function might be "overapplied", so we can't use `forallBoundedTelescope`.
+        -- That is to say, the arity might depend on the values of the arguments.
+        -- We look for the first explicit argument that is different.
+        -- Otherwise we look for the first implicit argument.
+        let mut as := a.getAppArgs
+        let mut bs := b.getAppArgs
+        let mut aFnType ← inferType a.getAppFn
+        let mut bFnType ← inferType b.getAppFn
+        let mut firstDiff? := none
+        for i in [0:as.size] do
+          unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType
+          unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType
+          -- These pattern matches are expected to succeed:
+          let .forallE _ _ abody abi := aFnType | return (a, b)
+          let .forallE _ _ bbody bbi := aFnType | return (a, b)
+          aFnType := abody.instantiate1 as[i]!
+          bFnType := bbody.instantiate1 bs[i]!
+          let explicit := abi.isExplicit && bbi.isExplicit
+          unless (← isDefEq as[i]! bs[i]!) do
+            if explicit then
+              let (ai, bi) ← visit as[i]! bs[i]!
+              let a := mkAppN a.getAppFn (as.set! i ai)
+              let b := mkAppN b.getAppFn (bs.set! i bi)
+              return (a, b)
+            else
+              firstDiff? := firstDiff? <|> some i
+        if let some i := firstDiff? then
+          let (ai, bi) ← visit as[i]! bs[i]!
+          as := as.set! i ai
+          bs := bs.set! i bi
+        let a := mkAppN a.getAppFn as
+        let b := mkAppN b.getAppFn bs
+        return (a.setPPExplicit true, b.setPPExplicit true)
     catch _ =>
       return (a, b)
 
-  hasExplicitDiff? (xs as bs : Array Expr) : MetaM (Option (Array Expr × Array Expr)) := do
-    for i in [:xs.size] do
-      let localDecl ← xs[i]!.fvarId!.getDecl
-      if localDecl.binderInfo.isExplicit then
-         unless (← isDefEq as[i]! bs[i]!) do
-           let (ai, bi) ← visit as[i]! bs[i]!
-           return some (as.set! i ai, bs.set! i bi)
-    return none
-
 /--
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 0a9115549f05..cd4c2d7398b2 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -58,8 +58,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.636 -> _uniq.312
-          • FVarAlias α: _uniq.635 -> _uniq.310
+          • FVarAlias a: _uniq.632 -> _uniq.312
+          • FVarAlias α: _uniq.631 -> _uniq.310
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -73,8 +73,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.667 -> _uniq.312
-          • FVarAlias n: _uniq.666 -> _uniq.310
+          • FVarAlias a: _uniq.663 -> _uniq.312
+          • FVarAlias n: _uniq.662 -> _uniq.310
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index b55e432900e8..a6f2f8e7561c 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,7 +1,7 @@
-1870.lean:21:2-21:35: error: type mismatch
-  congrArg ?_ (congrArg ?_ ?_)
+1870.lean:12:2-12:35: error: type mismatch
+  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
 has type
-  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
+  OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
 1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
diff --git a/tests/lean/run/addPPExplicitToExposeDiff.lean b/tests/lean/run/addPPExplicitToExposeDiff.lean
new file mode 100644
index 000000000000..e481dc1edb5f
--- /dev/null
+++ b/tests/lean/run/addPPExplicitToExposeDiff.lean
@@ -0,0 +1,50 @@
+/-!
+# Tests of `addPPExplicitToExposeDiff`
+-/
+set_option pp.mvars false
+
+/-!
+Does discretionary metavariable assignments so that we can see where the difference really was.
+In the following, `this` actually has type `?m = 3`.
+-/
+/--
+error: type mismatch
+  this
+has type
+  1 = 3 : Prop
+but is expected to have type
+  1 = 2 : Prop
+---
+error: unsolved goals
+⊢ 1 = 3
+-/
+#guard_msgs in example : 1 = 2 := by
+  change _ = 3
+
+
+/-!
+Error message shouldn't fake a higher order unification. This next one used to give
+```
+  type mismatch
+    test n2 ?m.648
+  has type
+    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
+  but is expected to have type
+    (fun x ↦ x * 2) (g2 n2) = n2 : Prop
+```
+-/
+
+theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :
+    f (g n) = n := hfg n
+
+/--
+error: type mismatch
+  test n2 ?_
+has type
+  ?_ (?_ n2) = n2 : Prop
+but is expected to have type
+  (fun x => x * 2) (g2 n2) = n2 : Prop
+-/
+#guard_msgs in
+example {g2 : Nat → Nat} (n2 : Nat) : (fun x => x * 2) (g2 n2) = n2 := by
+  with_reducible refine test n2 ?_

From 123c787bbb06fa02622e40dba7b93d9f13ad43d9 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 26 Oct 2024 17:00:12 -0700
Subject: [PATCH 3/6] pp.mvars for 4405

---
 tests/lean/run/4405.lean | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index e3ace5cd4fe8..096577e9b661 100644
--- a/tests/lean/run/4405.lean
+++ b/tests/lean/run/4405.lean
@@ -1,31 +1,33 @@
 import Lean.Elab.Command
 
+set_option pp.mvars false
+
 /--
 error: application type mismatch
-  ⟨Nat.lt_irrefl ↑(?m.58 n), Fin.is_lt (?m.58 n)⟩
+  ⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
 argument
-  Fin.is_lt (?m.58 n)
+  Fin.is_lt (?_ n)
 has type
-  ↑(?m.58 n) < ?m.57 n : Prop
+  ↑(?_ n) < ?_ n : Prop
 but is expected to have type
-  ↑(?m.58 n) < ↑(?m.58 n) : Prop
+  ↑(?_ n) < ↑(?_ n) : Prop
 -/
 #guard_msgs in
 def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
 
 /--
 error: type mismatch
-  Fin.is_lt ?m.181
+  Fin.is_lt ?_
 has type
-  ↑?m.181 < ?m.180 : Prop
+  ↑?_ < ?_ : Prop
 but is expected to have type
-  ?a < ?a : Prop
+  ?_ < ?_ : Prop
 ---
 error: unsolved goals
 case a
 ⊢ Nat
 
-this : ?a < ?a
+this : ?_ < ?_
 ⊢ True
 -/
 #guard_msgs in

From 2aec78c2592ba056c755c085773d3ddcdb254435 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 26 Oct 2024 17:33:25 -0700
Subject: [PATCH 4/6] be sure to instantiatemvars

---
 src/Lean/Meta/Check.lean                      | 95 +++++++++++--------
 tests/lean/run/addPPExplicitToExposeDiff.lean | 16 ++++
 2 files changed, 69 insertions(+), 42 deletions(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index aa6c86734b5c..a05afec8359f 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -81,48 +81,59 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
-      if !a.isApp || !b.isApp || a.getAppNumArgs != b.getAppNumArgs then
-        return (a, b)
-      else if a.getAppFn'.isMVar || b.getAppFn'.isMVar then
-        -- This is a failed higher-order unification. Do not proceed to `isDefEq`.
-        return (a, b)
-      else if !(← isDefEq a.getAppFn b.getAppFn) then
-        let (fa, fb) ← visit a.getAppFn b.getAppFn
-        return (mkAppN fa a.getAppArgs, mkAppN fb b.getAppArgs)
-      else
-        -- The function might be "overapplied", so we can't use `forallBoundedTelescope`.
-        -- That is to say, the arity might depend on the values of the arguments.
-        -- We look for the first explicit argument that is different.
-        -- Otherwise we look for the first implicit argument.
-        let mut as := a.getAppArgs
-        let mut bs := b.getAppArgs
-        let mut aFnType ← inferType a.getAppFn
-        let mut bFnType ← inferType b.getAppFn
-        let mut firstDiff? := none
-        for i in [0:as.size] do
-          unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType
-          unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType
-          -- These pattern matches are expected to succeed:
-          let .forallE _ _ abody abi := aFnType | return (a, b)
-          let .forallE _ _ bbody bbi := aFnType | return (a, b)
-          aFnType := abody.instantiate1 as[i]!
-          bFnType := bbody.instantiate1 bs[i]!
-          let explicit := abi.isExplicit && bbi.isExplicit
-          unless (← isDefEq as[i]! bs[i]!) do
-            if explicit then
-              let (ai, bi) ← visit as[i]! bs[i]!
-              let a := mkAppN a.getAppFn (as.set! i ai)
-              let b := mkAppN b.getAppFn (bs.set! i bi)
-              return (a, b)
-            else
-              firstDiff? := firstDiff? <|> some i
-        if let some i := firstDiff? then
-          let (ai, bi) ← visit as[i]! bs[i]!
-          as := as.set! i ai
-          bs := bs.set! i bi
-        let a := mkAppN a.getAppFn as
-        let b := mkAppN b.getAppFn bs
-        return (a.setPPExplicit true, b.setPPExplicit true)
+      match a, b with
+      | .mdata _ a', _ =>
+        let (a', b) ← visit a' b
+        return (a.updateMData! a', b)
+      | _, .mdata _ b' =>
+        let (a, b') ← visit a b'
+        return (a, b.updateMData! b')
+      | .app .., .app .. =>
+        if a.getAppNumArgs != b.getAppNumArgs then
+          return (a, b)
+        else if a.getAppFn'.isMVar || b.getAppFn'.isMVar then
+          -- This is a failed higher-order unification. Do not proceed to `isDefEq`.
+          return (a, b)
+        else if !(← isDefEq a.getAppFn b.getAppFn) then
+          let (fa, fb) ← visit a.getAppFn b.getAppFn
+          return (mkAppN fa a.getAppArgs, mkAppN fb b.getAppArgs)
+        else
+          -- The function might be "overapplied", so we can't use `forallBoundedTelescope`.
+          -- That is to say, the arity might depend on the values of the arguments.
+          -- We look for the first explicit argument that is different.
+          -- Otherwise we look for the first implicit argument.
+          -- We try `isDefEq` on all arguments to get discretionary mvar assigments.
+          let mut as := a.getAppArgs
+          let mut bs := b.getAppArgs
+          let mut aFnType ← inferType a.getAppFn
+          let mut bFnType ← inferType b.getAppFn
+          let mut firstExplicitDiff? := none
+          let mut firstImplicitDiff? := none
+          for i in [0:as.size] do
+            unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType
+            unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType
+            -- These pattern matches are expected to succeed:
+            let .forallE _ _ abody abi := aFnType | return (a, b)
+            let .forallE _ _ bbody bbi := bFnType | return (a, b)
+            aFnType := abody.instantiate1 as[i]!
+            bFnType := bbody.instantiate1 bs[i]!
+            let explicit := abi.isExplicit && bbi.isExplicit
+            unless (← isDefEq as[i]! bs[i]!) do
+              if explicit then
+                firstExplicitDiff? := firstExplicitDiff? <|> some i
+              else
+                firstImplicitDiff? := firstImplicitDiff? <|> some i
+          if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
+            let (ai, bi) ← visit (← instantiateMVars as[i]!) (← instantiateMVars bs[i]!)
+            as := as.set! i ai
+            bs := bs.set! i bi
+          let a := mkAppN a.getAppFn as
+          let b := mkAppN b.getAppFn bs
+          if firstExplicitDiff?.isSome then
+            return (a, b)
+          else
+            return (a.setPPExplicit true, b.setPPExplicit true)
+      | _, _ => return (a, b)
     catch _ =>
       return (a, b)
 
diff --git a/tests/lean/run/addPPExplicitToExposeDiff.lean b/tests/lean/run/addPPExplicitToExposeDiff.lean
index e481dc1edb5f..105da826132e 100644
--- a/tests/lean/run/addPPExplicitToExposeDiff.lean
+++ b/tests/lean/run/addPPExplicitToExposeDiff.lean
@@ -21,6 +21,22 @@ error: unsolved goals
 #guard_msgs in example : 1 = 2 := by
   change _ = 3
 
+/-!
+Does the assignments even for arguments beyond the difference.
+-/
+/--
+error: type mismatch
+  this
+has type
+  3 = 2 : Prop
+but is expected to have type
+  1 = 2 : Prop
+---
+error: unsolved goals
+⊢ 3 = 2
+-/
+#guard_msgs in example : 1 = 2 := by
+  change 3 = _
 
 /-!
 Error message shouldn't fake a higher order unification. This next one used to give

From 1c1df9bc57a71859f670125db3403a81f73b7212 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 26 Oct 2024 18:15:41 -0700
Subject: [PATCH 5/6] new strategy: do assignments, but without modifying state

---
 src/Lean/Meta/Check.lean                      | 14 ++---
 tests/lean/1870.lean.expected.out             |  4 +-
 tests/lean/run/addPPExplicitToExposeDiff.lean | 51 +++++++++----------
 3 files changed, 34 insertions(+), 35 deletions(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index a05afec8359f..ac6bcf286f85 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -69,15 +69,16 @@ but is expected to have type
 ```
 Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
 error messages.
-
-This function has side effects. It will make sensible metavariable assignments to represent partial completion of `isDefEq`,
-since that can give better error messages.
 -/
 partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
   if (← getOptions).getBool `pp.all false || (← getOptions).getBool `pp.explicit false then
     return (a, b)
   else
-    visit (← instantiateMVars a) (← instantiateMVars b)
+    -- We want to be able to assign metavariables to work out what why `isDefEq` failed,
+    -- but we don't want these assignments to leak out of the function.
+    -- Note: we shouldn't instantiate mvars in `visit` to prevent leakage.
+    withoutModifyingState do
+      visit (← instantiateMVars a) (← instantiateMVars b)
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
@@ -117,14 +118,13 @@ where
             let .forallE _ _ bbody bbi := bFnType | return (a, b)
             aFnType := abody.instantiate1 as[i]!
             bFnType := bbody.instantiate1 bs[i]!
-            let explicit := abi.isExplicit && bbi.isExplicit
             unless (← isDefEq as[i]! bs[i]!) do
-              if explicit then
+              if abi.isExplicit && bbi.isExplicit then
                 firstExplicitDiff? := firstExplicitDiff? <|> some i
               else
                 firstImplicitDiff? := firstImplicitDiff? <|> some i
           if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
-            let (ai, bi) ← visit (← instantiateMVars as[i]!) (← instantiateMVars bs[i]!)
+            let (ai, bi) ← visit as[i]! bs[i]!
             as := as.set! i ai
             bs := bs.set! i bi
           let a := mkAppN a.getAppFn as
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index a6f2f8e7561c..91f72724ce12 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,7 +1,7 @@
 1870.lean:12:2-12:35: error: type mismatch
-  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
+  congrArg ?_ (congrArg ?_ ?_)
 has type
-  OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
+  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
 1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
diff --git a/tests/lean/run/addPPExplicitToExposeDiff.lean b/tests/lean/run/addPPExplicitToExposeDiff.lean
index 105da826132e..87237b977685 100644
--- a/tests/lean/run/addPPExplicitToExposeDiff.lean
+++ b/tests/lean/run/addPPExplicitToExposeDiff.lean
@@ -4,50 +4,32 @@
 set_option pp.mvars false
 
 /-!
-Does discretionary metavariable assignments so that we can see where the difference really was.
-In the following, `this` actually has type `?m = 3`.
+Basic example.
 -/
 /--
 error: type mismatch
-  this
+  rfl
 has type
-  1 = 3 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   1 = 2 : Prop
----
-error: unsolved goals
-⊢ 1 = 3
 -/
 #guard_msgs in example : 1 = 2 := by
-  change _ = 3
+  exact rfl
 
-/-!
-Does the assignments even for arguments beyond the difference.
--/
-/--
-error: type mismatch
-  this
-has type
-  3 = 2 : Prop
-but is expected to have type
-  1 = 2 : Prop
----
-error: unsolved goals
-⊢ 3 = 2
--/
-#guard_msgs in example : 1 = 2 := by
-  change 3 = _
 
 /-!
-Error message shouldn't fake a higher order unification. This next one used to give
+Error message shouldn't fake a higher-order unification. This next one used to give
 ```
   type mismatch
-    test n2 ?m.648
+    test n2 ?_
   has type
     (fun x ↦ x * 2) (g2 n2) = n2 : Prop
   but is expected to have type
     (fun x ↦ x * 2) (g2 n2) = n2 : Prop
 ```
+It now doesn't for the stronger reason that we don't let `addPPExplicitToExposeDiff` have side effects,
+but still it avoids doing higher-order unifications in its reasoning.
 -/
 
 theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :
@@ -64,3 +46,20 @@ but is expected to have type
 #guard_msgs in
 example {g2 : Nat → Nat} (n2 : Nat) : (fun x => x * 2) (g2 n2) = n2 := by
   with_reducible refine test n2 ?_
+
+
+/-!
+Exposes an implicit argument because the explicit arguments can be unified.
+-/
+def f {a : Nat} (b : Nat) : Prop := a + b = 0
+/--
+error: type mismatch
+  sorry
+has type
+  @f 0 ?_ : Prop
+but is expected to have type
+  @f 1 2 : Prop
+-/
+#guard_msgs in
+example : @f 1 2 := by
+  exact (sorry : @f 0 _)

From b7e66cfbdb4cdebdb0a1c328a0ddb038986c6833 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 26 Oct 2024 18:27:23 -0700
Subject: [PATCH 6/6] test

---
 tests/lean/run/addPPExplicitToExposeDiff.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/addPPExplicitToExposeDiff.lean b/tests/lean/run/addPPExplicitToExposeDiff.lean
index 87237b977685..8d740ffa8025 100644
--- a/tests/lean/run/addPPExplicitToExposeDiff.lean
+++ b/tests/lean/run/addPPExplicitToExposeDiff.lean
@@ -29,7 +29,7 @@ Error message shouldn't fake a higher-order unification. This next one used to g
     (fun x ↦ x * 2) (g2 n2) = n2 : Prop
 ```
 It now doesn't for the stronger reason that we don't let `addPPExplicitToExposeDiff` have side effects,
-but still it avoids doing higher-order unifications in its reasoning.
+but still it avoids doing incorrect higher-order unifications in its reasoning.
 -/
 
 theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :