Deriving Applicative for sums of functors

Applicative_Sum.hs

type f ~> g = (forall x. f x -> g x)

infixr 0 ··>
type (··>) :: (Type -> Type) -> (Type -> Type) -> Type
type f ··> g = Proxy '(f, g) -> Type

type  Idiom :: f ··> g -> Constraint
class Idiom (hom :: f ··> g) where
 idiom :: f ~> g

type IdiomId :: forall f -> f ··> f
data IdiomId f proxy

instance Idiom (IdiomId f) where
 idiom :: f ~> f
 idiom = id
 
type IdiomPure :: forall f -> Par1 ··> f
data IdiomPure f proxy

instance Applicative f => Idiom (IdiomPure f) where
 idiom :: Par1 ~> f
 idiom (Par1 a) = pure a

type IdiomFst :: forall (f :: Type -> Type) -> forall (g :: Type -> Type) -> f:*:g ··> f
data IdiomFst f g proxy

instance Idiom (IdiomFst f g) where
 idiom :: (f :*: g) ~> f
 idiom (as :*: _) = as

newtype W hom f a = W (f a)
 deriving anyclass Functor

instance (Generic1 f, GApplicative hom (Rep1 f)) => Applicative (W hom f) where
  pure :: a -> W hom f a
  pure a = W do
    to1 do
      gpure @_ @_ @hom a

  liftA2 :: (a -> b -> c) -> (W hom f a -> W hom f b -> W hom f c)
  liftA2 (·) (W as) (W bs) = W do
    to1 do
      gliftA2 @_ @_ @hom (·) (from1 as) (from1 bs)

type  GApplicative :: (f ··> g) -> (Type -> Type) -> Constraint
class GApplicative hom rep where
  gpure   :: a -> rep a
  gliftA2 :: (a -> b -> c) -> (rep a -> rep b -> rep c)

instance GApplicative hom rep => GApplicative hom (M1 tag info rep) where
  gpure :: a -> M1 tag info rep a
  gpure a = M1 do
    gpure @_ @_ @hom a

  gliftA2 :: forall a b c. (a -> b -> c) -> (M1 tag info rep a -> M1 tag info rep b -> M1 tag info rep c)
  gliftA2 (·) (M1 as) (M1 bs) = M1 do
    gliftA2 @_ @_ @hom (·) as bs

instance (Idiom hom, Coercible rep f, Coercible rep1 g, Applicative rep, Applicative rep1) => GApplicative @f @g hom (rep :+: rep1) where
  gpure :: a -> (rep :+: rep1) a
  gpure = L1 . pure

  gliftA2 :: forall a b c. (a -> b ->c) -> ((rep :+: rep1) a -> (rep :+: rep1) b -> (rep :+: rep1) c)
  gliftA2 (·) (L1 as) (L1 bs) = L1 do liftA2 (·) as bs
  gliftA2 (·) (R1 as) (R1 bs) = R1 do liftA2 (·) as bs

  gliftA2 (·) (L1 as) (R1 bs) = R1 do liftA2 (·) as' bs where
    as' = coerce (idiom @f @g @hom @a (coerce as))

  gliftA2 (·) (R1 as) (L1 bs) = R1 do liftA2 (·) as bs' where
    bs' = coerce (idiom @f @g @hom @b (coerce bs))

-- >> liftA2 (+) (Ok1 10) (Ok1 20)
-- Ok1 30
-- >> liftA2 (+) (Ok2 10) (Ok2 20)
-- Ok2 30
-- >> liftA2 (+) (Ok1 10) (Ok2 20)
-- Ok2 30
-- >> liftA2 (+) (Ok2 10) (Ok1 20)
-- Ok2 30
type Ok :: Type -> Type
data Ok a = Ok1 a | Ok2 a
 deriving stock (Show, Generic1)

 deriving (Functor, Applicative)
 via W (IdiomId Par1) (NoMeta Ok)

type  Strip :: (k -> Type) -> Constraint
class Strip (rep :: k -> Type) where
 type Bye (rep :: k -> Type) :: (k -> Type)
 strip :: rep ~> Bye rep
 dress :: Bye rep ~> rep

instance Strip @k rep => Strip @k (M1 @k tag info rep) where
 type Bye (M1 @k tag info rep) = M1 @k tag info (Bye rep)
 strip :: M1 tag info rep ~> M1 tag info (Bye rep)
 strip (M1 as) = M1 (strip as)

 dress :: M1 tag info (Bye rep) ~> M1 tag info rep
 dress (M1 as) = M1 (dress as)

instance (Strip @k rep, Strip @k rep1) => Strip @k (rep :+: rep1) where
 type Bye (rep :+: rep1) = Bye rep :+: Bye rep1
 strip :: (rep :+: rep1) ~> (Bye rep :+: Bye rep1)
 strip (L1 as) = L1 (strip as)
 strip (R1 bs) = R1 (strip bs)

 dress :: (Bye rep :+: Bye rep1) ~> (rep :+: rep1)
 dress (L1 as) = L1 (dress as)
 dress (R1 bs) = R1 (dress bs)

instance (Strip @k rep, Strip @k rep1) => Strip @k (rep :*: rep1) where
 type Bye (rep :*: rep1) = Bye rep :*: Bye rep1
 strip :: (rep :*: rep1) ~> (Bye rep :*: Bye rep1)
 strip (as :*: bs) = strip as :*: strip bs

 dress :: (Bye rep :*: Bye rep1) ~> (rep :*: rep1)
 dress (as :*: bs) = dress as :*: dress bs
 
instance Strip (Rec1 f) where
 type Bye (Rec1 f) = f
 strip :: Rec1 f ~> f
 strip (Rec1 as) = as

 dress :: f ~> Rec1 f
 dress = Rec1

instance Strip Par1 where
 type Bye Par1 = Par1

 strip :: Par1 ~> Par1
 strip = id

 dress :: Par1 ~> Par1
 dress = id

type    NoMeta :: (k -> Type) -> k -> Type
newtype NoMeta f a = NoMeta (f a)

instance (Generic1 f, Strip @k (Rep1 f)) => Generic1 @k (NoMeta f) where
 type Rep1 (NoMeta f) = Bye (Rep1 f)

 from1 :: NoMeta f ~> Bye (Rep1 f)
 from1 (NoMeta as) = strip (from1 as)

 to1 :: Bye (Rep1 f) ~> NoMeta f