fix: oversight in isReadOnlyOrSyntheticOpaque

src/Lean/Meta/Basic.lean

@@ -720,15 +720,18 @@ def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
 /--
-Return true if `mvarId.isReadOnly` return true or if `mvarId` is a synthetic opaque metavariable.
+Returns true if `mvarId.isReadOnly` returns true or if `mvarId` is a synthetic opaque metavariable.
 
 Recall `isDefEq` will not assign a value to `mvarId` if `mvarId.isReadOnlyOrSyntheticOpaque`.
 -/
 def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Bool := do
   let mvarDecl ← mvarId.getDecl
-  match mvarDecl.kind with
-  | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
-  | _ => return mvarDecl.depth != (← getMCtx).depth
+  if mvarDecl.depth != (← getMCtx).depth then
+    return true
+  else
+    match mvarDecl.kind with
+    | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
+    | _ => return false
 
 @[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do

tests/lean/syntheticOpaqueReadOnly.lean

@@ -0,0 +1,12 @@
+import Lean
+
+open Lean Meta
+
+-- In a new MCtx depth, metavariables should not be assignable by `isDefEq`.
+
+run_meta do
+  let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
+  withAssignableSyntheticOpaque do
+  withNewMCtxDepth do
+  let eq ← isDefEq m (.const ``Nat [])
+  Lean.logInfo m! "{eq}"

tests/lean/syntheticOpaqueReadOnly.lean.expected.out

@@ -0,0 +1 @@
+false