`Lean.exprDependsOn'` does not take into account delayed assignments.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean.exprDependsOn' does not take into account delayed assignments, and so may miss dependencies.

This was originally noticed because of a bug in library_search that came down to this issue. However I've changed the implementation there in the meantime (to use Meta.getMVars, which correctly accounts for delayed assignments), so this issue is not holding up anything for library_search.

Steps to Reproduce

Apologies for the long test case

import Lean

open Lean Meta Elab Term Tactic

/-- Check if a goal is of a subsingleton type. -/
def Lean.MVarId.subsingleton? (g : MVarId) : MetaM Bool := do
  try
    _ ← Lean.Meta.synthInstance (← mkAppM `Subsingleton #[← g.getType])
    return true
  catch _ =>
    return false

/--
Check if a goal is "independent" of a list of other goals.
We say a goal is independent of other goals if assigning a value to it
can not change the solvability of the other goals.

This function only calculates a conservative approximation of this condition.
-/
def Lean.MVarId.independent? (L : List MVarId) (g : MVarId) : MetaM Bool := do
  let t ← instantiateMVars (← g.getType)
  if t.hasExprMVar then
    -- If the goal's type contains other meta-variables,
    -- we conservatively say that `g` is not independent.
    return false
  if t.isProp then
    -- If the goal is propositional,
    -- proof-irrelevance should ensure it is independent of any other goals.
    return true
  if ← g.subsingleton? then
    -- If the goal is a subsingleton, it should be independent of any other goals.
    return true
  -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
  let r ← L.allM fun g' => do
    let t' ← instantiateMVars (← g'.getType)
    pure <| !(← exprDependsOn' t' (.mvar g))
  return r

unsafe def evalTacticMUnsafe (stx : Syntax) : TermElabM (TacticM Unit) :=
  evalTerm (TacticM Unit) (mkApp (mkConst ``TacticM) (mkConst ``Unit)) stx

@[implemented_by evalTacticMUnsafe]
opaque evalTacticM (stx : Syntax) : TermElabM (TacticM Unit)

/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
elab (name := runTac) "run_tac " e:doSeq : tactic => do
  ← evalTacticM (← `(discard do $e))

example : Σ α, Option α := by
  constructor
  -- Goals are `?fst : Type` and `?snd : Option ?fst`.
  -- Correctly, `independent?` claims neither is independent.
  -- (`?snd` because its type contains a metavariable, and `?fst` because `?snd`'s type depends on it)
  run_tac do
    let gs ← getGoals
    for g in gs do
      guard ! (← g.independent? gs)
  exact some 0

example : Σ α, Option α := by
  constructor
  -- Now we introduce a hypothesis in the second goal,
  -- thereby introducing a delayed assignment.
  rotate_left
  have := 0
  rotate_left
  -- Now `independent?` incorrectly thinks `?fst` is independent.
  run_tac do
    let gs ← getGoals
    for g in gs do
      guard ! (← g.independent? gs) <|> throwError m!"{← g.getType} was incorrectly considered independent!"
  exact some 0

This can be fixed by changing the .mvar section of Lean.dependsOn.visitMain to

      | .mvar mvarId     => do
        match (← getExprMVarAssignment? mvarId) with
        | some a => visit a
        | none   =>
          if pm mvarId then
            return true
          else
            match ← getDelayedMVarAssignment? mvarId with
            | some d => visit (.mvar d.mvarIdPending)
            | none =>
              let lctx := (← getMCtx).getDecl mvarId |>.lctx
              return lctx.any fun decl => pf decl.fvarId

I'll make a draft PR of this change, but I'm worried that this change has effects that I'm not anticipating so would appreciate a skeptical review.

Start at the .mvar branch of Lean.dependsOn.visitMain and run the self-contained reproduction in the issue. Trace how delayed assignments are represented and checked, then verify that dependency detection handles them and that the reproduction no longer reports a false independence result.