fix: bug at isDefEqOffset

fixes #326

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

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