From 257e38394fa5a7c81ace9caf48e65283bce8164b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Aug 2021 18:52:39 -0700
Subject: [PATCH] feat: add strict implicit binder annotation

---
 src/Lean/Parser/Term.lean                    | 8 ++++++--
 tests/lean/partialVariable.lean.expected.out | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index fc382501c8..515e2b65bf 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -93,9 +93,12 @@ def binderTactic  := leading_parser atomic (symbol " := " >> " by ") >> Tactic.t
 def binderDefault := leading_parser " := " >> termParser
 def explicitBinder (requireType := false) := ppGroup $ leading_parser "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
 def implicitBinder (requireType := false) := ppGroup $ leading_parser "{" >> many1 binderIdent >> binderType requireType >> "}"
+def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
+def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
+def strictImplicitBinder (requireType := false) := ppGroup $ leading_parser strictImplicitLeftBracket >> many1 binderIdent >> binderType requireType >> strictImplicitRightBracket
 def instBinder := ppGroup $ leading_parser "[" >> optIdent >> termParser >> "]"
 def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" none (anonymous := false)) <|
-  explicitBinder requireType <|> implicitBinder requireType <|> instBinder
+  explicitBinder requireType <|> strictImplicitBinder requireType <|> implicitBinder requireType <|> instBinder
 
 /-
 It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
@@ -139,8 +142,9 @@ def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "genera
 @[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
+def funStrictImplicitBinder := atomic (lookahead (strictImplicitLeftBracket >> many1 binderIdent >> (symbol " : " <|> strictImplicitRightBracket))) >> strictImplicitBinder
 def funSimpleBinder   := atomic (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
-def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
+def funBinder : Parser := funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
 -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
 def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
 @[builtinTermParser] def «fun» := leading_parser:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
diff --git a/tests/lean/partialVariable.lean.expected.out b/tests/lean/partialVariable.lean.expected.out
index cf45478772..ef9db114f9 100644
--- a/tests/lean/partialVariable.lean.expected.out
+++ b/tests/lean/partialVariable.lean.expected.out
@@ -1 +1 @@
-partialVariable.lean:1:9: error: expected '(', '[' or '{'
+partialVariable.lean:1:9: error: expected '(', '[', '{' or '⦃'