haskell - この制約をどのように表現できますか?

Question

Constraintkind の on 型を表現したいと思いk -> k -> Typeます。これは英語で次のように言えます。

forall s、x x'、yおよびy'whereCoercible x x'およびCoercible y y'、Coercible (s x y) (s x' y')

または、より平易な英語で:

s2 つのパラメーターが強制可能な場合、常に強制可能な型。

後者はすでに 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 は aConstraintの右側にいるのが好きではないことが分かり=>ますtype。Constraint種類で型エイリアスを作成でき、 でtypeエイリアスを作成できるので=>、問題ありません。

問題は何ですか?この制約をghcが受け入れる方法で表現するにはどうすればよいですか?