fix: partial context infos

The previous version of this PR adjusted `withDeclName` to also save the `InfoContext`. This was incorrect because this saved `InfoContext` was not fully complete (e.g. it lacked assignments for metavariables).

The core issue is that we want to save some kind of context while elaborating a term, but cannot meaningfully do so until we are fully done with elaborating the term, lest parts of the saved context may be missing. We already work around this limitation in several other places, e.g. using `Info.updateContext?`, and the parent declaration name is just one more situation where this comes up.

To solve this issue, this commit introduces a notion of `PartialContextInfo` that replaces the `ContextInfo` in `InfoTree.context`. The underlying idea is that while constructing the `InfoTree`, we augment it with `PartialContextInfo`s where it makes sense, and then when traversing over the tree, we merge outer `ContextInfo`s with inner `PartialContextInfo`s (with fields from inner contexts shadowing those of outer context) into `ContextInfo`s to provide all the context that is available up to this point.

The old `ContextInfo` that was added by `liftTermElabM` has been renamed to `CommandContextInfo`.

Another adjustment made in this commit is to remove the incorrect unused variable linter tests checking for unused `where` declarations. `where` declarations are accessible from outside of a definition and should hence not be marked as unused, something that is also fixed by this PR.

src/Lean/Elab/Command.lean

@@ -238,10 +238,11 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArr
   let s ← get
   let scope := s.scopes.head!
   let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
-  return InfoTree.context {
+  let ctx := PartialContextInfo.commandCtx {
     env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace,
     openDecls := scope.openDecls, options := scope.opts, ngen := s.ngen
-  } tree
+  }
+  return InfoTree.context ctx tree
 
 private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
   | []                => withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <| throwError "unexpected syntax{indentD stx}"

src/Lean/Elab/InfoTree/Main.lean

@@ -6,26 +6,25 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Meta.PPGoal
 
-namespace Lean.Elab.ContextInfo
+namespace Lean.Elab.CommandContextInfo
 
-variable [Monad m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] [MonadTermCtx m]
+variable [Monad m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m]
 
-def saveNoFileMap : m ContextInfo := return {
+def saveNoFileMap : m CommandContextInfo := return {
     env           := (← getEnv)
     fileMap       := default
     mctx          := (← getMCtx)
     options       := (← getOptions)
     currNamespace := (← getCurrNamespace)
     openDecls     := (← getOpenDecls)
     ngen          := (← getNGen)
-    parentDecl?   := (← getDeclName?)
   }
 
-def save [MonadFileMap m] : m ContextInfo := do
+def save [MonadFileMap m] : m CommandContextInfo := do
   let ctx ← saveNoFileMap
   return { ctx with fileMap := (← getFileMap) }
 
-end ContextInfo
+end CommandContextInfo
 
 def CompletionInfo.stx : CompletionInfo → Syntax
   | dot i .. => i.stx
@@ -198,7 +197,7 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo
 partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
   match tree with
   | hole id     => return .nestD f!"• ?{toString id.name}"
-  | context i t => format t i
+  | context i t => format t <| i.mergeIntoOuter? ctx?
   | node i cs   => match ctx? with
     | none => return "• <context-not-available>"
     | some ctx =>
@@ -309,20 +308,52 @@ def withInfoTreeContext [MonadFinally m] (x : m α) (mkInfoTree : PersistentArra
 @[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := do
   withInfoTreeContext x (fun trees => do return InfoTree.node (← mkInfo) trees)
 
-/-- Resets the trees state `t₀`, runs `x` to produce a new trees
-state `t₁` and sets the state to be `t₀ ++ (InfoTree.context Γ <$> t₁)`
-where `Γ` is the context derived from the monad state. -/
-def withSaveInfoContext [MonadNameGenerator m] [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadTermCtx m] [MonadFileMap m] (x : m α) : m α := do
-  if (← getInfoState).enabled then
-    let treesSaved ← getResetInfoTrees
-    Prod.fst <$> MonadFinally.tryFinally' x fun _ => do
-      let st    ← getInfoState
-      let trees ← st.trees.mapM fun tree => do
-        let tree := tree.substitute st.assignment
-        pure <| InfoTree.context (← ContextInfo.save) tree
-      modifyInfoTrees fun _ => treesSaved ++ trees
-  else
-    x
+private def withSavedPartialInfoContext [MonadFinally m]
+    (x : m α)
+    (ctx? : m (Option PartialContextInfo))
+    : m α := do
+  if !(← getInfoState).enabled then
+    return ← x
+  let treesSaved ← getResetInfoTrees
+  Prod.fst <$> MonadFinally.tryFinally' x fun _ => do
+    let st    ← getInfoState
+    let trees ← st.trees.mapM fun tree => do
+      let tree := tree.substitute st.assignment
+      match (← ctx?) with
+      | none =>
+        pure tree
+      | some ctx =>
+        pure <| InfoTree.context ctx tree
+    modifyInfoTrees fun _ => treesSaved ++ trees
+
+/--
+Resets the trees state `t₀`, runs `x` to produce a new trees state `t₁` and sets the state to be
+`t₀ ++ (InfoTree.context (PartialContextInfo.commandCtx Γ) <$> t₁)` where `Γ` is the context derived
+from the monad state.
+-/
+def withSaveInfoContext
+    [MonadNameGenerator m]
+    [MonadFinally m]
+    [MonadEnv m]
+    [MonadOptions m]
+    [MonadMCtx m]
+    [MonadResolveName m]
+    [MonadFileMap m]
+    (x : m α)
+    : m α := do
+  withSavedPartialInfoContext x do
+    return some <| .commandCtx (← CommandContextInfo.save)
+
+/--
+Resets the trees state `t₀`, runs `x` to produce a new trees state `t₁` and sets the state to be
+`t₀ ++ (InfoTree.context (PartialContextInfo.parentDeclCtx Γ) <$> t₁)` where `Γ` is the parent decl
+name provided by `MonadParentDecl m`.
+-/
+def withSaveParentDeclInfoContext [MonadFinally m] [MonadParentDecl m] (x : m α) : m α := do
+  withSavedPartialInfoContext x do
+    let some declName ← getParentDeclName?
+      | return none
+    return some <| .parentDeclCtx declName
 
 def getInfoHoleIdAssignment? (mvarId : MVarId) : m (Option InfoTree) :=
   return (← getInfoState).assignment[mvarId]

src/Lean/Elab/InfoTree/Types.lean

@@ -12,19 +12,61 @@ import Lean.Data.Json
 
 namespace Lean.Elab
 
-/-- Context after executing `liftTermElabM`.
-   Note that the term information collected during elaboration may contain metavariables, and their
-   assignments are stored at `mctx`. -/
-structure ContextInfo where
+/--
+Context after executing `liftTermElabM`.
+Note that the term information collected during elaboration may contain metavariables, and their
+assignments are stored at `mctx`.
+-/
+structure CommandContextInfo where
   env           : Environment
   fileMap       : FileMap
   mctx          : MetavarContext := {}
   options       : Options        := {}
   currNamespace : Name           := Name.anonymous
-  parentDecl?   : Option Name    := none
   openDecls     : List OpenDecl  := []
   ngen          : NameGenerator -- We must save the name generator to implement `ContextInfo.runMetaM` and making we not create `MVarId`s used in `mctx`.
 
+/--
+Context from the root of the `InfoTree` up to this node.
+Note that the term information collected during elaboration may contain metavariables, and their
+assignments are stored at `mctx`.
+-/
+structure ContextInfo extends CommandContextInfo where
+  parentDecl? : Option Name := none
+
+/--
+Context for a sub-`InfoTree`.
+
+Within `InfoTree`, this must fulfill the invariant that every non-`commandCtx` `PartialContextInfo`
+node is always contained within a `commandCtx` node.
+-/
+inductive PartialContextInfo where
+  | commandCtx (info : CommandContextInfo)
+  | parentDeclCtx (parentDecl : Name)
+  -- TODO: More constructors for the different kinds of scopes `commandCtx` is currently
+  -- used for (e.g. eliminating `Info.updateContext?` would be nice!).
+
+/--
+Merges the `inner` partial context into the `outer` context s.t. fields of the `inner` context
+overwrite fields of the `outer` context. Panics if the invariant described in the documentation
+for `PartialContextInfo` is violated.
+
+When traversing an `InfoTree`, this function should be used to combine the context of outer
+nodes with the partial context of their subtrees. This ensures that the traversal has the context
+from the inner node to the root node of the `InfoTree` available, with partial contexts of
+inner nodes taking priority over contexts of outer nodes.
+-/
+def PartialContextInfo.mergeIntoOuter?
+    : (inner : PartialContextInfo) → (outer? : Option ContextInfo) → Option ContextInfo
+  | .commandCtx info, none =>
+    some { info with }
+  | .parentDeclCtx _, none =>
+    panic! "Unexpected incomplete InfoTree context info."
+  | .commandCtx innerInfo, some outer =>
+    some { outer with toCommandContextInfo := innerInfo }
+  | .parentDeclCtx innerParentDecl, some outer =>
+    some { outer with parentDecl? := innerParentDecl }
+
 /-- Base structure for `TermInfo`, `CommandInfo` and `TacticInfo`. -/
 structure ElabInfo where
   /-- The name of the elaborator that created this info. -/
@@ -168,8 +210,8 @@ inductive Info where
     `hole`s which are filled in later in the same way that unassigned metavariables are.
 -/
 inductive InfoTree where
-  /-- The context object is created by `liftTermElabM` at `Command.lean` -/
-  | context (i : ContextInfo) (t : InfoTree)
+  /-- The context object is created at appropriate points during elaboration -/
+  | context (i : PartialContextInfo) (t : InfoTree)
   /-- The children contain information for nested term elaboration and tactic evaluation -/
   | node (i : Info) (children : PersistentArray InfoTree)
   /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
@@ -208,9 +250,9 @@ instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
 def setInfoState [MonadInfoTree m] (s : InfoState) : m Unit :=
   modifyInfoState fun _ => s
 
-class MonadTermCtx (m : Type → Type) where
-  getDeclName? : m (Option Name)
+class MonadParentDecl (m : Type → Type) where
+  getParentDeclName? : m (Option Name)
 
-export MonadTermCtx (getDeclName?)
+export MonadParentDecl (getParentDeclName?)
 
 end Lean.Elab

src/Lean/Elab/Tactic/Basic.lean

@@ -51,8 +51,8 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
-instance : MonadTermCtx TacticM where
-  getDeclName? := Term.getDeclName?
+instance : MonadParentDecl TacticM where
+  getParentDeclName? := Term.getDeclName?
 
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals

src/Lean/Elab/Term.lean

@@ -371,12 +371,12 @@ def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecs
 /-- Return the declaration of the given metavariable -/
 def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := return (← getMCtx).getDecl mvarId
 
-instance : MonadTermCtx TermElabM where
-  getDeclName? := getDeclName?
+instance : MonadParentDecl TermElabM where
+  getParentDeclName? := getDeclName?
 
-/-- Execute `withSaveInfoContext x` with `declName? := name`. See `getDeclName?`. -/
+/-- Execute `withSaveParentDeclInfoContext x` with `declName? := name`. See `getDeclName?`. -/
 def withDeclName (name : Name) (x : TermElabM α) : TermElabM α :=
-  withReader (fun ctx => { ctx with declName? := name }) <| withSaveInfoContext x
+  withReader (fun ctx => { ctx with declName? := name }) <| withSaveParentDeclInfoContext x
 
 /-- Update the universe level parameter names. -/
 def setLevelNames (levelNames : List Name) : TermElabM Unit :=

src/Lean/Meta/Basic.lean

@@ -317,9 +317,6 @@ instance : MonadMCtx MetaM where
   getMCtx    := return (← get).mctx
   modifyMCtx f := modify fun s => { s with mctx := f s.mctx }
 
-instance : Elab.MonadTermCtx MetaM where
-  getDeclName? := pure none
-
 instance : MonadEnv MetaM where
   getEnv      := return (← getThe Core.State).env
   modifyEnv f := do modifyThe Core.State fun s => { s with env := f s.env, cache := {} }; modify fun s => { s with cache := {} }

src/Lean/Server/FileWorker.lean

@@ -196,7 +196,7 @@ section Initialization
       (headerMsgLog : MessageLog)
       (opts : Options)
       : Elab.Command.State :=
-    let headerContextInfo : Elab.ContextInfo := {
+    let headerContextInfo : Elab.CommandContextInfo := {
       env     := headerEnv
       fileMap := m.text
       ngen    := { namePrefix := `_worker }
@@ -210,7 +210,7 @@ section Initialization
     let headerInfoTree := Elab.InfoTree.node headerInfo headerInfoNodes.toPArray'
     let headerInfoState := {
       enabled := true
-      trees := #[Elab.InfoTree.context headerContextInfo headerInfoTree].toPArray'
+      trees := #[Elab.InfoTree.context (.commandCtx headerContextInfo) headerInfoTree].toPArray'
     }
     { Elab.Command.mkState headerEnv headerMsgLog opts with infoState := headerInfoState }
 

src/Lean/Server/InfoUtils.lean

@@ -35,14 +35,15 @@ structure InfoWithCtx where
   info : Elab.Info
   children : PersistentArray InfoTree
 
-/-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/
+/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
+and accumulating results on the way back up. -/
 partial def InfoTree.visitM [Monad m]
     (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
     : InfoTree → m (Option α) :=
   go none
 where go
-  | _, context ctx t => go ctx t
+  | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
   | some ctx, node i cs => do
     preNode ctx i cs
     let as ← cs.toList.mapM (go <| i.updateContext? ctx)
@@ -77,7 +78,7 @@ partial def InfoTree.deepestNodes (p : ContextInfo → Info → PersistentArray
 partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
   go none init
 where go ctx? a
-  | context ctx t => go ctx a t
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
   | node i ts =>
     let a := match ctx? with
       | none => a
@@ -367,7 +368,7 @@ partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option
 partial def InfoTree.hasSorry : InfoTree → IO Bool :=
   go none
 where go ci?
-  | .context ci t => go ci t
+  | .context ci t => go (ci.mergeIntoOuter? ci?) t
   | .node i cs =>
     if let (some ci, .ofTermInfo ti) := (ci?, i) then do
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)

src/Lean/Widget/InteractiveGoal.lean

@@ -191,7 +191,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId

tests/lean/linterUnusedVariables.lean

@@ -23,10 +23,10 @@ def usedAndUnusedVariables : Nat :=
     3
   x
 
-def unusedWhereVariable : Nat :=
+def whereVariable : Nat :=
   3
 where
-  x := 5
+  x := 5 -- x is globally available via `whereVariable.x`
 
 def unusedWhereArgument : Nat :=
   f 2

tests/lean/linterUnusedVariables.lean.expected.out

@@ -1,9 +1,7 @@
 linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables]
 linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
 linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]