haskell - 我该如何表达这个约束？

Question

我想表达一个Constraint关于种类k -> k -> Type ，可以用英语表示为:

A type s such that, forall x x', y, and y' where Coercible x x' and Coercible y y', Coercible (s x y) (s x' y')

或者用更简单的英语:

A type s that is always coercible if its two parameters are coercible.

后者似乎已经非常接近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 开启)。

• 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 内.因为我可以使用 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(参见 the GHC wiki):

• A type synonym has a CUSK if and only if all of its type variables and its RHS are annotated with kinds.