“implicit lambda” works with `exact`, but not `apply`

I find this surprising:

example : {a : Nat} → a+1 = a.succ := rfl -- works
example : {a : Nat} → a+1 = a.succ := by exact rfl -- works
example : {a : Nat} → a+1 = a.succ := by apply rfl -- does not work

As a user I expect to apply work when exact works.

By using a wrong term we can see a bit more what’s happening:

example : {a : Nat} → a+1 = a.succ := by exact Iff.rfl

type mismatch
  Iff.rfl
has type
  ?m.960 ↔ ?m.960 : Prop
but is expected to have type
  a✝ + 1 = a✝.succ : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : Nat
you can disable implicit lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

So exact somehow triggers “implicit lambda feature” but apply doesn’t. Should it?

Versions

4.12.0-nightly-2024-09-16

Additional Information

This causes unexpected(?) regressions(?) when using @[refl] rather than extending the rfl macro, #5359.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the three examples from the issue on Lean 4 version 4.12.0-nightly-2024-09-16, comparing exact and apply with implicit lambdas enabled and disabled. Investigate the elaboration paths for these tactics and the interaction with @[refl] noted in #5359. Done means the intended behavior is decided and the examples either agree or the discrepancy is documented and covered by a regression test.