fix: disable implicit lambda insertion at _, ?h, and by ...

@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.

BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".

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

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} → α → β → δ → α × β × δ