fix: Delaborator for constants

@Kha Could you please take a look at the fix?
This is an example posted by @JasonGross on Zulip.

src/Lean/Elab/Syntax.lean

@@ -458,12 +458,9 @@ def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax :=
 /-- Try to derive a `SimpleDelab` from a notation.
     The notation must be of the form `notation ... => c var_1 ... var_n`
     where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/
-def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax :=
+def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax := do
   match qrhs with
-  | `($c:ident $args*) => go c args
-  | `($c:ident)        => go c #[]
-  | _                  => failure
-  where go c args := do
+  | `($c:ident $args*) =>
     let [(c, [])] ← resolveGlobalName c.getId | failure
     guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
     guard <| args.allDiff
@@ -472,6 +469,10 @@ def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandEla
     `(@[appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun
        | `($qrhs) => `($pat)
        | _        => throw ())
+  | `($c:ident)        =>
+    let [(c, [])] ← resolveGlobalName c.getId | failure
+    `(@[appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun _ => `($pat))
+  | _                  => failure
 
 private def expandNotationAux (ref : Syntax)
     (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -141,13 +141,16 @@ def delabAppWithUnexpander : Delab := whenPPOption getPPNotation do
   let Expr.const c _ _ ← pure (← getExpr).getAppFn | failure
   let stx ← delabAppImplicit
   match stx with
-  | `($cPP:ident $args*) => do
+  | `($cPP:ident $args*) => do go c stx
+  | `($cPP:ident) => do go c stx
+  | _ => pure stx
+where
+  go c stx := do
     let some (f::_) ← pure <| (appUnexpanderAttribute.ext.getState (← getEnv)).table.find? c
       | pure stx
     let EStateM.Result.ok stx _ ← f stx |>.run ()
       | pure stx
     pure stx
-  | _ => pure stx
 
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where

tests/lean/constDelab.lean

@@ -0,0 +1,2 @@
+notation "ℕ" => Nat
+#check ℕ

tests/lean/constDelab.lean.expected.out

@@ -0,0 +1 @@
+ℕ : Type