How to solve the problem of universe level too big?

Stream: lean4

[Erika Su]

suppose i want to define a typeclass for array:

class IArray.{u, v, w} (Array : Type u -> Type v) : Type w where
 /-- some other function -/
  append            :         Append (Array β)
  assoc {β} [DecidableEq β] : {a b c : Array β} -> (a ++ b) ++ c = a ++ (b ++ c)
  -- error info of assoc : (kernel) universe level of type_of(arg #2) of 'IArray.mk' is too big for the corresponding inductive datatypeLean