import Lean
open Lean Lean.PrettyPrinter

def foo : PUnit → PUnit := id
def x   : PUnit := ()

@[app_unexpander foo] def unexpandFoo : Unexpander := fun _ => `(sorry)

#eval do
  let e : Expr := mkApp (mkMData {} $ mkConst `foo [Level.one]) (mkConst `x)
  formatTerm (← delab e)

#eval do
  let opts := ({}: MData).set `pp.universes true
  -- the MData annotation should make it not a regular application,
  -- so the unexpander should not be called.
  let e : Expr := mkApp (mkMData opts $ mkConst `foo [Level.one]) (mkConst `x)
  formatTerm (← delab e)