Instant stack overflow upon defining type class instance

[FWuermse]

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 #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: Goal view shows types and assists me with implementing the instance.

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.