Generic isomorphism between sums and heterogeneous sums

Is there a Haskell library providing (or assisting in writing) generic isomorphism between a sum type and an associated heterogenous sum type?

Take the following sum type,

data TR = TR_Index | TR_Inner R

Now we associate it with a heterogenous sum NS I xs (where the 'xs' is defined by a type-class; see MotleyRouteSubRoutes below). And then define a isomorphism to convert back and forth:

instance MotleyRoute TR where
  -- `SingletonRoute s` is isomorphic to `()`
  -- `PrefixedRoute s r` is isomorphic to `Const r s`
  type MotleyRouteSubRoutes TR = 
    '[ SingletonRoute "index.html"
     , PrefixedRoute "inner" R
     ]
  motleyRouteIso =
    iso
      ( \case
          TR_Index -> Z $ I SingletonRoute
          TR_Inner r -> S $ Z $ I $ PrefixedRoute r
      )
      ( \case
          Z (I SingletonRoute) -> TR_Index
          S (Z (I (PrefixedRoute r))) -> TR_Inner r
          S (S x) -> case x of {}
      )

My goal here is to write motleyRouteIso generically (as well as define MotleyRouteSubRoutes generically, but that maybe outside the scope here). I was going to do it from scratch using generics-sop, but I wonder if there already is a library that does this for me. generic-optics provides a IsList but that works for products not sums.

(For full context, see this PR)

Having seen no answer on this so far I'll assume for the moment no such prebuilt solution exists. So here's an approach I went with based on generics-sop.

RGeneric

First I added a RGeneric type-class to narrow the case where a route ADT can have constructors with 0 or 1 product only:

-- | Like `Generic` but for Route types only.
class RGeneric r where
  type RCode r :: [Type]
  rfrom :: r -> NS I (RCode r)
  rto :: NS I (RCode r) -> r

The implementation of this instance is fairly straightforward using generics-sop. You can see it here (the RouteNP constraint captures the expected "shape" of route types we are interested in).

Introduce Coercible for heavy-lifting

Note that the individual types in MotleyRouteSubRoutes are more or less coercible to the route type constructors. So I used that knowledge to "eliminate" the specific types from the equation thus getting one large step closer to a generic implementation. Specifically:

@@ -95,12 +95,12 @@ instance MotleyRoute TR where
   motleyRouteIso =
     iso
       ( \case
-          TR_Index -> Z $ I SingletonRoute
-          TR_Inner r -> S $ Z $ I $ PrefixedRoute r
+          TR_Index -> Z $ coerce ()
+          TR_Inner r -> S $ Z $ coerce r
       )
       ( \case
-          Z (I SingletonRoute) -> TR_Index
-          S (Z (I (PrefixedRoute r))) -> TR_Inner r
+          Z (I (coerce -> ())) -> TR_Index
+          S (Z r) -> TR_Inner $ coerce r
           S (S x) -> case x of {}
       )

Notice how in the new version there is no reference to SingletonRoute or PrefixedRoute.

Full diff here.

Generic Iso

With this place, it is now pretty straightforward to generically implement motleyRouteIso using trans_NS because the Coercible constraint does all the heavy lifting for us, with RGeneric abstracting out dealing with expected 'shape' of the route type. It looks like this:

-- Rough code (leaving out the constraints)
gmotleyRouteIso =
  iso (gtoMotley @r . rfrom) (rto . gfromMotley @r)
  where 
     gtoMotley = trans_NS (Proxy @Coercible) coerce
     gfromMotley = trans_NS (Proxy @Coercible) coerce

The change for this is here.