Rewrite fails to find instance correctly

[b-mehta]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Rewrite fails to identify an instance argument

Context

set_option autoImplicit true

section Mathlib.Init.ZeroOne

class One (α : Type) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

class MulOneClass (M : Type) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a

export MulOneClass (one_mul)

end Mathlib.Algebra.Group.Defs

section Mathlib.Algebra.Ring.Defs

class Distrib (R : Type) extends Mul R, Add R where
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

class RightDistribClass (R : Type) [Mul R] [Add R] : Prop where
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

instance Distrib.rightDistribClass (R : Type) [Distrib R] : RightDistribClass R :=
  ⟨Distrib.right_distrib⟩

theorem add_mul [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
    (a + b) * c = a * c + b * c :=
  RightDistribClass.right_distrib a b c

theorem add_one_mul [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
    (a + 1) * b = a * b + b := by
  rw [add_mul, one_mul]

class Semiring (R : Type) extends Distrib R, MulOneClass R

end Mathlib.Algebra.Ring.Defs

section Mathlib.Data.Nat.Basic

instance : Semiring Nat where
  add := Nat.add
  mul := Nat.mul
  one := Nat.succ Nat.zero
  one_mul := sorry
  right_distrib := sorry

end Mathlib.Data.Nat.Basic

#synth MulOneClass Nat       -- works
#synth RightDistribClass Nat -- works

example {a b : Nat} : (a + 1) * b = a * b + b :=
  have := add_one_mul a b -- works
  by rw [add_one_mul]     -- failed to synthesize instance: RightDistribClass ?m

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/regression.20in.20rw
Thanks to @semorrison for making it mathlib-free.

Steps to Reproduce

1. Code as above.

Expected behavior: The rewrite should succeed and close the goal.

Actual behavior: The rewrite fails, giving error "failed to synthesize instance RightDistribClass"

Versions

Lean (version 4.2.0-rc4, commit 819b5ea, Release)
MacOS

Additional Information

None

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[thorimur]

This is actually a more general issue with typeclass synthesis, and is not limited to rw (which essentially just does the following internally): prepend import Lean, then append the following to the above example:

open Lean Meta Elab Tactic in
elab "elab_term_then_synth " stx:term : tactic => withMainContext do
  let e ← Term.withSynthesize do Tactic.elabTerm stx none true
  logInfoAt stx m!"{e}"

example {a b : Nat} : (a + 1) * b = a * b + b :=
  have := add_one_mul a b -- works
  by elab_term_then_synth add_one_mul -- failed to synthesize instance: RightDistribClass ?m

Note that the above is just used to mimic rw; we can capture the issue more succinctly:

open Lean Meta Elab Tactic in
elab "elab_term " stx:term : tactic => withMainContext do
  let e ← Tactic.elabTerm stx none
  logInfoAt stx m!"{e}"

example {a b : Nat} : (a + 1) * b = a * b + b :=
  have := add_one_mul a b -- works
  by elab_term add_one_mul -- failed to synthesize instance: RightDistribClass ?m