`BitVec.ofBoolListLE` stack overflow for large lists

BitVec.ofBoolListLE crashes due to stack overflow for large lists. The implementation seems not to be tail-recursive.

Reproduce

The following code BitVec.ofBoolListLE on a large arbitrary list of booleans and does a popcount to make sure no optimizations can affect the result. An alternative implementation of BitVec.ofBoolListLE is included, which does not crash, thus demonstrating that it's really BitVec.ofBoolListLE causing it.

import Init.Data.BitVec.Basic

/-- Tail-recursive version of `BitVec.ofBoolListLE` -/
def BitVec.ofBoolListLE' (bs : List Bool) : BitVec bs.length :=
  let val := bs.reverse.foldl (fun acc b => acc * 2 + if b then 1 else 0) 0
  BitVec.ofNat bs.length val

def someBitSeq (n : Nat) : Bool := (n * n + 3 * n) % 17 < 8

/-- Using `BitVec.ofBoolListLE` -/
def randomBitVec (n : Nat) : BitVec n :=
  let list := List.ofFn fun m : Fin n ↦ someBitSeq m.toNat
  have : list.length = n := by grind
  BitVec.cast this (.ofBoolListLE list)

/-- Using custom `BitVec.ofBoolListLE'` -/
def randomBitVec' (n : Nat) : BitVec n :=
  let list := List.ofFn fun m : Fin n ↦ someBitSeq m.toNat
  have : list.length = n := by grind
  BitVec.cast this (.ofBoolListLE' list)

def BitVec.popcount {n : Nat} (bv : BitVec n) : Nat :=
  Fin.foldl n (fun acc i => acc + if bv.getLsbD i.val then 1 else 0) 0

def main (args : List String) : IO Unit := do
  let primed  := args.contains "--primed"
  let numArgs := args.filter (· != "--primed")
  match numArgs with
  | [nStr] =>
    match nStr.toNat? with
    | none   => IO.eprintln s!"error: '{nStr}' is not a valid number"
    | some n =>
      -- Make sure result is used and cannot be optimized away
      let ones := if primed then (randomBitVec' n).popcount
                             else (randomBitVec  n).popcount
      IO.println s!"{ones}"
  | _ => IO.eprintln "usage: ofBoolListLE-SO-demo <n> [--primed]"

lean --run ofBoolListLE-SO-demo.lean 1000000

Stack overflow detected. Aborting.
Aborted (core dumped)

lean --run ofBoolListLE-SO-demo.lean 1000000 --primed
647060

lean --version
Lean (version 4.28.0, x86_64-unknown-linux-gnu, commit 7e01a1bf5c70fc6167d49c345d3bf80596e9a79b, Release)

Zulip discussion

I asked about this at #general > `BitVec.ofBoolListLE` is not tail-recursive?) but with no responses yet.

Start in Init.Data.BitVec.Basic and inspect the implementation of BitVec.ofBoolListLE, comparing it with the tail-recursive alternative shown in the issue. Reproduce with the provided ofBoolListLE-SO-demo.lean command using a list size of 1000000, then confirm the original behavior completes without stack overflow and produces the expected popcount.