该类的独立类型签名是什么？

Question

我正在尝试将i以下类的类型注释移至 SAKS：

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

以下尝试均无效：

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

在 GHC 9.2.0.20210422 中没有办法为此编写 SAKS 吗？

Answer 1

这是可见依赖量化（forall->）的一个例子，其种类是

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

它是依赖的，因为结果取决于我们传入的类型：

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

任何多态类型都forall.可以变得可见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