Describing type roles as constraints

Show and Tell
#1

Introduction

Safe coercions and type roles are great. They solve problems of newtypes not being zero-runtime-cost 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 via-derive 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 scary-looking 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 mix-and-match 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 rank-2); 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 front-and-centre. 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.

8 Likes
#2

Thanks for sharing!

A couple of comments:

  1. Maybe it would be better to add a final example of the coerceFirst using the type synonyms.

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

  2. What I don’t fancy about this approach, as you mentioned, is that it relies on the users to guarantee that the instances are actually coercible. It would be great to find something in the middle between roles package and this approach.

#3

I’m not entirely sure what you mean by 2. Users don’t guarantee anything - the compiler will, because unless you can meet the requirements of the constraint, your code won’t even compile. This technique does little more than just spell out, in GHC-comprehensible terms, what it means for a type parameter to have a phantom or representational role. You don’t need to guarantee anything.

#4

My bad. I thought you could actually trick the compiler somehow and provide a coercible instance for f but that’s not possible (at least on basic examples).

As expected, the following does compile:

ys :: [Int] = [ 0,1,2]
yss = [ys, ys, ys]
r2 :: Maybe [MyInt] = coerceFirst yss

but the following does not:

set = Set.fromList @Int [ 0, 1, 2]
xs = [set, set, set]
r :: Maybe (Set MyInt) = coerceFirst xs
#5

One point of coerce is that it’s free (get’s compiled away).

I am not sure if the same will happen if your function receives a quantified constraint (which I expect is compiled to an argument that is itself a function that maps Coercible type class dictionaries to Coercible dictionaries). Did you check the Core to see if GHC somehow optimizes that away?

One could probably use inspection-testing to assert that it works, e.g. that the generated code is equal to the one using unsafeCoerce. But I am pessimistic…

1 Like
#6

That is a very good question. I haven’t checked, but I will. Will edit the post when I have answers.

2 Likes
#7

Did you get around to check this?

#8

I checked this a few days ago on GHC-8.6.5: it looks like a function with this
kind of constraint does take a real function parameter in Core and apply it to a Coercion to get a larger Coercion. In the Core output below, the quantified constraint is df, it’s applied to a MkCoercible, and the result is matched against MkCoercible.

f :: (forall a b. Coercible a b => Coercible (f a) (f b)) => f a -> f (Sum a)
f = coerce

-- RHS size: {terms: 9, types: 50, coercions: 4, joins: 0/0}
f :: forall (f :: * -> *) a.
     (forall a1 b. Coercible a1 b => Coercible (f a1) (f b)) =>
     f a -> f (Sum a)
f = \ (@ (f1 :: * -> *))
      (@ a)
      (df :: forall a1 b. Coercible a1 b => Coercible (f1 a1) (f1 b))
      (v :: f1 a) ->
      case df
             @ a
             @ (Sum a)
             (MkCoercible
                @ * @ a @ (Sum a) @~ (Sym (N:Sum[0] <a>_R) :: a ~R# Sum a))
      of
      { MkCoercible v1 ->
      v `cast` (v1 :: f1 a ~R# f1 (Sum a))
      }

When specialized and inlined sufficiently, it can eliminate the dictionary-manipulation: in the Core below, the implementation of g is the identity function g1, which is just coerced to the desired type. A few other more-complicated variations on this did still appear to be using normal statically-specified coercions.

g :: [a] -> [Sum a]
g = f

-- RHS size: {terms: 3, types: 4, coercions: 0, joins: 0/0}
g1 :: forall a. [a] -> [a]
g1 = \ (@ a) (v :: [a]) -> v

-- RHS size: {terms: 1, types: 0, coercions: 10, joins: 0/0}
g :: forall a. [a] -> [Sum a]
g = g1
    `cast` (forall (a :: <*>_N).
            <[a]>_R ->_R ([Sym (N:Sum[0] <a>_R)])_R
            :: (forall a. [a] -> [a]) ~R# (forall a. [a] -> [Sum a]))

So in theory, it’s not completely free, but a small constant overhead that might be optimized away. In either case, it does manage to avoid traversing and rebuilding whatever structure f represents, so it’s still a coercion at runtime, just one that potentially needs to pass around a few extra pointers.

Update: just checked 8.10.7 and 9.2.1; no meaningful differences.

3 Likes
#9

See also Remove the Coercible decomposition rule by treeowl · Pull Request #276 · ghc-proposals/ghc-proposals · GitHub. I got a bit pressed for time but I would love to circle back to this stuff at some point (even better to do it with others!). There a decent amount of cruft we should be able to get rid of.

1 Like