convert generates proof that is not accepted by the kernel

[gebner]

import tactic

example : 1 = 0 :=
begin
  convert of_mul_one,
  apply_instance,
  -- goals accomplished!
end

[robertylewis]

(To clarify for anyone who's reading this and worried, this is just a tactic bug. The proof is rejected by the type checker.)

[robertylewis]

This goes up the food chain:

import algebra.group.type_tags 

lemma test2 : (0 : ℕ) = (0 : additive ℕ) := 
by tactic.reflexivity 

I don't have a mathlib-free MWE yet. Not sure what it is about additive that allows this.

[gebner]

Reported upstream as leanprover-community/lean#644