RFC: unexpanders take priority

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -149,22 +149,6 @@ def delabAppImplicit : Delab := whenNotPPOption getPPExplicit do
         pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
   Syntax.mkApp fnStx argStxs
 
-@[builtinDelab app]
-def delabAppWithUnexpander : Delab := whenPPOption getPPNotation do
-  let Expr.const c _ _ ← pure (← getExpr).getAppFn | failure
-  let stx ← delabAppImplicit
-  match stx with
-  | `($cPP:ident $args*) => do go c stx
-  | `($cPP:ident) => do go c stx
-  | _ => pure stx
-where
-  go c stx := do
-    let f::_ ← pure <| appUnexpanderAttribute.getValues (← getEnv) c
-      | pure stx
-    let EStateM.Result.ok stx _ ← f stx |>.run ()
-      | pure stx
-    pure stx
-
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info      : MatcherInfo
@@ -517,6 +501,33 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
     else pure <| none
   `({ $[$fields, ]* $lastField $[: $ty]? })
 
+@[builtinDelab app]
+def delabAppWithUnexpander : Delab := whenPPOption getPPNotation do
+  let Expr.const c _ _ ← pure (← getExpr).getAppFn | failure
+  let fs@(f::_) ← pure <| appUnexpanderAttribute.getValues (← getEnv) c | failure
+  /-
+  Note: the following example will take exponential time:
+  ```
+  def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1)
+
+  @[appUnexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander
+    | `(foo $k $a) => `(My.foo $k $a)
+    | _ => throw ()
+
+  #check foo $ foo $ foo $ foo $ foo $ foo $ foo id -- exp-time
+  ```
+  -/
+  let stx ← delabAppImplicit
+  match stx with
+  | `($cPP:ident $args*) => do go fs stx
+  | `($cPP:ident) => do go fs stx
+  | _ => pure stx
+where
+  go fs stx := fs.firstM fun f =>
+    match f stx |>.run () with
+    | EStateM.Result.ok stx _ => pure stx
+    | _ => failure
+
 @[builtinDelab app.Prod.mk]
 def delabTuple : Delab := whenPPOption getPPNotation do
   let e ← getExpr

tests/lean/delabUnexpand.lean

@@ -0,0 +1,26 @@
+structure Foo where
+  x : Nat
+  y : Nat
+
+macro a:term " ♬ " b:term : term => `(Foo.mk $a $b)
+
+@[appUnexpander Foo.mk] def unexpandFooFailure1 : Lean.PrettyPrinter.Unexpander
+  | _ => throw ()
+
+@[appUnexpander Foo.mk] def unexpandFoo : Lean.PrettyPrinter.Unexpander
+  | `(Foo.mk $a $b) => `($a ♬ $b)
+  | _ => throw ()
+
+@[appUnexpander Foo.mk] def unexpandFooFailure2 : Lean.PrettyPrinter.Unexpander
+  | _ => throw ()
+
+#check 3 ♬ 4
+
+def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1)
+
+@[appUnexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander
+  | `(foo $k $a) => `(My.foo $k $a)
+  | _ => throw ()
+
+-- The following would take exponential time without the `delabCache`.
+#check foo $ foo $ foo $ foo $ foo $ foo $ id

tests/lean/delabUnexpand.lean.expected.out

@@ -0,0 +1,2 @@
+3 ♬ 4 : Foo
+foo (foo (foo (foo (foo (foo id))))) : Nat → Nat