diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean
index 78d9b4ba24..1a9a801f1d 100644
--- a/library/init/lean/parser/combinators.lean
+++ b/library/init/lean/parser/combinators.lean
@@ -126,7 +126,10 @@ instance sepBy1.View {α β} (p sep : Parser) (a) [Parser.HasView α p] [Parser.
   Parser.HasView (List (SepBy.Elem.View α β)) (sepBy1 p sep a) :=
 {..sepBy.view p sep a}
 
-def optional (r : Parser) : Parser :=
+/-- Optionally parse `r`. `require` can be used to conditionally override the
+    behavior without changing the structure of the syntax tree. -/
+def optional (r : Parser) (require := false) : Parser :=
+if require then r else
 do r ← optional $
      -- on error, wrap in "some"
      catch r (λ msg, throw {msg with custom := Syntax.list [msg.custom.get]}),
@@ -134,9 +137,9 @@ do r ← optional $
    | some r := Syntax.list [r]
    | none   := Syntax.list []
 
-instance optional.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (optional r) :=
+instance optional.tokens (r : Parser) [Parser.HasTokens r] (req) : Parser.HasTokens (optional r req) :=
 ⟨tokens r⟩
-instance optional.view (r : Parser) [Parser.HasView α r] : Parser.HasView (Option α) (optional r) :=
+instance optional.view (r : Parser) [Parser.HasView α r] (req) : Parser.HasView (Option α) (optional r req) :=
 { view := λ stx, match stx.asNode with
     | some {args := [], ..} := none
     | some {args := [stx], ..} := some $ HasView.view r stx
@@ -144,7 +147,7 @@ instance optional.view (r : Parser) [Parser.HasView α r] : Parser.HasView (Opti
   review := λ a, match a with
     | some a := Syntax.list [review r a]
     | none   := Syntax.list [] }
-instance optional.viewDefault (r : Parser) [Parser.HasView α r] : Parser.HasViewDefault (optional r) (Option α) none := ⟨⟩
+instance optional.viewDefault (r : Parser) [Parser.HasView α r] (req) : Parser.HasViewDefault (optional r req) (Option α) none := ⟨⟩
 
 /-- Parse a List `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
     Note that there is NO explicit encoding of which Parser was chosen;
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index d436ccb426..a92f69cbcc 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -79,10 +79,10 @@ nodeChoice! binderDefault {
 }
 
 @[derive HasTokens HasView]
-def binderContent.Parser : termParser :=
+def binderContent.Parser (requireType := false) : termParser :=
 node! binderContent [
   ids: binderIdent.Parser+,
-  type: optType.Parser,
+  type: optional typeSpec.Parser requireType,
   default: binderDefault.Parser?
 ]
 
@@ -132,11 +132,11 @@ node! anonymousConstructor ["⟨":maxPrec, args: sepBy (Term.Parser 0) (symbol "
 
        fun (x : t), s -/
 @[derive HasTokens HasView]
-def bracketedBinder.Parser : termParser :=
+def bracketedBinder.Parser (requireType := false) : termParser :=
 nodeChoice! bracketedBinder {
   explicit: node! explicitBinder ["(", content: nodeChoice! explicitBinderContent {
     «notation»: command.notationLike.Parser,
-    other: binderContent.Parser
+    other: binderContent.Parser requireType
   }, right: symbol ")"],
   implicit: node! implicitBinder ["{", content: binderContent.Parser, "}"],
   strictImplicit: node! strictImplicitBinder ["⦃", content: binderContent.Parser, "⦄"],
@@ -348,7 +348,7 @@ node! borrowed ["@&":maxPrec, Term: Term.Parser borrowPrec]
 --- Agda's `(x : e) → f`
 @[derive Parser.HasTokens Parser.HasView]
 def depArrow.Parser : termParser :=
-node! depArrow [binder: bracketedBinder.Parser, op: unicodeSymbol "→" "->" 25, range: Term.Parser 24]
+node! depArrow [binder: bracketedBinder.Parser true, op: unicodeSymbol "→" "->" 25, range: Term.Parser 24]
 
 -- TODO(Sebastian): replace with attribute
 @[derive HasTokens]