Raw kernel "invalid return type" error upon extending typeclass with unquantified type variable

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

Consider the MWE Link to lean playground

class TypeclassWithParameter (α : Type)   where 

class TypeclassNoParameter extends TypeclassWithParameter α where
-- (kernel) invalid return type for 'TypeclassNoParameter.mk'

Context

This was found when porting an eclectic use of data families+typeclass inference in Haskell in the frex library

Steps to Reproduce

Expected behavior: A non-kernel error message, preferably one such as:

variable 'α' occurs on the right-hand-side of extends,
at 'TypeclassWithParameter α',
but cannot be found on the left hand side of the typeclass definition,
at 'class TypeclassNoParameter'.

Actual behavior: Raw kernel errr.

Versions

"4.8.0-rc1"

Impact

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

Start by running the minimal reproducer from the issue, either locally or in the linked Lean playground, and trace handling of the typeclass extends declaration. The work is done when this invalid declaration produces a user-facing diagnostic explaining the unquantified variable instead of a raw kernel error.