Is this a bug?

Stream: lean4

[Dan Velleman]

Here's a definition in Lean.Meta.Tactic.Replace:

/--
Replace the type of `fvarId` at `mvarId` with `typeNew`.
Remark: this method assumes that `typeNew` is definitionally equal to the current type of `fvarId`.
-/
def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
  mvarId.withContext do
    let mvarDecl ← mvarId.getDecl
    if typeNew == mvarDecl.type then
      return mvarId
    else
      let lctxNew := (← getLCtx).modifyLocalDecl fvarId (·.setType typeNew)
      let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) mvarDecl.type mvarDecl.kind mvarDecl.userName
      mvarId.assign mvarNew
      return mvarNew.mvarId!

It looks like it's checking first to see if the replacement is really going to change anything, and if not it doesn't make the change. But isn't mvarDecl.type giving the type of mvarId? Shouldn't the check be comparing typeNew to the type of fvarId, not the type of mvarId?