feat: implement have this

src/Init/Meta.lean

@@ -271,10 +271,11 @@ abbrev CharLit := TSyntax charLitKind
 abbrev NameLit := TSyntax nameLitKind
 abbrev ScientificLit := TSyntax scientificLitKind
 abbrev NumLit := TSyntax numLitKind
+abbrev HygieneInfo := TSyntax hygieneInfoKind
 
 end Syntax
 
-export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit)
+export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit HygieneInfo)
 
 namespace TSyntax
 
@@ -921,6 +922,9 @@ def getChar (s : CharLit) : Char :=
 def getName (s : NameLit) : Name :=
   s.raw.isNameLit?.getD .anonymous
 
+def getHygieneInfo (s : HygieneInfo) : Name :=
+  s.raw[0].getId
+
 namespace Compat
 
 scoped instance : CoeTail (Array Syntax) (Syntax.TSepArray k sep) where
@@ -930,6 +934,11 @@ end Compat
 
 end TSyntax
 
+def HygieneInfo.mkIdent (s : HygieneInfo) (val : Name) (canonical := false) : Ident :=
+  let src := s.raw[0]
+  let id := { extractMacroScopes src.getId with name := val.eraseMacroScopes }.review
+  ⟨Syntax.ident (SourceInfo.fromRef src canonical) (toString val).toSubstring id []⟩
+
 /-- Reflect a runtime datum back to surface syntax (best-effort). -/
 class Quote (α : Type) (k : SyntaxNodeKind := `term) where
   quote : α → TSyntax k

src/Init/Notation.lean

@@ -496,12 +496,6 @@ macro_rules
     else
       `(%[ $elems,* | List.nil ])
 
--- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding).
--- The keyword prevents declaring a `this` binding except through metaprogramming, as is done by `have`/`show`.
-/-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
-macro tk:"this" : term =>
-  return (⟨(Syntax.ident tk.getHeadInfo "this".toSubstring `this [])⟩ : TSyntax `term)
-
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.

src/Init/Prelude.lean

@@ -3721,6 +3721,16 @@ abbrev nameLitKind : SyntaxNodeKind := `name
 /-- `fieldIdx` is the node kind of projection indices like the `2` in `x.2`. -/
 abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
+/--
+`hygieneInfo` is the node kind of the `hygieneInfo` parser, which is an
+"invisible token" which captures the hygiene information at the current point
+without parsing anything.
+
+They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`)
+as if they were introduced by the calling context, not the called macro.
+-/
+abbrev hygieneInfoKind : SyntaxNodeKind := `hygieneInfo
+
 /--
 `interpolatedStrLitKind` is the node kind of interpolated string literal
 fragments like `"value = {` and `}"` in `s!"value = {x}"`.

src/Init/Tactics.lean

@@ -511,7 +511,7 @@ macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_la
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
 /-- Similar to `have`, but using `refine'` -/
-macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x : _ := $p)
+macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 

src/Lean/Elab/Binders.lean

@@ -689,7 +689,7 @@ structure LetIdDeclView where
   value   : Syntax
 
 def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
-  -- `letIdDecl` is of the form `ident >> many bracketedBinder >> optType >> " := " >> termParser
+  -- `letIdDecl` is of the form `binderIdent >> many bracketedBinder >> optType >> " := " >> termParser
   let id      := letIdDecl[0]
   let binders := letIdDecl[1].getArgs
   let optType := letIdDecl[2]
@@ -708,6 +708,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
   let body    := stx[3]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
     let { id, binders, type, value } := mkLetIdDeclView letDecl
+    let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true)
     elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly
   else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
     -- node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushNone >> optType >> " := ") >> termParser
@@ -717,7 +718,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
     let optType := letDecl[2]
     let val     := letDecl[4]
     if pat.getKind == ``Parser.Term.hole then
-      -- `let _ := ...` should not be treated at a `letIdDecl`
+      -- `let _ := ...` should not be treated as a `letIdDecl`
       let id   ← mkFreshIdent pat (canonical := true)
       let type := expandOptType id optType
       elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly

src/Lean/Elab/BuiltinNotation.lean

@@ -104,17 +104,25 @@ open Meta
 
 @[builtin_macro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
   match stx with
-  | `(have $x $bs* $[: $type]? := $val; $body)            => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have%$tk $[: $type]? := $val; $body)                => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? := $val; $body)
-  | `(have $x $bs* $[: $type]? $alts; $body)              => `(let_fun $x $bs* $[: $type]? $alts; $body)
-  | `(have%$tk $[: $type]? $alts:matchAlts; $body)        => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? $alts:matchAlts; $body)
-  | `(have $pattern:term $[: $type]? := $val:term; $body) => `(let_fun $pattern:term $[: $type]? := $val:term ; $body)
-  | _                                                     => Macro.throwUnsupported
+  | `(have $hy:hygieneInfo $bs* $[: $type]? := $val; $body) =>
+    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? := $val; $body)
+  | `(have $hy:hygieneInfo $bs* $[: $type]? $alts; $body)   =>
+    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? $alts; $body)
+  | `(have $x:ident $bs* $[: $type]? := $val; $body) => `(let_fun $x $bs* $[: $type]? := $val; $body)
+  | `(have $x:ident $bs* $[: $type]? $alts; $body)   => `(let_fun $x $bs* $[: $type]? $alts; $body)
+  | `(have _%$x     $bs* $[: $type]? := $val; $body) => `(let_fun _%$x $bs* $[: $type]? := $val; $body)
+  | `(have _%$x     $bs* $[: $type]? $alts; $body)   => `(let_fun _%$x $bs* $[: $type]? $alts; $body)
+  | `(have $pattern:term $[: $type]? := $val; $body) => `(let_fun $pattern:term $[: $type]? := $val; $body)
+  | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $[$x :]? $type from $val; $body)            => `(have%$tk $[$x]? : $type := $body; $val)
-  | `(suffices%$tk $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have%$tk $[$x]? : $type := $body; by%$b $tac)
-  | _                                                          => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
+  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
+  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
+  | _                                                                 => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/Do.lean

@@ -49,7 +49,7 @@ private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
   else if k == ``Parser.Term.letEqnsDecl then
     true
   else if k == ``Parser.Term.letIdDecl then
-    -- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType
+    -- letIdLhs := binderIdent >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType
     let binders := letDeclArg[1]
     binders.getNumArgs > 0
   else
@@ -584,8 +584,11 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlo
   let terminal ← liftMacroM <| convertTerminalActionIntoJmp terminal.code jp xs
   return { code  := attachJP jpDecl terminal, uvars := k.uvars }
 
-def getLetIdDeclVar (letIdDecl : Syntax) : Var :=
-  letIdDecl[0]
+def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
+  if letIdDecl[0].isIdent then
+    #[letIdDecl[0]]
+  else
+    #[]
 
 -- support both regular and syntax match
 def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var) :=
@@ -600,43 +603,46 @@ def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := letPatDecl[0]
   getPatternVarsEx pattern
 
-def getLetEqnsDeclVar (letEqnsDecl : Syntax) : Var :=
-  letEqnsDecl[0]
+def getLetEqnsDeclVars (letEqnsDecl : Syntax) : Array Var :=
+  if letEqnsDecl[0].isIdent then
+    #[letEqnsDecl[0]]
+  else
+    #[]
 
 def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
   let arg := letDecl[0]
   if arg.getKind == ``Parser.Term.letIdDecl then
-    return #[getLetIdDeclVar arg]
+    return getLetIdDeclVars arg
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else if arg.getKind == ``Parser.Term.letEqnsDecl then
-    return #[getLetEqnsDeclVar arg]
+    return getLetEqnsDeclVars arg
   else
     throwError "unexpected kind of let declaration"
 
 def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
   -- leading_parser "let " >> optional "mut " >> letDecl
   getLetDeclVars doLet[2]
 
-def getHaveIdLhsVar (optIdent : Syntax) : TermElabM Var :=
-  if optIdent.isNone then
-    `(this)
+def getHaveIdLhsVar (optIdent : Syntax) : Var :=
+  if optIdent.getKind == hygieneInfoKind then
+    HygieneInfo.mkIdent optIdent[0] `this
   else
-    pure optIdent[0]
+    optIdent
 
 def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
   -- doHave := leading_parser "have " >> Term.haveDecl
   -- haveDecl := leading_parser haveIdDecl <|> letPatDecl <|> haveEqnsDecl
   let arg := doHave[1][0]
   if arg.getKind == ``Parser.Term.haveIdDecl then
     -- haveIdDecl := leading_parser atomic (haveIdLhs >> " := ") >> termParser
-    -- haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
-    return #[← getHaveIdLhsVar arg[0]]
+    -- haveIdLhs := (binderIdent <|> hygieneInfo) >> many letIdBinder >> optType
+    return #[getHaveIdLhsVar arg[0]]
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else if arg.getKind == ``Parser.Term.haveEqnsDecl then
     -- haveEqnsDecl := leading_parser haveIdLhs >> matchAlts
-    return #[← getHaveIdLhsVar arg[0]]
+    return #[getHaveIdLhsVar arg[0]]
   else
     throwError "unexpected kind of have declaration"
 
@@ -672,7 +678,7 @@ def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
 def getDoReassignVars (doReassign : Syntax) : TermElabM (Array Var) := do
   let arg := doReassign[0]
   if arg.getKind == ``Parser.Term.letIdDecl then
-    return #[getLetIdDeclVar arg]
+    return getLetIdDeclVars arg
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else

src/Lean/Elab/LetRec.lean

@@ -37,6 +37,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
     else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
+      unless declId.isIdent do
+        throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName

src/Lean/Elab/MutualDef.lean

@@ -210,6 +210,7 @@ private def expandWhereStructInst : Macro
         have : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) := ⟨(⟨·⟩)⟩
         val ← if binders.size > 0 then `(fun $binders* => $val) else pure val
         `(structInstField|$id:ident := $val)
+      | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
     let body ← `({ $structInstFields,* })
     match whereDecls? with

src/Lean/Elab/Syntax.lean

@@ -260,7 +260,7 @@ open Lean.Parser.Command
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
   if let .str _ suffix := catName then
-    let quotSymbol := "`(" ++ suffix ++ "|"
+    let quotSymbol := "`(" ++ suffix ++ "| "
     let name := catName ++ `quot
     let cmd ← `(
       @[term_parser] def $(mkIdent name) : Lean.ParserDescr :=

src/Lean/Parser.lean

@@ -27,7 +27,8 @@ builtin_initialize
   register_parser_alias (kind := charLitKind) "char" charLit
   register_parser_alias (kind := nameLitKind) "name" nameLit
   register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
-  register_parser_alias (kind := identKind) "ident" ident
+  register_parser_alias (kind := identKind) ident
+  register_parser_alias (kind := hygieneInfoKind) hygieneInfo
   register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
   register_parser_alias "colGe" checkColGe { stackSz? := some 0 }
   register_parser_alias "colEq" checkColEq { stackSz? := some 0 }

src/Lean/Parser/Basic.lean

@@ -1072,6 +1072,20 @@ def identEq (id : Name) : Parser := {
   info := mkAtomicInfo "ident"
 }
 
+def hygieneInfoFn : ParserFn := fun c s =>
+  let input := c.input
+  let pos   := s.pos
+  let str   := mkEmptySubstringAt input pos
+  let info  := SourceInfo.original str pos str pos
+  let ident := mkIdent info str .anonymous
+  let stx   := mkNode hygieneInfoKind #[ident]
+  s.pushSyntax stx
+
+def hygieneInfoNoAntiquot : Parser := {
+  fn   := hygieneInfoFn
+  info := nodeInfo hygieneInfoKind epsilonInfo
+}
+
 namespace ParserState
 
 def keepTop (s : SyntaxStack) (startStackSize : Nat) : SyntaxStack :=

src/Lean/Parser/Extra.lean

@@ -37,6 +37,9 @@ attribute [run_builtin_parser_attribute_hooks]
 @[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
+@[run_builtin_parser_attribute_hooks] def hygieneInfo : Parser :=
+  withAntiquot (mkAntiquot "hygieneInfo" hygieneInfoKind (anonymous := false)) hygieneInfoNoAntiquot
+
 @[run_builtin_parser_attribute_hooks] def numLit : Parser :=
   withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
 

src/Lean/Parser/Term.lean

@@ -119,6 +119,7 @@ def optSemicolon (p : Parser) : Parser :=
   "_"
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> hole)
+def binderIdent : Parser  := ident <|> hole
 /-- A temporary placeholder for a missing proof or value. -/
 @[builtin_term_parser] def «sorry» := leading_parser
   "sorry"
@@ -165,7 +166,7 @@ def fromTerm   := leading_parser
   "from " >> termParser
 def showRhs := fromTerm <|> byTactic'
 def sufficesDecl := leading_parser
-  optIdent >> termParser >> ppSpace >> showRhs
+  (atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
 @[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
@@ -209,7 +210,6 @@ In contrast to regular patterns, `e` may be an arbitrary term of the appropriate
 -/
 @[builtin_term_parser] def inaccessible := leading_parser
   ".(" >> withoutPosition termParser >> ")"
-def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser :=
   if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
 def binderTactic  := leading_parser
@@ -394,7 +394,7 @@ def letIdBinder :=
     binderIdent <|> bracketedBinder
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
 def letIdLhs    : Parser :=
-  ident >> notFollowedBy (checkNoWsBefore "" >> "[")
+  binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[")
     "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >>
   many (ppSpace >> letIdBinder) >> optType
 def letIdDecl   := leading_parser (withAnonymousAntiquot := false)
@@ -467,7 +467,7 @@ It is often used when building macros.
   withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
 
 /- like `let_fun` but with optional name -/
-def haveIdLhs    := optional (ppSpace >> ident >> many (ppSpace >> letIdBinder)) >> optType
+def haveIdLhs    := ((ppSpace >> binderIdent) <|> hygieneInfo) >> many (ppSpace >> letIdBinder) >> optType
 def haveIdDecl   := leading_parser (withAnonymousAntiquot := false)
   atomic (haveIdLhs >> " := ") >> termParser
 def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)

src/Lean/PrettyPrinter/Formatter.lean

@@ -489,6 +489,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter skip] def skip.formatter : Formatter := pure ()
 
 @[combinator_formatter pushNone] def pushNone.formatter : Formatter := goLeft
+@[combinator_formatter hygieneInfoNoAntiquot] def hygieneInfoNoAntiquot.formatter : Formatter := goLeft
 
 @[combinator_formatter interpolatedStr]
 def interpolatedStr.formatter (p : Formatter) : Formatter := do

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -492,6 +492,7 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
 @[combinator_parenthesizer skip] def skip.parenthesizer : Parenthesizer := pure ()
 
 @[combinator_parenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
+@[combinator_parenthesizer hygieneInfoNoAntiquot] def hygieneInfoNoAntiquot.parenthesizer : Parenthesizer := goLeft
 
 @[combinator_parenthesizer interpolatedStr]
 def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do