'rewrite' failed but it should work

Stream: lean4

[Tomas Skrivan]

I have encountered a problem with rewrite where I believe a certain class is not properly instantiated during unification.

mwe:

class Foo (α : Type) where
  decEq : DecidableEq α

instance instDecidableEq {α} [Foo α] : DecidableEq α := Foo.decEq
instance instFooNat : Foo Nat := ⟨by infer_instance⟩


def kron (i j : α) [DecidableEq α] : Nat := if (i=j) then 1 else 0
theorem kron_right_mul (α : Type) [foo : Foo α]  (i j : α) (x : Nat) : x * kron i j = kron i j * x := sorry


set_option trace.Meta.isDefEq true in
example {i j : Nat} : i * kron i j = kron i j * i :=
by
  rw[kron_right_mul]

The rewrite rw[kron_right_mul] fails with "tactic 'rewrite' failed, did not find instance of the pattern in the target expression" and tracing isDefEq reveals that the problematic step is to decide the following equality:

[Meta.isDefEq.step] instDecidableEqNat a b =?= instDecidableEq a b

Further inspection reveals that instDecidableEq is unfolded to Foo.decEq that is unfolded to ?foo.1. Why is it a metavariable? It should be instFooNat.1.
Nevertheless, ?foo gets assigned: [Meta.isDefEq.assign.final] ?foo := { decEq := Nat.decEq.match_1 } but the match still fails at the end for some reason.

The rewrite works if you specify the type α explicitly: rw[kron_right_mul Nat]

What is going on here?

[Leonardo de Moura]

Pushed a fix for this: https://github.com/leanprover/lean4/commit/fddc8b06ac97fa61d8137d25d15956b76be95323