feat: allow synthetic holes to be used as patterns

They are useful for getting meaningful pattern variable names when the hole
is not an inaccessible pattern. See new test.

We are going to use this feature to address issue 2 at #1018.

src/Lean/Elab/Match.lean

@@ -207,28 +207,29 @@ inductive PatternVarDecl where
   | localVar     (fvarId : FVarId)
 
 private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array PatternVarDecl → TermElabM α) : TermElabM α :=
-  let rec loop (i : Nat) (decls : Array PatternVarDecl) := do
+  let rec loop (i : Nat) (decls : Array PatternVarDecl) (userNames : Array Name) := do
     if h : i < pVars.size then
       match pVars.get ⟨i, h⟩ with
-      | PatternVar.anonymousVar mvarId =>
+      | PatternVar.anonymousVar mvarId userName =>
         let type ← mkFreshTypeMVar
-        let userName ← mkFreshBinderName
-        withLocalDecl userName BinderInfo.default type fun x =>
-          loop (i+1) (decls.push (PatternVarDecl.anonymousVar mvarId x.fvarId!))
+        let userNameFVar ← if userName.isAnonymous then mkFreshBinderName else pure userName
+        withLocalDecl userNameFVar BinderInfo.default type fun x =>
+          loop (i+1) (decls.push (PatternVarDecl.anonymousVar mvarId x.fvarId!)) (userNames.push userName)
       | PatternVar.localVar userName   =>
         let type ← mkFreshTypeMVar
         withLocalDecl userName BinderInfo.default type fun x =>
-          loop (i+1) (decls.push (PatternVarDecl.localVar x.fvarId!))
+          loop (i+1) (decls.push (PatternVarDecl.localVar x.fvarId!)) (userNames.push Name.anonymous)
     else
       /- We must create the metavariables for `PatternVar.anonymousVar` AFTER we create the new local decls using `withLocalDecl`.
          Reason: their scope must include the new local decls since some of them are assigned by typing constraints. -/
-      decls.forM fun decl => match decl with
+      for decl in decls, userName in userNames do
+        match decl with
         | PatternVarDecl.anonymousVar mvarId fvarId => do
           let type ← inferType (mkFVar fvarId)
-          discard <| mkFreshExprMVarWithId mvarId type
+          discard <| mkFreshExprMVarWithId mvarId type (userName := userName)
         | _ => pure ()
       k decls
-  loop 0 #[]
+  loop 0 #[] #[]
 
 /-
 Remark: when performing dependent pattern matching, we often had to write code such as
@@ -454,11 +455,12 @@ private def mkLocalDeclFor (mvar : Expr) : M Pattern := do
   | some val => return Pattern.inaccessible val
   | none =>
     let fvarId ← mkFreshFVarId
-    let type   ← inferType mvar
+    let mvarDecl ← getMVarDecl mvarId
+    let type := mvarDecl.type
     /- HACK: `fvarId` is not in the scope of `mvarId`
        If this generates problems in the future, we should update the metavariable declarations. -/
     assignExprMVar mvarId (mkFVar fvarId)
-    let userName ← mkFreshBinderName
+    let userName ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName
     let newDecl := LocalDecl.cdecl default fvarId userName type BinderInfo.default
     modify fun s =>
       { s with
@@ -538,12 +540,15 @@ partial def main (e : Expr) : M Pattern := do
 
 end ToDepElimPattern
 
-def withDepElimPatterns {α} (localDecls : Array LocalDecl) (ps : Array Expr) (k : Array LocalDecl → Array Pattern → TermElabM α) : TermElabM α := do
+def withDepElimPatterns {α} (patternVarDecls : Array PatternVarDecl) (localDecls : Array LocalDecl) (ps : Array Expr) (k : Array LocalDecl → Array Pattern → TermElabM α) : TermElabM α := do
   let (patterns, s) ← (ps.mapM ToDepElimPattern.main).run { localDecls := localDecls }
   let localDecls ← s.localDecls.mapM fun d => instantiateLocalDeclMVars d
   /- toDepElimPatterns may have added new localDecls. Thus, we must update the local context before we execute `k` -/
   let lctx ← getLCtx
-  let lctx := localDecls.foldl (fun (lctx : LocalContext) d => lctx.erase d.fvarId) lctx
+  let lctx := patternVarDecls.foldl (init := lctx) fun (lctx : LocalContext) d =>
+    match d with
+    | PatternVarDecl.anonymousVar _ fvarId =>  lctx.erase fvarId
+    | PatternVarDecl.localVar fvarId => lctx.erase fvarId
   let lctx := localDecls.foldl (fun (lctx : LocalContext) d => lctx.addDecl d) lctx
   withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
     k localDecls patterns
@@ -554,7 +559,7 @@ private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array Patte
   id (α := TermElabM α) do
     let localDecls ← finalizePatternDecls patternVarDecls
     let patterns ← patterns.mapM (instantiateMVars ·)
-    withDepElimPatterns localDecls patterns fun localDecls patterns =>
+    withDepElimPatterns patternVarDecls localDecls patterns fun localDecls patterns => do
       k { ref := ref, fvarDecls := localDecls.toList, patterns := patterns.toList } matchType
 
 private def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : ExceptT PatternElabException TermElabM (AltLHS × Expr) := withRef alt.ref do
@@ -650,7 +655,7 @@ where
       trace[Meta.debug] "pathToIndex: {toString pathToIndex}"
       let some index ← getIndexToInclude? discrs[patternIdx] pathToIndex
         | throwEx (← updateFirst first? ex)
-      trace[Meta.debug] "index: {index}"
+      trace[Elab.match] "index to include: {index}"
       if (← discrs.anyM fun discr => isDefEq discr index) then
         throwEx (← updateFirst first? ex)
       let first ← updateFirst first? ex

src/Lean/Elab/PatternVar.lean

@@ -14,11 +14,11 @@ open Meta
 inductive PatternVar where
   | localVar     (userName : Name)
   -- anonymous variables (`_`) are encoded using metavariables
-  | anonymousVar (mvarId   : MVarId)
+  | anonymousVar (mvarId   : MVarId) (userName : Name)
 
 instance : ToString PatternVar := ⟨fun
-  | PatternVar.localVar x          => toString x
-  | PatternVar.anonymousVar mvarId => s!"?m{mvarId.name}"⟩
+  | PatternVar.localVar x            => toString x
+  | PatternVar.anonymousVar mvarId _ => s!"?m{mvarId.name}"⟩
 
 /--
   Create an auxiliary Syntax node wrapping a fresh metavariable id.
@@ -172,7 +172,12 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     return stx.setArg 2 <| mkNullNode fields
   else if k == ``Lean.Parser.Term.hole then
     let r ← mkMVarSyntax
-    modify fun s => { s with vars := s.vars.push <| PatternVar.anonymousVar <| getMVarSyntaxMVarId r }
+    modify fun s => { s with vars := s.vars.push <| PatternVar.anonymousVar (getMVarSyntaxMVarId r) Name.anonymous }
+    return r
+  else if k == ``Lean.Parser.Term.syntheticHole then
+    let r ← mkMVarSyntax
+    let userName := if stx[1].isIdent then stx[1].getId else Name.anonymous
+    modify fun s => { s with vars := s.vars.push <| PatternVar.anonymousVar (getMVarSyntaxMVarId r) userName }
     return r
   else if k == ``Lean.Parser.Term.paren then
     let arg := stx[1]

tests/lean/syntheticHolesAsPatterns.lean

@@ -0,0 +1,8 @@
+inductive Fam2 : Type → Type → Type 1 where
+  | any : Fam2 α α
+  | nat : Nat → Fam2 Nat Nat
+
+example (a : α) (x : Fam2 α β) : β :=
+  match α, β, a, x with
+  | ?α, ?β, ?a, Fam2.any   => _
+  | ?α, ?β, ?a, Fam2.nat n => _

tests/lean/syntheticHolesAsPatterns.lean.expected.out

@@ -0,0 +1,15 @@
+syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
+context:
+α✝ β : Type
+a✝ : α✝
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α
+syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
+context:
+α β : Type
+a✝ : α
+x : Fam2 α β
+a n : Nat
+⊢ Nat