{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Typeable
import GHC.Generics

rewrite_
  :: (Generic a, Generic b, Rewriter (Rep a), Rewrite (Rep a) ~ Rep b)
  => a -> b
rewrite_ = to . rewrite Both . from

data What = First | Last | Both | None
  deriving Eq

splitWhat :: What -> (What, What)
splitWhat Both  = (First, Last)
splitWhat First = (First, None)
splitWhat Last  = (None,  Last)
splitWhat None  = (None,  None)

class Rewriter f where
  type Rewrite f :: * -> *
  rewrite :: What -> f a -> (Rewrite f) a

instance Rewriter f => Rewriter (M1 i c f) where
  type Rewrite (M1 i c f) = M1 i c (Rewrite f)
  rewrite x = M1 . rewrite x . unM1

instance Typeable c => Rewriter (K1 i c) where
  type Rewrite (K1 i c) = K1 i String
  rewrite w (K1 x) | w /= None, Just val <- cast x = K1 val
  rewrite _ _ = K1 "NIL"

instance (Rewriter a, Rewriter b) => Rewriter (a :*: b) where
  type Rewrite (a :*: b) = Rewrite a :*: Rewrite b
  rewrite x (a :*: b) = rewrite y a :*: rewrite z b
    where (y, z) = splitWhat x

y0 :: (String, Int, Double)
y0 = ("something", 3, 4.788)

y1 :: (String, String, String, (Int, Int))
y1 = ("something else", "Hello", "NIL", (4,6))

y2 :: (Double, Int, String)
y2 = (4.788, 3, "something")

y3 :: (String, Double, String)
y3 = ("something", 4.788, "something else")

main :: IO ()
main = do
  print (rewrite_ y0 :: (String, String, String))
  print (rewrite_ y1 :: (String, String, String, String))
  print (rewrite_ y2 :: (String, String, String))
  print (rewrite_ y3 :: (String, String, String))