fix: fixes #220 and #223

src/Lean/Delaborator.lean

@@ -457,13 +457,20 @@ def delabMData : Delab := do
   -- only interpret `pp.` values by default
   let Expr.mdata m _ _ ← getExpr | unreachable!
   let mut posOpts := (← read).optionsPerPos
+  let mut inaccessible := false
   let pos := (← read).pos
   for (k, v) in m do
     if (`pp).isPrefixOf k then
       let opts := posOpts.find? pos |>.getD {}
       posOpts := posOpts.insert pos (opts.insert k v)
-  withReader ({ · with optionsPerPos := posOpts }) <|
-    withMDataExpr delab
+    if k == `inaccessible then
+      inaccessible := true
+  withReader ({ · with optionsPerPos := posOpts }) do
+    let s ← withMDataExpr delab
+    if inaccessible then
+      `(.($s))
+    else
+      pure s
 
 /--
 Check for a `Syntax.ident` of the given name anywhere in the tree.
@@ -780,6 +787,14 @@ def delabListToArray : Delab := whenPPOption getPPNotation do
   | `([$xs*]) => `(#[$xs*])
   | _         => failure
 
+@[builtinDelab app.namedPattern]
+def delabNamedPattern : Delab := do
+  guard $ (← getExpr).getAppNumArgs == 3
+  let x ← withAppFn $ withAppArg delab
+  let p ← withAppArg delab
+  guard x.isIdent
+  `($x:ident@$p:term)
+
 end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/

src/Lean/Elab/Match.lean

@@ -35,9 +35,9 @@ structure MatchAltView :=
   (rhs      : Syntax)
 
 def mkMatchAltView (ref : Syntax) (matchAlt : Syntax) : MatchAltView := {
-  ref := ref,
-  patterns := matchAlt[0].getSepArgs,
-  rhs := matchAlt[2]
+  ref      := ref
+  patterns := matchAlt[0].getSepArgs
+  rhs      := matchAlt[2]
 }
 
 private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do

src/Lean/Meta/Match/Basic.lean

@@ -29,17 +29,29 @@ partial def toMessageData : Pattern → MessageData
   | arrayLit _ pats        => m!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
   | as varId p             => m!"{mkFVar varId}@{toMessageData p}"
 
-partial def toExpr : Pattern → MetaM Expr
-  | inaccessible e                 => pure e
-  | var fvarId                     => pure $ mkFVar fvarId
-  | val e                          => pure e
-  | as _ p                         => toExpr p
-  | arrayLit type xs               => do
-    let xs ← xs.mapM toExpr;
-    mkArrayLit type xs
-  | ctor ctorName us params fields => do
-    let fields ← fields.mapM toExpr;
-    pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
+partial def toExpr (p : Pattern) (annotate := false) : MetaM Expr :=
+  visit p
+where
+  visit (p : Pattern) := do
+    match p with
+    | inaccessible e                 =>
+      if annotate then
+        pure (mkAnnotation `inaccessible e)
+      else
+        pure e
+    | var fvarId                     => pure $ mkFVar fvarId
+    | val e                          => pure e
+    | as fvarId p                    =>
+      if annotate then
+        mkAppM `namedPattern #[mkFVar fvarId, (← visit p)]
+      else
+        visit p
+    | arrayLit type xs               =>
+      let xs ← xs.mapM visit
+      mkArrayLit type xs
+    | ctor ctorName us params fields =>
+      let fields ← fields.mapM visit
+      pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
 
 /- Apply the free variable substitution `s` to the given pattern -/
 partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern

src/Lean/Meta/Match/Match.lean

@@ -28,7 +28,7 @@ private def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt →
 where
   mkMinorType (xs : Array Expr) (lhs : AltLHS) : MetaM Expr :=
     withExistingLocalDecls lhs.fvarDecls do
-      let args ← lhs.patterns.toArray.mapM Pattern.toExpr
+      let args ← lhs.patterns.toArray.mapM (Pattern.toExpr · (annotate := true))
       let minorType := mkAppN motive args
       mkForallFVars xs minorType
 

tests/lean/220.lean

@@ -0,0 +1,5 @@
+def f : List Nat → List Nat
+  | a::xs@(b::bs) => xs
+  | _             => []
+
+#print f

tests/lean/220.lean.expected.out

@@ -0,0 +1,5 @@
+def f : List Nat → List Nat :=
+fun (x : List Nat) =>
+  match x with 
+  | a :: xs@(b :: bs) => xs
+  | x_1 => []

tests/lean/223.lean

@@ -0,0 +1,14 @@
+universes u v
+
+inductive Imf {α : Type u} {β : Type v} (f : α → β) : β → Type (max u v)
+| mk : (a : α) → Imf f (f a)
+
+def h {α β} {f : α → β} : {b : β} → Imf f b → α
+| _, Imf.mk a => a
+
+#print h
+
+theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
+  | α, _, rfl, a => HEq.refl a
+
+#print ex

tests/lean/223.lean.expected.out

@@ -0,0 +1,8 @@
+def h.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → {f : α → β} → {b : β} → Imf f b → α :=
+fun {α : Type u_1} {β : Type u_2} {f : α → β} (x : β) (x_1 : Imf f x) =>
+  match x, x_1 with 
+  | .(f a), Imf.mk a => a
+theorem ex.{u} : {α β : Sort u} → (h : α = β) → (a : α) → cast h a ≅ a :=
+fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) =>
+  match x, x_1, x_2, x_3 with 
+  | α, .(α), Eq.refl α, a => HEq.refl a