From 0694731af8c259972a35720db1ad6bbb67ad5fbe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Nov 2022 05:42:20 -0800
Subject: [PATCH] fix: fixes #1870

---
 src/Lean/Meta/ExprDefEq.lean         |  6 ++++++
 tests/lean/1870.lean                 | 31 ++++++++++++++++++++++++++++
 tests/lean/1870.lean.expected.out    | 17 +++++++++++++++
 tests/lean/run/aStructPerfIssue.lean |  2 +-
 4 files changed, 55 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/1870.lean
 create mode 100644 tests/lean/1870.lean.expected.out

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index bb2380d2aa..edd3797dde 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1714,6 +1714,12 @@ private def getCachedResult (key : Expr × Expr) : MetaM LBool := do
   | none => return .undef
 
 private def cacheResult (key : Expr × Expr) (result : Bool) : MetaM Unit := do
+  /-
+  We must ensure that all assigned metavariables in the key are replaced by their current assingments.
+  Otherwise, the key is invalid after the assignment is "backtracked".
+  See issue #1870 for an example.
+  -/
+  let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
   modifyDefEqCache fun c => c.insert key result
 
 @[export lean_is_expr_def_eq]
diff --git a/tests/lean/1870.lean b/tests/lean/1870.lean
new file mode 100644
index 0000000000..1bfb5ebda5
--- /dev/null
+++ b/tests/lean/1870.lean
@@ -0,0 +1,31 @@
+class Zero.{u} (α : Type u) where
+  zero : α
+
+instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero α›.1
+
+instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
+  zero := 0
+
+class One (α : Type u) where
+  one : α
+
+instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
+  one := 1
+
+theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  refine' congrArg _ (congrArg _ _)
+  rfl
+
+example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl
+
+theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
new file mode 100644
index 0000000000..8f5b51d420
--- /dev/null
+++ b/tests/lean/1870.lean.expected.out
@@ -0,0 +1,17 @@
+1870.lean:21:2-21:5: error: tactic 'rfl' failed, equality lhs
+  Zero.ofOfNat0
+is not definitionally equal to rhs
+  { zero := 1 }
+⊢ Zero.ofOfNat0 = { zero := 1 }
+1870.lean:26:2-26:11: error: tactic 'apply' failed, failed to unify
+  ?a = ?a
+with
+  Zero.ofOfNat0 = { zero := 1 }
+case h.h
+⊢ Zero.ofOfNat0 = { zero := 1 }
+1870.lean:31:2-31:11: error: tactic 'apply' failed, failed to unify
+  ?a = ?a
+with
+  Zero.ofOfNat0 = { zero := 1 }
+case h.h
+⊢ Zero.ofOfNat0 = { zero := 1 }
diff --git a/tests/lean/run/aStructPerfIssue.lean b/tests/lean/run/aStructPerfIssue.lean
index 917bc3f0d7..2e85d2b8f1 100644
--- a/tests/lean/run/aStructPerfIssue.lean
+++ b/tests/lean/run/aStructPerfIssue.lean
@@ -313,7 +313,7 @@ def op (𝒞 : Precategory) : Precategory :=
 Precategory.intro 𝒞.hset (λ a b => 𝒞.μ b a) 𝒞.cod 𝒞.dom ∄
 
 postfix:max "ᵒᵖ" => op
-
+set_option maxHeartbeats 400000
 def dual (𝒞 : Precategory) (η : category 𝒞) : category 𝒞ᵒᵖ :=
 { defDec      := @defDec 𝒞 η,
   bottomLeft  := @bottomRight 𝒞 η,