{-# 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.TypeLits
import Generic.Data.Function.Common.TypeLits ( natVal'', symbolVal'' )
import Generic.Data.Function.Common.Error ( eNoEmpty )

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 )

-- | Implementation enumeration type class for generic 'traverse'.
--
-- The type variable is uninstantiated, used purely as a tag.
-- Good types include the type class used inside (providing you define the
-- type class/it's not an orphan instance), or a custom void data type.
-- 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

    -- | Action to run when trying to parse a 'V1' (void data type).
    --
    -- Defaults to 'error', but you may wrap it in your functor if it pleases.
    genericTraverseV1 :: GenericTraverseF tag (V1 p)
    -- NOTE: Prior to GHC 9.8, we can't default to a compile-time error here,
    -- due to TypeError limitations. From GHC 9.8, we can use Unsatisfiable.
    -- But I'm still not sure it works how I would like it to. Let's just stick
    -- with 'error' for now. One can always use generic-type-asserts.
    {-
    default genericTraverseV1
        :: Unsatisfiable (ENoEmpty tag) => GenericTraverseF tag (V1 p)
    genericTraverseV1 = unsatisfiable
    -}
    genericTraverseV1 = [Char] -> GenericTraverseF tag (V1 p)
forall a. HasCallStack => [Char] -> a
error [Char]
eNoEmpty

type ENoEmpty tag =
         'Text "Attempted to derive generic traverse for the void data type"
    :$$: 'Text "To override, implement genericTraverseV1 on:"
    :$$: 'Text "instance GenericTraverse (" :<>: 'ShowType tag :<>: 'Text ")"

-- | '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 =>
[Char]
-> [Char]
-> Maybe [Char]
-> Natural
-> GenericTraverseF (NoRec0 f) a
genericTraverseAction = [Char] -> [Char] -> Maybe [Char] -> Natural -> f a
[Char]
-> [Char]
-> Maybe [Char]
-> 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 =>
[Char]
-> [Char]
-> Maybe [Char]
-> Natural
-> GenericTraverseF (EmptyRec0 f) a
genericTraverseAction [Char]
_ [Char]
_ Maybe [Char]
_ Natural
_ = f a
GenericTraverseF (EmptyRec0 f) a
forall a. f a
forall (f :: Type -> Type) a. Alternative f => f a
empty

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

instance
  ( Applicative (GenericTraverseF tag)
  , GTraverseC tag cd cc si                 l
  , GTraverseC tag cd cc (si + ProdArity r) r
  ) => GTraverseC tag cd cc si (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 (tag :: k) (cd :: Symbol) (cc :: Symbol) (si :: Natural)
       (gf :: Type -> Type) p.
GTraverseC tag cd cc si gf =>
GenericTraverseF tag (gf p)
forall {k} {k} (tag :: k) (cd :: Symbol) (cc :: Symbol)
       (si :: Natural) (gf :: k -> Type) (p :: k).
GTraverseC tag cd cc si gf =>
GenericTraverseF tag (gf p)
gTraverseC @tag @cd @cc @si)
                   (forall (tag :: k) (cd :: Symbol) (cc :: Symbol) (si :: Natural)
       (gf :: Type -> Type) p.
GTraverseC tag cd cc si gf =>
GenericTraverseF tag (gf p)
forall {k} {k} (tag :: k) (cd :: Symbol) (cc :: Symbol)
       (si :: Natural) (gf :: k -> Type) (p :: k).
GTraverseC tag cd cc si gf =>
GenericTraverseF tag (gf p)
gTraverseC @tag @cd @cc @(si + ProdArity r))

instance
  ( GenericTraverse tag, GenericTraverseC tag a
  , Functor (GenericTraverseF tag)
  , KnownNat si, ReifyMaybeSymbol mSelName, KnownSymbol cc, KnownSymbol cd
  ) => GTraverseC tag cd cc si (S1 (MetaSel mSelName _ms2 _ms3 _ms4) (Rec0 a)) where
    gTraverseC :: forall (p :: k).
GenericTraverseF
  tag (S1 ('MetaSel mSelName _ms2 _ms3 _ms4) (Rec0 a) p)
gTraverseC = (K1 R a p -> M1 S ('MetaSel mSelName _ms2 _ms3 _ms4) (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 ('MetaSel mSelName _ms2 _ms3 _ms4) (Rec0 a) p)
-> (a -> K1 R a p)
-> a
-> M1 S ('MetaSel mSelName _ms2 _ms3 _ms4) (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 ('MetaSel mSelName _ms2 _ms3 _ms4) (Rec0 a) p)
-> GenericTraverseF tag a
-> GenericTraverseF
     tag (M1 S ('MetaSel mSelName _ms2 _ms3 _ms4) (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) =>
[Char]
-> [Char] -> Maybe [Char] -> Natural -> GenericTraverseF tag a
forall {k} (tag :: k) a.
(GenericTraverse tag, GenericTraverseC tag a) =>
[Char]
-> [Char] -> Maybe [Char] -> Natural -> GenericTraverseF tag a
genericTraverseAction @tag [Char]
cd [Char]
cc Maybe [Char]
cs Natural
si
      where
        cs :: Maybe [Char]
cs = forall (mstr :: Maybe Symbol).
ReifyMaybeSymbol mstr =>
Maybe [Char]
reifyMaybeSymbol @mSelName
        cd :: [Char]
cd = forall (sym :: Symbol). KnownSymbol sym => [Char]
symbolVal'' @cd
        cc :: [Char]
cc = forall (sym :: Symbol). KnownSymbol sym => [Char]
symbolVal'' @cc
        si :: Natural
si = forall (n :: Natural). KnownNat n => Natural
natVal'' @si

instance Applicative (GenericTraverseF tag) => GTraverseC tag cd cc 0 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

class ReifyMaybeSymbol (mstr :: Maybe Symbol) where
    reifyMaybeSymbol :: Maybe String
instance ReifyMaybeSymbol Nothing where reifyMaybeSymbol :: Maybe [Char]
reifyMaybeSymbol = Maybe [Char]
forall a. Maybe a
Nothing
instance KnownSymbol str => ReifyMaybeSymbol (Just str) where
    reifyMaybeSymbol :: Maybe [Char]
reifyMaybeSymbol = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just (forall (sym :: Symbol). KnownSymbol sym => [Char]
symbolVal'' @str)