Instant stack overflow upon defining type class instance

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When defining a type class instance (Proper), the program immediately runs into a stack overflow error. It may be related to https://github.com/leanprover/lean4/issues/6229 but the error occurs instantly.

Context

I'm translating the Coq type classes and instances proposed in the paper "A New Look at Generalized Rewriting in Type
Theory" by Matthieu Sozeau.

This relates to this channel: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Rewriting.20congruent.20relations

Steps to Reproduce

def Relation (α : Sort u) := α → α → Prop

def respectful {α β : Sort u} (r : Relation α) (r' : Relation β) : Relation (α → β) :=
  fun f g => ∀ x y, r x y → r' (f x) (g y)

notation:55 r " ⟹ " r' => respectful r r'

class Proper {α : Sort u} (r : Relation α) (m : α) where
  proper : r m m

class Subrel {α : Sort u} (q r : Relation α) : Prop where
  subrelation : ∀ x y, q x y → r x y

instance : Proper (@Subrel β ⟹ @Subrel (α → β)) sorry := sorry

Expected behaviour: Lean shows error "error: stuck at solving universe constraint"

Actual behavior: Lean Server crashes with "Lean server printed an error: Stack overflow detected. Aborting."

Versions

Lean 4.13.0, Lean 4.14.0-rc1, Lean 4.14.0-rc2, Lean 4.14.0-rc3
Target: arm64-apple-darwin23.6.0 macOS

live.lean-lang.org:
Lean 4.15.0-nightly-2024-11-28
Target: x86_64-unknown-linux-gnu

Additional Information

I tested this locally on linux as well and ran into the same issue.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal self-contained reproducer in the issue and confirm the behavior in live.lean-lang.org or a current nightly build. Investigate the type class instance elaboration and universe-constraint handling; done means the example reports the expected stuck universe constraint instead of causing a stack overflow or server crash.