feat: add @ to consts/locals with pi {..} type

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -14,15 +14,18 @@ open Lean.Meta
 open Lean.Parser.Term
 open SubExpr
 
+def maybeAddExplicit (ident : Syntax) : DelabM Syntax := do
+  if ← getPPOption getPPAnalysisNeedsExplicit then `(@$ident:ident) else ident
+
 @[builtinDelab fvar]
 def delabFVar : Delab := do
 let Expr.fvar id _ ← getExpr | unreachable!
 try
   let l ← getLocalDecl id
-  pure $ mkIdent l.userName
+  maybeAddExplicit (mkIdent l.userName)
 catch _ =>
   -- loose free variable, use internal name
-  pure $ mkIdent id
+  maybeAddExplicit $ mkIdent id
 
 -- loose bound variable, use pseudo syntax
 @[builtinDelab bvar]
@@ -113,17 +116,21 @@ def delabConst : Delab := do
     c := (privateToUserName? c).getD c
 
   let ppUnivs ← getPPOption getPPUniverses
-  if ls.isEmpty || !ppUnivs then
-    if (← getLCtx).usesUserName c then
-      -- `c` is also a local declaration
-      if c == c₀ && !(← read).inPattern then
-        -- `c` is the fully qualified named. So, we append the `_root_` prefix
-        c := `_root_ ++ c
-      else
-        c := c₀
-    return mkIdent c
-  else
-    `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+
+  let stx ←
+    if ls.isEmpty || !ppUnivs then
+      if (← getLCtx).usesUserName c then
+        -- `c` is also a local declaration
+        if c == c₀ && !(← read).inPattern then
+          -- `c` is the fully qualified named. So, we append the `_root_` prefix
+          c := `_root_ ++ c
+        else
+          c := c₀
+      return mkIdent c
+    else
+      `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+
+    maybeAddExplicit stx
 
 inductive ParamKind where
   | explicit

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -67,11 +67,12 @@ 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 getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownFOType2TypeHOFuns.name pp.analyze.trustKnownFOType2TypeHOFuns.defValue
 
-def getPPAnalysisSkip        (o : Options) : Bool := o.get `pp.analysis.skip false
-def getPPAnalysisHole        (o : Options) : Bool := o.get `pp.analysis.hole false
-def getPPAnalysisNamedArg    (o : Options) : Bool := o.get `pp.analysis.namedArg false
-def getPPAnalysisLetVarType  (o : Options) : Bool := o.get `pp.analysis.letVarType true
-def getPPAnalysisNeedsType   (o : Options) : Bool := o.get `pp.analysis.needsType false
+def getPPAnalysisSkip          (o : Options) : Bool := o.get `pp.analysis.skip false
+def getPPAnalysisHole          (o : Options) : Bool := o.get `pp.analysis.hole false
+def getPPAnalysisNamedArg      (o : Options) : Bool := o.get `pp.analysis.namedArg false
+def getPPAnalysisLetVarType    (o : Options) : Bool := o.get `pp.analysis.letVarType true
+def getPPAnalysisNeedsType     (o : Options) : Bool := o.get `pp.analysis.needsType false
+def getPPAnalysisNeedsExplicit (o : Options) : Bool := o.get `pp.analysis.needsExplicit false
 
 namespace PrettyPrinter.Delaborator
 
@@ -197,9 +198,10 @@ def isSubstLike (e : Expr) : Bool :=
 open SubExpr
 
 structure Context where
-  knowsType  : Bool
-  knowsLevel : Bool -- only constants look at this
-  inBottomUp : Bool := false
+  knowsType   : Bool
+  knowsLevel  : Bool -- only constants look at this
+  inBottomUp  : Bool := false
+  parentIsApp : Bool := false
   deriving Inhabited, Repr
 
 structure State where
@@ -227,22 +229,23 @@ def annotateName (n : Name) (v : Name) : AnalyzeM Unit := do
   let opts := (← get).annotations.findD pos {} |>.setName n v
   modify fun s => { s with annotations := s.annotations.insert pos opts }
 
-partial def analyze : AnalyzeM Unit := do
+partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do
   checkMaxHeartbeats "Delaborator.topDownAnalyze"
   trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel} {← getExpr}"
-  match (← getExpr) with
-  | Expr.app ..     => analyzeApp
-  | Expr.forallE .. => analyzePi
-  | Expr.lam ..     => analyzeLam
-  | Expr.const ..   => analyzeConst
-  | Expr.sort ..    => analyzeSort
-  | Expr.proj ..    => analyzeProj
-  | Expr.fvar ..    => analyzeFVar
-  | Expr.mdata ..   => analyzeMData
-  | Expr.letE ..    => analyzeLet
-  | Expr.lit ..     => pure ()
-  | Expr.mvar ..    => pure ()
-  | Expr.bvar ..    => unreachable!
+  withReader (fun ctx => { ctx with parentIsApp := parentIsApp }) do
+    match (← getExpr) with
+    | Expr.app ..     => analyzeApp
+    | Expr.forallE .. => analyzePi
+    | Expr.lam ..     => analyzeLam
+    | Expr.const ..   => analyzeConst
+    | Expr.sort ..    => analyzeSort
+    | Expr.proj ..    => analyzeProj
+    | Expr.fvar ..    => analyzeFVar
+    | Expr.mdata ..   => analyzeMData
+    | Expr.letE ..    => analyzeLet
+    | Expr.lit ..     => pure ()
+    | Expr.mvar ..    => pure ()
+    | Expr.bvar ..    => unreachable!
 where
   analyzeApp := do
     withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
@@ -283,7 +286,7 @@ where
       higherOrders := higherOrders.set! i true
 
     -- Now, if this is the first staging, analyze the n-ary function without expected type
-    if !f.isApp then withKnowing false !(← instantiateMVars fType).hasLevelMVar $ withNaryFn analyze
+    if !f.isApp then withKnowing false !(← instantiateMVars fType).hasLevelMVar $ withNaryFn (analyze (parentIsApp := true))
 
     let disableNamedImplicits : Bool := getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr)
 
@@ -316,11 +319,19 @@ where
 
       if not rest.isEmpty then analyzeAppStaged (mkAppN f args) rest
 
+  maybeAddExplicit : AnalyzeM Unit := do
+    -- See `MonadLift.noConfusion for an example where this is necessary.
+    if !(← read).parentIsApp then
+      let type ← inferType (← getExpr)
+      if type.isForall && type.bindingInfo! == BinderInfo.implicit then
+        annotateBool `pp.analysis.needsExplicit true
+
   analyzeConst : AnalyzeM Unit := do
-    -- TODO: currently, the analyzer never uses @,
+    -- TODO: currently, the analyzer never uses @ for applications,
     -- even though named arguments do not work for inaccessible names
     let Expr.const n ls .. ← getExpr | unreachable!
     annotateBool `pp.universes (!(← read).knowsLevel && !ls.isEmpty)
+    maybeAddExplicit
 
   analyzePi : AnalyzeM Unit := do
     annotateBool `pp.binderTypes true
@@ -342,7 +353,7 @@ where
 
   analyzeSort  : AnalyzeM Unit := pure ()
   analyzeProj  : AnalyzeM Unit := withProj analyze
-  analyzeFVar  : AnalyzeM Unit := pure ()
+  analyzeFVar  : AnalyzeM Unit := maybeAddExplicit
   analyzeMData : AnalyzeM Unit := withMDataExpr analyze
 
   valUnknown (e : Expr) : AnalyzeM Bool := do

tests/lean/run/PPTopDownAnalyze.lean

@@ -223,6 +223,10 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 #testDelabN Lean.Syntax.getOptionalIdent?
 #testDelabN Lean.Meta.ppExpr
 #testDelabN Eq.mprProp
+#testDelabN MonadLift.noConfusion
+#testDelabN MonadLift.noConfusionType
+#testDelabN MonadExcept.noConfusion
+#testDelabN MonadFinally.noConfusion
 
 -- TODO: this test is broken because of the inability to solve structural max constraints
 -- (See https://github.com/leanprover/lean4/issues/590)
@@ -234,11 +238,5 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 -- #testDelabN Std.ShareCommon.ObjectMap.find?
 -- #testDelabN Std.ShareCommon.ObjectMap.insert
 
--- TODO: these all fail currently because of implicit lambdas
--- #testDelabN MonadLift.noConfusion
--- #testDelabN MonadLift.noConfusionType
--- #testDelabN MonadExcept.noConfusion
--- #testDelabN MonadFinally.noConfusion
-
 -- TODO: these fail because we are not disable named patterns when not using `match` syntax
 -- #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1