我如何表达这个约束？

Question

我想表达一个Constrainton types of kind k -> k -> Type，可以用英文表述为：

一种类型，s例如 forall x x'、y、 以及y'whereCoercible x x'和Coercible y y'、Coercible (s x y) (s x' y')

或者用更简单的英语：

s如果其两个参数是可强制转换的，则该类型始终是可强制转换的。

后者似乎已经非常接近 haskell，而且我有一些看起来确实应该这样做的代码：

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')

但是这不起作用，ghc 想要Coercible (s x y) (s x' y')成为一种类型，但它是Constraint(ConstraintKinds并且QuantifiedConstraints是 on)。

• Expected a type, but
  ‘Coercible (s x y) (s x' y')’ has kind
  ‘Constraint’
• In the type ‘forall x x' y y'.
               (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')’
  In the type declaration for ‘Representational2’

我不完全了解什么是要去，但据我了解，GHC不喜欢Constraint上的右手侧是=>内部的type。由于我可以使用 kind 创建类型别名，Constraint并且可以使用 来创建type别名=>，所以没问题。

有什么问题，我如何才能以它接受的方式表达对 ghc 的这种限制？

Answer 1

这有效：

{-# LANGUAGE ConstraintKinds, PolyKinds, RankNTypes, QuantifiedConstraints #-}

import Data.Kind
import Data.Coerce

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y') :: Constraint

我所做的只是添加:: Constraint到您的类型中。由于 GHC 已经知道 RHS 的类型Constraint（由于错误消息），我真的没有很好的解释为什么这使它起作用。

编辑：我有一个部分解释：通过将那种签名添加到 RHS，您的类型同义词现在有一个 CUSK（请参阅GHC wiki）：

• 类型同义词具有 CUSK 当且仅当其所有类型变量及其 RHS 都用类型进行注释。