Foo.hs

{-# LANGUAGE
    DeriveGeneric,
    FlexibleInstances,
    FlexibleContexts,
    AllowAmbiguousTypes,
    ScopedTypeVariables,
    TypeApplications,
    TypeFamilies,
    TypeOperators,
    PartialTypeSignatures,
    UndecidableInstances #-}

import Data.Kind (Type)
import Data.Coerce
import GHC.Generics

-- Example

data Foo
  = Foo1
  | Foo2 Foo
  | Foo3 Foo Foo
  deriving Generic

data T3 a b c = T3 a b c
  deriving Generic

foo1 :: _
foo2 :: _
foo3 :: _
(T3 foo1 foo2 foo3) = magic @Foo @(T3 _ _ _)

example :: [Foo]
example = [foo1, foo2 Foo1, foo3 Foo1 Foo1]

-- Implementation

type family Productify (a :: Type) (f :: Type -> Type) :: Type -> Type where
  Productify a (M1 D c f) = M1 D c (Productify a f)
  Productify a (f :+: g) = Productify a f :*: Productify a g
  Productify a (M1 C c f) = M1 S c (K1 R (Arrowify f a))

type family Arrowify (f :: Type -> Type) (a :: Type) :: Type where
  Arrowify (f :*: g) a = Arrowify f (Arrowify g a)
  Arrowify U1 a = a
  Arrowify (M1 S c (K1 i t)) a = t -> a

class GProductify f where
  gproductify :: (f p -> a) -> Productify a f p

instance GProductify f => GProductify (M1 D c f) where
  gproductify f = M1 (gproductify (f . M1))

instance (GProductify f, GProductify g) => GProductify (f :+: g) where
  gproductify f = gproductify (f . L1) :*: gproductify (f . R1)

instance GArrowify f => GProductify (M1 C c f) where
  gproductify f = M1 (K1 (garrowify (f . M1)))

class GArrowify f where
  garrowify :: (f p -> a) -> Arrowify f a

instance (GArrowify f, GArrowify g) => GArrowify (f :*: g) where
  garrowify f = garrowify (\x -> garrowify (\y -> f (x :*: y)))

instance GArrowify (M1 S c (K1 i t)) where
  garrowify = coerce

instance GArrowify U1 where
  garrowify f = f U1

type family Fields (f :: Type -> Type) :: Type where
  Fields (M1 i c f) = Fields f
  Fields (f :*: g) = (Fields f, Fields g)
  Fields (K1 i a) = a

productify_ :: forall a p. (Generic a, GProductify (Rep a)) => Productify a (Rep a) ()
productify_ = gproductify @(Rep a) @() @a (to @a)

magic :: forall a b.
  ( Generic a, GProductify (Rep a)
  , Generic b, Coercible (Productify a (Rep a)) (Rep b), Fields (Productify a (Rep a)) ~ Fields (Rep b)) =>
  b
magic = to (coerce' (productify_ @a @())) where
  coerce' :: Productify a (Rep a) () -> Rep b ()
  coerce' = coerce