Introduction
Safe coercions and type roles are great. They solve problems of newtype
s not being zeroruntimecost with certainty, enable a range of very cool features, and for the most part, Just Work™ with no extra effort. However, sometimes, roles can be a bit intrusive in surprising ways. For example, you might have seen an error message like this one:
• 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
This can happen for a range of reasons: a common one is trying to viaderive Traversable
, which we can’t do much about, but it can arise in cases that are a little less opaque, and that we can do something about. Specifically, consider the example below:
coerceFirst :: (Coercible a b) => [f a] > Maybe (f b)
coerceFirst [] = Nothing
coerceFirst (x:_) = Just (coerce x)
Now, this clearly cannot work in general for arbitrary f
, and this is precisely what GHC will complain about if we try to compile this (with an error message similar to the one above). More specifically, GHC is trying to tell us:
I cannot be sure what the role of ‘f’ is, so I have to be as conservative as possible.
But what if we could convince GHC that it doesn’t have to be so conservative? Specifically, what if we could say, in some way:
It’s OK GHC, I promise that I will only pass representational (or phantom) 'f’s, but I want you to keep me honest.
This post will show you how you can do this. The technique is known, but is a bit folkloric, and can produce some rather scarylooking error messages; we will demystify this, and hopefully put it in a place anyone can find if they want to.
tl;dr
If all you want is the solution, without any explanation. You will need GHC at least 8.6.1.
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
module Role.Constraints (Phantom, Representational) where
type Phantom (f :: Type > Type) =
forall a b . Coercible (f a) (f b) :: Constraint
type Representational (f :: Type > Type) =
forall a b . (Coercible a b) => Coercible (f a) (f b) :: Constraint
You can use these type synonyms (or better, the definitions) to indicate that the type parameter of f
is phantom (or representational). You can extend this to something of kind different to Type > Type
:
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
Or mixandmatch to indicate that different type parameters have different roles:
 Representational in first parameter, phantom in second
type RepresentationalPhantom (f :: Type > Type > Type) =
forall a b c d . (Coercible a b) => Coercible (f a c) (f b d) :: Constraint
If you are OK with (yet another) extension (and are on at least GHC 8.10.1), you can remove the :: Constraint
and replace it with a kind signature like so:
type Representational :: (Type > Type) > Constraint
type Representational f = forall a b . (Coercible a b) => Coercible (f a) (f b)
Wtf?
Glad you asked! Let’s review the example:
coerceFirst :: (Coercible a b) => [f a] > Maybe (f b)
coerceFirst [] = Nothing
coerceFirst (x:_) = Just (coerce x)
Clearly, in order for this to work, we have to have f
's first parameter have at least a representational role. There are a few suitable candidates: Maybe
would work, as would Proxy
and []
. However, imagine if f
was Set
: that would potentially be a huge problem! Therefore, for GHC to accept this, we need to provide some kind of evidence of the ‘representationality’ or ‘phantomality’ (‘phantasmalness’?) of the type parameter of f
. Furthermore, we cannot have this behaviour depend on what said type parameter is chosen to be; to see why, consider that the signature actually says something like this:
coerceFirst :: forall f a b . (Coercible a b) => [f a] > Maybe (f b)
This in particular means that the caller of coerceFirst
is allowed to choose any f
, a
and b
that they please, provided the constraints are satisfied.
The solution are quantified constraints:
 Needs QuantifiedConstraints
coerceFirst (Coercible a b,
forall c d . (Coercible c d) => Coercible (f c) (f d)) =>
[f a] > Maybe (f b)
The quantified constraint here says something like:
For any choice of ‘c’ and ‘d’, so long as we can coerce from ‘c’ to ‘d’, we can coerce from ‘f c’ to ‘f d’.
This is exactly what it means for f
's type parameter to have a representational role! Now, GHC has been informed, and we can coerce
to our heart’s content, and GHC will happily keep us honest. We can (although we shouldn’t) even wrap it up in a type synonym:
 Needs RankNTypes, ConstraintKinds, KindSignatures as well
type Representational (f :: Type > Type) =
forall a b . (Coercible a b) => Coercible (f a) (f b)
However, if we try to compile this, GHC will become a bit confused:
• Expected a type, but
‘Coercible (f a) (f b)’ has kind
‘Constraint’
• In the type ‘forall a b.
(Coercible a b) => Coercible (f a) (f b)’
In the type declaration for ‘Representational’

19  forall a b. (Coercible a b) => Coercible (f a) (f b)
 ^^^^^^^^^^^^^^^^^^^^^
The reason this happens is that inference fails (due to that rank2); we need an explicit type signature:
 Needs RankNTypes, ConstraintKinds, KindSignatures as well
type Representational (f :: Type > Type) =
forall a b . (Coercible a b) => Coercible (f a) (f b) :: Constraint
Alternatively, we can specify an explicit kind signature, provided we’re on at least GHC 8.10.1 (and don’t mind another extension):
 Needs RankNTypes, ConstraintKinds, KindSignatures, and StandaloneKindSignatures
type Representational :: (Type > Type) > Constraint  kind signature
type Representational f =
forall a b . (Coercible a b) => Coercible (f a) (f b)
We can do something similar for phantom roles:
type Phantom (f :: Type > Type) =
forall a b . Coercible (f a) (f b) :: Constraint
Now go forth and coerce
!
Thanks to
This writeup uses a technique originally described by Ryan Scott, in part 2 of his series on quantified constraints. I figured that the technique is a bit buried, and decided to dust it off and put it frontandcentre. Also, thanks Iceland Jack, for helping me figure out how to make those synonyms compile without standalone kind signatures. Lastly, thanks to the roles
library, from which I shamelessly stole my example, for making me realize that we have progressed in at least one area since 2017.