From 79943bedc1e85ffd54854425ee02e5f32a6472e4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 13 Sep 2024 10:53:08 +0200
Subject: [PATCH] fix: unused variable false positive under `match` +
 `assumption`

---
 src/Lean/Elab/InfoTree/Main.lean                 |  2 +-
 src/Lean/Linter/UnusedVariables.lean             |  9 +++++++--
 tests/lean/1018unknowMVarIssue.lean.expected.out |  8 ++++----
 tests/lean/linterUnusedVariables.lean            | 11 +++++++++++
 4 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 813ffa3185ce..5ba988886f3b 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index b3a71e7707f2..a2a7bfb53d36 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -447,7 +447,10 @@ def unusedVariables : Linter where
     let fvarAliases : Std.HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
       m.insert id (followAliases s.fvarAliases baseId)
 
+    let getCanonVar (id : FVarId) : FVarId := fvarAliases.getD id id
+
     -- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
+    -- Unlike `s.fvarUses`, `fvarUsesRef` is guaranteed to contain no aliases.
     let fvarUsesRef ← IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
       if fvarUses.contains id then fvarUses.insert baseId else fvarUses
 
@@ -461,7 +464,7 @@ def unusedVariables : Linter where
       let fvarUses ← fvarUsesRef.get
       -- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
       -- `fvarUses`, then it is used
-      if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+      if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
       -- If this is a global declaration then it is (potentially) used after the command
       if s.constDecls.contains range then continue
 
@@ -493,10 +496,12 @@ def unusedVariables : Linter where
       if !initializedMVars then
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
+        -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
+        fvarUsesRef.modify fun fvarUses => fvarUses.toList.map getCanonVar |> .ofList
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now
-        if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+        if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
 
       -- If we made it this far then the variable is unused and not ignored
       unused := unused.push (declStx, userName)
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 3fe4323d4567..aaf8ca4506de 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -55,8 +55,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias α
+        • FVarAlias a: _uniq.636 -> _uniq.312
+        • FVarAlias α: _uniq.635 -> _uniq.310
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -70,8 +70,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias n
+        • FVarAlias a: _uniq.667 -> _uniq.312
+        • FVarAlias n: _uniq.666 -> _uniq.310
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index aa285db063d9..96a2633f3ede 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -255,3 +255,14 @@ def ignoreEverything : Lean.Linter.IgnoreFunction :=
   fun _ _ _ => true
 
 def ignored (x : Nat) := 0
+
+inductive A where
+  | intro : Nat → A
+
+def A.out : A → Nat
+  | .intro n => n
+
+/-! `h` is used indirectly via an alias introduced by `match` that is used only via the mvar ctx -/
+theorem problematicAlias (n : A) (i : Nat) (h : i ≤ n.out) : i ≤ n.out :=
+  match n with
+  | .intro _ => by assumption