From 3ed2d9b3ad47c2562896f786236a7585ff94a600 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 11 Apr 2024 17:12:10 +0200
Subject: [PATCH] perf: fix linearity issue in insertIfNew (#3881)

This fixes a linearity isssue in `insertIfNew`. As `insertIfNew` is used
in `Lean.finalizeImport` we expect this to improve performance.
---
 src/Lean/Data/HashMap.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 279cbf6090..dc30823cb7 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -122,7 +122,7 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     let bkt    := buckets.val[i]
     if let some b := bkt.find? a then
-      (m, some b)
+      (⟨size, buckets⟩, some b)
     else
       let size'    := size + 1
       let buckets' := buckets.update i (AssocList.cons a b bkt) h