GHC 9.2中如何为Demote类型类编写正确的Standalone Kind Signature

可行方案 #

你需要先开启以下GHC扩展：

• StandaloneKindSignatures
• DataKinds
• PolyKinds

正确的SAKS写法如下：

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

失败原因说明 #

1. 第一次尝试的问题：你在SAKS中给i声明的参数kind是独立的变量k，和类的第一个参数t没有任何关联，导致i的入参kind和demote方法要求的t' :: t无法统一，因此编译失败。
2. 第二次尝试的问题：直接将k ~ t的相等约束放在SAKS顶层的写法不符合GHC的SAKS语法规则，这类约束无法将未显式绑定的kind变量和类参数关联，因此不会生效。

GHC 9.2.0.20210422版本完全支持上述写法，符合你原类定义的语义。

内容的提问来源于stack exchange，提问作者Vanson Samuel