From 4db3ccaddb32ed00d37c8c3b9dea4606de39a7f6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 May 2021 17:54:52 -0700
Subject: [PATCH] feat: type ascription should disable implicit lambdas

---
 src/Lean/Elab/Term.lean        | 8 +++++++-
 tests/lean/run/typeAscImp.lean | 7 +++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/typeAscImp.lean

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 290f28eabc..c66039b054 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1021,6 +1021,11 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
   | `(noImplicitLambda% $x:term) => true
   | _ => false
 
+private def isTypeAscription (stx : Syntax) : Bool :=
+  match stx with
+  | `(($e : $type)) => true
+  | _               => false
+
 def mkNoImplicitLambdaAnnotation (type : Expr) : Expr :=
   mkAnnotation `noImplicitLambda type
 
@@ -1031,7 +1036,8 @@ def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
 def blockImplicitLambda (stx : Syntax) : Bool :=
   let stx := dropTermParens stx
   -- TODO: make it extensible
-  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx || isNoImplicitLambda stx
+  isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx ||
+  isNoImplicitLambda stx || isTypeAscription stx
 
 /--
   Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and
diff --git a/tests/lean/run/typeAscImp.lean b/tests/lean/run/typeAscImp.lean
new file mode 100644
index 0000000000..8b25de924f
--- /dev/null
+++ b/tests/lean/run/typeAscImp.lean
@@ -0,0 +1,7 @@
+def Ctx := String → Type
+abbrev State (Γ : Ctx) := {x : String} → Γ x
+
+constant p {Γ : Ctx} (s : State Γ) : Prop
+
+theorem ex {Γ : Ctx} (s : State Γ) (h : (a : State Γ) → @p Γ a) : @p Γ s :=
+  h ‹_›