local instance reduction bug

Stream: lean4

[Michael Jam]

Good evening,
Below piece of code was working on: nightly-2022-02-11, and stopped working on nightly-2022-02-13 and still isn't working today on nightly-2022-02-19.

class Op where op : Nat
class Op_Law [Op] where op_law : Op.op = 0
class Op_Class extends Op, Op_Law
instance : Op_Class :=
  let this : Op := ⟨0⟩
  let this : Op_Law := ⟨rfl⟩
  ⟨⟩

Lean fails to reduce Op.op to 0 in Op_Law's constructor, but I think it should work, since Op's instance is provided just before.
Thanks again for debugging it...!