with_reducible ignoring implicit arguments?

Stream: lean4

[Heather Macbeth]

In the following example I was surprised to see the last line work, when the variants before it fail. It seems that with_reducible stops explicit arguments from being unfolded but still unfolds implicit arguments. Is this a bug or is it intended behaviour?

def f1 (a b : Nat) := a * b ^ 2
def f2 (a b : Nat) := a * b ^ 2

def bar {g : Nat → Nat → Nat} : Nat → Nat → Nat := g
def foo (g : Nat → Nat → Nat) : Nat → Nat → Nat := g

-- these all fail
example : f1 = f2 := by with_reducible eq_refl
example : bar (g := f1) = bar (g := f2) := by with_reducible { delta bar; eq_refl }
example : bar (g := f1) = bar (g := f2) := by with_reducible { unfold bar; eq_refl }
example : foo (g := f1) = foo (g := f2) := by with_reducible eq_refl

-- this works, why?
example : bar (g := f1) = bar (g := f2) := by with_reducible eq_refl

[Joachim Breitner]

It looks like it’s intended:

  for i in postponedImplicit do
    /- Second pass: unify implicit arguments.
       In the second pass, we make sure we are unfolding at
       least non reducible definitions (default setting). -/
    let a₁   := args₁[i]!
    let a₂   := args₂[i]!
    let info := finfo.paramInfo[i]!
    if info.isInstImplicit then
      discard <| trySynthPending a₁
      discard <| trySynthPending a₂
    unless (← withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do
      return false

[Joachim Breitner]

This seems to go back to 2017: https://github.com/leanprover/lean4/commit/e59fd2927a91e4dbe00c825764632786b6388df2