Recently I have been trying to incorporate Higher-Kinded Data (HKD) approach to the project I am working on, but I am having issues coming up with something that satisfies all my needs. I initially tried to use the `barbies`

library. However, the representation `barbies`

went for doesn’t allow nested HKDs. An example could be the following:

```
data Inner f = Inner
{ inner :: f String }
data Outer f = Outer
{ outer :: f (Inner f) }
deriving instance (forall a. Show a => Show (f a)) => Show (Inner f)
deriving instance (forall a. Show a => Show (f a)) => Show (Outer f)
```

The reason why this doesn’t work as-is is briefly explained in this `barbies`

GitHub issue, and an alternative encoding is offered by the author. However, after some time fiddling with it, I couldn’t make it work, so I decided to roll my own thing. Essentially, in order to have these nested HKDs, one needs a `Functor`

constraint on the mapping function, and that’s what I used for my HKD representation:

```
class HFunctor (b :: (Type -> Type) -> Type) where
hmap :: forall f g. (Functor f) => (forall a. f a -> g a) -> b f -> b g
instance HFunctor Inner where
hmap :: Functor f => (forall a. f a -> g a) -> Inner f -> Inner g
hmap f (Inner inner) = Inner (f inner)
instance HFunctor Outer where
hmap :: Functor f => (forall a. f a -> g a) -> Outer f -> Outer g
hmap f (Outer outer) = Outer $ f (hmap f <$> outer)
```

…and it works as expected:

```
-- >>> hmap maybeToList (Inner (Just "foo"))
-- Inner {inner = ["foo"]}
-- 'Outer' works too:
-- >>> hmap maybeToList (Outer (Just (Inner (Just "foo"))))
-- Outer {outer = [Inner {inner = ["foo"]}]}
```

Here comes the problem: I also want to be able to use natural transformations that impose constraints on the argument. However, `hmap`

as we currently have it doesn’t work with such functions:

```
showIt :: Show a => Maybe a -> Const String a
showIt = Const . show
-- >>> hmap showIt (Inner (Just "foo"))
-- No instance for (Show a_aK2d[sk:2]) arising from a use of `showIt'
-- Possible fix:
-- add (Show a_aK2d[sk:2]) to the context of
-- a type expected by the context:
-- forall a. Maybe a -> Const String a
-- In the first argument of `hmap', namely `showIt'
-- In the expression: hmap showIt (Inner (Just "foo"))
-- In an equation for `it_aK0i':
-- it_aK0i = hmap showIt (Inner (Just "foo"))
```

The way `barbies`

handles this is by reifying the constraint and pairing it up with the original argument, so that the mapping function fits the expected structure of a natural transformation. I employed the same trick:

```
-- Set up the machinery to reify the constraint, similar to
-- the 'constraints' library:
data Dict c a where
Dict :: c a => Dict c a
requiringDict :: (c a => r) -> Dict c a -> r
requiringDict r Dict = r
showItPacked :: Product (Dict Show) Maybe a -> Const String a
showItPacked (Pair d ma) = requiringDict (showIt ma) d
-- Let's try 'hmap' again:
-- >>> :t hmap showItPacked
-- Could not deduce (Functor (Dict Show)) arising from a use of `hmap'
-- from the context: HFunctor b_a1mrR[sk:1]
-- bound by the inferred type of
-- it_a1ms2 :: HFunctor b_a1mrR[sk:1] =>
-- b_a1mrR[sk:1] (Product (Dict Show) Maybe)
-- -> b_a1mrR[sk:1] (Const String)
-- at <interactive>:1:1
-- In the expression: hmap showItPacked
```

Right, `Dict Show`

doesn’t have a `Functor`

instance. However, the way I see it, it *can’t* have a lawful `Functor`

instance. Just because you have a function that turns `a`

's into `b`

's, and `a`

is `Show`

able, doesn’t mean that `b`

needs to be `Show`

able as well.

At this point, I couldn’t figure out how to proceed further with this. The way I understand it, the `Functor`

constraint on `hmap`

is essential to make nested HKDs work. However, it doesn’t play nicely with constraints. I have tried to employ some (Co)yoneda trickeries to potentially “defer” the `Functor`

constraint on the mapping function, but to no avail.

### TL;DR:

I am looking for a way to make nested Higher-Kinded Data approach play nicely with mapping functions that involve constraints.