How can I express this Constraint?

Question

I would like to express a Constraint on types of kind k -> k -> Type, which can be stated in English as:

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

Or in even plainer English:

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

The latter seems tantalizingly close to haskell already, and I have some code that really looks like it should do it:

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

However this doesn't work, ghc wants Coercible (s x y) (s x' y') to be a type but it is a Constraint (ConstraintKinds and QuantifiedConstraints are 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’

I don't fully understand what is going on but I gather that ghc does not like a Constraint being on the right hand side of => within a type. Since I can create type aliases with Constraint kinds and I can create type aliases with =>, no problem.

What is the issue and how can I express this contraint to ghc in a manner it accepts?

Answer 1

This works:

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

All I did was add :: Constraint to your type. Since GHC already knew the kind of the RHS was Constraint (due to the error message), I don't really have a good explanation for why this makes it work.

---

Edit: I have a partial explanation: by adding that kind signature to the RHS, your type synonym now has a CUSK (see 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.