v4.27.0-rc1: (kernel) deep recursion detected

Stream: new members

[Shubakur Mitra]

After updating v4.24.0 → v4.27.0-rc1, one of our theorems that was compiling quickly started failing with the error (kernel) deep recursion detected. We were able to isolate this MWE:

import Mathlib

def xs : List ℕ :=
  Std.HashSet.ofList (List.replicate 20000 0) |>.toList

example : xs.head?.getD 0 ∉ [] := by
  unfold Option.getD
  split
  all_goals sorry

However, this MWE also fails on v4.24.0 with the same error. But still, this seems unexpected. We never unfold the definition of xs. Is this expected and if so, how to prevent deep recursion?

[Aaron Liu]

you don't even need the split

[Shubakur Mitra]

This compiles quickly on v4.24, but fails on v4.27:

import Mathlib

def mp : Std.ExtDHashMap ℕ (fun _ => ℕ) :=
  .ofList $ List.replicate 20000 ⟨0, 0⟩

def xs : List ((_ : ℕ) × ℕ) :=
  mp.1.lift (·.toList.mergeSort (·.1 ≤ ·.1)) sorry

example : xs.head?.getD ⟨0, 0⟩ = ⟨0, 0⟩ := by
  unfold Option.getD
  all_goals sorry