feat: better coe support

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -189,16 +189,12 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
 -- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
 -- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
-  if not (← isCoe) then failure
+  if not (← isCoe (← getExpr)) then failure
   let e ← getExpr
   match stx with
   | `($fn $arg)   => arg
   | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
   | _             => failure
-where
-  isCoe : DelabM Bool := do
-    let e ← getExpr
-    e.isAppOfArity `coe 4 || e.isAppOfArity `coeFun 4
 
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -116,6 +116,12 @@ def isIdLike (arg : Expr) : Bool := do
   | Expr.lam _ _ (Expr.bvar ..) .. => true
   | _ => false
 
+def isCoe (e : Expr) : Bool :=
+  -- TODO: `coeSort? Builtins doesn't seem to render them anyway
+  e.isAppOfArity `coe 4
+  || (e.isAppOf `coeFun && e.getAppNumArgs >= 4)
+  || e.isAppOfArity `coeSort 4
+
 namespace TopDownAnalyze
 
 def replaceLPsWithVars (e : Expr) : MetaM Expr := do
@@ -213,10 +219,6 @@ def isFunLike (e : Expr) : MetaM Bool := do
 def isSubstLike (e : Expr) : Bool :=
   e.isAppOfArity `Eq.ndrec 6
 
-def isCoeLike (e : Expr) : Bool :=
-  -- TODO: `coeSort? Builtins doesn't seem to render them anyway
-  e.isAppOfArity `coe 4 || e.isAppOfArity `coeFun 4
-
 def nameNotRoundtrippable (n : Name) : Bool :=
   n.hasMacroScopes || isPrivateName n || containsNum n
 where
@@ -326,7 +328,7 @@ where
 
     let forceRegularApp : Bool :=
       (getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr))
-      || (getPPAnalyzeTrustCoe (← getOptions) && isCoeLike (← getExpr))
+      || (getPPAnalyzeTrustCoe (← getOptions) && isCoe (← getExpr))
 
     -- Now, if this is the first staging, analyze the n-ary function without expected type
     if !f.isApp then withKnowing false (forceRegularApp || !(← instantiateMVars fType).hasLevelMVar) $ withNaryFn (analyze (parentIsApp := true))

tests/lean/run/PPTopDownAnalyze.lean

@@ -225,6 +225,13 @@ set_option pp.analyze.typeAscriptions false in
 #testDelab (fun (x : Unit) => @id (ReaderT Bool IO Bool) (do read : ReaderT Bool IO Bool)) ()
   expecting (fun (x : Unit) => id read) ()
 
+instance : CoeFun Bool (fun b => Bool → Bool) := { coe := fun b x => b && x }
+set_option pp.analyze.trustCoe false in
+#testDelab coeFun true false expecting coeFun (γ := fun b => Bool → Bool) true false
+
+set_option pp.analyze.trustCoe true in
+#testDelab coeFun true false expecting true false
+
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
 #testDelabN Nat.mod_lt