feat: pp.instances and pp.instanceTypes

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -136,10 +136,14 @@ def delabConst : Delab := do
 
   maybeAddBlockImplicit stx
 
-inductive ParamKind where
-  | explicit
-  -- combines implicit params, optParams, and autoParams
-  | implicit (name : Name) (defVal : Option Expr)
+structure ParamKind where
+  name        : Name
+  bInfo       : BinderInfo
+  defVal      : Option Expr := none
+  isAutoParam : Bool := false
+
+def ParamKind.isRegularExplicit (param : ParamKind) : Bool :=
+  param.bInfo.isExplicit && !param.isAutoParam && param.defVal.isNone
 
 /-- Return array with n-th element set to kind of n-th parameter of `e`. -/
 partial def getParamKinds : DelabM (Array ParamKind) := do
@@ -149,13 +153,7 @@ partial def getParamKinds : DelabM (Array ParamKind) := do
       forallTelescopeArgs e.getAppFn e.getAppArgs fun params _ => do
         params.mapM fun param => do
           let l ← getLocalDecl param.fvarId!
-          match l.type.getOptParamDefault? with
-          | some val => pure $ ParamKind.implicit l.userName val
-          | _ =>
-            if l.type.isAutoParam || !l.binderInfo.isExplicit then
-              pure $ ParamKind.implicit l.userName none
-            else
-              pure ParamKind.explicit
+          pure { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
   catch _ => pure #[] -- recall that expr may be nonsensical
 where
   forallTelescopeArgs f args k := do
@@ -170,16 +168,26 @@ where
 @[builtinDelab app]
 def delabAppExplicit : Delab := whenPPOption getPPExplicit do
   let paramKinds ← getParamKinds
-  let (fnStx, argStxs) ← withAppFnArgs
+  let (fnStx, _, argStxs) ← withAppFnArgs
     (do
       let fn ← getExpr
       let stx ← if fn.isConst then delabConst else delab
-      let needsExplicit := paramKinds.any (fun | ParamKind.explicit => false | _ => true) && stx.getKind != `Lean.Parser.Term.explicit
+      let needsExplicit := paramKinds.any (fun param => !param.isRegularExplicit) && stx.getKind != `Lean.Parser.Term.explicit
       let stx ← if needsExplicit then `(@$stx) else pure stx
-      pure (stx, #[]))
-    (fun ⟨fnStx, argStxs⟩ => do
-      let argStx ← if ← getPPOption getPPAnalysisHole then `(_) else delab
-      pure (fnStx, argStxs.push argStx))
+      pure (stx, paramKinds.toList, #[]))
+    (fun ⟨fnStx, paramKinds, argStxs⟩ => do
+      let isInstImplicit := match paramKinds with
+                            | [] => false
+                            | param :: _ => param.bInfo == BinderInfo.instImplicit
+      let argStx ← if ← getPPOption getPPAnalysisHole then `(_)
+                   else if isInstImplicit == true then
+                     let stx ← if ← getPPOption getPPInstances then delab else `(_)
+                     if ← getPPOption getPPInstanceTypes then
+                       let typeStx ← withType delab
+                       `(($stx : $typeStx))
+                     else stx
+                   else delab
+      pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
   Syntax.mkApp fnStx argStxs
 
 def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
@@ -252,7 +260,7 @@ def delabAppImplicit : Delab := do
   -- TODO: always call the unexpanders, make them guard on the right # args?
   let paramKinds ← getParamKinds
   if ← getPPOption getPPExplicit then
-    if paramKinds.any (fun | ParamKind.explicit => false | _ => true) then failure
+    if paramKinds.any (fun param => !param.isRegularExplicit) then failure
 
   let (fnStx, _, argStxs) ← withAppFnArgs
     (do
@@ -269,13 +277,14 @@ def delabAppImplicit : Delab := do
         else if ← getPPOption getPPAnalysisHole then `(_)
         else
           match paramKinds with
-          | [ParamKind.implicit _ (some v)] =>
-            if !v.hasLooseBVars && v == arg then none else delab
-          | ParamKind.implicit name none :: _  =>
-            if ← getPPOption getPPAnalysisNamedArg <||> (name == `motive <&&> shouldShowMotive arg opts)
-            then mkNamedArg name (← delab)
-            else none
-          | _ => delab
+          | [] => delab
+          | param :: rest =>
+            if param.defVal.isSome && rest.isEmpty then
+              let v := param.defVal.get!
+              if !v.hasLooseBVars && v == arg then none else delab
+            else if !param.isRegularExplicit && param.defVal.isNone then
+              if ← getPPOption getPPAnalysisNamedArg <||> (param.name == `motive <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else none
+            else delab
       let argStxs := match argStx? with
         | none => argStxs
         | some stx => argStxs.push stx

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -95,6 +95,16 @@ register_builtin_option pp.proofs.withType : Bool := {
   group    := "pp"
   descr    := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"
 }
+register_builtin_option pp.instances : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) if set to false, replace inst-implicit arguments to explicit applications with placeholders"
+}
+register_builtin_option pp.instanceTypes : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) when printing explicit applications, show the types of inst-implicit arguments"
+}
 register_builtin_option pp.motives.pi : Bool := {
   defValue := true
   group    := "pp"
@@ -174,5 +184,7 @@ def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp
 def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue
 def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue
 def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue
+def getPPInstances (o : Options) : Bool := o.get pp.instances.name pp.instances.defValue
+def getPPInstanceTypes (o : Options) : Bool := o.get pp.instanceTypes.name pp.instanceTypes.defValue
 
 end Lean

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -539,7 +539,10 @@ mutual
             -- Note: apparently checking valUnknown here is not sound, because the elaborator
             -- will not happily assign instImplicits that it cannot synthesize
             let mut provided := true
-            if getPPAnalyzeCheckInstances (← getOptions) then
+            if !getPPInstances (← getOptions) then
+              annotateBool `pp.analysis.skip
+              provided := false
+            else if getPPAnalyzeCheckInstances (← getOptions) then
               let instResult ← try trySynthInstance argType catch _ => LOption.undef
               match instResult with
               | LOption.some inst =>
@@ -548,7 +551,7 @@ mutual
               | _                 => annotateNamedArg (← mvarName mvars[i])
             else provided := false
             modify fun s => { s with provideds := s.provideds.set! i provided }
-          | BinderInfo.auxDecl        => pure ()
+          | BinderInfo.auxDecl => pure ()
           if (← get).provideds[i] then withKnowing (not (← typeUnknown mvars[i])) true analyze
           tryUnify mvars[i] args[i]
 
@@ -559,6 +562,8 @@ mutual
         for i in [:args.size] do
           if !(← get).provideds[i] then
             withNaryArg (f.getAppNumArgs + i) do annotateBool `pp.analysis.hole
+          if bInfos[i] == BinderInfo.instImplicit && getPPInstanceTypes (← getOptions) then
+            withType (withKnowing true false analyze)
 
 end
 

tests/lean/PPInstances.lean

@@ -0,0 +1,45 @@
+class Semiring (α : Type) where add : α → α → α
+class Ring (α : Type) where add : α → α → α
+
+class AddCommMonoid (α : Type) where
+class AddCommGroup (α : Type) where
+
+class Module (α β : Type) [Semiring α] [AddCommMonoid β] where
+
+class NormedField (α : Type) where
+  add : α → α → α
+  add_comm  : ∀ (x y : α), @Add.add _ ⟨add⟩ x y = @Add.add _ ⟨add⟩ y x
+
+class SemiNormedGroup (α : Type) where
+class SemiNormedSpace (α β : Type) [NormedField α] [SemiNormedGroup β] where
+
+instance SemiNormedGroup.toAddCommMonoid [SemiNormedGroup α] : AddCommMonoid α := {}
+instance Ring.toSemiring [instR : Ring α] : Semiring α := { add := instR.add }
+instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := instNF.add }
+
+instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {}
+
+constant R : Type := Unit
+constant foo (a b : R) : R := a
+
+instance R.NormedField : NormedField R := { add := foo, add_comm := sorry }
+instance R.Ring : Ring R := { add := foo }
+
+variable {E : Type} [instSNG : SemiNormedGroup E] [instSNS : SemiNormedSpace R E]
+
+set_option pp.all true
+set_option pp.instances false in
+set_option pp.instanceTypes false in
+#check Module R E
+
+set_option pp.instances false in
+set_option pp.instanceTypes true in
+#check Module R E
+
+set_option pp.instances true in
+set_option pp.instanceTypes false in
+#check Module R E
+
+set_option pp.instances true in
+set_option pp.instanceTypes true in
+#check Module R E

tests/lean/PPInstances.lean.expected.out

@@ -0,0 +1,6 @@
+PPInstances.lean:25:68-25:73: warning: declaration uses 'sorry'
+@Module R E _ _ : Type
+@Module R E (_ : Semiring R) (_ : AddCommMonoid E) : Type
+@Module R E (@Ring.toSemiring R R.Ring) (@SemiNormedGroup.toAddCommMonoid E instSNG) : Type
+@Module R E (@Ring.toSemiring R (R.Ring : Ring R) : Semiring R)
+  (@SemiNormedGroup.toAddCommMonoid E (instSNG : SemiNormedGroup E) : AddCommMonoid E) : Type