How to coerce functors applied to coercible arguments

Question

Consider the following Haskell code:

import Data.Coerce

newtype Decorated s a = Decorated a

fancyFunction :: Ctx s => f (Decorated s a) -> r
fancyFunction = ...

instance Ctx s => SomeClass (Decorated s a)

myFunction :: Functor f => f a -> r
myFunction = fancyFunction . fmap coerce

I'd like to make myFunction faster by replacing fmap coerce with coerce. The rationale is that coerce behaves like id and one of the functor laws is fmap id = id.

The only way I can see of doing this is to add Coercible (f a) (f (Decorated s a)) to the context but it refers to s which is not referred to anywhere else. Even worse, if a is bound in a universal type, I cannot express the constraint. Is there a constraint I could express in terms of f only to let me use coerce to convert between f a and f (Decorated s a)?

Is this something that the compiler figures out on its own from the fact that f is a functor? If so, does it also work with bifunctors, traversables and bitraverables?

Answer 1

Unfortunately, Coercible (f a) (f (Decorated s a)) really what you want in your constraint given the current state of GHC. Now, the fact that s and a don't show up elsewhere is not something good - it means GHC won't know what to do with them (they are ambiguous)! I won't get into that...

---

Depending on the role of the type parameter fed to the type constructor f, Coercible a b may or may not imply Coercible (f a) (f b). In this case, we'd want that role to be nominal - but there isn't (yet at least) a way to express this in a constraint. To explain what I mean, consider the following two data definitions:

{-# LANGUAGE TypeFamilies #-}
import Data.Coerce

-- type role of `a` is "representational"
data Data1 a = Data1 a

-- type role of `a` is "nominal"
data Data2 a = Data2 (TypeFunction a)
type family TypeFunction x where
  TypeFunction Bool = Char
  TypeFunction _ = ()

Then, while it is true that Coercible a b entails Coercible (Data1 a) (Data1 b), it does not entail Coercible (Data2 a) (Data2 b). To make this concrete, load up the above in GHCi, then try:

ghci> newtype MyInt = My Int
ghci> let c1 = coerce :: (Data1 MyInt) -> (Data1 Int)
ghci> let c2 = coerce :: (Data2 MyInt) -> (Data2 Int) -- This doesn't work! 

Unfortunately, there is no built-in constraint based way of enforcing that the role of a type variable is representational. You can make your own classes for this, as Edward Kmett has done, but GHC doesn't automatically create instances of some of these classes the way class instances for Coercible are.

This led to this trac ticket where they discuss the possibility of having a class Representational f with instances generated like for Coercible which could have things like

instance (Representational f, Coercible a b) => Coercible (f a) (f b)

If this was actually a thing today, all you would need in your constraint would be Representational f. Furthermore, as Richard Eisenberg observes on the ticket, we really ought to be able to figure out that a in f a has a representational role for any reasonable functor f. Then, we might not even need any constraint on top of Functor f as Representational could be a superclass of Functor.

Here is a good discussion of the current limitations of roles.

Answer 2

Now that you have QuantifiedConstraints, I think you can do this:

type Parametric f = (forall a b. (Coercible a b => Coercible (f a) (f b)) :: Constraint)

newtype Foo = Foo Int

myFunction :: (Parametric f) => f Foo -> f Int
myFunction = coerce

test :: [Int]
test = myFunction [Foo 1, Foo 2, Foo 3]

This is nice, because an instance of Parametric f witnesses that f is an endofunctor on a category where the objects are types and a morphism between types A and B is an instance of Coercible A B.