From 28cf146d00f81588854dcb75f901af12b6d5a313 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 13 Nov 2024 08:22:31 -0800
Subject: [PATCH] fix: make sure monad lift coercion elaborator has no side
 effects (#6024)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a bug where the monad lift coercion elaborator would
partially unify expressions even if they were not monads. This could be
taken advantage of to propagate information that could help elaboration
make progress, for example the first `change` worked because the monad
lift coercion elaborator was unifying `@Eq _ _` with `@Eq (Nat × Nat)
p`:
```lean
example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked
```
As such, this is a breaking change; you may need to adjust expressions
to include additional implicit arguments.
---
 src/Init/Data/Fin/Lemmas.lean                 |  2 +-
 src/Lean/Meta/Coe.lean                        |  6 +++--
 .../1018unknowMVarIssue.lean.expected.out     |  8 +++----
 tests/lean/1081.lean.expected.out             |  4 ++--
 tests/lean/1433.lean.expected.out             |  2 +-
 tests/lean/755.lean                           |  2 ++
 tests/lean/755.lean.expected.out              | 24 +++++++++----------
 tests/lean/calcErrors.lean.expected.out       |  2 +-
 tests/lean/coeM.lean                          | 17 +++++++++++++
 tests/lean/etaStructIssue.lean.expected.out   |  2 +-
 tests/lean/isDefEqOffsetBug.lean.expected.out |  2 +-
 .../mulcommErrorMessage.lean.expected.out     |  8 +------
 .../phashmap_inst_coherence.lean.expected.out |  2 +-
 tests/lean/run/1017.lean                      |  2 +-
 tests/lean/run/4405.lean                      |  8 +++----
 tests/lean/run/4413.lean                      |  6 +++--
 tests/lean/run/PPTopDownAnalyze.lean          |  2 ++
 tests/lean/run/scopedLocalReducibility.lean   |  9 +++----
 tests/lean/run/sealCommand.lean               |  6 +++--
 tests/lean/run/wfirred.lean                   | 14 ++++++-----
 tests/pkg/builtin_attr/UserAttr/Tst.lean      |  3 ++-
 21 files changed, 78 insertions(+), 53 deletions(-)

diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 06040969e1..03521a8900 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -642,7 +642,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
   ext
   simp
 
-@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (subNat 1 i h).succ = i := by
+@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by
   ext
   simp
   omega
diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean
index 2d51e2d60a..5527ff1cf2 100644
--- a/src/Lean/Meta/Coe.lean
+++ b/src/Lean/Meta/Coe.lean
@@ -157,9 +157,11 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   let eType ← instantiateMVars (← inferType e)
   let some (n, β) ← isTypeApp? expectedType | return none
   let some (m, α) ← isTypeApp? eType | return none
+  -- Need to save and restore the state in case `m` and `n` are defeq but not monads to prevent this procedure from having side effects.
+  let saved ← saveState
   if (← isDefEq m n) then
-    let some monadInst ← isMonad? n | return none
-    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => return none
+    let some monadInst ← isMonad? n | restoreState saved; return none
+    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => restoreState saved; return none
   else if autoLift.get (← getOptions) then
     try
       -- Construct lift from `m` to `n`
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 885000ad3b..a7585de9af 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -56,8 +56,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.632 -> _uniq.312
-          • FVarAlias α: _uniq.631 -> _uniq.310
+          • FVarAlias a: _uniq.585 -> _uniq.312
+          • FVarAlias α: _uniq.584 -> _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⟩
@@ -71,8 +71,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.663 -> _uniq.312
-          • FVarAlias n: _uniq.662 -> _uniq.310
+          • FVarAlias a: _uniq.616 -> _uniq.312
+          • FVarAlias n: _uniq.615 -> _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/1081.lean.expected.out b/tests/lean/1081.lean.expected.out
index da51d3223c..f91fb5ca47 100644
--- a/tests/lean/1081.lean.expected.out
+++ b/tests/lean/1081.lean.expected.out
@@ -1,12 +1,12 @@
 1081.lean:7:2-7:5: error: type mismatch
   rfl
 has type
-  f 0 y = f 0 y : Prop
+  ?m = ?m : Prop
 but is expected to have type
   f 0 y = y : Prop
 1081.lean:23:4-23:7: error: type mismatch
   rfl
 has type
-  insert a ⟨0, ⋯⟩ v = insert a ⟨0, ⋯⟩ v : Prop
+  ?m = ?m : Prop
 but is expected to have type
   insert a ⟨0, ⋯⟩ v = cons a v : Prop
diff --git a/tests/lean/1433.lean.expected.out b/tests/lean/1433.lean.expected.out
index 433c07cc71..27fd5f033d 100644
--- a/tests/lean/1433.lean.expected.out
+++ b/tests/lean/1433.lean.expected.out
@@ -1,6 +1,6 @@
 1433.lean:11:49-11:52: error: type mismatch
   rfl
 has type
-  dividend % divisor = dividend % divisor : Prop
+  ?m = ?m : Prop
 but is expected to have type
   dividend % divisor = wrongRem : Prop
diff --git a/tests/lean/755.lean b/tests/lean/755.lean
index e39bcf6ffe..9ae005d7c4 100644
--- a/tests/lean/755.lean
+++ b/tests/lean/755.lean
@@ -1,3 +1,5 @@
+set_option pp.mvars false
+
 def Additive (α : Type) := α
 
 instance [OfNat α 1] : OfNat (Additive α) (nat_lit 0) := ⟨(1 : α)⟩
diff --git a/tests/lean/755.lean.expected.out b/tests/lean/755.lean.expected.out
index e36765b870..3239108018 100644
--- a/tests/lean/755.lean.expected.out
+++ b/tests/lean/755.lean.expected.out
@@ -1,24 +1,24 @@
-755.lean:5:44-5:47: error: type mismatch
+755.lean:7:44-7:47: error: type mismatch
   rfl
 has type
-  0 = @OfNat.ofNat Nat 0 (instOfNatNat 0) : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
-  0 = @OfNat.ofNat (Additive Nat) 0 instOfNatAdditiveOfOfNatNat : Prop
-755.lean:24:2-24:5: error: type mismatch
+  0 = 0 : Prop
+755.lean:26:2-26:5: error: type mismatch
   rfl
 has type
-  2 * 3 = @HMul.hMul Nat Nat Nat instHMul 2 3 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
-  2 * 3 = @HMul.hMul (Foo Nat) (Foo Nat) (Foo Nat) instHMulFooOfHAdd 2 3 : Prop
-755.lean:27:2-27:5: error: type mismatch
+  2 * 3 = 2 * 3 : Prop
+755.lean:29:2-29:5: error: type mismatch
   rfl
 has type
-  2 + 3 = @HAdd.hAdd Nat Nat Nat instHAdd 2 3 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
-  2 + 3 = @HAdd.hAdd (Foo Nat) (Foo Nat) (Foo Nat) instHAddFoo 2 3 : Prop
-755.lean:30:2-30:5: error: type mismatch
+  2 + 3 = 2 + 3 : Prop
+755.lean:32:2-32:5: error: type mismatch
   rfl
 has type
-  2 - 3 = @HSub.hSub Nat Nat Nat instHSub 2 3 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
-  2 - 3 = @HSub.hSub (Foo Nat) (Foo Nat) (Foo Nat) instHSubFooOfHAdd 2 3 : Prop
+  2 - 3 = 2 - 3 : Prop
diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out
index 50195236c4..cdd831923c 100644
--- a/tests/lean/calcErrors.lean.expected.out
+++ b/tests/lean/calcErrors.lean.expected.out
@@ -1,7 +1,7 @@
 calcErrors.lean:7:30-7:33: error: type mismatch
   rfl
 has type
-  b + b = b + b : Prop
+  ?m = ?m : Prop
 but is expected to have type
   b + b = 0 + c + b : Prop
 calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand side is
diff --git a/tests/lean/coeM.lean b/tests/lean/coeM.lean
index b36b52d008..b16400e296 100644
--- a/tests/lean/coeM.lean
+++ b/tests/lean/coeM.lean
@@ -4,6 +4,8 @@
 The functions inserted for the coercions are supposed to be inlined immediately during elaboration.
 -/
 
+set_option pp.mvars false
+
 variable (p : Nat → Prop) (m : IO (Subtype p))
 
 /-!
@@ -15,3 +17,18 @@ variable (p : Nat → Prop) (m : IO (Subtype p))
 `Lean.Internal.coeM`
 -/
 #check (m : IO Nat)
+
+/-!
+Making sure the monad lift coercion elaborator does not have side effects.
+
+It used to be responsible for hinting that the LHSs of equalities were defeq, like in the following example.
+It was checking that `Eq (some true)` and `Eq _` were defeq monads. The defeq check caused `_` to be solved as `some true`.
+-/
+/--
+error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
+  ?_
+-/
+#guard_msgs in
+example : some true = (some true).map id := by
+  refine show _ = .some true from ?_
+  rfl
diff --git a/tests/lean/etaStructIssue.lean.expected.out b/tests/lean/etaStructIssue.lean.expected.out
index 111dd2af8d..b812890c04 100644
--- a/tests/lean/etaStructIssue.lean.expected.out
+++ b/tests/lean/etaStructIssue.lean.expected.out
@@ -1,6 +1,6 @@
 etaStructIssue.lean:20:2-20:5: error: type mismatch
   rfl
 has type
-  mkNat e x₁ = mkNat e x₁ : Prop
+  ?m = ?m : Prop
 but is expected to have type
   mkNat e x₁ = mkNat e.mk x₂ : Prop
diff --git a/tests/lean/isDefEqOffsetBug.lean.expected.out b/tests/lean/isDefEqOffsetBug.lean.expected.out
index 14aea3e053..4d89f3ab96 100644
--- a/tests/lean/isDefEqOffsetBug.lean.expected.out
+++ b/tests/lean/isDefEqOffsetBug.lean.expected.out
@@ -1,6 +1,6 @@
 isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
   rfl
 has type
-  0 + 0 = 0 + 0 : Prop
+  ?m = ?m : Prop
 but is expected to have type
   0 + 0 = 0 : Prop
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index e2e6b0d859..35ba3fa7d2 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -8,16 +8,10 @@ the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
-mulcommErrorMessage.lean:11:22-11:25: error: type mismatch
-  rfl
-has type
-  true = true : Prop
-but is expected to have type
-  true = false : Prop
 mulcommErrorMessage.lean:12:22-12:25: error: type mismatch
   rfl
 has type
-  false = false : Prop
+  ?m = ?m : Prop
 but is expected to have type
   false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index a6bd7a91b6..30fd0369a0 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -5,4 +5,4 @@ argument
 has type
   @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type
 but is expected to have type
-  @PersistentHashMap Nat Nat instBEqOfDecidableEq natDiffHash : Type
+  @PersistentHashMap Nat Nat ?m natDiffHash : Type
diff --git a/tests/lean/run/1017.lean b/tests/lean/run/1017.lean
index 9bb289d4ee..408e5d4530 100644
--- a/tests/lean/run/1017.lean
+++ b/tests/lean/run/1017.lean
@@ -25,7 +25,7 @@ def isFinite : Prop :=
 
 instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where
   rel := λ s1 s2 => hasNext s2.val s1.val
-  wf := ⟨λ ⟨s,h⟩ => ⟨⟨s,h⟩, by
+  wf := ⟨λ ⟨s,h⟩ => ⟨Subtype.mk s h, by
     simp only [Subtype.forall]
     cases h; case intro w h =>
     induction w generalizing s
diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index 096577e9b6..215056b089 100644
--- a/tests/lean/run/4405.lean
+++ b/tests/lean/run/4405.lean
@@ -4,13 +4,13 @@ set_option pp.mvars false
 
 /--
 error: application type mismatch
-  ⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
+  ⟨Nat.lt_irrefl (?_ n), Fin.is_lt ?_⟩
 argument
-  Fin.is_lt (?_ n)
+  Fin.is_lt ?_
 has type
-  ↑(?_ n) < ?_ n : Prop
+  ↑?_ < ?_ : Prop
 but is expected to have type
-  ↑(?_ n) < ↑(?_ n) : Prop
+  ?_ n < ?_ n : Prop
 -/
 #guard_msgs in
 def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
diff --git a/tests/lean/run/4413.lean b/tests/lean/run/4413.lean
index d101360b2c..8690181126 100644
--- a/tests/lean/run/4413.lean
+++ b/tests/lean/run/4413.lean
@@ -1,3 +1,5 @@
+set_option pp.mvars false
+
 structure Note where
   pitch : UInt64
   start : Nat
@@ -16,13 +18,13 @@ theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
 error: type mismatch
   rfl
 has type
-  n = n : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   n = n - 1 : Prop
 -/
 #guard_msgs in
 set_option maxRecDepth 100 in
-set_option maxHeartbeats 100 in
+set_option maxHeartbeats 200 in
 example (n : UInt64) : n = n - 1 :=
   rfl
 
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 1a93555361..bf41f81590 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -328,9 +328,11 @@ set_option pp.analyze.explicitHoles false in
 #testDelab ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ _) → f₁ = f₂
   expecting ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂
 
+/- TODO(kmill) 2024-11-10 fix the following test
 set_option pp.analyze.trustSubtypeMk true in
 #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
   expecting fun n val property => (Subtype.val (p := fun x => x.length = n) (⟨val, property⟩ : { x : List Nat // x.length = n })).length = n
+-/
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
diff --git a/tests/lean/run/scopedLocalReducibility.lean b/tests/lean/run/scopedLocalReducibility.lean
index 3475b80b56..b6ca268ad7 100644
--- a/tests/lean/run/scopedLocalReducibility.lean
+++ b/tests/lean/run/scopedLocalReducibility.lean
@@ -1,10 +1,11 @@
 @[irreducible] def f (x : Nat) := x + 1
 set_option allowUnsafeReducibility true
+set_option pp.mvars false
 /--
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -22,7 +23,7 @@ end
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -38,7 +39,7 @@ end Boo
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -54,7 +55,7 @@ example : f x = x + 1 :=
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
diff --git a/tests/lean/run/sealCommand.lean b/tests/lean/run/sealCommand.lean
index e02babfe52..03172a197a 100644
--- a/tests/lean/run/sealCommand.lean
+++ b/tests/lean/run/sealCommand.lean
@@ -1,3 +1,5 @@
+set_option pp.mvars false
+
 def f (x : Nat) := x + 1
 
 example : f x = x + 1 := rfl
@@ -6,7 +8,7 @@ example : f x = x + 1 := rfl
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
@@ -22,7 +24,7 @@ seal f
 error: type mismatch
   rfl
 has type
-  f x = f x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   f x = x + 1 : Prop
 -/
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
index ef3bffc967..ea3052b584 100644
--- a/tests/lean/run/wfirred.lean
+++ b/tests/lean/run/wfirred.lean
@@ -2,6 +2,8 @@
 Tests that definitions by well-founded recursion are irreducible.
 -/
 
+set_option pp.mvars false
+
 def foo : Nat → Nat
   | 0 => 0
   | n+1 => foo n
@@ -11,7 +13,7 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  foo 0 = foo 0 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   foo 0 = 0 : Prop
 -/
@@ -22,7 +24,7 @@ example : foo 0 = 0 := rfl
 error: type mismatch
   rfl
 has type
-  foo (n + 1) = foo (n + 1) : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   foo (n + 1) = foo n : Prop
 -/
@@ -70,7 +72,7 @@ end Unsealed
 error: type mismatch
   rfl
 has type
-  foo 0 = foo 0 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   foo 0 = 0 : Prop
 -/
@@ -89,7 +91,7 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  foo = foo : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   foo = bar : Prop
 -/
@@ -114,7 +116,7 @@ seal baz in
 error: type mismatch
   rfl
 has type
-  baz 0 = baz 0 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   baz 0 = 0 : Prop
 -/
@@ -136,7 +138,7 @@ seal quux in
 error: type mismatch
   rfl
 has type
-  quux 0 = quux 0 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   quux 0 = 0 : Prop
 -/
diff --git a/tests/pkg/builtin_attr/UserAttr/Tst.lean b/tests/pkg/builtin_attr/UserAttr/Tst.lean
index 721e43b111..f026980a11 100644
--- a/tests/pkg/builtin_attr/UserAttr/Tst.lean
+++ b/tests/pkg/builtin_attr/UserAttr/Tst.lean
@@ -5,11 +5,12 @@ import UserAttr.BlaAttr
 
 attribute [local irreducible] myFun
 
+set_option pp.mvars false
 /--
 error: type mismatch
   rfl
 has type
-  myFun x = myFun x : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   myFun x = x + 1 : Prop
 -/