chore: remove unexpanded coercion support from pp.analyze

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -206,15 +206,6 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
     | EStateM.Result.ok stx _ => pure stx
     | _ => failure
 
--- 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 (← getExpr)) then failure
-  match stx with
-  | `($_ $arg)   => return arg
-  | `($_ $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
-  | _            => failure
-
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv
   let e ← getExpr
@@ -285,7 +276,6 @@ def delabAppImplicit : Delab := do
   if ← isRegularApp then
     (guard (← getPPOption getPPNotation) *> unexpandRegularApp stx)
     <|> (guard (← getPPOption getPPStructureInstances) *> unexpandStructureInstance stx)
-    <|> (guard (← getPPOption getPPNotation) *> unexpandCoe stx)
     <|> pure stx
   else pure stx
 

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -68,12 +68,6 @@ register_builtin_option pp.analyze.trustOfScientific : Bool := {
   descr    := "(pretty printer analyzer) always 'pretend' `OfScientific.ofScientific` applications can elab bottom-up"
 }
 
-register_builtin_option pp.analyze.trustCoe : Bool := {
-  defValue := false
-  group    := "pp.analyze"
-  descr    := "(pretty printer analyzer) always assume a coercion can be correctly inserted"
-}
-
 -- TODO: this is an arbitrary special case of a more general principle.
 register_builtin_option pp.analyze.trustSubtypeMk : Bool := {
   defValue := true
@@ -118,7 +112,6 @@ def getPPAnalyzeTrustSubst                  (o : Options) : Bool := o.get pp.ana
 def getPPAnalyzeTrustOfNat                  (o : Options) : Bool := o.get pp.analyze.trustOfNat.name pp.analyze.trustOfNat.defValue
 def getPPAnalyzeTrustOfScientific           (o : Options) : Bool := o.get pp.analyze.trustOfScientific.name pp.analyze.trustOfScientific.defValue
 def getPPAnalyzeTrustId                     (o : Options) : Bool := o.get pp.analyze.trustId.name pp.analyze.trustId.defValue
-def getPPAnalyzeTrustCoe                    (o : Options) : Bool := o.get pp.analyze.trustCoe.name pp.analyze.trustCoe.defValue
 def getPPAnalyzeTrustSubtypeMk              (o : Options) : Bool := o.get pp.analyze.trustSubtypeMk.name pp.analyze.trustSubtypeMk.defValue
 def getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownFOType2TypeHOFuns.name pp.analyze.trustKnownFOType2TypeHOFuns.defValue
 def getPPAnalyzeOmitMax                     (o : Options) : Bool := o.get pp.analyze.omitMax.name pp.analyze.omitMax.defValue
@@ -160,13 +153,6 @@ def isIdLike (arg : Expr) : Bool :=
   | Expr.lam _ _ (Expr.bvar ..) .. => true
   | _ => false
 
-def isCoe (e : Expr) : Bool :=
-  -- TODO: `coeSort? Builtins doesn't seem to render them anyway
-  -- TODO: should we delete this function, we want to eagerly expand all coercions
-  e.isAppOfArity ``CoeT.coe 4
-  || (e.isAppOf ``CoeFun.coe && e.getAppNumArgs >= 4)
-  || e.isAppOfArity ``CoeSort.coe 4
-
 def isStructureInstance (e : Expr) : MetaM Bool := do
   match e.isConstructorApp? (← getEnv) with
   | some s => return isStructure (← getEnv) s.induct
@@ -418,7 +404,6 @@ mutual
 
       let forceRegularApp : Bool :=
         (getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr))
-        || (getPPAnalyzeTrustCoe (← getOptions) && isCoe (← getExpr))
         || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity ``Subtype.mk 4)
 
       analyzeAppStagedCore { f, fType, args, mvars, bInfos, forceRegularApp } |>.run' {

tests/lean/439.lean

@@ -1,5 +1,3 @@
-set_option pp.analyze.trustCoe true
-
 universe u
 
 structure Fn (E I : Sort u) := (exp : E) (imp : I)

tests/lean/439.lean.expected.out

@@ -1,15 +1,15 @@
 fn.imp : {p : P} → Bar.fn p
-439.lean:20:7-20:12: error: function expected at
+439.lean:18:7-18:12: error: function expected at
   Fn.imp fn
 term has type
   Bar.fn ?m
-439.lean:31:7-31:11: error: function expected at
+439.lean:29:7-29:11: error: function expected at
   Fn.imp fn
 term has type
   Bar.fn ?m
 Fn.imp fn : Bar.fn p
 Fn.imp fn' Bp : Bar.fn p
-439.lean:41:11-41:12: error: application type mismatch
+439.lean:39:11-39:12: error: application type mismatch
   Fn.imp fn' p
 argument
   p