Why is there a metavariable in this error message

Stream: lean4

[Bolton Bailey]

Hello again folks, I am here to continue to make my working errors more and more minimal

def p {σ τ : Type} (f : σ → τ) : Prop := True

def injectivizing_id {σ τ : Type} {f : σ → τ} (hf : p f) : σ → τ := f

theorem injectivizing_id_comp {σ : Type} {f : σ → σ} (hf : p f) (x : σ) : injectivizing_id hf x = f x := by
  rw [injectivizing_id]

theorem injectivizing_id_comp_diff {σ τ : Type} {f : σ → τ} (hf : p f) (x : σ) : injectivizing_id hf x = f x := by
  apply injectivizing_id_comp (f := f) hf x

The problem here is that the first theorem is not general enough to prove the second, since the first assumes the input and output of f are the same. But I don't get why it produces the following error

tactic 'apply' failed, failed to unify
  injectivizing_id hf x = ?m.180 x
with
  injectivizing_id hf x = f x

It seems to me that the provision of the (f := f) implicit argument should make it so that the metavariable on the RHS is known to be f. What I would like to see is an error message more like what refine or exact give in the same situation:

application type mismatch
  @injectivizing_id_comp σ f
argument
  f
has type
  σ → τ : Type
but is expected to have type
  σ → σ : Type

Frankly, I thought using apply with a type that wasn't a function was equivalent to exact. Is there a good reason why apply gives a different error message here?

[Floris van Doorn]

The reason has probably to do with the elaboration strategy: apply elaborates the term without knowing the expected type (because Lean cannot know yet what the expected type is), while exact and refine know that the term has to match the target, so elaborate using that information. This probably causes the elaboration to get stuck at a different point, and therefore give you a different error message.

I do hope that the apply error message can be improved though, it is indeed not pinpointing the right problem.