What is the Standalone Kind Signature for this class?

Question

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?

Answer 1

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

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

It is dependent because the result depends on the type we pass in:

>> :k Demote
.. :: forall t -> (t -> Type) -> Constraint
>> :k Demote Bool
.. :: (Bool -> Type) -> Constraint
>> :k Demote [Nat]
.. :: ([Nat] -> Type) -> Constraint

Any kind that is polymorphic forall. can be made visible forall->.

type Proxy :: forall k. k -> Type
data Proxy a where
  Proxy :: Proxy @k a

type ProxyVDQ :: forall k -> k -> Type
data ProxyVDQ k a where
  ProxyVDQ :: ProxyVDQ k a