feat: elaborate noImplicitLambda% notation

src/Lean/Elab/Term.lean

@@ -1009,11 +1009,22 @@ private def isTacticBlock (stx : Syntax) : Bool :=
   | `(by $x:tacticSeq) => true
   | _ => false
 
+private def isNoImplicitLambda (stx : Syntax) : Bool :=
+  match stx with
+  | `(noImplicitLambda% $x:term) => true
+  | _ => false
+
+def mkNoImplicitLambdaAnnotation (type : Expr) : Expr :=
+  mkAnnotation `noImplicitLambda type
+
+def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
+  annotation? `noImplicitLambda type |>.isSome
+
 /-- 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
   -- TODO: make it extensible
-  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx
+  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx || isNoImplicitLambda stx
 
 /--
   Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and
@@ -1023,10 +1034,13 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te
     pure none
   else match expectedType? with
     | some expectedType => do
-      let expectedType ← whnfForall expectedType
-      match expectedType with
-      | Expr.forallE _ _ _ c => if c.binderInfo.isExplicit then pure none else pure $ some expectedType
-      | _                    => pure none
+      if hasNoImplicitLambdaAnnotation expectedType then
+        pure none
+      else
+        let expectedType ← whnfForall expectedType
+        match expectedType with
+        | Expr.forallE _ _ _ c => if c.binderInfo.isExplicit then pure none else pure $ some expectedType
+        | _                    => pure none
     | _         => pure none
 
 private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
@@ -1328,6 +1342,9 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   | some expectedType => mkTacticMVar expectedType stx
   | none => throwError ("invalid 'by' tactic, expected type has not been provided")
 
+@[builtinTermElab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
+  elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
+
 def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   let lctx ← getLCtx
   let view := extractMacroScopes n

tests/lean/run/impLambdaTac.lean

@@ -0,0 +1,33 @@
+example (P : Prop) : ∀ {p : P}, P := by
+  exact fun {p} => p
+
+example (P : Prop) : ∀ {p : P}, P := by
+  intro h; exact h
+
+example (P : Prop) : ∀ {p : P}, P := by
+  exact @id _
+
+example (P : Prop) : ∀ {p : P}, P := by
+  exact noImplicitLambda% id
+
+macro "exact'" x:term : tactic => `(exact noImplicitLambda% $x)
+
+example (P : Prop) : ∀ {p : P}, P := by
+  exact' id
+
+example (P : Prop) : ∀ {p : P}, P := by
+  apply id
+
+example (P : Prop) : ∀ p : P, P := by
+  have _ from 1
+  apply id
+
+example (P : Prop) : ∀ {p : P}, P := by
+  refine noImplicitLambda% (have _ from 1; ?_)
+  apply id
+
+#exit
+-- After update stage0, we fix this
+example (P : Prop) : ∀ {p : P}, P := by
+  have _ from 1
+  apply id