From acfc11ae425cecd4be1344387e1606e0d7acaec5 Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Mon, 10 Mar 2025 14:13:48 -0400
Subject: [PATCH] fix: correctly collect let-rec fvars through delayed-assigned
 mvar (#7304)

This PR fixes an issue where nested `let rec` declarations within
`match` expressions or tactic blocks failed to compile if they were
nested within, and recursively called, a `let rec` that referenced a
variable bound by a containing declaration.

Closes #6927

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
---
 src/Lean/Elab/MutualDef.lean | 50 +++++++++++++++++--
 tests/lean/run/6927.lean     | 93 ++++++++++++++++++++++++++++++++++++
 2 files changed, 138 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/6927.lean

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index e7fd345c45..a7de0e8de7 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -614,16 +614,26 @@ private def mkInitialUsedFVarsMap [Monad m] [MonadMCtx m] (sectionVars : Array E
   for mainFVarId in mainFVarIds do
     usedFVarMap := usedFVarMap.insert mainFVarId sectionVarSet
   for toLift in letRecsToLift do
-    let state := Lean.collectFVars {} toLift.val
-    let state := Lean.collectFVars state toLift.type
-    let mut set := state.fvarSet
+    let mut state := Lean.collectFVars {} toLift.val
+    state := Lean.collectFVars state toLift.type
+    let mut set := {}
     /- toLift.val may contain metavariables that are placeholders for nested let-recs. We should collect the fvarId
        for the associated let-rec because we need this information to compute the fixpoint later. -/
     let mvarIds := (toLift.val.collectMVars {}).result
     for mvarId in mvarIds do
-      match (← letRecsToLift.findSomeM? fun (toLift : LetRecToLift) => return if toLift.mvarId == (← getDelayedMVarRoot mvarId) then some toLift.fvarId else none) with
+      let root ← getDelayedMVarRoot mvarId
+      match letRecsToLift.findSome? fun (toLift : LetRecToLift) => if toLift.mvarId == root then some toLift.fvarId else none with
       | some fvarId => set := set.insert fvarId
-      | none        => pure ()
+      | none        =>
+        /- If the metavariable is not a nested let-rec, it may contribute additional free-variable
+           dependencies not caught in the fixed-point routine. In particular, delayed assignments
+           due to `match` expressions or tactic blocks induce fvar dependencies that we need to
+           account for (see #6927) but cannot ascertain through instantiation if those expressions
+           contain still-unassigned metavariable placeholders for other let-recs. See Note
+           [Delayed-Assigned Metavariables in Free Variable Collection] for more information. -/
+        let some rootAssignment ← getExprMVarAssignment? root | continue
+        state := Lean.collectFVars state rootAssignment
+    set := state.fvarSet.union set
     usedFVarMap := usedFVarMap.insert toLift.fvarId set
   return usedFVarMap
 
@@ -1170,3 +1180,33 @@ builtin_initialize
 
 end Command
 end Lean.Elab
+
+/-!
+# Note [Delayed-Assigned Metavariables in Free Variable Collection]
+
+Nested declarations using `let rec` should compile correctly even when nested within expressions
+that are elaborated using delayed metavariable assignments, such as `match` expressions and tactic
+blocks. Previously, declaring a `let rec` within such an expression in the following fashion
+```lean
+def f x :=
+  let rec g :=
+    match ... with
+    | pat =>
+      let rec h := ... g ...
+      ... x ...
+```
+where `g` depends on some free variable bound by `f` (like `x` above) would cause `MutualClosure` to
+fail to detect that transitive fvar dependency of `h` (which must pass it as an argument to `g`),
+leading to an unbound fvar in the body of `h` that was ultimately fed to the kernel. This occurred
+because `MutualClosure` processes let-recs from most to least nested. Initially, the body of `g` is
+an application of the delayed-assigned metavariable generated by `match` elaboration; the root
+metavariable of that delayed assignment is, in turn, assigned to an expression that refers to the
+mvar that will eventually be assigned to `g` once we process that declaration. Therefore, when we
+initially process the most-nested declaration `h` (before `g`), we cannot instantiate the
+`match`-expression mvar's delayed assignment (since the metavariable that will eventually be
+assigned to the yet-unprocessed `g` remains unassigned). Thus, we do not detect any of the fvar
+dependencies of `g` in the `match` body -- namely, that corresponding to `x`, which `h` should
+therefore also take as a parameter. This also caused a knock-on effect in certain situations,
+wherein `h` would compile as an `axiom` rather than as `opaque`, rendering `f` erroneously
+noncomputable.
+-/
diff --git a/tests/lean/run/6927.lean b/tests/lean/run/6927.lean
new file mode 100644
index 0000000000..c4f9ddeccb
--- /dev/null
+++ b/tests/lean/run/6927.lean
@@ -0,0 +1,93 @@
+import Lean
+/-
+# Nested `let rec` declarations in the presence of delayed metavariable assignments
+
+https://github.com/leanprover/lean4/issues/6927
+
+Nested declarations using `let rec` should compile correctly even when nested within expressions
+that are elaborated using delayed metavariable assignments, such as `match` expressions and tactic
+blocks. See the Note [Delayed-Assigned Metavariables in Free Variable Collection] in
+`MutualDef.lean` for additional details.
+-/
+
+inductive Tree : Type where
+  | leaf
+  | node (p : Nat) (brs : List Tree)
+def Tree.substNats (M : Tree) (σ : Nat → Nat) : Tree :=
+  let rec go M : Tree := match M with
+    | .leaf => leaf
+    | .node p brs =>
+      let rec goList : List Tree → List Tree
+        | [] => []
+        | M :: Ms => go M :: goList Ms
+      .node (σ p) (goList brs)
+  go M
+
+
+/-
+Previously, free variable dependencies in `inner` were not correctly detected, leading that
+declaration to contain free variables when sent to the kernel.
+-/
+namespace Ex1
+def outer (f : Nat → Nat) :=
+  let rec middle n := match n with
+  | Nat.zero => 0 | .succ _ =>
+    let rec inner := middle n
+    f 0
+  ()
+end Ex1
+
+/-
+`by` blocks induced behavior similar to the above, since they also produce metavariables during
+elaboration.
+-/
+def tac (f : Nat → Nat) :=
+  let rec middle n := by
+    let rec inner := middle (Nat.succ n)
+    exact f 0
+  ()
+
+/- Previously, `inner` was incorrectly compiled as an `axiom`, rendering `outer` noncomputable. -/
+namespace Ex2
+/--
+error: fail to show termination for
+  Ex2.outer.middle.inner
+  Ex2.outer.middle
+with errors
+failed to infer structural recursion:
+Not considering parameter f of Ex2.outer.middle.inner:
+  it is unchanged in the recursive calls
+Not considering parameter f of Ex2.outer.middle:
+  it is unchanged in the recursive calls
+Cannot use parameters n✝ of Ex2.outer.middle.inner and n of Ex2.outer.middle:
+  failed to eliminate recursive application
+    outer.middle f✝ (n + 1)
+Cannot use parameters n of Ex2.outer.middle.inner and n of Ex2.outer.middle:
+  failed to eliminate recursive application
+    outer.middle f✝ (n + 1)
+
+
+Could not find a decreasing measure.
+The basic measures relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+Call from Ex2.outer.middle.inner to Ex2.outer.middle at 89:6-20:
+  n✝ n
+n  ? ?
+Call from Ex2.outer.middle to Ex2.outer.middle.inner at 91:4-11:
+   n
+n✝ _
+n  _
+
+Please use `termination_by` to specify a decreasing measure.
+-/
+#guard_msgs in
+def outer (f : Nat → Nat) (n : Nat) : Nat :=
+  let rec middle n : Nat := match n with
+  | 0 => 1
+  | n + 1 =>
+    let rec inner (n : Nat) : Nat :=
+      middle (n + 1)
+    let _ := f
+    inner n
+  middle n
+end Ex2