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?
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