diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 25d98fb3aa..e94f5d02f6 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -976,10 +976,23 @@ private partial def dropTermParens : Syntax → Syntax := fun stx =>
   | `(($stx)) => dropTermParens stx
   | _         => stx
 
+private def isHole (stx : Syntax) : Bool :=
+  match stx with
+  | `(_)          => true
+  | `(? _)        => true
+  | `(? $x:ident) => true
+  | _             => false
+
+private def isTacticBlock (stx : Syntax) : Bool :=
+  match stx with
+  | `(by $x:tacticSeq) => true
+  | _ => false
+
 /-- Block usage of implicit lambdas if `stx` is `@f` or `@f arg1 ...` or `fun` with an implicit binder annotation. -/
 def blockImplicitLambda (stx : Syntax) : Bool :=
   let stx := dropTermParens stx
-  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx
+  -- TODO: make it extensible
+  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx
 
 /--
   Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index 25440e32aa..48c1afc265 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -15,15 +15,13 @@ context:
 α : Type u_1
 inst✝¹ : Inhabited α
 inst✝ inst : α
-β✝ δ✝ : Type
-⊢ α → β✝ → δ✝ → α × β✝ × δ✝
+⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.68 : Inhabited α
+inst.66 : Inhabited α
 inst inst : α
-β.93 δ.94 : Type
-⊢ α → β.93 → δ.94 → α × β.93 × δ.94
+⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
@@ -32,5 +30,4 @@ inst✝² : α
 inst✝¹ b : β
 inst : α
 inst✝ : Inhabited α
-β✝ δ✝ : Type
-⊢ α → β✝ → δ✝ → α × β✝ × δ✝
+⊢ {β δ : Type} → α → β → δ → α × β × δ