What is the Standalone Kind Signature for this class?-CodePudding

I am trying to move the kind annotation for i from the class below to a SAKS:

class Demote t (i :: t -> Type) where
    demote :: forall (t' :: t) . i t' -> t

The following attempts did not work:

-- fails because k and t will not unify?
type Demote :: Type -> (k -> Type) -> Constraint
class Demote t i where
    demote :: forall (t' :: t) . i t' -> t

-- fails because the SAKS and class head do not share the same namespace?
type Demote :: (k ~ t) => Type -> (k -> Type) -> Constraint
class Demote t i where
    demote :: forall (t' :: t) . i t' -> t

Is there no way to write a SAKS for this in GHC 9.2.0.20210422?

CodePudding user response：

This is an example of visible dependent quantification (forall->), the kind is

type  Demote :: forall t -> (t -> Type) -> Constraint
class Demote t i where
  demote :: forall (t' :: t) . i t' -> t