Question on `apply` vs. `exact`

Stream: general

[Michael Stoll]

Consider the following.

import data.zmod.basic
open zmod

example (a : ℕ) : ((a : zmod 8) : zmod 4) = a :=
begin
  apply cast_nat_cast (by norm_num : 4 ∣ 8) a,
  -- leaves `char_p (zmod 4) 4`
  apply_instance, -- why is this not found automatically?
end

example (a : ℕ) : ((a : zmod 8) : zmod 4) = a :=
begin
  exact cast_nat_cast (by norm_num : 4 ∣ 8) a, -- works
end

I'm wondering why apply does not clear the goal by itself. Can somebody enlighten me?

[Ruben Van de Velde]

As I understand it - the flexibility of apply means it first has to evaluate (elaborate?) the expression to some point and then find a way to match it to the current goal, and that by the time it's figured out what the typeclass goals are, exactly, it's too late to deal with them (or the implementation doesn't bother anymore). refine and exact know that the expression needs to match exactly, so they can use the current goal to figure things out earlier.

(I'm assuming plenty of people here could explain better, but I'm hoping this is somewhere near the truth, at least.)

[Kevin Buzzard]

If anyone ever says "oh why doesn't apply work here" I just say "oh that'll be the apply bug".

[Alex J. Best]

rw has exactly the same behaviour here, leaving the typeclass as a side goal in the same way it does any other arguments that can't be inferred from what it is rewriting. I think having versions of these tactics that were a bit smarter in these instances would be useful, but there may be some trade-off with efficiency if they try to do this all the time to consider.