No function coercion on apply?

Stream: lean4

[Mac]

Why does the apply tactic not force its term into a function (using CoeFun)? For example:

class ExFalso :=
  toFun : (p : Prop) -> False -> p

namespace ExFalso
def funType (K : ExFalso) := (p : Prop) -> False -> p
instance : CoeFun ExFalso funType := {coe := fun K => K.toFun}
end ExFalso

-- Works as expected
def trueExFalso [K : ExFalso] := K True

theorem trueExFalso' [K : ExFalso] : False -> True
:= by
  -- Fails unexpectedly
  apply K
  /-
  tactic 'apply' failed, failed to unify
    ExFalso
  with
    False → True
  K : ExFalso
  ⊢ False → True
  -/

[Mario Carneiro]

apply already has a pretty hard job matching the goal to the input up to some extra _'s and definitional equality. Adding coercions to the mix would make it very underdetermined

[Mac]

Mario Carneiro said:

apply already has a pretty hard job matching the goal to the input up to some extra _'s and definitional equality. Adding coercions to the mix would make it very underdetermined

This doesn't seem like it would be that complicated, as it simply has to apply CoeFun.coe to its argument. Furthermore, without this coercion, apply is essentially the same as refine for non-functions, which makes no sense to me. I can not think of a time when I would expect apply not to treat its argument like a function.