diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 1ff649285c..3f169351d4 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -378,13 +378,6 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
 
 open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.as Pattern.val Pattern.arrayLit AltLHS MatcherResult)
 
-private def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
-  Core.transform e fun e =>
-    if let some e := inaccessible? e then
-      return TransformStep.visit e
-    else
-      return TransformStep.visit e
-
 namespace ToDepElimPattern
 
 private def throwInvalidPattern (e : Expr) : MetaM α :=
@@ -438,15 +431,18 @@ private def withMVar (mvarId : MVarId) (x : M α) : M α := do
 partial def normalize (e : Expr) : M Expr := do
   match inaccessible? e with
   | some e => processInaccessible e
+  | none =>
+  match patternWithRef? e with
+  | some (ref, e) => return mkPatternWithRef (← normalize e) ref
   | none =>
     match e.arrayLit? with
     | some (α, lits) => mkArrayLit α (← lits.mapM normalize)
     | none =>
-      if e.isAppOfArity ``_root_.namedPattern 4 then
+      if let some e := Match.isNamedPattern? e then
         let x := e.getArg! 1
         let p := e.getArg! 2
         let h := e.getArg! 3
-        unless x.isFVar && h.isFVar do
+        unless x.consumeMData.isFVar && h.consumeMData.isFVar do
           throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
         addVar x
         let p ← normalize p
@@ -485,32 +481,35 @@ partial def normalize (e : Expr) : M Expr := do
               return mkAppN e.getAppFn (params ++ fields))
 where
   addVar (e : Expr) : M Unit := do
+    let e ← erasePatternRefAnnotations e
     unless (← get).patternVars.contains e do
       modify fun s => { s with patternVars := s.patternVars.push e }
 
   processVar (e : Expr) : M Expr := do
-    if (← get).patternVars.contains e then
-      return mkInaccessible e
+    let e' ← erasePatternRefAnnotations e
+    if (← get).patternVars.contains e' then
+      return mkInaccessible (← eraseInaccessibleAnnotations e)
     else
-      if e.isMVar then
-        setMVarTag e.mvarId! (← read).userName
-      modify fun s => { s with patternVars := s.patternVars.push e }
+      if e'.isMVar then
+        setMVarTag e'.mvarId! (← read).userName
+      modify fun s => { s with patternVars := s.patternVars.push e' }
       return e
 
   processInaccessible (e : Expr) : M Expr := do
-    match e with
+    let e' ← erasePatternRefAnnotations e
+    match e' with
     | Expr.fvar fvarId _ =>
-      if (← isExplicitPatternVar e) then
+      if (← isExplicitPatternVar e') then
         processVar e
       else
         return mkInaccessible e
     | _ =>
-      if e.getAppFn.isMVar then
-        let eNew ← instantiateMVars e
-        if eNew != e then
-          withMVar e.getAppFn.mvarId! <| processInaccessible eNew
-        else if e.isMVar then
-          withMVar e.mvarId! <| processVar e
+      if e'.getAppFn.isMVar then
+        let eNew ← instantiateMVars e'
+        if eNew != e' then
+          withMVar e'.getAppFn.mvarId! <| processInaccessible eNew
+        else if e'.isMVar then
+          withMVar e'.mvarId! <| processVar e'
         else
           throwInvalidPattern e
       else
@@ -542,7 +541,7 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
     match e.arrayLit? with
     | some (α, lits) => return Pattern.arrayLit α (← lits.mapM toPattern)
     | none =>
-      if e.isAppOfArity ``_root_.namedPattern 4 then
+      if let some e := Match.isNamedPattern? e then
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
@@ -603,6 +602,20 @@ where
           modify fun s => { s with result := s.result.push e }
     | _ => return ()
 
+/--
+  Save pattern information in the info tree, and remove `patternWithRef?` annotations.
+-/
+def savePatternInfo (p : Expr) : TermElabM Expr :=
+  withReader (fun ctx => { ctx with inPattern := false }) do
+    let post (e : Expr) : TermElabM TransformStep := do
+      if let some (stx, e) := patternWithRef? e then
+        -- TODO: track whether we are inside of an inaccessible, and set `isBinder`
+        addTermInfo' stx e
+        return .done e
+      else
+        return .done e
+    transform p (post := post)
+
 /--
   Main method for `withDepElimPatterns`.
   - `PatternVarDecls`: are the explicit pattern variables provided by the user.
@@ -612,21 +625,23 @@ where
   - `k` is the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that, `patternVarDecls` are all
      replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.
  -/
-def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
+partial def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
   let explicitPatternVars := patternVarDecls.map fun decl => decl.fvarId
   let (ps, s) ← ps.mapM normalize |>.run { explicitPatternVars } |>.run {}
   let patternVars ← topSort s.patternVars
+  trace[Elab.match] "patternVars after topSort: {patternVars}"
   for explicit in explicitPatternVars do
     unless patternVars.any (· == mkFVar explicit) do
       withInPattern do
         throwError "invalid patterns, `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
   let packed ← pack patternVars ps matchType
+  trace[Elab.match] "packed: {packed}"
   let lctx := explicitPatternVars.foldl (init := (← getLCtx)) fun lctx d => lctx.erase d
   withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
     check packed
-    lambdaTelescope packed fun patternVars packed => do
+    unpack packed fun patternVars patterns matchType => do
       let localDecls ← patternVars.mapM fun x => getLocalDecl x.fvarId!
-      let (matchType, patterns) := unpackMatchTypePatterns packed
+      trace[Elab.match] "patternVars: {patternVars}, matchType: {matchType}"
       k localDecls (← patterns.mapM fun p => toPattern p) matchType
 where
   pack (patternVars : Array Expr) (ps : Array Expr) (matchType : Expr) : MetaM Expr := do
@@ -642,7 +657,7 @@ where
      ```
     -/
     let setMVarsAt (e : Expr) : StateRefT (Array MVarId) MetaM Unit := do
-      let mvarIds ← setMVarUserNamesAt e patternVars
+      let mvarIds ← setMVarUserNamesAt (← erasePatternRefAnnotations e) patternVars
       modify (· ++ mvarIds)
     let go : StateRefT (Array MVarId) MetaM Expr := do
       try
@@ -653,6 +668,19 @@ where
         resetMVarUserNames (← get)
     go |>.run' #[]
 
+  unpack (packed : Expr) (k : (patternVars : Array Expr) → (patterns : Array Expr) → (matchType : Expr) → TermElabM α) : TermElabM α :=
+    let rec go (packed : Expr) (patternVars : Array Expr) : TermElabM α := do
+      match packed with
+      | .lam n d b _ =>
+        withLocalDeclD n (← erasePatternRefAnnotations (← eraseInaccessibleAnnotations d)) fun patternVar =>
+          go (b.instantiate1 patternVar) (patternVars.push patternVar)
+      | _ =>
+        let (matchType, patterns) := unpackMatchTypePatterns packed
+        let matchType ← erasePatternRefAnnotations (← eraseInaccessibleAnnotations matchType)
+        let patterns ← patterns.mapM (savePatternInfo ·)
+        k patternVars patterns matchType
+    go packed #[]
+
 end ToDepElimPattern
 
 def withDepElimPatterns (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index c104eb0b50..b3fa15c49b 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -129,8 +129,10 @@ where
     let go (e : Expr) (ω) : ST ω FVarIdSet := do
       let ref ← ST.mkRef {}
       e.forEach fun e => do
-        if e.isAppOfArity ``namedPattern 4 && e.appArg!.isFVar then
-          ST.Prim.Ref.modify ref (·.insert e.appArg!.fvarId!)
+        if let some e := Match.isNamedPattern? e then
+          let arg := e.appArg!.consumeMData
+          if arg.isFVar then
+            ST.Prim.Ref.modify ref (·.insert arg.fvarId!)
       ST.Prim.Ref.get ref
     runST (go e)
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index bed9b0c6dc..1110e12c28 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -994,16 +994,21 @@ def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Op
     return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
 
 def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Expr := do
-  -- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
-  withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
-  return e
+  if (← read).inPattern then
+    return mkPatternWithRef e stx
+  else
+    withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
+    return e
 
 def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
   discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
 
 def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
-  -- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
-  Elab.withInfoContext' x mkInfo
+  if (← read).inPattern then
+    let e ← x
+    return mkPatternWithRef e stx
+  else
+    Elab.withInfoContext' x mkInfo
 
 /-
   Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 97dc5bf431..e82a2bc357 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1259,6 +1259,40 @@ def mkInaccessible (e : Expr) : Expr :=
 def inaccessible? (e : Expr) : Option Expr :=
   annotation? `_inaccessible e
 
+private def patternRefAnnotationKey := `_patWithRef
+
+/--
+  During elaboration expressions corresponding to pattern matching terms
+  are annotated with `Syntax` objects. This function returns `some (stx, p')` if
+  `p` is the pattern `p'` annotated with `stx`
+-/
+def patternWithRef? (p : Expr) : Option (Syntax × Expr) :=
+  match p with
+  | Expr.mdata d b _ =>
+    match d.find patternRefAnnotationKey with
+    | some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!)
+    | _ => none
+  | _                => none
+
+/--
+  Annotate the pattern `p` with `stx`. This is an auxiliary annotation
+  for producing better hover information.
+-/
+def mkPatternWithRef (p : Expr) (stx : Syntax) : Expr :=
+  if patternWithRef? p |>.isSome then
+    p
+  else
+    mkMData (KVMap.empty.insert patternRefAnnotationKey (DataValue.ofSyntax stx)) p
+
+/-- Return `some p` if `e` is an annotated pattern (`inaccessible?` or `patternWithRef?`) -/
+def patternAnnotation? (e : Expr) : Option Expr :=
+  if let some e := inaccessible? e then
+    some e
+  else if let some (_, e) := patternWithRef? e then
+    some e
+  else
+    none
+
 /--
   Annotate `e` with the LHS annotation. The delaborator displays
   expressions of the form `lhs = rhs` as `lhs` when they have this annotation.
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index aec8cb7074..f45a504eb1 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1381,16 +1381,16 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
       -- ⊢ q ((fun x => x + 1) 0)
       sorry
     ```
-    However, the inaccessible pattern annotation must be consumed.
+    However, pattern annotations (`inaccessible?` and `patternWithRef?`) must be consumed.
     The frontend relies on the fact that is must not be propagated by `isDefEq`.
     Thus, we consume it here. This is a bit hackish since it is very adhoc.
     We might other annotations in the future that we should not preserve.
     Perhaps, we should mark the annotation we do want to preserve ones
     (e.g., hints for the pretty printer), and consume all other
   -/
-  if let some t := inaccessible? t then
+  if let some t := patternAnnotation? t then
     isDefEqQuick t s
-  else if let some s := inaccessible? s then
+  else if let some s := patternAnnotation? s then
     isDefEqQuick t s
   else if t == s then
     return LBool.true
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index 8435b70ceb..8de4794148 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -9,6 +9,16 @@ import Lean.Meta.Match.CaseArraySizes
 
 namespace Lean.Meta.Match
 
+def mkNamedPattern (x h p : Expr) : MetaM Expr :=
+  mkAppM ``namedPattern #[x, p, h]
+
+def isNamedPattern? (e : Expr) : Option Expr :=
+  let e := e.consumeMData
+  if e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern then
+    some e
+  else
+    none
+
 inductive Pattern : Type where
   | inaccessible (e : Expr) : Pattern
   | var          (fvarId : FVarId) : Pattern
@@ -44,7 +54,7 @@ where
     | as fvarId p hId                =>
       -- TODO
       if annotate then
-        mkAppM ``namedPattern #[mkFVar fvarId, (← visit p), mkFVar hId]
+        mkNamedPattern (mkFVar fvarId) (mkFVar hId) (← visit p)
       else
         visit p
     | arrayLit type xs               =>
@@ -276,7 +286,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
     | some (α, lits) =>
       return Pattern.arrayLit α (← lits.mapM toPattern)
     | none =>
-      if e.isAppOfArity ``namedPattern 4 then
+      if let some e := isNamedPattern? e then
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 99823dae80..0791fdd28e 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -53,10 +53,9 @@ def casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId)) := do
 
 namespace Match
 
-
 def unfoldNamedPattern (e : Expr) : MetaM Expr := do
   let visit (e : Expr) : MetaM TransformStep := do
-    if e.isAppOfArity ``namedPattern 4 then
+    if let some e := isNamedPattern? e then
       if let some eNew ← unfoldDefinition? e then
         return TransformStep.visit eNew
     return TransformStep.visit e
@@ -103,7 +102,10 @@ where
 
   isNamedPatternProof (type : Expr) (h : Expr) : Bool :=
     Option.isSome <| type.find? fun e =>
-      e.isAppOfArity ``namedPattern 4 && e.appArg! == h
+      if let some e := isNamedPattern? e then
+        e.appArg! == h
+      else
+        false
 
 namespace SimpH
 
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index aa5b46a745..11ac42a722 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -142,5 +142,11 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
       | _ => return TransformStep.visit e
     Core.transform e (pre := pre)
 
+def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
+  Core.transform e (post := fun e => return TransformStep.done <| if let some e := inaccessible? e then e else e)
+
+def erasePatternRefAnnotations (e : Expr) : CoreM Expr :=
+  Core.transform e (post := fun e => return TransformStep.done <| if let some (_, e) := patternWithRef? e then e else e)
+
 end Meta
 end Lean
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index d514e60e26..ea99fa75f5 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich
 import Lean.KeyedDeclsAttribute
 import Lean.ProjFns
 import Lean.Syntax
+import Lean.Meta.Transform
 import Lean.Meta.Match.Match
 import Lean.Elab.Term
 import Lean.Elab.AuxDiscr
@@ -264,6 +265,9 @@ end Delaborator
 open Delaborator (OptionsPerPos topDownAnalyze Pos)
 
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Syntax × Std.RBMap Pos Elab.Info compare) := do
+  /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
+     `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
+  let e ← Meta.erasePatternRefAnnotations e
   trace[PrettyPrinter.delab.input] "{Std.format e}"
   let mut opts ← getOptions
   -- default `pp.proofs` to `true` if `e` is a proof
diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean
index 450d92f5d1..1c4f3e0eb3 100644
--- a/src/Lean/Util/Recognizers.lean
+++ b/src/Lean/Util/Recognizers.lean
@@ -81,18 +81,19 @@ def isDIte (e : Expr) :=
 
 partial def listLit? (e : Expr) : Option (Expr × List Expr) :=
   let rec loop (e : Expr) (acc : List Expr) :=
-    if e.isAppOfArity ``List.nil 1 then
-      some (e.appArg!, acc.reverse)
-    else if e.isAppOfArity ``List.cons 3 then
-      loop e.appArg! (e.appFn!.appArg! :: acc)
+    if e.isAppOfArity' ``List.nil 1 then
+      some (e.appArg!', acc.reverse)
+    else if e.isAppOfArity' ``List.cons 3 then
+      loop e.appArg!' (e.appFn!'.appArg!' :: acc)
     else
       none
   loop e []
 
 def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
-  match e.app2? ``List.toArray with
-  | some (_, e) => e.listLit?
-  | none        => none
+  if e.isAppOfArity' ``List.toArray 2 then
+    listLit? e.appArg!'
+  else
+    none
 
 /-- Recognize `α × β` -/
 def prod? (e : Expr) : Option (Expr × Expr) :=
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index f3ee58db46..df7a71dbaf 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -40,33 +40,23 @@ a : α
     [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
     @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
     a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
-      [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.651]) ([mdata _inaccessible:1 ?_uniq.652]) @ ⟨9, 4⟩-⟨9, 12⟩
-      @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-      ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
-        ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
-    a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
-      a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩†
+    [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.654]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.655]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+    α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+    α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+    α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+    Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+    a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
     ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
     [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
     Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
     [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
     a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp
-      [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.683]) ([mdata _inaccessible:1 ?_uniq.684]) @ ⟨10, 4⟩-⟨10, 12⟩
-      Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-      n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent
-        n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
-      a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+    [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.686]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.687]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+    n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+    Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+    a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
     n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
       n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
   @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 720d4a9cf3..51ca11ded8 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -213,14 +213,10 @@
                 @Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
                 [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
                 [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
-                (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ @ Lean.Elab.Term.elabApp
-                  @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
-                  Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
-                  Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
-                  z : Nat @ ⟨23, 9⟩-⟨23, 10⟩ @ Lean.Elab.Term.elabIdent
-                    z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
-                  w : Nat @ ⟨23, 12⟩-⟨23, 13⟩ @ Lean.Elab.Term.elabIdent
-                    w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
+                Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
+                z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
+                w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
+                (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
                 let z1 := z + w;
                 z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl
                   Nat : Type @ ⟨24, 8⟩†-⟨24, 10⟩† @ Lean.Elab.Term.elabHole
diff --git a/tests/lean/interactive/matchPatternHover.lean b/tests/lean/interactive/matchPatternHover.lean
new file mode 100644
index 0000000000..a8d2ad3473
--- /dev/null
+++ b/tests/lean/interactive/matchPatternHover.lean
@@ -0,0 +1,15 @@
+inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
+  | nil  : HList β []
+  | cons : β i → HList β is → HList β (i::is)
+
+infix:67 " :: " => HList.cons
+
+inductive Member : α → List α → Type
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+
+def HList.get : HList β is → Member i is → β i
+  | a::as, .head => a
+     --v textDocument/hover
+  | a::as, .tail h => as.get h
+               --^ textDocument/hover
diff --git a/tests/lean/interactive/matchPatternHover.lean.expected.out b/tests/lean/interactive/matchPatternHover.lean.expected.out
new file mode 100644
index 0000000000..7990334045
--- /dev/null
+++ b/tests/lean/interactive/matchPatternHover.lean.expected.out
@@ -0,0 +1,10 @@
+{"textDocument": {"uri": "file://matchPatternHover.lean"},
+ "position": {"line": 13, "character": 7}}
+{"range":
+ {"start": {"line": 13, "character": 7}, "end": {"line": 13, "character": 9}},
+ "contents": {"value": "```lean\nas : HList β is✝\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://matchPatternHover.lean"},
+ "position": {"line": 13, "character": 17}}
+{"range":
+ {"start": {"line": 13, "character": 17}, "end": {"line": 13, "character": 18}},
+ "contents": {"value": "```lean\nh : Member i is✝\n```", "kind": "markdown"}}
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index 7022bdeaca..885525f22a 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,49 +1,3 @@
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.arrow G T EG getCtx
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
 jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
@@ -108,6 +62,52 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.arrow G T EG getCtx
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
 jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index f93585f587..a288156e7b 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -96,7 +96,8 @@ def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β
 def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
 | _, nil,            nil,         f => none
 | _, @cons _ n a as, cons b bs,   f => some (f a b)
-#eval checkWithMkMatcherInput ``Vec.mapHead2.match_1
+set_option pp.match false in
+#print Vec.mapHead2 -- reused Vec.mapHead1.match_1
 
 def Vec.mapHead3 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
 | _, nil,            nil,         f => none
diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
index 17ac7d15f5..6f87351734 100644
--- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out
+++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -11,8 +11,13 @@ context:
 α β : Type
 a✝ : α
 x : Fam2 α β
-a : Nat
-n : Nat
+a n : Nat
+⊢ Nat
+syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
+context:
+α β : Type
+x : Fam2 α β
+n a : Nat
 ⊢ Nat
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
@@ -21,9 +26,3 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
-syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
-context:
-α β : Type
-x : Fam2 α β
-n a : Nat
-⊢ Nat