Coercible a b => Coercible (f a) (f b) using QuantifiedConstraints

coercible.hs

{-
coerceFirst :: (Coercible a b) => [f a] -> Maybe (f b)
coerceFirst []    = Nothing
coerceFirst (x:_) = Just (coerce x)

* Couldn't match representation of type `f a' with that of `f b'
    arising from a use of `coerce'
  NB: We cannot know what roles the parameters to `f' have;
    we must assume that the role is nominal

There is the `roles` package: https://hackage.haskell.org/package/roles
which solves this issue but using an alternative (old) technique.

What we want to say is:

coerceFirst
  :: (Coercible a b,
      forall c d . (Coercible c d) => Coercible (f c) (f d))
coerceFirst []    = Nothing
coerceFirst (x:_) = Just (coerce x)
-}


type Phantom :: (Type -> Type) -> Constraint
type Phantom f = forall a b . Coercible (f a) (f b)

type Representational :: (Type -> Type) -> Constraint
type Representational f = forall a b . (Coercible a b) => Coercible (f a) (f b) :: Constraint

{-
type Representational3 (f :: Type -> Type -> Type) =
    forall a b c d . (Coercible a b, Coercible c d) => Coercible (f a c) (f b d) :: Constraint

type RepresentationalPhantom (f :: Type -> Type -> Type) =
    forall a b c d . (Coercible a b) => Coercible (f a c) (f b d) :: Constraint
-}

coerceFirst
  :: (Coercible a b, Representational f)
  => [f a]
  -> Maybe (f b)
coerceFirst []    = Nothing
coerceFirst (x:_) = Just (coerce x)