feat: empty type ascription syntax (e :)

src/Lean/Elab/Binders.lean

@@ -374,14 +374,13 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
               else
                 processAsPattern ()
             | none => processAsPattern ()
-          else if special[0].getKind != `Lean.Parser.Term.typeAscription then
+          else if special[0].getKind != ``Lean.Parser.Term.typeAscription then
             processAsPattern ()
-          else
-            -- typeAscription := `:` term
-            let type := special[0][1]
-            match (← getFunBinderIds? term) with
-            | some idents => loop body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
-            | none        => processAsPattern ()
+          -- typeAscription := `:` (term)?
+          else if let some idents ← getFunBinderIds? term then
+            let type := special[0][1].getOptional?.getD (mkHole binder)
+            loop body (i+1) (newBinders ++ idents.map (mkExplicitBinder · type))
+          else processAsPattern ()
       | _ => processAsPattern ()
     else
       pure (newBinders, body, false)

src/Lean/Elab/BuiltinNotation.lean

@@ -218,9 +218,9 @@ where
 
 @[builtin_macro Lean.Parser.Term.paren] def expandParen : Macro
   | `(())           => `(Unit.unit)
-  | `(($e : $type)) => do
+  | `(($e : $(type)?)) => do
     match (← expandCDot? e) with
-    | some e => `(($e : $type))
+    | some e => `(($e : $(type)?))
     | none   => Macro.throwUnsupported
   | `(($e))         => return (← expandCDot? e).getD e
   | `(($e, $es,*))  => do
@@ -233,12 +233,15 @@ where
     else
       throw <| Macro.Exception.error stx "unexpected parentheses notation"
 
-@[builtin_term_elab paren] def elabParen : TermElab := fun stx _ => do
+@[builtin_term_elab paren] def elabParen : TermElab := fun stx expectedType? => do
   match stx with
-  | `(($e : $type)) =>
+  | `(($e : $type:term)) =>
     let type ← withSynthesize (mayPostpone := true) <| elabType type
     let e ← elabTerm e type
     ensureHasType type e
+  | `(($e :)) =>
+    let e ← withSynthesize (mayPostpone := false) <| elabTerm e none
+    ensureHasType expectedType? e
   | _ => throwUnsupportedSyntax
 
 /-- Return `true` if `lhs` is a free variable and `rhs` does not depend on it. -/

src/Lean/Elab/Do.lean

@@ -12,6 +12,9 @@ import Lean.Parser.Do
 -- HACK: avoid code explosion until heuristics are improved
 set_option compiler.reuse false
 
+-- remove after stage0 update
+set_option quotPrecheck false
+
 namespace Lean.Elab.Term
 open Lean.Parser.Term
 open Meta

src/Lean/Elab/Quotation/Precheck.lean

@@ -117,12 +117,13 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
   | _ => throwUnsupportedSyntax
 
 @[builtin_quot_precheck Lean.Parser.Term.paren] def precheckParen : Precheck
-  | `(())           => pure ()
-  | `(($e : $type)) => do
+  | `(())                => pure ()
+  | `(($e : $type:term)) => do
     precheck e
     precheck type
-  | `(($e))         => precheck e
-  | `(($e, $es,*))  => do
+  | `(($e :))
+  | `(($e))              => precheck e
+  | `(($e, $es,*))       => do
     precheck e
     es.getElems.raw.forM precheck
   | _ => throwUnsupportedSyntax

src/Lean/Parser/Term.lean

@@ -120,7 +120,7 @@ For example, `(· + ·)` is equivalent to `fun x y => x + y`.
 @[builtin_term_parser] def cdot   := leading_parser
   symbol "·" <|> "."
 def typeAscription := leading_parser
-  " : " >> termParser
+  " : " >> optional termParser
 def tupleTail      := leading_parser
   ", " >> sepBy1 termParser ", "
 def parenSpecial : Parser :=

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     opts = opts.update({"pp", "rawOnError"}, true);
 #endif
     return opts;