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

module Generic.Data.Function.Contra.Constructor where

import Data.Functor.Contravariant
import Data.Functor.Contravariant.Divisible

import GHC.Generics
import Data.Kind ( type Type, type Constraint )

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

-- | TODO
--
-- 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 GenericContra tag where
    type GenericContraF tag :: Type -> Type
    type GenericContraC tag a :: Constraint
    genericContraF :: GenericContraC tag a => GenericContraF tag a

-- | over types with no fields in any constructor
instance GenericContra (NoRec0 (f :: Type -> Type)) where
    type GenericContraF (NoRec0 f) = f
    type GenericContraC (NoRec0 f) _ = TypeError ENoRec0
    genericContraF :: forall a.
GenericContraC (NoRec0 f) a =>
GenericContraF (NoRec0 f) a
genericContraF = f a
GenericContraF (NoRec0 f) a
forall a. HasCallStack => a
undefined

-- | over types where all fields map to 'mempty'
instance GenericContra (EmptyRec0 (f :: Type -> Type)) where
    type GenericContraF (EmptyRec0 f) = f
    type GenericContraC (EmptyRec0 f) _ = Divisible f
    genericContraF :: forall a.
GenericContraC (EmptyRec0 f) a =>
GenericContraF (EmptyRec0 f) a
genericContraF = f a
GenericContraF (EmptyRec0 f) a
forall a. f a
forall (f :: Type -> Type) a. Divisible f => f a
conquer

class GContraC tag gf where gContraC :: GenericContraF tag (gf p)

instance
  ( Divisible (GenericContraF tag)
  , GContraC tag l, GContraC tag r
  ) => GContraC tag (l :*: r) where
    gContraC :: forall (p :: k). GenericContraF tag ((:*:) l r p)
gContraC = ((:*:) l r p -> (l p, r p))
-> GenericContraF tag (l p)
-> GenericContraF tag (r p)
-> GenericContraF tag ((:*:) l r p)
forall a b c.
(a -> (b, c))
-> GenericContraF tag b
-> GenericContraF tag c
-> GenericContraF tag a
forall (f :: Type -> Type) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide (\(l p
l :*: r p
r) -> (l p
l, r p
r)) (forall (tag :: k) (gf :: k -> Type) (p :: k).
GContraC tag gf =>
GenericContraF tag (gf p)
forall {k} {k} (tag :: k) (gf :: k -> Type) (p :: k).
GContraC tag gf =>
GenericContraF tag (gf p)
gContraC @tag) (forall (tag :: k) (gf :: k -> Type) (p :: k).
GContraC tag gf =>
GenericContraF tag (gf p)
forall {k} {k} (tag :: k) (gf :: k -> Type) (p :: k).
GContraC tag gf =>
GenericContraF tag (gf p)
gContraC @tag)

instance
  ( Contravariant (GenericContraF tag)
  , GenericContra tag, GenericContraC tag a
  ) => GContraC tag (S1 c (Rec0 a)) where
    gContraC :: forall (p :: k). GenericContraF tag (S1 c (Rec0 a) p)
gContraC = (M1 S c (Rec0 a) p -> a)
-> GenericContraF tag a -> GenericContraF tag (M1 S c (Rec0 a) p)
forall a' a.
(a' -> a) -> GenericContraF tag a -> GenericContraF tag a'
forall (f :: Type -> Type) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (K1 R a p -> a
forall k i c (p :: k). K1 i c p -> c
unK1 (K1 R a p -> a)
-> (M1 S c (Rec0 a) p -> K1 R a p) -> M1 S c (Rec0 a) p -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 S c (Rec0 a) p -> K1 R a p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1) (forall (tag :: k) a.
(GenericContra tag, GenericContraC tag a) =>
GenericContraF tag a
forall {k} (tag :: k) a.
(GenericContra tag, GenericContraC tag a) =>
GenericContraF tag a
genericContraF @tag)

instance Divisible (GenericContraF tag) => GContraC tag U1 where
    gContraC :: forall (p :: k). GenericContraF tag (U1 p)
gContraC = GenericContraF tag (U1 p)
forall a. GenericContraF tag a
forall (f :: Type -> Type) a. Divisible f => f a
conquer