diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index b64f555520..af2a96f7ff 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -33,10 +33,10 @@ where
   synthesizeInstance (x type : Expr) : SimpM Bool := do
     match (← trySynthInstance type) with
     | LOption.some val =>
-      if (← isDefEq x val) then
+      if (← withReducibleAndInstances <| isDefEq x val) then
         return true
       else
-        trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign instance{indentExpr type}"
+        trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
         return false
     | _ =>
       trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to synthesize instance{indentExpr type}"
diff --git a/tests/lean/run/790.lean b/tests/lean/run/790.lean
new file mode 100644
index 0000000000..2964aef56c
--- /dev/null
+++ b/tests/lean/run/790.lean
@@ -0,0 +1,20 @@
+class Vec (X : Type) extends Add X, Inhabited X
+
+class Vec' (X : Type) extends Vec X
+
+def differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y := f dx
+
+@[simp]
+theorem differential_of_linear {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
+        : differential f x dx = f dx := by simp[differential]
+
+example {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
+        : differential f x dx = f dx := by simp
+
+instance : Vec Nat := ⟨⟩
+instance : Vec' Nat := ⟨⟩
+
+set_option trace.Meta.Tactic.simp true
+example {Y : Type} [Vec Y] (f : Nat → Y) (x dx : Nat)
+        : @differential _ _ Vec'.toVec _ f x dx = f dx :=
+  by simp