Stack overflow in LSP/lake build for snippet

[badly-drawn-wizards]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following MWE causes a stack overflow in lake build or causes the LSP to hang

inductive A
  | foo : A → A

inductive B : A → A → Type where
  | foo : B (.foo q) q

structure ImageR (R : α → α → Type) (a : α) where
  {b : α}
  (r : R a b)

instance : Ord (ImageR B p) where
  compare i j := match i.r with
    | .foo => match j.r with
      | .foo => sorry

Steps to Reproduce

1. Put this snippet in a lean project
2. lake build

Expected behavior: No stack overflow
Actual behavior: Stack overflow

Versions

[Output of #eval Lean.versionString or of lean --version in the folder that the issue occured in] 4.7.0-rc2
[OS version] NixOS 24.05pre-git (Uakari) x86_64

[Kha]

Does not reproduce anymore