understanding simp

Stream: general

[Johan Commelin]

I'm baffled. I added

@[simp] lemma with_zero.coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl

to algebra/group.lean and suddenly there is breakage in algebra/ordered_ring.lean because simp is applying that lemma in the context of with_top α. What's going on?

[Johan Commelin]

I thought that this simp-lemma wouldn't apply because of the ((1 : α) : with_zero α) on the right-hand-side.

[Johan Commelin]

Is this a bad simp-lemma, because the with_zero somehow gets hidden inside a has_coe, and then with_zero and with_top are both defined as option, so they turn out to be defeq, and hence the simp-lemma applies?