{-# LANGUAGE UndecidableInstances #-} -- due to type class design
{-# LANGUAGE AllowAmbiguousTypes #-}  -- due to type class design
{-# LANGUAGE ApplicativeDo #-} -- TODO because I'm lazy

module Generic.Data.Function.Traverse.Constructor where

import GHC.Generics
import GHC.TypeNats ( Natural, KnownNat, type (+) )
import Generic.Data.Function.Util.Generic ( datatypeName', conName', selName'' )
import Generic.Data.Function.Util.TypeNats ( natVal'' )

import Control.Applicative ( liftA2 )

import Data.Kind ( type Type, type Constraint )

import Generic.Data.Function.Via
import GHC.TypeLits ( TypeError )

import Data.Monoid
data A a = A a (Sum Int) ()
    deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (A a) x -> A a
forall a x. A a -> Rep (A a) x
$cto :: forall a x. Rep (A a) x -> A a
$cfrom :: forall a x. A a -> Rep (A a) x
Generic, Int -> A a -> ShowS
forall a. Show a => Int -> A a -> ShowS
forall a. Show a => [A a] -> ShowS
forall a. Show a => A a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [A a] -> ShowS
$cshowList :: forall a. Show a => [A a] -> ShowS
show :: A a -> String
$cshow :: forall a. Show a => A a -> String
showsPrec :: Int -> A a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> A a -> ShowS
Show)

-- | 'Applicative' functors that can be generically 'traverse'd.
class GenericTraverse f where
    -- | The type class providing (applicative) actions for permitted types.
    type GenericTraverseC f a :: Constraint

    -- | The action in 'traverse' (first argument).
    --
    -- We include data type metadata because this function is useful for monadic
    -- parsers, which can record it in error messages. (We don't do it for
    -- foldMap because it's pure.)
    genericTraverseAction
        :: GenericTraverseC f a
        => String       {- ^ data type name -}
        -> String       {- ^ constructor name -}
        -> Maybe String {- ^ record name (if present) -}
        -> Natural      {- ^ field index -}
        -> f a

-- | 'traverse' over types with no fields in any constructor.
instance GenericTraverse NoRec0 where
    type GenericTraverseC NoRec0 a = TypeError ENoRec0
    genericTraverseAction :: forall a.
GenericTraverseC NoRec0 a =>
String -> String -> Maybe String -> Natural -> NoRec0 a
genericTraverseAction = forall a. HasCallStack => a
undefined

-- | 'traverse' over types where all fields map to their respective 'mempty'.
--
-- Can result in type errors lacking context: a field missing a 'Monoid'
-- instance will type error with a regular "no instance for" message, without
-- telling you the surrounding type.
--
-- Maybe silly.
instance GenericTraverse EmptyRec0 where
    type GenericTraverseC EmptyRec0 a = Monoid a
    genericTraverseAction :: forall a.
GenericTraverseC EmptyRec0 a =>
String -> String -> Maybe String -> Natural -> EmptyRec0 a
genericTraverseAction String
_ String
_ Maybe String
_ Natural
_ = forall a. a -> EmptyRec0 a
EmptyRec0 forall a. Monoid a => a
mempty

class GTraverseC cd cc (si :: Natural) f f' where gTraverseC :: f (f' p)

instance (Applicative f, GTraverseC cd cc si f l, GTraverseC cd cc (si + ProdArity r) f r)
  => GTraverseC cd cc si f (l :*: r) where
    gTraverseC :: forall p. f ((:*:) l r p)
gTraverseC = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
                   (forall {k} {k} {k} {k} (cd :: k) (cc :: k) (si :: Natural)
       (f :: k -> Type) (f' :: k -> k) (p :: k).
GTraverseC cd cc si f f' =>
f (f' p)
gTraverseC @cd @cc @si)
                   (forall {k} {k} {k} {k} (cd :: k) (cc :: k) (si :: Natural)
       (f :: k -> Type) (f' :: k -> k) (p :: k).
GTraverseC cd cc si f f' =>
f (f' p)
gTraverseC @cd @cc @(si + ProdArity r))

instance (GenericTraverse f, GenericTraverseC f a, Functor f, KnownNat si, Selector cs, Constructor cc, Datatype cd)
  => GTraverseC cd cc si f (S1 cs (Rec0 a)) where
    gTraverseC :: forall (p :: k). f (S1 cs (Rec0 a) p)
gTraverseC = (forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
K1) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: Type -> Type) a.
(GenericTraverse f, GenericTraverseC f a) =>
String -> String -> Maybe String -> Natural -> f a
genericTraverseAction String
cd String
cc Maybe String
cs Natural
si
      where
        cs :: Maybe String
cs = forall {k} (s :: k). Selector s => Maybe String
selName'' @cs
        cd :: String
cd = forall {k} (d :: k). Datatype d => String
datatypeName' @cd
        cc :: String
cc = forall {k} (c :: k). Constructor c => String
conName' @cc
        si :: Natural
si = forall (n :: Natural). KnownNat n => Natural
natVal'' @si

instance Applicative f => GTraverseC cd cc 0 f U1 where gTraverseC :: forall (p :: k). f (U1 p)
gTraverseC = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall k (p :: k). U1 p
U1

type family ProdArity (f :: Type -> Type) :: Natural where
    ProdArity (S1 c f)  = 1
    ProdArity (l :*: r) = ProdArity l + ProdArity r