Unification hints for vector notation

Stream: mathlib4

[Eric Wieser]

Is there any hope of something like this working?

import Mathlib.Data.Fin.VecNotation

unif_hint {α : Type*} {n : ℕ} (x : α) (xs : Fin n → α) (i : Fin n.succ) (y : α) where
  i ≟ 0
  y ≟ x
  ⊢
  y ≟ @Matrix.vecCons α _ x xs i

variables (A B C D : ℕ) (hf : ![A, B, C, D].Injective)

example : A ≠ B := by
  refine hf.ne ?_ -- fails

example : A ≠ B := by
  refine hf.ne (show 0 ≠ 1 from ?_)  -- works
  sorry

https://lean-lang.org/lean4/doc/unifhint.html is still blank, so I don't have much to go by