inferring coe as a function

Stream: new members

[Yakov Pechersky]

Why is coe not inferred as a function in the second rw attempt below?

import data.fin

-- works
example {n : ℕ} (x : fin (n + 1)) (y : fin n) :
  ((x.succ_above y) : ℕ) = (ite (y.cast_succ < x) (y : ℕ) ((y : ℕ) + 1)) :=
begin
  unfold fin.succ_above,
  rw apply_ite (coe),
  simp
end

-- rw fails
example {n : ℕ} (x : fin (n + 1)) (y : fin n) :
  ((x.succ_above y) : ℕ) = (ite (y.cast_succ < x) (y : ℕ) ((y : ℕ) + 1)) :=
begin
  unfold fin.succ_above,
  rw apply_ite _ (y.cast_succ < x) y.cast_succ y.succ,
  sorry
end

[Kenny Lau]

function unification is noncomputable