apply tactic produces incorrect proof

[gebner]

def additive (α : Type*) := α

instance {α} [has_one α] : has_zero (additive α) := ⟨(1 : α)⟩

example : (0 : ℕ) = (0 : additive ℕ) :=
by apply eq.refl

[gebner]

This is getting more and more interesting:

#eval tactic.is_def_eq `(0 : ℕ) `(0 : additive ℕ) -- succeeds!?!