From f1245f9dc7ae58fef08468a3967505d841a896de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Mar 2021 17:22:22 -0800
Subject: [PATCH] fix: bug at `isDefEqOffset`

fixes #326
---
 src/Lean/Meta/Offset.lean |  5 +++--
 tests/lean/run/326.lean   | 14 ++++++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/326.lean

diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index 3c72d534e1..e6ca7863a3 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -21,7 +21,7 @@ private abbrev withInstantiatedMVars (e : Expr) (k : Expr → OptionT MetaM α)
 partial def evalNat : Expr → OptionT MetaM Nat
   | Expr.lit (Literal.natVal n) _ => return n
   | Expr.mdata _ e _              => evalNat e
-  | Expr.const `Nat.zero _ _      => return 0
+  | Expr.const `Nat.zero ..       => return 0
   | e@(Expr.app ..)               => visit e
   | e@(Expr.mvar ..)              => visit e
   | _                             => failure
@@ -137,7 +137,8 @@ private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
 def isDefEqOffset (s t : Expr) : MetaM LBool := do
   let ifNatExpr (x : MetaM LBool) : MetaM LBool := do
     let type ← inferType s
-    if (← Meta.isExprDefEqAux type (mkConst ``Nat)) then
+    -- Remark: we use `withNewMCtxDepth` to make sure we don't assing metavariables when performing the `isDefEq` test
+    if (← withNewMCtxDepth <| Meta.isExprDefEqAux type (mkConst ``Nat)) then
       x
     else
       return LBool.undef
diff --git a/tests/lean/run/326.lean b/tests/lean/run/326.lean
new file mode 100644
index 0000000000..f944f1d0f8
--- /dev/null
+++ b/tests/lean/run/326.lean
@@ -0,0 +1,14 @@
+abbrev Zero α := OfNat α (natLit! 0)
+
+class Monoid (α : Type u) [Zero α] extends Add α where
+  zero_add (a : α) : 0 + a = a
+  add_zero (a : α) : a + 0 = a
+
+attribute [simp] Monoid.zero_add Monoid.add_zero
+
+variable {α : Type u} [Zero α] [Monoid α]
+
+-- works
+example (a : α) : 0 + a = a := by simp
+
+example (a : α) : a + 0 = a := by simp