From 05022cc80b7f061df1d1f7ca6d08d167a7b328ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Mar 2021 16:04:47 -0700
Subject: [PATCH] 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             | 15 ++++++++++++++-
 tests/lean/shadow.lean.expected.out | 11 ++++-------
 2 files changed, 18 insertions(+), 8 deletions(-)

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