From 27080dca352dcd739d7cbed32e8a0949e2a2cb3b Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 13 Jun 2025 15:55:15 -0700
Subject: [PATCH] chore: use FVarIdHashSet in LCNF collectUsed (#8778)

---
 src/Lean/Compiler/LCNF/Basic.lean        | 16 ++++++++--------
 src/Lean/Compiler/LCNF/PullFunDecls.lean |  2 +-
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean
index 41d3e4df4a..ee4235b23a 100644
--- a/src/Lean/Compiler/LCNF/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Basic.lean
@@ -659,7 +659,7 @@ def Decl.isTemplateLike (decl : Decl) : CoreM Bool := do
   else
     return false
 
-private partial def collectType (e : Expr) : FVarIdSet → FVarIdSet :=
+private partial def collectType (e : Expr) : FVarIdHashSet → FVarIdHashSet :=
   match e with
   | .forallE _ d b _ => collectType b ∘ collectType d
   | .lam _ d b _     => collectType b ∘ collectType d
@@ -669,30 +669,30 @@ private partial def collectType (e : Expr) : FVarIdSet → FVarIdSet :=
   | .proj .. | .letE .. => unreachable!
   | _                => id
 
-private def collectArg (arg : Arg) (s : FVarIdSet) : FVarIdSet :=
+private def collectArg (arg : Arg) (s : FVarIdHashSet) : FVarIdHashSet :=
   match arg with
   | .erased => s
   | .fvar fvarId => s.insert fvarId
   | .type e => collectType e s
 
-private def collectArgs (args : Array Arg) (s : FVarIdSet) : FVarIdSet :=
+private def collectArgs (args : Array Arg) (s : FVarIdHashSet) : FVarIdHashSet :=
   args.foldl (init := s) fun s arg => collectArg arg s
 
-private def collectLetValue (e : LetValue) (s : FVarIdSet) : FVarIdSet :=
+private def collectLetValue (e : LetValue) (s : FVarIdHashSet) : FVarIdHashSet :=
   match e with
   | .fvar fvarId args => collectArgs args <| s.insert fvarId
   | .const _ _ args => collectArgs args s
   | .proj _ _ fvarId => s.insert fvarId
   | .lit .. | .erased => s
 
-private partial def collectParams (ps : Array Param) (s : FVarIdSet) : FVarIdSet :=
+private partial def collectParams (ps : Array Param) (s : FVarIdHashSet) : FVarIdHashSet :=
   ps.foldl (init := s) fun s p => collectType p.type s
 
 mutual
-partial def FunDecl.collectUsed (decl : FunDecl) (s : FVarIdSet := {}) : FVarIdSet :=
+partial def FunDecl.collectUsed (decl : FunDecl) (s : FVarIdHashSet := {}) : FVarIdHashSet :=
   decl.value.collectUsed <| collectParams decl.params <| collectType decl.type s
 
-partial def Code.collectUsed (code : Code) (s : FVarIdSet := {}) : FVarIdSet :=
+partial def Code.collectUsed (code : Code) (s : FVarIdHashSet := {}) : FVarIdHashSet :=
   match code with
   | .let decl k => k.collectUsed <| collectLetValue decl.value <| collectType decl.type s
   | .jp decl k | .fun decl k => k.collectUsed <| decl.collectUsed s
@@ -708,7 +708,7 @@ partial def Code.collectUsed (code : Code) (s : FVarIdSet := {}) : FVarIdSet :=
   | .jmp fvarId args => collectArgs args <| s.insert fvarId
 end
 
-abbrev collectUsedAtExpr (s : FVarIdSet) (e : Expr) : FVarIdSet :=
+abbrev collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet :=
   collectType e s
 
 /--
diff --git a/src/Lean/Compiler/LCNF/PullFunDecls.lean b/src/Lean/Compiler/LCNF/PullFunDecls.lean
index 36b4d34e1c..2635469403 100644
--- a/src/Lean/Compiler/LCNF/PullFunDecls.lean
+++ b/src/Lean/Compiler/LCNF/PullFunDecls.lean
@@ -17,7 +17,7 @@ Local function declaration and join point being pulled.
 structure ToPull where
   isFun : Bool
   decl  : FunDecl
-  used  : FVarIdSet
+  used  : FVarIdHashSet
   deriving Inhabited
 
 /--