fix: fixes #1870

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]

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

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 }

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 𝒞 η,