fix: some ExtraModUses

src/Lean/Elab/Command.lean

@@ -599,7 +599,6 @@ macro expansion etc.
 def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
   withReader ({ · with suppressElabErrors :=
     stx.hasMissing && !showPartialSyntaxErrors.get (← getOptions) }) do
-  recordUsedSyntaxKinds stx
   -- initialize quotation context using hash of input string
   let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false)
   withInitQuotContext (ss?.map (hash ·.toString.trim)) do
@@ -612,6 +611,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       -- `end` command of the `in` macro would be skipped and the option would be leaked to the outside!
       elabCommand stx
     finally
+      -- This call could be placed at a prior point in this function except that it
+      -- would then record uses of `#guard_msgs` before that elaborator is run, which
+      -- would increase noise in related tests. Thus all other things being equal, we
+      -- place it here.
+      recordUsedSyntaxKinds stx
       -- Make sure `snap?` is definitely resolved; we do not use it for reporting as `#guard_msgs` may
       -- be the caller of this function and add new messages and info trees
       if let some snap := (← read).snap? then

src/Lean/Elab/ErrorExplanation.lean

@@ -101,11 +101,12 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do
 open Command in
 @[builtin_command_elab registerErrorExplanationStx] def elabRegisterErrorExplanation : CommandElab
 | `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
-  unless (← getEnv).contains ``Lean.ErrorExplanation do
+  unless (← getEnv).contains ``ErrorExplanation.Metadata do
     throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
+  recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
   let tp := mkConst ``ErrorExplanation.Metadata
   let metadata ← runTermElabM <| fun _ => unsafe do
-    let e ← elabTerm t tp
+    let e ← elabTermEnsuringType t tp
     if e.hasSyntheticSorry then throwAbortTerm
     evalExpr ErrorExplanation.Metadata tp e
   let name := id.getId

src/Lean/Elab/Quotation.lean

@@ -134,6 +134,8 @@ private partial def quoteSyntax : Syntax → TermElabM Term
     -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
     -- See the paper for details.
     let consts ← resolveGlobalName val
+    -- Record all constants to make sure they can still be resolved after shaking imports
+    consts.forM fun (n, _) => recordExtraModUseFromDecl (isMeta := false) n
     -- extension of the paper algorithm: also store unique section variable names as top-level scopes
     -- so they can be captured and used inside the section, but not outside
     let sectionVars := resolveSectionVariable (← read).sectionVars val

src/Lean/Elab/Syntax.lean

@@ -94,6 +94,7 @@ def elabParserName? (stx : Syntax.Ident) (checkMeta := true) : TermElabM (Option
   | [n@(.parser parser _)] =>
     if checkMeta && getIRPhases (← getEnv) parser == .runtime then
       throwError m!"Declaration `{.ofConstName parser}` must be marked or imported as `meta` to be used as parser"
+    recordExtraModUseFromDecl (isMeta := true) parser
     addTermInfo' stx (Lean.mkConst parser)
     return n
   | [n@(.alias _)] =>

src/Lean/Elab/Util.lean

@@ -122,8 +122,10 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa
     evalKey       := fun _ stx => do
       let kind ← syntaxNodeKindOfAttrParam parserNamespace stx
       /- Recall that a `SyntaxNodeKind` is often the name of the parser, but this is not always true, and we must check it. -/
-      if (← getEnv).contains kind && (← getInfoState).enabled then
-        addConstInfo stx[1] kind none
+      if (← getEnv).contains kind then
+        recordExtraModUseFromDecl (isMeta := false) kind
+        if (← getInfoState).enabled then
+          addConstInfo stx[1] kind none
       return kind
     onAdded       := fun builtin declName kind => do
       if builtin then

src/Lean/KeyedDeclsAttribute.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.ScopedEnvExtension
 import Lean.Compiler.InitAttr
 import Lean.Compiler.IR.CompilerM
+import Lean.ExtraModUses
 
 public section
 
@@ -43,8 +44,10 @@ structure Def (γ : Type) where
   evalKey (builtin : Bool) (stx : Syntax) : AttrM Key := private_decl% (do
     let stx ← Attribute.Builtin.getIdent stx
     let kind := stx.getId
-    if (← getEnv).contains kind && (← Elab.getInfoState).enabled then
-      Elab.addConstInfo stx kind none
+    if (← getEnv).contains kind then
+      recordExtraModUseFromDecl (isMeta := false) kind
+      if (← Elab.getInfoState).enabled then
+        Elab.addConstInfo stx kind none
     pure kind)
   onAdded (builtin : Bool) (declName : Name) (key : Key) : AttrM Unit := pure ()
   deriving Inhabited

src/Lean/Linter/MissingDocs.lean

@@ -95,6 +95,7 @@ builtin_initialize
       let decl ← getConstInfo declName
       let fnNameStx ← Attribute.Builtin.getIdent stx
       let key ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
+      recordExtraModUseFromDecl (isMeta := false) key
       unless decl.levelParams.isEmpty && (decl.type == .const ``Handler [] || decl.type == .const ``SimpleHandler []) do
         throwError m!"Unexpected type for missing docs handler: Expected `{.ofConstName ``Handler}` or \
           `{.ofConstName ``SimpleHandler}`, but `{declName}` has type{indentExpr decl.type}"

src/Lean/Meta/Coe.lean

@@ -33,6 +33,15 @@ coercions.
 def isCoeDecl (env : Environment) (declName : Name) : Bool :=
   coeDeclAttr.hasTag env declName
 
+/-- Recurse through projection functions (e.g. `(f a b c).fst.snd` => `f`) -/
+private partial def recProjTarget (e : Expr) (nm : Name := e.getAppFn.constName!) : MetaM Name := do
+  let some info ← getProjectionFnInfo? nm | return nm
+  let target := e.getArgD info.numParams (.sort .zero)
+  if target.getAppFn.isConst then
+    recProjTarget target
+  else
+    return nm
+
 /-- Expand coercions occurring in `e` -/
 partial def expandCoe (e : Expr) : MetaM Expr :=
   withReducibleAndInstances do
@@ -41,11 +50,13 @@ partial def expandCoe (e : Expr) : MetaM Expr :=
       if f.isConst then
         let declName := f.constName!
         if isCoeDecl (← getEnv) declName then
-          for arg in e.getAppArgs do
-            -- The following should record at least the top-level instance as a dependency, which
-            -- appears to be good enough for now.
-            if let .const n .. := arg then
-              recordExtraModUseFromDecl (isMeta := false) n
+          /-
+          Unfolding an instance projection corresponds to unfolding the target of the projection
+          (and then reducing the projection). Thus we can recursively visit projections before
+          recording the declaration. We shouldn't need to record any other arguments because they
+          should still appear after unfolding (unless there are unused variables in the instances).
+          -/
+          recordExtraModUseFromDecl (isMeta := false) (← recProjTarget e)
           if let some e ← unfoldDefinition? e then
             return .visit e.headBeta
       return .continue

src/Lean/Parser/Tactic/Doc.lean

@@ -12,6 +12,7 @@ import Lean.DocString.Extension
 import Lean.Elab.InfoTree.Main
 meta import Lean.Parser.Attr
 import Lean.Parser.Extension
+import Lean.ExtraModUses
 
 public section
 
@@ -80,6 +81,7 @@ builtin_initialize
         | throwError "Invalid `[{name}]` attribute syntax"
 
       let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
+      recordExtraModUseFromDecl (isMeta := false) tgtName
 
       if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "`{tgtName}` is not a tactic"
       -- If the target is a known syntax kind, ensure that it's a tactic

src/Lean/ParserCompiler/Attribute.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Attributes
 public import Lean.Compiler.InitAttr
 public import Lean.ToExpr
+import Lean.ExtraModUses
 
 public section
 
@@ -35,6 +36,7 @@ def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by
     add   := fun decl stx _ => do
       let env ← getEnv
       let parserDeclName ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      recordExtraModUseFromDecl (isMeta := false) parserDeclName
       setEnv <| ext.addEntry env (parserDeclName, decl)
   }
   registerBuiltinAttribute attrImpl

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -13,6 +13,7 @@ public import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 import Lean.Elab.InfoTree.Main
 meta import Init.Data.String.Basic
 meta import Init.Data.ToString.Name
+import Lean.ExtraModUses
 
 public section
 
@@ -120,6 +121,7 @@ unsafe builtin_initialize delabAttribute : KeyedDeclsAttribute Delab ←
       if (← Elab.getInfoState).enabled && kind.getRoot == `app then
         let c := kind.replacePrefix `app .anonymous
         if (← getEnv).contains c then
+          recordExtraModUseFromDecl (isMeta := false) c
           Elab.addConstInfo stx c none
       pure kind
   }
@@ -470,7 +472,9 @@ unsafe builtin_initialize appUnexpanderAttribute : KeyedDeclsAttribute Unexpande
     descr := "Register an unexpander for applications of a given constant.",
     valueTypeName := `Lean.PrettyPrinter.Unexpander
     evalKey := fun _ stx => do
-      Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      let id ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      recordExtraModUseFromDecl (isMeta := false) id
+      return id
   }
 
 end Delaborator

src/Lean/PrettyPrinter/Formatter.lean

@@ -13,6 +13,7 @@ public import Lean.KeyedDeclsAttribute
 public import Lean.ParserCompiler.Attribute
 public import Lean.PrettyPrinter.Basic
 public import Lean.PrettyPrinter.Delaborator.Options
+import Lean.ExtraModUses
 
 public section
 
@@ -84,8 +85,10 @@ unsafe builtin_initialize formatterAttribute : KeyedDeclsAttribute Formatter ←
       -- synthesize a formatter for it immediately, so we just check for a declaration in this case
       unless (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id do
         throwError "Invalid `[formatter]` argument: Unknown syntax kind `{id}`"
-      if (← getEnv).contains id && (← Elab.getInfoState).enabled then
-        Elab.addConstInfo stx id none
+      if (← getEnv).contains id then
+        recordExtraModUseFromDecl (isMeta := false) id
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx id none
       pure id
   }
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -11,6 +11,7 @@ public import Lean.Parser.StrInterpolation
 public import Lean.ParserCompiler.Attribute
 public import Lean.PrettyPrinter.Basic
 public import Lean.PrettyPrinter.Delaborator.Options
+import Lean.ExtraModUses
 
 public section
 
@@ -139,8 +140,10 @@ unsafe builtin_initialize parenthesizerAttribute : KeyedDeclsAttribute Parenthes
       -- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
       unless (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id do
         throwError "Invalid `[parenthesizer]` argument: Unknown syntax kind `{id}`"
-      if (← getEnv).contains id && (← Elab.getInfoState).enabled then
-        Elab.addConstInfo stx id none
+      if (← getEnv).contains id then
+        recordExtraModUseFromDecl (isMeta := false) id
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx id none
       pure id
   }
 
@@ -168,8 +171,10 @@ unsafe builtin_initialize categoryParenthesizerAttribute : KeyedDeclsAttribute C
       let id := stx.getId
       let some cat := (Parser.parserExtension.getState env).categories.find? id
         | throwError "Invalid `[category_parenthesizer]` argument: Unknown parser category `{toString id}`"
-      if (← Elab.getInfoState).enabled && (← getEnv).contains cat.declName then
-        Elab.addConstInfo stx cat.declName none
+      if (← getEnv).contains cat.declName then
+        recordExtraModUseFromDecl (isMeta := false) cat.declName
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx cat.declName none
       pure id
   }
 

src/Lean/Server/CodeActions/Attr.lean

@@ -127,6 +127,7 @@ builtin_initialize
       let `(attr| command_code_action $args*) := stx | return
       let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      args.forM (recordExtraModUseFromDecl (isMeta := false))
       modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
   }