diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index eea29d2920..308b8ae989 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -429,7 +429,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   Remark: This is syntactic check and no reduction is performed.
 -/
 private def hasUnusedArguments : Expr → Bool
-  | Expr.forallE _ d b _ => b.hasLooseBVar 0 || hasUnusedArguments b
+  | Expr.forallE _ d b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
   | _ => false
 
 /--
@@ -768,12 +768,14 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
               return true
 
 builtin_initialize
+  registerTraceClass `Meta.synthPending
   registerTraceClass `Meta.synthInstance
   registerTraceClass `Meta.synthInstance.globalInstances
   registerTraceClass `Meta.synthInstance.newSubgoal
   registerTraceClass `Meta.synthInstance.tryResolve
   registerTraceClass `Meta.synthInstance.resume
   registerTraceClass `Meta.synthInstance.generate
-  registerTraceClass `Meta.synthPending
+  registerTraceClass `Meta.synthInstance.unusedArgs
+  registerTraceClass `Meta.synthInstance.newAnswer
 
 end Lean.Meta
diff --git a/tests/lean/815b.lean b/tests/lean/815b.lean
new file mode 100644
index 0000000000..c3dd07a13f
--- /dev/null
+++ b/tests/lean/815b.lean
@@ -0,0 +1,21 @@
+def is_smooth {α β} (f : α → β) : Prop := sorry
+
+class IsSmooth {α β} (f : α → β) : Prop where
+  (proof : is_smooth f)
+
+instance identity : IsSmooth fun a : α => a := sorry
+instance const (b : β) : IsSmooth fun a : α => b := sorry
+instance swap (f : α → β → γ) [∀ a, IsSmooth (f a)] : IsSmooth (λ b a => f a b) := sorry
+instance parm (f : α → β → γ) [IsSmooth f] (b : β) : IsSmooth (λ a => f a b) := sorry
+instance comp (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmooth (fun a => f (g a)) := sorry
+instance diag (f : β → δ → γ) (g : α → β) (h : α → δ) [IsSmooth f] [∀ b, IsSmooth (f b)] [IsSmooth g] [IsSmooth h] : IsSmooth (λ a => f (g a) (h a)) := sorry
+
+set_option trace.Meta.synthInstance true
+set_option trace.Meta.synthInstance.globalInstances false
+set_option trace.Meta.synthInstance.newSubgoal false
+set_option trace.Meta.synthInstance.tryResolve false
+set_option trace.Meta.synthInstance.resume false
+set_option trace.Meta.synthInstance.generate false
+set_option trace.Meta.synthInstance.newAnswer false
+set_option trace.Meta.synthInstance.unusedArgs true
+example (f : β → δ → γ) [IsSmooth f] (d : δ) : IsSmooth (λ (g : α → β) a => f (g a) d) := by infer_instance
diff --git a/tests/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out
new file mode 100644
index 0000000000..847bf8e388
--- /dev/null
+++ b/tests/lean/815b.lean.expected.out
@@ -0,0 +1,61 @@
+815b.lean:1:42-1:47: warning: declaration uses 'sorry'
+815b.lean:6:47-6:52: warning: declaration uses 'sorry'
+815b.lean:7:52-7:57: warning: declaration uses 'sorry'
+815b.lean:8:83-8:88: warning: declaration uses 'sorry'
+815b.lean:9:80-9:85: warning: declaration uses 'sorry'
+815b.lean:10:97-10:102: warning: declaration uses 'sorry'
+815b.lean:11:152-11:157: warning: declaration uses 'sorry'
+[Meta.synthInstance] preprocess: IsSmooth fun g a => f (g a) d ==> IsSmooth fun g a => f (g a) d
+  [Meta.synthInstance] 
+    [Meta.synthInstance] main goal IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    has unused arguments, reduced type
+      IsSmooth f
+    Transformer
+      fun redf a => redf
+    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    has unused arguments, reduced type
+      IsSmooth f
+    Transformer
+      fun redf a => redf
+    [Meta.synthInstance.unusedArgs] α → ∀ (b : β), IsSmooth (f b)
+    has unused arguments, reduced type
+      ∀ (b : β), IsSmooth (f b)
+    Transformer
+      fun redf a b => redf b
+    [Meta.synthInstance.unusedArgs] α → δ → IsSmooth f
+    has unused arguments, reduced type
+      IsSmooth f
+    Transformer
+      fun redf a a => redf
+    [Meta.synthInstance.unusedArgs] α → δ → ∀ (b : β), IsSmooth (f b)
+    has unused arguments, reduced type
+      ∀ (b : β), IsSmooth (f b)
+    Transformer
+      fun redf a a b => redf b
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a)
+    has unused arguments, reduced type
+      ∀ (a : α), IsSmooth fun g => f (g a)
+    Transformer
+      fun redf a a_1 => redf a
+    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    has unused arguments, reduced type
+      IsSmooth f
+    Transformer
+      fun redf a => redf
+    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    has unused arguments, reduced type
+      IsSmooth fun g => g
+    Transformer
+      fun redf a => redf
+    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    has unused arguments, reduced type
+      IsSmooth fun g => g
+    Transformer
+      fun redf a => redf
+    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    has unused arguments, reduced type
+      IsSmooth fun g => g
+    Transformer
+      fun redf a => redf
+  [Meta.synthInstance] result swap fun a g => f (g a) d
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index 5517447647..b150b2d7c9 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,3 +1,33 @@
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
 jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
@@ -32,12 +62,8 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -51,8 +77,12 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
+  @EGrfl
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -101,33 +131,3 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G