{-# LANGUAGE UndecidableInstances #-} -- due to type class design
{-# LANGUAGE AllowAmbiguousTypes  #-}  -- due to type class design

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 qualified as Applicative
import Control.Applicative ( Alternative(empty) )

import Data.Kind ( type Type, type Constraint )

import Generic.Data.Wrappers ( NoRec0, type ENoRec0, EmptyRec0 )
import GHC.TypeLits ( TypeError )

-- import Data.Monoid

-- | Implementation enumeration type class for generic 'traverse'.
--
-- The type variable is uninstantiated, used purely as a tag.
--
-- Avoid orphan instances by defining custom empty types to use here.
-- See the binrep library on Hackage for an example.
class GenericTraverse tag where
    -- | The target 'Applicative' to 'traverse' to.
    type GenericTraverseF tag :: Type -> Type

    -- | The type class providing the action in 'traverse' for permitted types.
    type GenericTraverseC tag 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 tag a
        => String       {- ^ data type name -}
        -> String       {- ^ constructor name -}
        -> Maybe String {- ^ record name (if present) -}
        -> Natural      {- ^ field index -}
        -> GenericTraverseF tag a

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

-- | 'traverse' over types where all fields are replaced with the functor's
--   'empty'.
--
-- Note that one may write a valid instance using a 'Monoid' on @a@s instead.
-- I don't think you should. But I can't explain why.
instance GenericTraverse (EmptyRec0 (f :: Type -> Type)) where
    type GenericTraverseF (EmptyRec0 f) = f
    type GenericTraverseC (EmptyRec0 f) _ = Alternative f
    genericTraverseAction :: forall a.
GenericTraverseC (EmptyRec0 f) a =>
String
-> String
-> Maybe String
-> Natural
-> GenericTraverseF (EmptyRec0 f) a
genericTraverseAction String
_ String
_ Maybe String
_ Natural
_ = f a
GenericTraverseF (EmptyRec0 f) a
forall a. f a
forall (f :: Type -> Type) a. Alternative f => f a
empty

class GTraverseC cd cc (si :: Natural) tag gf where
    gTraverseC :: GenericTraverseF tag (gf p)

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

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

instance Applicative (GenericTraverseF tag) => GTraverseC cd cc 0 tag U1 where
    gTraverseC :: forall (p :: k). GenericTraverseF tag (U1 p)
gTraverseC = U1 p -> GenericTraverseF tag (U1 p)
forall a. a -> GenericTraverseF tag a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure U1 p
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