norm_num on fields

Stream: general

[Kevin Kappelmann]

I get some interesting behaviour when using norm_num on fields. It discharges the goal, but returns an error message.

import tactic.norm_num
variables {α : Type*} [field α]

example : (1 : α) / 1 = 1 := -- type mismatch at application...
begin
  norm_num, -- all goals accomplished
end

error message:

type mismatch at application
  id (eq_true_intro (eq.refl (1 / 1)))
term
  eq_true_intro (eq.refl (1 / 1))
has type
  1 / 1 = 1 / 1 = true
but is expected to have type
  1 / 1 = 1 = true

If I change field to linear_ordered_field, the example works. Any idea what's going on?