chore: right => left

This is an auxiliary procedured used by `rw` and `apply` tactics. It
synthesizes pending type class instances.
The new test contains an example where it failed. The comment at
`synthAppInstances.step` explains why, and the fix.

src/Lean/Meta/Tactic/Apply.lean

@@ -29,18 +29,73 @@ private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType :
     return m!"{indentExpr eType}\nwith{indentExpr targetType}"
   throwTacticEx `apply mvarId m!"failed to unify{explanation}"
 
-def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
-    (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=
-  newMVars.size.forM fun i => do
-    if binderInfos[i]!.isInstImplicit then
-      let mvar := newMVars[i]!
+def synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo)
+    (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := do
+  let mut todo := #[]
+  -- Collect metavariables to synthesize
+  for mvar in mvarsNew, binderInfo in binderInfos do
+    if binderInfo.isInstImplicit then
       if synthAssignedInstances || !(← mvar.mvarId!.isAssigned) then
-        let mvarType ← inferType mvar
-        try
-          let mvarVal  ← synthInstance mvarType
-          unless (← isDefEq mvar mvarVal) do
+        todo := todo.push mvar
+  while !todo.isEmpty do
+    todo ← step todo
+where
+  /--
+  Try to synthesize instances for the metavariables `mvars`.
+  Returns metavariables that still need to be synthesized.
+  We can view the resulting array as the set of metavariables that we should try again.
+  This is needed when applying or rewriting with functions with complex instances.
+  For example, consider `rw [@map_smul]` where `map_smul` is
+  ```
+  map_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {φ : M → N}
+           {X : Type u_4} {Y : Type u_5}
+           [SMul M X] [SMul N Y] [FunLike F X Y] [MulActionSemiHomClass F φ X Y]
+           (f : F) (c : M) (x : X) : DFunLike.coe f (c • x) = φ c • DFunLike.coe f x
+  ```
+  and `MulActionSemiHomClass` is defined as
+  ```
+  class MulActionSemiHomClass (F : Type _)
+     {M N : outParam (Type _)} (φ : outParam (M → N))
+     (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
+  ```
+  The left-hand-side of the equation does not bind `N`. Thus, `SMul N Y` cannot
+  be synthesized until we synthesize `MulActionSemiHomClass F φ X Y`. Note that
+  `N` is an output parameter for `MulActionSemiHomClass`.
+  -/
+  step (mvars : Array Expr) : MetaM (Array Expr) := do
+    -- `ex?` stores the exception for this first synthesis failure in this step.
+    let mut ex? := none
+    -- `true` if we managed to synthesize an instance after we hit a failure.
+    -- That is, there is a chance we may succeed if we try again.
+    let mut progressAfterEx := false
+    -- Metavariables that we failed to synthesize.
+    let mut postponed := #[]
+    for mvar in mvars do
+      let mvarType ← inferType mvar
+      let mvarVal? ← try
+        let mvarVal ← synthInstance mvarType
+        unless postponed.isEmpty do
+          progressAfterEx := true
+        pure (some mvarVal)
+      catch ex =>
+        ex? := some ex
+        postponed := postponed.push mvar
+        pure none
+      if let some mvarVal := mvarVal? then
+        unless (← isDefEq mvar mvarVal) do
+          -- There is no point in trying again for this kind of failure
+          unless allowSynthFailures do
             throwTacticEx tacticName mvarId "failed to assign synthesized instance"
-        catch e => unless allowSynthFailures do throw e
+    if let some ex := ex? then
+      if progressAfterEx then
+        return postponed
+      else
+        -- There is no point in running `step` again. We should give up (`allowSynthFailures`),
+        -- or throw the first exception we found in this `step`.
+        if allowSynthFailures then return #[] else throw ex
+    else
+      -- Done. We successfully synthesized all metavariables.
+      return #[]
 
 def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
   let parentTag ← mvarId.getTag

tests/lean/run/synthInstsIssue.lean

@@ -0,0 +1,142 @@
+/-!
+This is a minimization of an issue widely seen in Mathlib after
+https://github.com/leanprover/lean4/pull/2793.
+We find that we need to either specify a named argument or use `..` in certain rewrites.
+-/
+
+section Mathlib.Init.ZeroOne
+
+set_option autoImplicit true
+
+class Zero.{u} (α : Type u) where
+  zero : α
+
+instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero α›.1
+
+end Mathlib.Init.ZeroOne
+
+section Mathlib.Algebra.Group.Defs
+
+universe u v w
+
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
+class SMul (M : Type u) (α : Type v) where
+  smul : M → α → α
+
+infixr:73 " • " => HSMul.hSMul
+
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
+end Mathlib.Algebra.Group.Defs
+
+section Mathlib.Data.FunLike.Basic
+
+class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
+  coe : F → ∀ a : α, β a
+
+abbrev FunLike F α β := DFunLike F α fun _ => β
+
+instance (priority := 100) hasCoeToFun {F α β} [_i : DFunLike F α β] :
+    CoeFun F (fun _ ↦ ∀ a : α, β a) where
+  coe := @DFunLike.coe _ _ β _
+
+end Mathlib.Data.FunLike.Basic
+
+section Mathlib.Algebra.Group.Hom.Defs
+
+variable {M N : Type _}
+variable {F : Type _}
+
+class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N] [FunLike F M N] :
+    Prop where
+  map_zero : ∀ f : F, f 0 = 0
+
+variable [Zero M] [Zero N] [FunLike F M N]
+
+theorem map_zero [ZeroHomClass F M N] (f : F) : f 0 = 0 :=
+  ZeroHomClass.map_zero f
+
+end Mathlib.Algebra.Group.Hom.Defs
+
+section Mathlib.GroupTheory.GroupAction.Defs
+
+variable {M A : Type _}
+
+class SMulZeroClass (M A : Type _) [Zero A] extends SMul M A where
+  smul_zero : ∀ a : M, a • (0 : A) = 0
+
+@[simp]
+theorem smul_zero [Zero A] [SMulZeroClass M A] (a : M) : a • (0 : A) = 0 :=
+  SMulZeroClass.smul_zero _
+
+end Mathlib.GroupTheory.GroupAction.Defs
+
+section Mathlib.Algebra.SMulWithZero
+
+variable (R M)
+
+class SMulWithZero [Zero R] [Zero M] extends SMulZeroClass R M where
+
+@[simp]
+theorem zero_smul {M} [Zero R] [Zero M] [SMulWithZero R M] (m : M) : (0 : R) • m = 0 := sorry
+
+end Mathlib.Algebra.SMulWithZero
+
+section Mathlib.GroupTheory.GroupAction.Hom
+
+class MulActionSemiHomClass (F : Type _)
+    {M N : outParam (Type _)} (φ : outParam (M → N))
+    (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
+  map_smulₛₗ : ∀ (f : F) (c : M) (x : X), f (c • x) = (φ c) • (f x)
+
+export MulActionSemiHomClass (map_smulₛₗ)
+
+end Mathlib.GroupTheory.GroupAction.Hom
+
+section Mathlib.Algebra.Module.LinearMap.Defs
+
+variable {R S S₃ T M M₃ : Type _}
+
+class LinearMapClass (F : Type _) (R : outParam (Type _))
+  (M M₂ : outParam (Type _)) [Add M] [Add M₂]
+    [SMul R M] [SMul R M₂] [FunLike F M M₂]
+    extends MulActionSemiHomClass F (id : R → R) M M₂ : Prop
+
+variable (F : Type _)
+variable [Zero R]
+variable [Zero M] [Add M] [Zero M₃] [Add M₃]
+variable [SMulWithZero R M] [SMulWithZero R M₃]
+
+def inst1 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
+  { map_zero := fun f ↦
+      show f 0 = 0 by
+        rw [← zero_smul R (0 : M), @map_smulₛₗ]
+        simp only [id_eq, zero_smul]
+  }
+
+def inst2 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
+  { map_zero := fun f ↦
+      show f 0 = 0 by
+        rw [← zero_smul R (0 : M), map_smulₛₗ (N := R)]
+        simp only [id_eq, zero_smul]
+  }
+
+def inst3 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
+  { map_zero := fun f ↦
+      show f 0 = 0 by
+        rw [← zero_smul R (0 : M), map_smulₛₗ ]
+        simp only [id_eq, zero_smul]
+  }
+
+def inst4 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
+  { map_zero := fun f ↦
+      show f 0 = 0 by
+        rw [← zero_smul R (0 : M), map_smulₛₗ ..]
+        simp only [id_eq, zero_smul]
+  }
+
+end Mathlib.Algebra.Module.LinearMap.Defs