Deriving a nonrecursive base functor from a recursive datatype using GHC.Generics

Rollable.hs

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, DefaultSignatures, DeriveAnyClass, DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}
module Rollable where

import Data.Functor.Foldable
import GHC.Generics

data Tree = Empty | Node Tree Int Tree
  deriving (Eq, Generic, Ord, Rollable, Show)

depth :: Tree -> Int
depth = cata (\ node -> case node of
  L1 _                           -> 0
  R1 (Par1 l :*: (_ :*: Par1 r)) -> 1 + (l `max` r))


type instance Base Tree = Unrolled Tree

instance Recursive   Tree where project = unroll
instance Corecursive Tree where embed   = roll


-- | Given some datatype @t@ isomorphic to @µF@, derive the functor @F@.
class Rollable t where
  type Unrolled t :: * -> *
  type Unrolled t = GUnrolled (EqK t (Rep t)) t (Rep t)

  unroll ::          t   -> Unrolled t t
  roll   :: Unrolled t t ->          t

  default unroll :: forall eq . (Generic t, eq ~ EqK t (Rep t), GRollable eq t (Rep t), Unrolled t ~ GUnrolled eq t (Rep t))
                 =>          t   -> Unrolled t t
  default roll   :: forall eq . (Generic t, eq ~ EqK t (Rep t), GRollable eq t (Rep t), Unrolled t ~ GUnrolled eq t (Rep t))
                 => Unrolled t t ->          t

  unroll = gunroll @eq @t @(Rep t) . from
  roll   =                              to   . groll @eq @t @(Rep t)

class  GRollable (eq :: Bool) t (rep :: * -> *) where
  type GUnrolled  eq          t  rep :: * -> *
  gunroll ::                rep t -> GUnrolled eq t rep t
  groll   :: GUnrolled eq t rep t ->                rep t

instance ( eqF ~ EqK t f
         , GRollable eqF t f
         )
      => GRollable 'False t (M1 i c f) where
  type   GUnrolled 'False t (M1 i c f) = GUnrolled (EqK t f) t f
  gunroll = gunroll @eqF @t @f . unM1
  groll   =                        M1 . groll @eqF @t @f

instance ( eqL ~ EqK t l
         , eqR ~ EqK t r
         , GRollable eqL t l
         , GRollable eqR t r
         )
      => GRollable 'False t (l :*: r) where
  type   GUnrolled 'False t (l :*: r)
    = (   GUnrolled (EqK t l) t l
      :*: GUnrolled (EqK t r) t r )
  gunroll = gunroll @eqL @t @l **** gunroll @eqR @t @r
  groll   = groll   @eqL @t @l **** groll   @eqR @t @r

instance ( eqL ~ EqK t l
         , eqR ~ EqK t r
         , GRollable eqL t l
         , GRollable eqR t r
         )
      => GRollable 'False t (l :+: r) where
  type   GUnrolled 'False t (l :+: r)
    = (   GUnrolled (EqK t l) t l
      :+: GUnrolled (EqK t r) t r)
  gunroll = gunroll @eqL @t @l ++++ gunroll @eqR @t @r
  groll   = groll   @eqL @t @l ++++ groll   @eqR @t @r

instance GRollable 'True t (K1 i t) where
  type   GUnrolled 'True t (K1 i t) = Par1
  gunroll = coerce
  groll   = coerce

instance GRollable 'False t (K1 i k) where
  type   GUnrolled 'False t (K1 i k) = K1 i k
  gunroll = coerce
  groll   = coerce

instance GRollable 'False t U1 where
  type   GUnrolled 'False t U1 = U1
  gunroll = coerce
  groll   = coerce

type family EqK a (b :: * -> *) :: Bool where
  EqK t (K1 i t) = 'True
  EqK t _        = 'False